explicit resolution of ambiguous dictionaries
authorhaftmann
Tue Jun 14 20:48:41 2016 +0200 (2016-06-14)
changeset 633037cffe366d333
parent 63302 d15dde801536
child 63304 00a135c0a17f
explicit resolution of ambiguous dictionaries
NEWS
src/Doc/Codegen/Further.thy
src/Tools/Code/code_ml.ML
src/Tools/Code/code_scala.ML
src/Tools/Code/code_thingol.ML
     1.1 --- a/NEWS	Tue Jun 14 15:54:28 2016 +0100
     1.2 +++ b/NEWS	Tue Jun 14 20:48:41 2016 +0200
     1.3 @@ -132,6 +132,9 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Code generation for scala: ambiguous implicts in class diagrams
     1.8 +are spelt out explicitly.
     1.9 +
    1.10  * Abstract locales semigroup, abel_semigroup, semilattice,
    1.11  semilattice_neutr, ordering, ordering_top, semilattice_order,
    1.12  semilattice_neutr_order, comm_monoid_set, semilattice_set,
     2.1 --- a/src/Doc/Codegen/Further.thy	Tue Jun 14 15:54:28 2016 +0100
     2.2 +++ b/src/Doc/Codegen/Further.thy	Tue Jun 14 20:48:41 2016 +0200
     2.3 @@ -39,71 +39,8 @@
     2.4    the type arguments are just appended.  Otherwise they are ignored;
     2.5    hence user-defined adaptations for polymorphic constants have to be
     2.6    designed very carefully to avoid ambiguity.
     2.7 -
     2.8 -  Isabelle's type classes are mapped onto @{text Scala} implicits; in
     2.9 -  cases with diamonds in the subclass hierarchy this can lead to
    2.10 -  ambiguities in the generated code:
    2.11 -\<close>
    2.12 -
    2.13 -class %quote class1 =
    2.14 -  fixes foo :: "'a \<Rightarrow> 'a"
    2.15 -
    2.16 -class %quote class2 = class1
    2.17 -
    2.18 -class %quote class3 = class1
    2.19 -
    2.20 -text \<open>
    2.21 -  \noindent Here both @{class class2} and @{class class3} inherit from @{class class1},
    2.22 -  forming the upper part of a diamond.
    2.23 -\<close>
    2.24 -
    2.25 -definition %quote bar :: "'a :: {class2, class3} \<Rightarrow> 'a" where
    2.26 -  "bar = foo"
    2.27 -
    2.28 -text \<open>
    2.29 -  \noindent This yields the following code:
    2.30 -\<close>
    2.31 -
    2.32 -text %quotetypewriter \<open>
    2.33 -  @{code_stmts bar (Scala)}
    2.34  \<close>
    2.35  
    2.36 -text \<open>
    2.37 -  \noindent This code is rejected by the @{text Scala} compiler: in
    2.38 -  the definition of @{text bar}, it is not clear from where to derive
    2.39 -  the implicit argument for @{text foo}.
    2.40 -
    2.41 -  The solution to the problem is to close the diamond by a further
    2.42 -  class with inherits from both @{class class2} and @{class class3}:
    2.43 -\<close>
    2.44 -
    2.45 -class %quote class4 = class2 + class3
    2.46 -
    2.47 -text \<open>
    2.48 -  \noindent Then the offending code equation can be restricted to
    2.49 -  @{class class4}:
    2.50 -\<close>
    2.51 -
    2.52 -lemma %quote [code]:
    2.53 -  "(bar :: 'a::class4 \<Rightarrow> 'a) = foo"
    2.54 -  by (simp only: bar_def)
    2.55 -
    2.56 -text \<open>
    2.57 -  \noindent with the following code:
    2.58 -\<close>
    2.59 -
    2.60 -text %quotetypewriter \<open>
    2.61 -  @{code_stmts bar (Scala)}
    2.62 -\<close>
    2.63 -
    2.64 -text \<open>
    2.65 -  \noindent which exposes no ambiguity.
    2.66 -
    2.67 -  Since the preprocessor (cf.~\secref{sec:preproc}) propagates sort
    2.68 -  constraints through a system of code equations, it is usually not
    2.69 -  very difficult to identify the set of code equations which actually
    2.70 -  needs more restricted sort constraints.
    2.71 -\<close>
    2.72  
    2.73  subsection \<open>Modules namespace\<close>
    2.74  
     3.1 --- a/src/Tools/Code/code_ml.ML	Tue Jun 14 15:54:28 2016 +0100
     3.2 +++ b/src/Tools/Code/code_ml.ML	Tue Jun 14 20:48:41 2016 +0200
     3.3 @@ -87,13 +87,13 @@
     3.4            ((str o deresolve_inst) inst ::
     3.5              (if is_pseudo_fun (Class_Instance inst) then [str "()"]
     3.6              else map_filter (print_dicts is_pseudo_fun BR) dss))
     3.7 -      | print_plain_dict is_pseudo_fun fxy (Dict_Var { var, index, length }) =
     3.8 +      | print_plain_dict is_pseudo_fun fxy (Dict_Var { var, index, length, ... }) =
     3.9            [str (if length = 1 then Name.enforce_case true var ^ "_"
    3.10              else Name.enforce_case true var ^ string_of_int (index + 1) ^ "_")]
    3.11      and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
    3.12      val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
    3.13 -      (map_index (fn (i, _) =>
    3.14 -        Dict ([], Dict_Var { var = v, index = i, length = length sort })) sort));
    3.15 +      (map_index (fn (i, _) => Dict ([],
    3.16 +         Dict_Var { var = v, index = i, length = length sort, class = nth sort i, unique = true })) sort));
    3.17      fun print_term is_pseudo_fun some_thm vars fxy (IConst const) =
    3.18            print_app is_pseudo_fun some_thm vars fxy (const, [])
    3.19        | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
    3.20 @@ -399,13 +399,13 @@
    3.21            brackify BR ((str o deresolve_inst) inst ::
    3.22              (if is_pseudo_fun (Class_Instance inst) then [str "()"]
    3.23              else map_filter (print_dicts is_pseudo_fun BR) dss))
    3.24 -      | print_plain_dict is_pseudo_fun fxy (Dict_Var { var, index, length }) =
    3.25 +      | print_plain_dict is_pseudo_fun fxy (Dict_Var { var, index, length, ... }) =
    3.26            str (if length = 1 then "_" ^ Name.enforce_case true var
    3.27              else "_" ^ Name.enforce_case true var ^ string_of_int (index + 1))
    3.28      and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
    3.29      val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
    3.30 -      (map_index (fn (i, _) =>
    3.31 -        Dict ([], Dict_Var { var = v, index = i, length = length sort })) sort));
    3.32 +      (map_index (fn (i, _) => Dict ([],
    3.33 +         Dict_Var { var = v, index = i, length = length sort, class = nth sort i, unique = true })) sort));
    3.34      fun print_term is_pseudo_fun some_thm vars fxy (IConst const) =
    3.35            print_app is_pseudo_fun some_thm vars fxy (const, [])
    3.36        | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
     4.1 --- a/src/Tools/Code/code_scala.ML	Tue Jun 14 15:54:28 2016 +0100
     4.2 +++ b/src/Tools/Code/code_scala.ML	Tue Jun 14 20:48:41 2016 +0200
     4.3 @@ -53,7 +53,16 @@
     4.4              str "=>", print_typ tyvars NOBR ty];
     4.5      fun constraint p1 p2 = Pretty.block [p1, str ":", Pretty.brk 1, p2];
     4.6      fun print_var vars NONE = str "_"
     4.7 -      | print_var vars (SOME v) = (str o lookup_var vars) v
     4.8 +      | print_var vars (SOME v) = (str o lookup_var vars) v;
     4.9 +    fun applify_dict tyvars (Dict (_, d)) = applify_plain_dict tyvars d
    4.10 +    and applify_plain_dict tyvars (Dict_Const (inst, dss)) =
    4.11 +          applify_dictss tyvars ((str o deresolve o Class_Instance) inst) dss
    4.12 +      | applify_plain_dict tyvars (Dict_Var { var, class, ... }) =
    4.13 +          Pretty.block [str "implicitly",
    4.14 +            enclose "[" "]" [Pretty.block [(str o deresolve_class) class,
    4.15 +              enclose "[" "]" [(str o lookup_tyvar tyvars) var]]]]
    4.16 +    and applify_dictss tyvars p dss =
    4.17 +      applify "(" ")" (applify_dict tyvars) NOBR p (flat dss)
    4.18      fun print_term tyvars is_pat some_thm vars fxy (IConst const) =
    4.19            print_app tyvars is_pat some_thm vars fxy (const, [])
    4.20        | print_term tyvars is_pat some_thm vars fxy (t as (t1 `$ t2)) =
    4.21 @@ -88,22 +97,29 @@
    4.22               ], vars')
    4.23             end
    4.24      and print_app tyvars is_pat some_thm vars fxy
    4.25 -        (app as ({ sym, typargs, dom, ... }, ts)) =
    4.26 +        (app as ({ sym, typargs, dom, dicts, ... }, ts)) =
    4.27        let
    4.28          val k = length ts;
    4.29          val typargs' = if is_pat then [] else typargs;
    4.30          val syntax = case sym of
    4.31              Constant const => const_syntax const
    4.32            | _ => NONE;
    4.33 +        val applify_dicts =
    4.34 +          if is_pat orelse is_some syntax orelse is_constr sym
    4.35 +            orelse Code_Thingol.unambiguous_dictss dicts
    4.36 +          then fn p => K p
    4.37 +          else applify_dictss tyvars;
    4.38          val (l, print') = case syntax of
    4.39 -            NONE => (args_num sym, fn fxy => fn ts => gen_applify (is_constr sym) "(" ")"
    4.40 +            NONE => (args_num sym, fn fxy => fn ts => applify_dicts
    4.41 +              (gen_applify (is_constr sym) "(" ")"
    4.42                (print_term tyvars is_pat some_thm vars NOBR) fxy
    4.43                  (applify "[" "]" (print_typ tyvars NOBR)
    4.44 -                  NOBR ((str o deresolve) sym) typargs') ts)
    4.45 -          | SOME (k, Plain_printer s) => (k, fn fxy => fn ts => applify "(" ")"
    4.46 +                  NOBR ((str o deresolve) sym) typargs') ts) dicts)
    4.47 +          | SOME (k, Plain_printer s) => (k, fn fxy => fn ts => applify_dicts
    4.48 +              (applify "(" ")"
    4.49                (print_term tyvars is_pat some_thm vars NOBR) fxy
    4.50                  (applify "[" "]" (print_typ tyvars NOBR)
    4.51 -                  NOBR (str s) typargs') ts)
    4.52 +                  NOBR (str s) typargs') ts) dicts)
    4.53            | SOME (k, Complex_printer print) =>
    4.54                (k, fn fxy => fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy
    4.55                  (ts ~~ take k dom))
     5.1 --- a/src/Tools/Code/code_thingol.ML	Tue Jun 14 15:54:28 2016 +0100
     5.2 +++ b/src/Tools/Code/code_thingol.ML	Tue Jun 14 20:48:41 2016 +0200
     5.3 @@ -19,7 +19,7 @@
     5.4        Dict of (class * class) list * plain_dict
     5.5    and plain_dict = 
     5.6        Dict_Const of (string * class) * dict list list
     5.7 -    | Dict_Var of { var: vname, index: int, length: int };
     5.8 +    | Dict_Var of { var: vname, index: int, length: int, class: class, unique: bool };
     5.9    datatype itype =
    5.10        `%% of string * itype list
    5.11      | ITyVar of vname;
    5.12 @@ -55,6 +55,7 @@
    5.13    val is_IAbs: iterm -> bool
    5.14    val eta_expand: int -> const * iterm list -> iterm
    5.15    val contains_dict_var: iterm -> bool
    5.16 +  val unambiguous_dictss: dict list list -> bool
    5.17    val add_constsyms: iterm -> Code_Symbol.T list -> Code_Symbol.T list
    5.18    val add_tyconames: iterm -> string list -> string list
    5.19    val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a
    5.20 @@ -132,7 +133,7 @@
    5.21      Dict of (class * class) list * plain_dict
    5.22  and plain_dict = 
    5.23      Dict_Const of (string * class) * dict list list
    5.24 -  | Dict_Var of { var: vname, index: int, length: int };
    5.25 +  | Dict_Var of { var: vname, index: int, length: int, class: class, unique: bool };
    5.26  
    5.27  datatype itype =
    5.28      `%% of string * itype list
    5.29 @@ -259,17 +260,18 @@
    5.30        (Name.invent_names vars "a" ((take l o drop j) tys));
    5.31    in vs_tys `|==> IConst const `$$ ts @ map (IVar o fst) vs_tys end;
    5.32  
    5.33 -fun contains_dict_var t =
    5.34 -  let
    5.35 -    fun cont_dict (Dict (_, d)) = cont_plain_dict d
    5.36 -    and cont_plain_dict (Dict_Const (_, dss)) = (exists o exists) cont_dict dss
    5.37 -      | cont_plain_dict (Dict_Var _) = true;
    5.38 -    fun cont_term (IConst { dicts = dss, ... }) = (exists o exists) cont_dict dss
    5.39 -      | cont_term (IVar _) = false
    5.40 -      | cont_term (t1 `$ t2) = cont_term t1 orelse cont_term t2
    5.41 -      | cont_term (_ `|=> t) = cont_term t
    5.42 -      | cont_term (ICase { primitive = t, ... }) = cont_term t;
    5.43 -  in cont_term t end;
    5.44 +fun exists_dict_var f (Dict (_, d)) = exists_plain_dict_var_pred f d
    5.45 +and exists_plain_dict_var_pred f (Dict_Const (_, dss)) = exists_dictss_var f dss
    5.46 +  | exists_plain_dict_var_pred f (Dict_Var x) = f x
    5.47 +and exists_dictss_var f dss = (exists o exists) (exists_dict_var f) dss;
    5.48 +
    5.49 +fun contains_dict_var (IConst { dicts = dss, ... }) = exists_dictss_var (K true) dss
    5.50 +  | contains_dict_var (IVar _) = false
    5.51 +  | contains_dict_var (t1 `$ t2) = contains_dict_var t1 orelse contains_dict_var t2
    5.52 +  | contains_dict_var (_ `|=> t) = contains_dict_var t
    5.53 +  | contains_dict_var (ICase { primitive = t, ... }) = contains_dict_var t;
    5.54 +
    5.55 +val unambiguous_dictss = not o exists_dictss_var (fn { unique, ... } => not unique);
    5.56  
    5.57  
    5.58  (** statements, abstract programs **)
    5.59 @@ -469,20 +471,27 @@
    5.60      Weakening of (class * class) list * plain_typarg_witness
    5.61  and plain_typarg_witness =
    5.62      Global of (string * class) * typarg_witness list list
    5.63 -  | Local of string * (int * sort);
    5.64 +  | Local of { var: string, index: int, sort: sort, unique: bool };
    5.65 +
    5.66 +fun brand_unique unique (w as Global _) = w
    5.67 +  | brand_unique unique (Local { var, index, sort, unique = _ }) =
    5.68 +      Local { var = var, index = index, sort = sort, unique = unique };
    5.69  
    5.70  fun construct_dictionaries ctxt (proj_sort, algebra) permissive some_thm (ty, sort) (deps, program) =
    5.71    let
    5.72 -    fun class_relation ((Weakening (classrels, x)), sub_class) super_class =
    5.73 -      Weakening ((sub_class, super_class) :: classrels, x);
    5.74 +    fun class_relation unique (Weakening (classrels, x), sub_class) super_class =
    5.75 +      Weakening ((sub_class, super_class) :: classrels, brand_unique unique x);
    5.76      fun type_constructor (tyco, _) dss class =
    5.77        Weakening ([], Global ((tyco, class), (map o map) fst dss));
    5.78      fun type_variable (TFree (v, sort)) =
    5.79        let
    5.80          val sort' = proj_sort sort;
    5.81 -      in map_index (fn (n, class) => (Weakening ([], Local (v, (n, sort'))), class)) sort' end;
    5.82 +      in map_index (fn (n, class) => (Weakening ([], Local
    5.83 +        { var = v, index = n, sort = sort', unique = true }), class)) sort'
    5.84 +      end;
    5.85      val typarg_witnesses = Sorts.of_sort_derivation algebra
    5.86 -      {class_relation = fn _ => fn _ => Sorts.classrel_derivation algebra class_relation,
    5.87 +      {class_relation = fn _ => fn unique =>
    5.88 +         Sorts.classrel_derivation algebra (class_relation unique),
    5.89         type_constructor = type_constructor,
    5.90         type_variable = type_variable} (ty, proj_sort sort)
    5.91        handle Sorts.CLASS_ERROR e => not_wellsorted ctxt permissive some_thm deps ty sort e;
    5.92 @@ -752,16 +761,18 @@
    5.93    #>> (fn sort => (unprefix "'" v, sort))
    5.94  and translate_dicts ctxt algbr eqngr permissive some_thm (ty, sort) =
    5.95    let
    5.96 -    fun mk_dict (Weakening (classrels, x)) =
    5.97 +    fun mk_dict (Weakening (classrels, d)) =
    5.98            fold_map (ensure_classrel ctxt algbr eqngr permissive) classrels
    5.99 -          ##>> mk_plain_dict x
   5.100 +          ##>> mk_plain_dict d
   5.101            #>> Dict 
   5.102      and mk_plain_dict (Global (inst, dss)) =
   5.103            ensure_inst ctxt algbr eqngr permissive inst
   5.104            ##>> (fold_map o fold_map) mk_dict dss
   5.105 -          #>> (fn (inst, dss) => Dict_Const (inst, dss))
   5.106 -      | mk_plain_dict (Local (v, (index, sort))) =
   5.107 -          pair (Dict_Var { var = unprefix "'" v, index = index, length = length sort })
   5.108 +          #>> Dict_Const
   5.109 +      | mk_plain_dict (Local { var, index, sort, unique }) =
   5.110 +          ensure_class ctxt algbr eqngr permissive (nth sort index)
   5.111 +          #>> (fn class => Dict_Var { var = unprefix "'" var, index = index,
   5.112 +            length = length sort, class = class, unique = unique })
   5.113    in
   5.114      construct_dictionaries ctxt algbr permissive some_thm (ty, sort)
   5.115      #-> (fn typarg_witnesses => fold_map mk_dict typarg_witnesses)