adding the body type as well to the code generation for constants as it is required for type annotations of constants
authorbulwahn
Wed Sep 07 13:51:32 2011 +0200 (2011-09-07)
changeset 447895a062c23c7db
parent 44788 8b935f1b3cf8
child 44790 c13fdf710a40
adding the body type as well to the code generation for constants as it is required for type annotations of constants
src/Tools/Code/code_haskell.ML
src/Tools/Code/code_ml.ML
src/Tools/Code/code_printer.ML
src/Tools/Code/code_scala.ML
src/Tools/Code/code_thingol.ML
src/Tools/nbe.ML
     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