1.1 --- a/src/Tools/Code/code_haskell.ML Thu Jun 17 15:59:46 2010 +0200
1.2 +++ b/src/Tools/Code/code_haskell.ML Thu Jun 17 15:59:47 2010 +0200
1.3 @@ -75,7 +75,7 @@
1.4 then print_case tyvars some_thm vars fxy cases
1.5 else print_app tyvars some_thm vars fxy c_ts
1.6 | NONE => print_case tyvars some_thm vars fxy cases)
1.7 - and print_app_expr tyvars some_thm vars ((c, (_, tys)), ts) = case contr_classparam_typs c
1.8 + and print_app_expr tyvars some_thm vars ((c, (_, function_typs)), ts) = case contr_classparam_typs c
1.9 of [] => (str o deresolve) c :: map (print_term tyvars some_thm vars BR) ts
1.10 | fingerprint => let
1.11 val ts_fingerprint = ts ~~ take (length ts) fingerprint;
1.12 @@ -86,7 +86,7 @@
1.13 brackets [print_term tyvars some_thm vars NOBR t, str "::", print_typ tyvars NOBR ty];
1.14 in
1.15 if needs_annotation then
1.16 - (str o deresolve) c :: map2 print_term_anno ts_fingerprint (take (length ts) tys)
1.17 + (str o deresolve) c :: map2 print_term_anno ts_fingerprint (take (length ts) function_typs)
1.18 else (str o deresolve) c :: map (print_term tyvars some_thm vars BR) ts
1.19 end
1.20 and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) syntax_const
1.21 @@ -163,7 +163,7 @@
1.22 print_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
1.23 ]
1.24 end
1.25 - | print_stmt (name, Code_Thingol.Datatype (_, (vs, [(co, [ty])]))) =
1.26 + | print_stmt (name, Code_Thingol.Datatype (_, (vs, [((co, _), [ty])]))) =
1.27 let
1.28 val tyvars = intro_vars (map fst vs) reserved;
1.29 in
1.30 @@ -179,7 +179,7 @@
1.31 | print_stmt (name, Code_Thingol.Datatype (_, (vs, co :: cos))) =
1.32 let
1.33 val tyvars = intro_vars (map fst vs) reserved;
1.34 - fun print_co (co, tys) =
1.35 + fun print_co ((co, _), tys) =
1.36 concat (
1.37 (str o deresolve_base) co
1.38 :: map (print_typ tyvars BR) tys
1.39 @@ -214,7 +214,7 @@
1.40 str "};"
1.41 ) (map print_classparam classparams)
1.42 end
1.43 - | print_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, classparam_instances))) =
1.44 + | print_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, (classparam_instances, _)))) =
1.45 let
1.46 val tyvars = intro_vars (map fst vs) reserved;
1.47 fun print_classparam_instance ((classparam, const), (thm, _)) = case syntax_const classparam
2.1 --- a/src/Tools/Code/code_ml.ML Thu Jun 17 15:59:46 2010 +0200
2.2 +++ b/src/Tools/Code/code_ml.ML Thu Jun 17 15:59:47 2010 +0200
2.3 @@ -33,13 +33,13 @@
2.4 ML_Function of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
2.5 | ML_Instance of string * ((class * (string * (vname * sort) list))
2.6 * ((class * (string * (string * dict list list))) list
2.7 - * ((string * const) * (thm * bool)) list));
2.8 + * (((string * const) * (thm * bool)) list * ((string * const) * (thm * bool)) list)));
2.9
2.10 datatype ml_stmt =
2.11 ML_Exc of string * (typscheme * int)
2.12 | ML_Val of ml_binding
2.13 | ML_Funs of ml_binding list * string list
2.14 - | ML_Datas of (string * ((vname * sort) list * (string * itype list) list)) list
2.15 + | ML_Datas of (string * ((vname * sort) list * ((string * vname list) * itype list) list)) list
2.16 | ML_Class of string * (vname * ((class * string) list * (string * itype) list));
2.17
2.18 fun stmt_name_of_binding (ML_Function (name, _)) = name
2.19 @@ -121,9 +121,9 @@
2.20 then print_case is_pseudo_fun some_thm vars fxy cases
2.21 else print_app is_pseudo_fun some_thm vars fxy c_ts
2.22 | NONE => print_case is_pseudo_fun some_thm vars fxy cases)
2.23 - and print_app_expr is_pseudo_fun some_thm vars (app as ((c, ((_, iss), tys)), ts)) =
2.24 + and print_app_expr is_pseudo_fun some_thm vars (app as ((c, ((_, iss), function_typs)), ts)) =
2.25 if is_cons c then
2.26 - let val k = length tys in
2.27 + let val k = length function_typs in
2.28 if k < 2 orelse length ts = k
2.29 then (str o deresolve) c
2.30 :: the_list (print_tuple (print_term is_pseudo_fun some_thm vars) BR ts)
2.31 @@ -174,8 +174,8 @@
2.32 [str "val", str (deresolve name), str ":", print_typscheme typscheme];
2.33 fun print_datatype_decl definer (tyco, (vs, cos)) =
2.34 let
2.35 - fun print_co (co, []) = str (deresolve co)
2.36 - | print_co (co, tys) = concat [str (deresolve co), str "of",
2.37 + fun print_co ((co, _), []) = str (deresolve co)
2.38 + | print_co ((co, _), tys) = concat [str (deresolve co), str "of",
2.39 enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
2.40 in
2.41 concat (
2.42 @@ -219,7 +219,7 @@
2.43 ))
2.44 end
2.45 | print_def is_pseudo_fun _ definer
2.46 - (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, classparam_instances)))) =
2.47 + (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, (classparam_instances, _))))) =
2.48 let
2.49 fun print_super_instance (_, (classrel, dss)) =
2.50 concat [
2.51 @@ -466,8 +466,8 @@
2.52 [str "val", str (deresolve name), str ":", print_typscheme typscheme];
2.53 fun print_datatype_decl definer (tyco, (vs, cos)) =
2.54 let
2.55 - fun print_co (co, []) = str (deresolve co)
2.56 - | print_co (co, tys) = concat [str (deresolve co), str "of",
2.57 + fun print_co ((co, _), []) = str (deresolve co)
2.58 + | print_co ((co, _), tys) = concat [str (deresolve co), str "of",
2.59 enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
2.60 in
2.61 concat (
2.62 @@ -554,7 +554,7 @@
2.63 ))
2.64 end
2.65 | print_def is_pseudo_fun _ definer
2.66 - (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, classparam_instances)))) =
2.67 + (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, (classparam_instances, _))))) =
2.68 let
2.69 fun print_super_instance (_, (classrel, dss)) =
2.70 concat [
3.1 --- a/src/Tools/Code/code_printer.ML Thu Jun 17 15:59:46 2010 +0200
3.2 +++ b/src/Tools/Code/code_printer.ML Thu Jun 17 15:59:47 2010 +0200
3.3 @@ -256,12 +256,12 @@
3.4 fold_map (Code_Thingol.ensure_declared_const thy) cs naming
3.5 |-> (fn cs' => pair (n, f literals cs'));
3.6
3.7 -fun gen_print_app print_app_expr print_term syntax_const thm vars fxy (app as ((c, (_, tys)), ts)) =
3.8 +fun gen_print_app print_app_expr print_term syntax_const thm vars fxy (app as ((c, (_, function_typs)), ts)) =
3.9 case syntax_const c
3.10 of NONE => brackify fxy (print_app_expr thm vars app)
3.11 | SOME (k, print) =>
3.12 let
3.13 - fun print' fxy ts = print (print_term thm) thm vars fxy (ts ~~ take k tys);
3.14 + fun print' fxy ts = print (print_term thm) thm vars fxy (ts ~~ take k function_typs);
3.15 in if k = length ts
3.16 then print' fxy ts
3.17 else if k < length ts
4.1 --- a/src/Tools/Code/code_simp.ML Thu Jun 17 15:59:46 2010 +0200
4.2 +++ b/src/Tools/Code/code_simp.ML Thu Jun 17 15:59:47 2010 +0200
4.3 @@ -51,8 +51,8 @@
4.4
4.5 fun add_stmt (Code_Thingol.Fun (_, ((_, eqs), some_cong))) ss =
4.6 ss addsimps (map_filter (fst o snd)) eqs addcongs (the_list some_cong)
4.7 - | add_stmt (Code_Thingol.Classinst (_, (_, classparam_insts))) ss =
4.8 - ss addsimps (map (fst o snd) classparam_insts)
4.9 + | add_stmt (Code_Thingol.Classinst (_, (_, (classparam_instances, _)))) ss =
4.10 + ss addsimps (map (fst o snd) classparam_instances)
4.11 | add_stmt _ ss = ss;
4.12
4.13 val add_program = Graph.fold (add_stmt o fst o snd)
5.1 --- a/src/Tools/nbe.ML Thu Jun 17 15:59:46 2010 +0200
5.2 +++ b/src/Tools/nbe.ML Thu Jun 17 15:59:47 2010 +0200
5.3 @@ -417,7 +417,7 @@
5.4 []
5.5 | eqns_of_stmt (_, Code_Thingol.Classparam _) =
5.6 []
5.7 - | eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arity_args)), (super_instances, classparam_instances))) =
5.8 + | eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arity_args)), (super_instances, (classparam_instances, _)))) =
5.9 [(inst, (arity_args, [([], IConst (class, (([], []), [])) `$$
5.10 map (fn (_, (_, (inst, dss))) => IConst (inst, (([], dss), []))) super_instances
5.11 @ map (IConst o snd o fst) classparam_instances)]))];