--- a/src/Tools/Code/code_haskell.ML Wed Jul 03 00:08:29 2013 +0200
+++ b/src/Tools/Code/code_haskell.ML Thu Jul 04 09:13:49 2013 +0200
@@ -228,7 +228,7 @@
of NONE => NONE
| SOME (Code_Printer.Plain_const_syntax _) => SOME 0
| SOME (Code_Printer.Complex_const_syntax (k,_ )) => SOME k;
- fun print_classparam_instance ((classparam, const), (thm, _)) =
+ fun print_classparam_instance ((classparam, (const, _)), (thm, _)) =
case requires_args classparam
of NONE => semicolon [
(str o Long_Name.base_name o deresolve) classparam,
--- a/src/Tools/Code/code_ml.ML Wed Jul 03 00:08:29 2013 +0200
+++ b/src/Tools/Code/code_ml.ML Thu Jul 04 09:13:49 2013 +0200
@@ -30,8 +30,8 @@
ML_Function of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
| ML_Instance of string * { class: string, tyco: string, vs: (vname * sort) list,
superinsts: (class * (string * (string * dict list list))) list,
- inst_params: ((string * const) * (thm * bool)) list,
- superinst_params: ((string * const) * (thm * bool)) list };
+ inst_params: ((string * (const * int)) * (thm * bool)) list,
+ superinst_params: ((string * (const * int)) * (thm * bool)) list };
datatype ml_stmt =
ML_Exc of string * (typscheme * int)
@@ -215,7 +215,7 @@
str "=",
print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const x))
];
- fun print_classparam_instance ((classparam, const), (thm, _)) =
+ fun print_classparam_instance ((classparam, (const, _)), (thm, _)) =
concat [
(str o Long_Name.base_name o deresolve) classparam,
str "=",
@@ -552,7 +552,7 @@
str "=",
print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const x))
];
- fun print_classparam_instance ((classparam, const), (thm, _)) =
+ fun print_classparam_instance ((classparam, (const, _)), (thm, _)) =
concat [
(str o deresolve) classparam,
str "=",
--- a/src/Tools/Code/code_scala.ML Wed Jul 03 00:08:29 2013 +0200
+++ b/src/Tools/Code/code_scala.ML Thu Jul 04 09:13:49 2013 +0200
@@ -260,17 +260,21 @@
let
val tyvars = intro_tyvars vs reserved;
val classtyp = (class, tyco `%% map (ITyVar o fst) vs);
- fun print_classparam_instance ((classparam, const as { dom, ... }), (thm, _)) =
+ fun print_classparam_instance ((classparam, (const as { dom, ... }, dom_length)), (thm, _)) =
let
val aux_dom = Name.invent_names (snd reserved) "a" dom;
val auxs = map fst aux_dom;
val vars = intro_vars auxs reserved;
- val aux_abstr = if null auxs then [] else [enum "," "(" ")"
- (map (fn (aux, ty) => constraint ((str o lookup_var vars) aux)
- (print_typ tyvars NOBR ty)) aux_dom), str "=>"];
+ val (aux_dom1, aux_dom2) = chop dom_length aux_dom;
+ fun abstract_using [] = []
+ | abstract_using aux_dom = [enum "," "(" ")"
+ (map (fn (aux, ty) => constraint ((str o lookup_var vars) aux)
+ (print_typ tyvars NOBR ty)) aux_dom), str "=>"];
+ val aux_abstr1 = abstract_using aux_dom1;
+ val aux_abstr2 = abstract_using aux_dom2;
in
concat ([str "val", print_method classparam, str "="]
- @ aux_abstr @| print_app tyvars false (SOME thm) vars NOBR
+ @ aux_abstr1 @ aux_abstr2 @| print_app tyvars false (SOME thm) vars NOBR
(const, map (IVar o SOME) auxs))
end;
in
--- a/src/Tools/Code/code_thingol.ML Wed Jul 03 00:08:29 2013 +0200
+++ b/src/Tools/Code/code_thingol.ML Thu Jul 04 09:13:49 2013 +0200
@@ -78,8 +78,8 @@
| Classparam of string * class
| Classinst of { class: string, tyco: string, vs: (vname * sort) list,
superinsts: (class * (string * (string * dict list list))) list,
- inst_params: ((string * const) * (thm * bool)) list,
- superinst_params: ((string * const) * (thm * bool)) list };
+ inst_params: ((string * (const * int)) * (thm * bool)) list,
+ superinst_params: ((string * (const * int)) * (thm * bool)) list };
type program = stmt Graph.T
val empty_funs: program -> string list
val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm
@@ -428,8 +428,8 @@
| Classparam of string * class
| Classinst of { class: string, tyco: string, vs: (vname * sort) list,
superinsts: (class * (string * (string * dict list list))) list,
- inst_params: ((string * const) * (thm * bool)) list,
- superinst_params: ((string * const) * (thm * bool)) list };
+ inst_params: ((string * (const * int)) * (thm * bool)) list,
+ superinst_params: ((string * (const * int)) * (thm * bool)) list };
type program = stmt Graph.T;
@@ -448,7 +448,7 @@
primitive = map_terms_bottom_up f t0 });
fun map_classparam_instances_as_term f =
- (map o apfst o apsnd) (fn const => case f (IConst const) of IConst const' => const')
+ (map o apfst o apsnd o apfst) (fn const => case f (IConst const) of IConst const' => const')
fun map_terms_stmt f NoStmt = NoStmt
| map_terms_stmt f (Fun (c, ((tysm, eqs), case_cong))) = Fun (c, ((tysm, (map o apfst)
@@ -708,13 +708,14 @@
fun translate_classparam_instance (c, ty) =
let
val raw_const = Const (c, map_type_tfree (K arity_typ') ty);
+ val dom_length = length (fst (strip_type ty))
val thm = Axclass.unoverload_conv thy (Thm.cterm_of thy raw_const);
val const = (apsnd Logic.unvarifyT_global o dest_Const o snd
o Logic.dest_equals o Thm.prop_of) thm;
in
ensure_const thy algbr eqngr permissive c
##>> translate_const thy algbr eqngr permissive (SOME thm) (const, NONE)
- #>> (fn (c, IConst const') => ((c, const'), (thm, true)))
+ #>> (fn (c, IConst const') => ((c, (const', dom_length)), (thm, true)))
end;
val stmt_inst =
ensure_class thy algbr eqngr permissive class
--- a/src/Tools/nbe.ML Wed Jul 03 00:08:29 2013 +0200
+++ b/src/Tools/nbe.ML Thu Jul 04 09:13:49 2013 +0200
@@ -439,7 +439,7 @@
| eqns_of_stmt (inst, Code_Thingol.Classinst { class, vs, superinsts, inst_params, ... }) =
[(inst, (vs, [([], dummy_const class [] `$$
map (fn (_, (_, (inst, dss))) => dummy_const inst dss) superinsts
- @ map (IConst o snd o fst) inst_params)]))];
+ @ map (IConst o fst o snd o fst) inst_params)]))];
(* compile whole programs *)