--- 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,
--- 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:
-\<close>
-
-class %quote class1 =
- fixes foo :: "'a \<Rightarrow> 'a"
-
-class %quote class2 = class1
-
-class %quote class3 = class1
-
-text \<open>
- \noindent Here both @{class class2} and @{class class3} inherit from @{class class1},
- forming the upper part of a diamond.
-\<close>
-
-definition %quote bar :: "'a :: {class2, class3} \<Rightarrow> 'a" where
- "bar = foo"
-
-text \<open>
- \noindent This yields the following code:
-\<close>
-
-text %quotetypewriter \<open>
- @{code_stmts bar (Scala)}
\<close>
-text \<open>
- \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}:
-\<close>
-
-class %quote class4 = class2 + class3
-
-text \<open>
- \noindent Then the offending code equation can be restricted to
- @{class class4}:
-\<close>
-
-lemma %quote [code]:
- "(bar :: 'a::class4 \<Rightarrow> 'a) = foo"
- by (simp only: bar_def)
-
-text \<open>
- \noindent with the following code:
-\<close>
-
-text %quotetypewriter \<open>
- @{code_stmts bar (Scala)}
-\<close>
-
-text \<open>
- \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.
-\<close>
subsection \<open>Modules namespace\<close>
--- 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) =
--- 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))
--- 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)