# HG changeset patch # User haftmann # Date 1465930121 -7200 # Node ID 7cffe366d3332c16ded5d85c30bf1e91d59970b3 # Parent d15dde801536f6c2003a8dc79d5cb5b3f34a8e90 explicit resolution of ambiguous dictionaries diff -r d15dde801536 -r 7cffe366d333 NEWS --- a/NEWS Tue Jun 14 15:54:28 2016 +0100 +++ b/NEWS Tue Jun 14 20:48:41 2016 +0200 @@ -132,6 +132,9 @@ *** HOL *** +* Code generation for scala: ambiguous implicts in class diagrams +are spelt out explicitly. + * Abstract locales semigroup, abel_semigroup, semilattice, semilattice_neutr, ordering, ordering_top, semilattice_order, semilattice_neutr_order, comm_monoid_set, semilattice_set, diff -r d15dde801536 -r 7cffe366d333 src/Doc/Codegen/Further.thy --- a/src/Doc/Codegen/Further.thy Tue Jun 14 15:54:28 2016 +0100 +++ b/src/Doc/Codegen/Further.thy Tue Jun 14 20:48:41 2016 +0200 @@ -39,71 +39,8 @@ the type arguments are just appended. Otherwise they are ignored; hence user-defined adaptations for polymorphic constants have to be designed very carefully to avoid ambiguity. - - Isabelle's type classes are mapped onto @{text Scala} implicits; in - cases with diamonds in the subclass hierarchy this can lead to - ambiguities in the generated code: -\ - -class %quote class1 = - fixes foo :: "'a \ 'a" - -class %quote class2 = class1 - -class %quote class3 = class1 - -text \ - \noindent Here both @{class class2} and @{class class3} inherit from @{class class1}, - forming the upper part of a diamond. -\ - -definition %quote bar :: "'a :: {class2, class3} \ 'a" where - "bar = foo" - -text \ - \noindent This yields the following code: -\ - -text %quotetypewriter \ - @{code_stmts bar (Scala)} \ -text \ - \noindent This code is rejected by the @{text Scala} compiler: in - the definition of @{text bar}, it is not clear from where to derive - the implicit argument for @{text foo}. - - The solution to the problem is to close the diamond by a further - class with inherits from both @{class class2} and @{class class3}: -\ - -class %quote class4 = class2 + class3 - -text \ - \noindent Then the offending code equation can be restricted to - @{class class4}: -\ - -lemma %quote [code]: - "(bar :: 'a::class4 \ 'a) = foo" - by (simp only: bar_def) - -text \ - \noindent with the following code: -\ - -text %quotetypewriter \ - @{code_stmts bar (Scala)} -\ - -text \ - \noindent which exposes no ambiguity. - - Since the preprocessor (cf.~\secref{sec:preproc}) propagates sort - constraints through a system of code equations, it is usually not - very difficult to identify the set of code equations which actually - needs more restricted sort constraints. -\ subsection \Modules namespace\ diff -r d15dde801536 -r 7cffe366d333 src/Tools/Code/code_ml.ML --- a/src/Tools/Code/code_ml.ML Tue Jun 14 15:54:28 2016 +0100 +++ b/src/Tools/Code/code_ml.ML Tue Jun 14 20:48:41 2016 +0200 @@ -87,13 +87,13 @@ ((str o deresolve_inst) inst :: (if is_pseudo_fun (Class_Instance inst) then [str "()"] else map_filter (print_dicts is_pseudo_fun BR) dss)) - | print_plain_dict is_pseudo_fun fxy (Dict_Var { var, index, length }) = + | print_plain_dict is_pseudo_fun fxy (Dict_Var { var, index, length, ... }) = [str (if length = 1 then Name.enforce_case true var ^ "_" else Name.enforce_case true var ^ string_of_int (index + 1) ^ "_")] and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun); val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR - (map_index (fn (i, _) => - Dict ([], Dict_Var { var = v, index = i, length = length sort })) sort)); + (map_index (fn (i, _) => Dict ([], + Dict_Var { var = v, index = i, length = length sort, class = nth sort i, unique = true })) sort)); fun print_term is_pseudo_fun some_thm vars fxy (IConst const) = print_app is_pseudo_fun some_thm vars fxy (const, []) | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) = @@ -399,13 +399,13 @@ brackify BR ((str o deresolve_inst) inst :: (if is_pseudo_fun (Class_Instance inst) then [str "()"] else map_filter (print_dicts is_pseudo_fun BR) dss)) - | print_plain_dict is_pseudo_fun fxy (Dict_Var { var, index, length }) = + | print_plain_dict is_pseudo_fun fxy (Dict_Var { var, index, length, ... }) = str (if length = 1 then "_" ^ Name.enforce_case true var else "_" ^ Name.enforce_case true var ^ string_of_int (index + 1)) and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun); val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR - (map_index (fn (i, _) => - Dict ([], Dict_Var { var = v, index = i, length = length sort })) sort)); + (map_index (fn (i, _) => Dict ([], + Dict_Var { var = v, index = i, length = length sort, class = nth sort i, unique = true })) sort)); fun print_term is_pseudo_fun some_thm vars fxy (IConst const) = print_app is_pseudo_fun some_thm vars fxy (const, []) | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) = diff -r d15dde801536 -r 7cffe366d333 src/Tools/Code/code_scala.ML --- a/src/Tools/Code/code_scala.ML Tue Jun 14 15:54:28 2016 +0100 +++ b/src/Tools/Code/code_scala.ML Tue Jun 14 20:48:41 2016 +0200 @@ -53,7 +53,16 @@ str "=>", print_typ tyvars NOBR ty]; fun constraint p1 p2 = Pretty.block [p1, str ":", Pretty.brk 1, p2]; fun print_var vars NONE = str "_" - | print_var vars (SOME v) = (str o lookup_var vars) v + | print_var vars (SOME v) = (str o lookup_var vars) v; + fun applify_dict tyvars (Dict (_, d)) = applify_plain_dict tyvars d + and applify_plain_dict tyvars (Dict_Const (inst, dss)) = + applify_dictss tyvars ((str o deresolve o Class_Instance) inst) dss + | applify_plain_dict tyvars (Dict_Var { var, class, ... }) = + Pretty.block [str "implicitly", + enclose "[" "]" [Pretty.block [(str o deresolve_class) class, + enclose "[" "]" [(str o lookup_tyvar tyvars) var]]]] + and applify_dictss tyvars p dss = + applify "(" ")" (applify_dict tyvars) NOBR p (flat dss) fun print_term tyvars is_pat some_thm vars fxy (IConst const) = print_app tyvars is_pat some_thm vars fxy (const, []) | print_term tyvars is_pat some_thm vars fxy (t as (t1 `$ t2)) = @@ -88,22 +97,29 @@ ], vars') end and print_app tyvars is_pat some_thm vars fxy - (app as ({ sym, typargs, dom, ... }, ts)) = + (app as ({ sym, typargs, dom, dicts, ... }, ts)) = let val k = length ts; val typargs' = if is_pat then [] else typargs; val syntax = case sym of Constant const => const_syntax const | _ => NONE; + val applify_dicts = + if is_pat orelse is_some syntax orelse is_constr sym + orelse Code_Thingol.unambiguous_dictss dicts + then fn p => K p + else applify_dictss tyvars; val (l, print') = case syntax of - NONE => (args_num sym, fn fxy => fn ts => gen_applify (is_constr sym) "(" ")" + NONE => (args_num sym, fn fxy => fn ts => applify_dicts + (gen_applify (is_constr sym) "(" ")" (print_term tyvars is_pat some_thm vars NOBR) fxy (applify "[" "]" (print_typ tyvars NOBR) - NOBR ((str o deresolve) sym) typargs') ts) - | SOME (k, Plain_printer s) => (k, fn fxy => fn ts => applify "(" ")" + NOBR ((str o deresolve) sym) typargs') ts) dicts) + | SOME (k, Plain_printer s) => (k, fn fxy => fn ts => applify_dicts + (applify "(" ")" (print_term tyvars is_pat some_thm vars NOBR) fxy (applify "[" "]" (print_typ tyvars NOBR) - NOBR (str s) typargs') ts) + NOBR (str s) typargs') ts) dicts) | SOME (k, Complex_printer print) => (k, fn fxy => fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy (ts ~~ take k dom)) diff -r d15dde801536 -r 7cffe366d333 src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Tue Jun 14 15:54:28 2016 +0100 +++ b/src/Tools/Code/code_thingol.ML Tue Jun 14 20:48:41 2016 +0200 @@ -19,7 +19,7 @@ Dict of (class * class) list * plain_dict and plain_dict = Dict_Const of (string * class) * dict list list - | Dict_Var of { var: vname, index: int, length: int }; + | Dict_Var of { var: vname, index: int, length: int, class: class, unique: bool }; datatype itype = `%% of string * itype list | ITyVar of vname; @@ -55,6 +55,7 @@ val is_IAbs: iterm -> bool val eta_expand: int -> const * iterm list -> iterm val contains_dict_var: iterm -> bool + val unambiguous_dictss: dict list list -> bool val add_constsyms: iterm -> Code_Symbol.T list -> Code_Symbol.T list val add_tyconames: iterm -> string list -> string list val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a @@ -132,7 +133,7 @@ Dict of (class * class) list * plain_dict and plain_dict = Dict_Const of (string * class) * dict list list - | Dict_Var of { var: vname, index: int, length: int }; + | Dict_Var of { var: vname, index: int, length: int, class: class, unique: bool }; datatype itype = `%% of string * itype list @@ -259,17 +260,18 @@ (Name.invent_names vars "a" ((take l o drop j) tys)); in vs_tys `|==> IConst const `$$ ts @ map (IVar o fst) vs_tys end; -fun contains_dict_var t = - let - fun cont_dict (Dict (_, d)) = cont_plain_dict d - and cont_plain_dict (Dict_Const (_, dss)) = (exists o exists) cont_dict dss - | cont_plain_dict (Dict_Var _) = true; - fun cont_term (IConst { dicts = dss, ... }) = (exists o exists) cont_dict dss - | cont_term (IVar _) = false - | cont_term (t1 `$ t2) = cont_term t1 orelse cont_term t2 - | cont_term (_ `|=> t) = cont_term t - | cont_term (ICase { primitive = t, ... }) = cont_term t; - in cont_term t end; +fun exists_dict_var f (Dict (_, d)) = exists_plain_dict_var_pred f d +and exists_plain_dict_var_pred f (Dict_Const (_, dss)) = exists_dictss_var f dss + | exists_plain_dict_var_pred f (Dict_Var x) = f x +and exists_dictss_var f dss = (exists o exists) (exists_dict_var f) dss; + +fun contains_dict_var (IConst { dicts = dss, ... }) = exists_dictss_var (K true) dss + | contains_dict_var (IVar _) = false + | contains_dict_var (t1 `$ t2) = contains_dict_var t1 orelse contains_dict_var t2 + | contains_dict_var (_ `|=> t) = contains_dict_var t + | contains_dict_var (ICase { primitive = t, ... }) = contains_dict_var t; + +val unambiguous_dictss = not o exists_dictss_var (fn { unique, ... } => not unique); (** statements, abstract programs **) @@ -469,20 +471,27 @@ Weakening of (class * class) list * plain_typarg_witness and plain_typarg_witness = Global of (string * class) * typarg_witness list list - | Local of string * (int * sort); + | Local of { var: string, index: int, sort: sort, unique: bool }; + +fun brand_unique unique (w as Global _) = w + | brand_unique unique (Local { var, index, sort, unique = _ }) = + Local { var = var, index = index, sort = sort, unique = unique }; fun construct_dictionaries ctxt (proj_sort, algebra) permissive some_thm (ty, sort) (deps, program) = let - fun class_relation ((Weakening (classrels, x)), sub_class) super_class = - Weakening ((sub_class, super_class) :: classrels, x); + fun class_relation unique (Weakening (classrels, x), sub_class) super_class = + Weakening ((sub_class, super_class) :: classrels, brand_unique unique x); fun type_constructor (tyco, _) dss class = Weakening ([], Global ((tyco, class), (map o map) fst dss)); fun type_variable (TFree (v, sort)) = let val sort' = proj_sort sort; - in map_index (fn (n, class) => (Weakening ([], Local (v, (n, sort'))), class)) sort' end; + in map_index (fn (n, class) => (Weakening ([], Local + { var = v, index = n, sort = sort', unique = true }), class)) sort' + end; val typarg_witnesses = Sorts.of_sort_derivation algebra - {class_relation = fn _ => fn _ => Sorts.classrel_derivation algebra class_relation, + {class_relation = fn _ => fn unique => + Sorts.classrel_derivation algebra (class_relation unique), type_constructor = type_constructor, type_variable = type_variable} (ty, proj_sort sort) handle Sorts.CLASS_ERROR e => not_wellsorted ctxt permissive some_thm deps ty sort e; @@ -752,16 +761,18 @@ #>> (fn sort => (unprefix "'" v, sort)) and translate_dicts ctxt algbr eqngr permissive some_thm (ty, sort) = let - fun mk_dict (Weakening (classrels, x)) = + fun mk_dict (Weakening (classrels, d)) = fold_map (ensure_classrel ctxt algbr eqngr permissive) classrels - ##>> mk_plain_dict x + ##>> mk_plain_dict d #>> Dict and mk_plain_dict (Global (inst, dss)) = ensure_inst ctxt algbr eqngr permissive inst ##>> (fold_map o fold_map) mk_dict dss - #>> (fn (inst, dss) => Dict_Const (inst, dss)) - | mk_plain_dict (Local (v, (index, sort))) = - pair (Dict_Var { var = unprefix "'" v, index = index, length = length sort }) + #>> Dict_Const + | mk_plain_dict (Local { var, index, sort, unique }) = + ensure_class ctxt algbr eqngr permissive (nth sort index) + #>> (fn class => Dict_Var { var = unprefix "'" var, index = index, + length = length sort, class = class, unique = unique }) in construct_dictionaries ctxt algbr permissive some_thm (ty, sort) #-> (fn typarg_witnesses => fold_map mk_dict typarg_witnesses)