adding the body type as well to the code generation for constants as it is required for type annotations of constants
1.1 --- a/src/Tools/Code/code_haskell.ML Wed Sep 07 13:51:30 2011 +0200
1.2 +++ b/src/Tools/Code/code_haskell.ML Wed Sep 07 13:51:32 2011 +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, ((_, function_typs), _)), 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;
2.1 --- a/src/Tools/Code/code_ml.ML Wed Sep 07 13:51:30 2011 +0200
2.2 +++ b/src/Tools/Code/code_ml.ML Wed Sep 07 13:51:32 2011 +0200
2.3 @@ -117,7 +117,7 @@
2.4 then print_case is_pseudo_fun some_thm vars fxy cases
2.5 else print_app is_pseudo_fun some_thm vars fxy c_ts
2.6 | NONE => print_case is_pseudo_fun some_thm vars fxy cases)
2.7 - and print_app_expr is_pseudo_fun some_thm vars (app as ((c, (((_, iss), function_typs), _)), ts)) =
2.8 + and print_app_expr is_pseudo_fun some_thm vars (app as ((c, (((_, iss), (function_typs, _)), _)), ts)) =
2.9 if is_cons c then
2.10 let val k = length function_typs in
2.11 if k < 2 orelse length ts = k
2.12 @@ -417,7 +417,7 @@
2.13 then print_case is_pseudo_fun some_thm vars fxy cases
2.14 else print_app is_pseudo_fun some_thm vars fxy c_ts
2.15 | NONE => print_case is_pseudo_fun some_thm vars fxy cases)
2.16 - and print_app_expr is_pseudo_fun some_thm vars (app as ((c, (((_, iss), tys), _)), ts)) =
2.17 + and print_app_expr is_pseudo_fun some_thm vars (app as ((c, (((_, iss), (tys, _)), _)), ts)) =
2.18 if is_cons c then
2.19 let val k = length tys in
2.20 if length ts = k
3.1 --- a/src/Tools/Code/code_printer.ML Wed Sep 07 13:51:30 2011 +0200
3.2 +++ b/src/Tools/Code/code_printer.ML Wed Sep 07 13:51:32 2011 +0200
3.3 @@ -315,7 +315,7 @@
3.4 |-> (fn cs' => pair (Complex_const_syntax (n, f literals cs')));
3.5
3.6 fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy
3.7 - (app as ((c, ((_, function_typs), _)), ts)) =
3.8 + (app as ((c, ((_, (function_typs, _)), _)), ts)) =
3.9 case const_syntax c of
3.10 NONE => brackify fxy (print_app_expr some_thm vars app)
3.11 | SOME (Plain_const_syntax (_, s)) =>
4.1 --- a/src/Tools/Code/code_scala.ML Wed Sep 07 13:51:30 2011 +0200
4.2 +++ b/src/Tools/Code/code_scala.ML Wed Sep 07 13:51:32 2011 +0200
4.3 @@ -72,7 +72,7 @@
4.4 else print_app tyvars is_pat some_thm vars fxy c_ts
4.5 | NONE => print_case tyvars some_thm vars fxy cases)
4.6 and print_app tyvars is_pat some_thm vars fxy
4.7 - (app as ((c, (((arg_typs, _), function_typs), _)), ts)) =
4.8 + (app as ((c, (((arg_typs, _), (function_typs, _)), _)), ts)) =
4.9 let
4.10 val k = length ts;
4.11 val arg_typs' = if is_pat orelse
4.12 @@ -265,7 +265,7 @@
4.13 let
4.14 val tyvars = intro_tyvars vs reserved;
4.15 val classtyp = (class, tyco `%% map (ITyVar o fst) vs);
4.16 - fun print_classparam_instance ((classparam, const as (_, ((_, tys), _))), (thm, _)) =
4.17 + fun print_classparam_instance ((classparam, const as (_, ((_, (tys, _)), _))), (thm, _)) =
4.18 let
4.19 val aux_tys = Name.invent_names (snd reserved) "a" tys;
4.20 val auxs = map fst aux_tys;
5.1 --- a/src/Tools/Code/code_thingol.ML Wed Sep 07 13:51:30 2011 +0200
5.2 +++ b/src/Tools/Code/code_thingol.ML Wed Sep 07 13:51:32 2011 +0200
5.3 @@ -22,7 +22,7 @@
5.4 datatype itype =
5.5 `%% of string * itype list
5.6 | ITyVar of vname;
5.7 - type const = string * (((itype list * dict list list) * itype list) * bool)
5.8 + type const = string * (((itype list * dict list list) * (itype list * itype)) * bool)
5.9 (* f [T1..Tn] {dicts} (_::S1) .. (_..Sm) =^= (f, (([T1..Tn], dicts), [S1..Sm]) *)
5.10 datatype iterm =
5.11 IConst of const
5.12 @@ -145,8 +145,8 @@
5.13 `%% of string * itype list
5.14 | ITyVar of vname;
5.15
5.16 -type const = string * (((itype list * dict list list) * itype list (*types of arguments*))
5.17 - * bool (*requires type annotation*))
5.18 +type const = string * (((itype list * dict list list) *
5.19 + (itype list (*types of arguments*) * itype (*body type*))) * bool (*requires type annotation*))
5.20
5.21 datatype iterm =
5.22 IConst of const
5.23 @@ -241,7 +241,7 @@
5.24 val vs_tys = (map o apfst) SOME (Name.invent_names ctxt "a" tys);
5.25 in (vs_tys, t `$$ map (IVar o fst) vs_tys) end;
5.26
5.27 -fun eta_expand k (c as (name, ((_, tys), _)), ts) =
5.28 +fun eta_expand k (c as (name, ((_, (tys, _)), _)), ts) =
5.29 let
5.30 val j = length ts;
5.31 val l = k - j;
5.32 @@ -751,14 +751,14 @@
5.33 else ()
5.34 val arg_typs = Sign.const_typargs thy (c, ty);
5.35 val sorts = Code_Preproc.sortargs eqngr c;
5.36 - val function_typs = Term.binder_types ty;
5.37 + val (function_typs, body_typ) = Term.strip_type ty;
5.38 in
5.39 ensure_const thy algbr eqngr permissive c
5.40 ##>> fold_map (translate_typ thy algbr eqngr permissive) arg_typs
5.41 ##>> fold_map (translate_dicts thy algbr eqngr permissive some_thm) (arg_typs ~~ sorts)
5.42 - ##>> fold_map (translate_typ thy algbr eqngr permissive) function_typs
5.43 - #>> (fn (((c, arg_typs), dss), function_typs) =>
5.44 - IConst (c, (((arg_typs, dss), function_typs), false))) (* FIXME *)
5.45 + ##>> fold_map (translate_typ thy algbr eqngr permissive) (body_typ :: function_typs)
5.46 + #>> (fn (((c, arg_typs), dss), body_typ :: function_typs) =>
5.47 + IConst (c, (((arg_typs, dss), (function_typs, body_typ)), false))) (* FIXME *)
5.48 end
5.49 and translate_app_const thy algbr eqngr permissive some_thm ((c_ty, ts), some_abs) =
5.50 translate_const thy algbr eqngr permissive some_thm (c_ty, some_abs)
5.51 @@ -803,7 +803,7 @@
5.52 val ts_clause = nth_drop t_pos ts;
5.53 val clauses = if null case_pats
5.54 then mk_clause (fn ([t], body) => (t, body)) [ty] (the_single ts_clause)
5.55 - else maps (fn ((constr as IConst (_, ((_, tys), _)), n), t) =>
5.56 + else maps (fn ((constr as IConst (_, ((_, (tys, _)), _)), n), t) =>
5.57 mk_clause (fn (ts, body) => (constr `$$ ts, body)) (take n tys) t)
5.58 (constrs ~~ ts_clause);
5.59 in ((t, ty), clauses) end;
6.1 --- a/src/Tools/nbe.ML Wed Sep 07 13:51:30 2011 +0200
6.2 +++ b/src/Tools/nbe.ML Wed Sep 07 13:51:32 2011 +0200
6.3 @@ -425,7 +425,7 @@
6.4 val params = Name.invent Name.context "d" (length names);
6.5 fun mk (k, name) =
6.6 (name, ([(v, [])],
6.7 - [([IConst (class, ((([], []), []), false)) `$$ map (IVar o SOME) params],
6.8 + [([IConst (class, ((([], []), ([], ITyVar "")), false)) `$$ map (IVar o SOME) params],
6.9 IVar (SOME (nth params k)))]));
6.10 in map_index mk names end
6.11 | eqns_of_stmt (_, Code_Thingol.Classrel _) =
6.12 @@ -433,8 +433,8 @@
6.13 | eqns_of_stmt (_, Code_Thingol.Classparam _) =
6.14 []
6.15 | eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arity_args)), (super_instances, (classparam_instances, _)))) =
6.16 - [(inst, (arity_args, [([], IConst (class, ((([], []), []), false)) `$$
6.17 - map (fn (_, (_, (inst, dss))) => IConst (inst, ((([], dss), []), false))) super_instances
6.18 + [(inst, (arity_args, [([], IConst (class, ((([], []), ([], ITyVar "")), false)) `$$
6.19 + map (fn (_, (_, (inst, dss))) => IConst (inst, ((([], dss), ([], ITyVar "")), false))) super_instances
6.20 @ map (IConst o snd o fst) classparam_instances)]))];
6.21
6.22