# HG changeset patch # User bulwahn # Date 1315396292 -7200 # Node ID 5a062c23c7db9802627f4d652bbeba72793b78ba # Parent 8b935f1b3cf886bc190591b0ee5a2f95e99f74c6 adding the body type as well to the code generation for constants as it is required for type annotations of constants diff -r 8b935f1b3cf8 -r 5a062c23c7db src/Tools/Code/code_haskell.ML --- a/src/Tools/Code/code_haskell.ML Wed Sep 07 13:51:30 2011 +0200 +++ b/src/Tools/Code/code_haskell.ML Wed Sep 07 13:51:32 2011 +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, ((_, function_typs), _)), 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; diff -r 8b935f1b3cf8 -r 5a062c23c7db src/Tools/Code/code_ml.ML --- a/src/Tools/Code/code_ml.ML Wed Sep 07 13:51:30 2011 +0200 +++ b/src/Tools/Code/code_ml.ML Wed Sep 07 13:51:32 2011 +0200 @@ -117,7 +117,7 @@ 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), function_typs), _)), 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 function_typs in if k < 2 orelse length ts = k @@ -417,7 +417,7 @@ 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), (tys, _)), _)), ts)) = if is_cons c then let val k = length tys in if length ts = k diff -r 8b935f1b3cf8 -r 5a062c23c7db src/Tools/Code/code_printer.ML --- a/src/Tools/Code/code_printer.ML Wed Sep 07 13:51:30 2011 +0200 +++ b/src/Tools/Code/code_printer.ML Wed Sep 07 13:51:32 2011 +0200 @@ -315,7 +315,7 @@ |-> (fn cs' => pair (Complex_const_syntax (n, f literals cs'))); fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy - (app as ((c, ((_, function_typs), _)), ts)) = + (app as ((c, ((_, (function_typs, _)), _)), ts)) = case const_syntax c of NONE => brackify fxy (print_app_expr some_thm vars app) | SOME (Plain_const_syntax (_, s)) => diff -r 8b935f1b3cf8 -r 5a062c23c7db src/Tools/Code/code_scala.ML --- a/src/Tools/Code/code_scala.ML Wed Sep 07 13:51:30 2011 +0200 +++ b/src/Tools/Code/code_scala.ML Wed Sep 07 13:51:32 2011 +0200 @@ -72,7 +72,7 @@ else print_app tyvars is_pat some_thm vars fxy c_ts | NONE => print_case tyvars some_thm vars fxy cases) and print_app tyvars is_pat some_thm vars fxy - (app as ((c, (((arg_typs, _), function_typs), _)), ts)) = + (app as ((c, (((arg_typs, _), (function_typs, _)), _)), ts)) = let val k = length ts; val arg_typs' = if is_pat orelse @@ -265,7 +265,7 @@ let val tyvars = intro_tyvars vs reserved; val classtyp = (class, tyco `%% map (ITyVar o fst) vs); - fun print_classparam_instance ((classparam, const as (_, ((_, tys), _))), (thm, _)) = + fun print_classparam_instance ((classparam, const as (_, ((_, (tys, _)), _))), (thm, _)) = let val aux_tys = Name.invent_names (snd reserved) "a" tys; val auxs = map fst aux_tys; diff -r 8b935f1b3cf8 -r 5a062c23c7db src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Wed Sep 07 13:51:30 2011 +0200 +++ b/src/Tools/Code/code_thingol.ML Wed Sep 07 13:51:32 2011 +0200 @@ -22,7 +22,7 @@ datatype itype = `%% of string * itype list | ITyVar of vname; - type const = string * (((itype list * dict list list) * itype list) * bool) + type const = string * (((itype list * dict list list) * (itype list * itype)) * bool) (* f [T1..Tn] {dicts} (_::S1) .. (_..Sm) =^= (f, (([T1..Tn], dicts), [S1..Sm]) *) datatype iterm = IConst of const @@ -145,8 +145,8 @@ `%% of string * itype list | ITyVar of vname; -type const = string * (((itype list * dict list list) * itype list (*types of arguments*)) - * bool (*requires type annotation*)) +type const = string * (((itype list * dict list list) * + (itype list (*types of arguments*) * itype (*body type*))) * bool (*requires type annotation*)) datatype iterm = IConst of const @@ -241,7 +241,7 @@ val vs_tys = (map o apfst) SOME (Name.invent_names ctxt "a" tys); in (vs_tys, t `$$ map (IVar o fst) vs_tys) end; -fun eta_expand k (c as (name, ((_, tys), _)), ts) = +fun eta_expand k (c as (name, ((_, (tys, _)), _)), ts) = let val j = length ts; val l = k - j; @@ -751,14 +751,14 @@ else () val arg_typs = Sign.const_typargs thy (c, ty); val sorts = Code_Preproc.sortargs eqngr c; - val function_typs = Term.binder_types ty; + val (function_typs, body_typ) = Term.strip_type ty; in ensure_const thy algbr eqngr permissive c ##>> fold_map (translate_typ thy algbr eqngr permissive) arg_typs ##>> fold_map (translate_dicts thy algbr eqngr permissive some_thm) (arg_typs ~~ sorts) - ##>> fold_map (translate_typ thy algbr eqngr permissive) function_typs - #>> (fn (((c, arg_typs), dss), function_typs) => - IConst (c, (((arg_typs, dss), function_typs), false))) (* FIXME *) + ##>> fold_map (translate_typ thy algbr eqngr permissive) (body_typ :: function_typs) + #>> (fn (((c, arg_typs), dss), body_typ :: function_typs) => + IConst (c, (((arg_typs, dss), (function_typs, body_typ)), false))) (* FIXME *) end and translate_app_const thy algbr eqngr permissive some_thm ((c_ty, ts), some_abs) = translate_const thy algbr eqngr permissive some_thm (c_ty, some_abs) @@ -803,7 +803,7 @@ val ts_clause = nth_drop t_pos ts; val clauses = if null case_pats then mk_clause (fn ([t], body) => (t, body)) [ty] (the_single ts_clause) - else maps (fn ((constr as IConst (_, ((_, tys), _)), n), t) => + else maps (fn ((constr as IConst (_, ((_, (tys, _)), _)), n), t) => mk_clause (fn (ts, body) => (constr `$$ ts, body)) (take n tys) t) (constrs ~~ ts_clause); in ((t, ty), clauses) end; diff -r 8b935f1b3cf8 -r 5a062c23c7db src/Tools/nbe.ML --- a/src/Tools/nbe.ML Wed Sep 07 13:51:30 2011 +0200 +++ b/src/Tools/nbe.ML Wed Sep 07 13:51:32 2011 +0200 @@ -425,7 +425,7 @@ val params = Name.invent Name.context "d" (length names); fun mk (k, name) = (name, ([(v, [])], - [([IConst (class, ((([], []), []), false)) `$$ map (IVar o SOME) params], + [([IConst (class, ((([], []), ([], ITyVar "")), false)) `$$ map (IVar o SOME) params], IVar (SOME (nth params k)))])); in map_index mk names end | eqns_of_stmt (_, Code_Thingol.Classrel _) = @@ -433,8 +433,8 @@ | eqns_of_stmt (_, Code_Thingol.Classparam _) = [] | eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arity_args)), (super_instances, (classparam_instances, _)))) = - [(inst, (arity_args, [([], IConst (class, ((([], []), []), false)) `$$ - map (fn (_, (_, (inst, dss))) => IConst (inst, ((([], dss), []), false))) super_instances + [(inst, (arity_args, [([], IConst (class, ((([], []), ([], ITyVar "")), false)) `$$ + map (fn (_, (_, (inst, dss))) => IConst (inst, ((([], dss), ([], ITyVar "")), false))) super_instances @ map (IConst o snd o fst) classparam_instances)]))];