--- a/src/Tools/Code/code_haskell.ML Thu Jun 17 15:59:46 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML Thu Jun 17 15:59:47 2010 +0200
@@ -75,7 +75,7 @@
then print_case tyvars some_thm vars fxy cases
else print_app tyvars some_thm vars fxy c_ts
| NONE => print_case tyvars some_thm vars fxy cases)
- and print_app_expr tyvars some_thm vars ((c, (_, tys)), ts) = case contr_classparam_typs c
+ and print_app_expr tyvars some_thm vars ((c, (_, function_typs)), ts) = case contr_classparam_typs c
of [] => (str o deresolve) c :: map (print_term tyvars some_thm vars BR) ts
| fingerprint => let
val ts_fingerprint = ts ~~ take (length ts) fingerprint;
@@ -86,7 +86,7 @@
brackets [print_term tyvars some_thm vars NOBR t, str "::", print_typ tyvars NOBR ty];
in
if needs_annotation then
- (str o deresolve) c :: map2 print_term_anno ts_fingerprint (take (length ts) tys)
+ (str o deresolve) c :: map2 print_term_anno ts_fingerprint (take (length ts) function_typs)
else (str o deresolve) c :: map (print_term tyvars some_thm vars BR) ts
end
and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) syntax_const
@@ -163,7 +163,7 @@
print_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
]
end
- | print_stmt (name, Code_Thingol.Datatype (_, (vs, [(co, [ty])]))) =
+ | print_stmt (name, Code_Thingol.Datatype (_, (vs, [((co, _), [ty])]))) =
let
val tyvars = intro_vars (map fst vs) reserved;
in
@@ -179,7 +179,7 @@
| print_stmt (name, Code_Thingol.Datatype (_, (vs, co :: cos))) =
let
val tyvars = intro_vars (map fst vs) reserved;
- fun print_co (co, tys) =
+ fun print_co ((co, _), tys) =
concat (
(str o deresolve_base) co
:: map (print_typ tyvars BR) tys
@@ -214,7 +214,7 @@
str "};"
) (map print_classparam classparams)
end
- | print_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, classparam_instances))) =
+ | print_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, (classparam_instances, _)))) =
let
val tyvars = intro_vars (map fst vs) reserved;
fun print_classparam_instance ((classparam, const), (thm, _)) = case syntax_const classparam
--- a/src/Tools/Code/code_ml.ML Thu Jun 17 15:59:46 2010 +0200
+++ b/src/Tools/Code/code_ml.ML Thu Jun 17 15:59:47 2010 +0200
@@ -33,13 +33,13 @@
ML_Function of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
| ML_Instance of string * ((class * (string * (vname * sort) list))
* ((class * (string * (string * dict list list))) list
- * ((string * const) * (thm * bool)) list));
+ * (((string * const) * (thm * bool)) list * ((string * const) * (thm * bool)) list)));
datatype ml_stmt =
ML_Exc of string * (typscheme * int)
| ML_Val of ml_binding
| ML_Funs of ml_binding list * string list
- | ML_Datas of (string * ((vname * sort) list * (string * itype list) list)) list
+ | ML_Datas of (string * ((vname * sort) list * ((string * vname list) * itype list) list)) list
| ML_Class of string * (vname * ((class * string) list * (string * itype) list));
fun stmt_name_of_binding (ML_Function (name, _)) = name
@@ -121,9 +121,9 @@
then print_case is_pseudo_fun some_thm vars fxy cases
else print_app is_pseudo_fun some_thm vars fxy c_ts
| NONE => print_case is_pseudo_fun some_thm vars fxy cases)
- and print_app_expr is_pseudo_fun some_thm vars (app as ((c, ((_, iss), tys)), ts)) =
+ and print_app_expr is_pseudo_fun some_thm vars (app as ((c, ((_, iss), function_typs)), ts)) =
if is_cons c then
- let val k = length tys in
+ let val k = length function_typs in
if k < 2 orelse length ts = k
then (str o deresolve) c
:: the_list (print_tuple (print_term is_pseudo_fun some_thm vars) BR ts)
@@ -174,8 +174,8 @@
[str "val", str (deresolve name), str ":", print_typscheme typscheme];
fun print_datatype_decl definer (tyco, (vs, cos)) =
let
- fun print_co (co, []) = str (deresolve co)
- | print_co (co, tys) = concat [str (deresolve co), str "of",
+ fun print_co ((co, _), []) = str (deresolve co)
+ | print_co ((co, _), tys) = concat [str (deresolve co), str "of",
enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
in
concat (
@@ -219,7 +219,7 @@
))
end
| print_def is_pseudo_fun _ definer
- (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, classparam_instances)))) =
+ (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, (classparam_instances, _))))) =
let
fun print_super_instance (_, (classrel, dss)) =
concat [
@@ -466,8 +466,8 @@
[str "val", str (deresolve name), str ":", print_typscheme typscheme];
fun print_datatype_decl definer (tyco, (vs, cos)) =
let
- fun print_co (co, []) = str (deresolve co)
- | print_co (co, tys) = concat [str (deresolve co), str "of",
+ fun print_co ((co, _), []) = str (deresolve co)
+ | print_co ((co, _), tys) = concat [str (deresolve co), str "of",
enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
in
concat (
@@ -554,7 +554,7 @@
))
end
| print_def is_pseudo_fun _ definer
- (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, classparam_instances)))) =
+ (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, (classparam_instances, _))))) =
let
fun print_super_instance (_, (classrel, dss)) =
concat [
--- a/src/Tools/Code/code_printer.ML Thu Jun 17 15:59:46 2010 +0200
+++ b/src/Tools/Code/code_printer.ML Thu Jun 17 15:59:47 2010 +0200
@@ -256,12 +256,12 @@
fold_map (Code_Thingol.ensure_declared_const thy) cs naming
|-> (fn cs' => pair (n, f literals cs'));
-fun gen_print_app print_app_expr print_term syntax_const thm vars fxy (app as ((c, (_, tys)), ts)) =
+fun gen_print_app print_app_expr print_term syntax_const thm vars fxy (app as ((c, (_, function_typs)), ts)) =
case syntax_const c
of NONE => brackify fxy (print_app_expr thm vars app)
| SOME (k, print) =>
let
- fun print' fxy ts = print (print_term thm) thm vars fxy (ts ~~ take k tys);
+ fun print' fxy ts = print (print_term thm) thm vars fxy (ts ~~ take k function_typs);
in if k = length ts
then print' fxy ts
else if k < length ts
--- a/src/Tools/Code/code_simp.ML Thu Jun 17 15:59:46 2010 +0200
+++ b/src/Tools/Code/code_simp.ML Thu Jun 17 15:59:47 2010 +0200
@@ -51,8 +51,8 @@
fun add_stmt (Code_Thingol.Fun (_, ((_, eqs), some_cong))) ss =
ss addsimps (map_filter (fst o snd)) eqs addcongs (the_list some_cong)
- | add_stmt (Code_Thingol.Classinst (_, (_, classparam_insts))) ss =
- ss addsimps (map (fst o snd) classparam_insts)
+ | add_stmt (Code_Thingol.Classinst (_, (_, (classparam_instances, _)))) ss =
+ ss addsimps (map (fst o snd) classparam_instances)
| add_stmt _ ss = ss;
val add_program = Graph.fold (add_stmt o fst o snd)
--- a/src/Tools/nbe.ML Thu Jun 17 15:59:46 2010 +0200
+++ b/src/Tools/nbe.ML Thu Jun 17 15:59:47 2010 +0200
@@ -417,7 +417,7 @@
[]
| eqns_of_stmt (_, Code_Thingol.Classparam _) =
[]
- | eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arity_args)), (super_instances, classparam_instances))) =
+ | eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arity_args)), (super_instances, (classparam_instances, _)))) =
[(inst, (arity_args, [([], IConst (class, (([], []), [])) `$$
map (fn (_, (_, (inst, dss))) => IConst (inst, (([], dss), []))) super_instances
@ map (IConst o snd o fst) classparam_instances)]))];