changed representation of constants

--- a/src/Pure/Tools/codegen_package.ML	Sat Feb 10 09:26:24 2007 +0100
+++ b/src/Pure/Tools/codegen_package.ML	Sat Feb 10 09:26:25 2007 +0100
@@ -349,10 +349,11 @@
 and appgen_default thy algbr funcgr strct ((c, ty), ts) trns =
   trns
   |> ensure_def_const thy algbr funcgr strct (CodegenConsts.norm_of_typ thy (c, ty))
-  ||>> exprgen_type thy algbr funcgr strct ty
+  ||>> fold_map (exprgen_type thy algbr funcgr strct) ((fst o Term.strip_type) ty)
+  ||>> exprgen_type thy algbr funcgr strct ((snd o Term.strip_type) ty)
   ||>> exprgen_dict_parms thy algbr funcgr strct (c, ty)
   ||>> fold_map (exprgen_term thy algbr funcgr strct) ts
-  |>> (fn (((c, ty), iss), ts) => IConst (c, (iss, ty)) `$$ ts)
+  |>> (fn ((((c, tys), ty), iss), ts) => IConst (c, (iss, tys)) `$$ ts)
 and select_appgen thy algbr funcgr strct ((c, ty), ts) trns =
   case Symtab.lookup (fst (CodegenPackageData.get thy)) c
    of SOME (i, (appgen, _)) =>
@@ -579,7 +580,7 @@
       error ("Term" ^ Sign.string_of_term thy t ^ "is polymorhpic"))
       t;
     val t' = codegen_term thy t;
-  in CodegenSerializer.eval_term thy (Code.get thy) (ref_spec, t') end;
+  in CodegenSerializer.eval_term thy CodegenNames.labelled_name (Code.get thy) (ref_spec, t') end;
 
 
 (* constant specifications with wildcards *)
@@ -623,7 +624,7 @@
 fun code raw_cs seris thy =
   let
     val seris' = map (fn (target, args as _ :: _) =>
-          (target, SOME (CodegenSerializer.get_serializer thy target args))
+          (target, SOME (CodegenSerializer.get_serializer thy target args CodegenNames.labelled_name))
       | (target, []) => (CodegenSerializer.assert_serializer thy target, NONE)) seris;
     val targets = case map fst seris' of [] => NONE | xs => SOME xs;
     val cs = maps (read_constspec thy targets) raw_cs;
@@ -654,8 +655,8 @@
     >> (fn (raw_cs, seris) => code raw_cs seris)
   );
 
-val (print_codethmsK, codeK, code_abstypeK, code_axiomsK) =
-  ("print_codethms", "code_gen", "code_abstype", "code_axioms");
+val (codeK, code_abstypeK, code_axiomsK, code_thmsK) =
+  ("code_gen", "code_abstype", "code_axioms", "code_thms");
 
 in
 
@@ -681,15 +682,13 @@
     >> (Toplevel.theory o constsubst_e)
   );
 
-val print_codethmsP =
-  OuterSyntax.improper_command print_codethmsK "print code theorems of this theory" OuterKeyword.diag
-    (Scan.option (P.$$$ "(" |-- Scan.repeat P.term --| P.$$$ ")")
-      >> (fn NONE => CodegenData.print_thms
-           | SOME cs => fn thy => print_codethms_e thy cs)
-      >> (fn f => Toplevel.no_timing o Toplevel.unknown_theory
-      o Toplevel.keep (f o Toplevel.theory_of)));
+val code_thmsP =
+  OuterSyntax.improper_command code_thmsK "print cached defining equations" OuterKeyword.diag
+    (Scan.repeat P.term
+      >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
+        o Toplevel.keep ((fn thy => print_codethms_e thy cs) o Toplevel.theory_of)));
 
-val _ = OuterSyntax.add_parsers [codeP, code_abstypeP, code_axiomsP, print_codethmsP];
+val _ = OuterSyntax.add_parsers [codeP, code_abstypeP, code_axiomsP, code_thmsP];
 
 end; (* local *)
 

--- a/src/Pure/Tools/codegen_thingol.ML	Sat Feb 10 09:26:24 2007 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML	Sat Feb 10 09:26:25 2007 +0100
@@ -23,7 +23,7 @@
       `%% of string * itype list
     | ITyVar of vname;
   datatype iterm =
-      IConst of string * (dict list list * itype)
+      IConst of string * (dict list list * itype list (*types of arguments*))
     | IVar of vname
     | `$ of iterm * iterm
     | `|-> of (vname * itype) * iterm
@@ -51,8 +51,8 @@
   val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option;
   val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm;
   val unfold_const_app: iterm ->
-    ((string * (dict list list * itype)) * iterm list) option;
-  val eta_expand: (string * (dict list list * itype)) * iterm list -> int -> iterm;
+    ((string * (dict list list * itype list)) * iterm list) option;
+  val eta_expand: (string * (dict list list * itype list)) * iterm list -> int -> iterm;
   val fold_constnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
   val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
   val fold_unbound_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
@@ -124,7 +124,7 @@
   | ITyVar of vname;
 
 datatype iterm =
-    IConst of string * (dict list list * itype)
+    IConst of string * (dict list list * itype list)
   | IVar of vname
   | `$ of iterm * iterm
   | `|-> of (vname * itype) * iterm
@@ -236,13 +236,12 @@
           add vs td #> fold (fn (p, t) => add vs p #> add vs t) bs;
   in add [] end;
 
-fun eta_expand (c as (_, (_, ty)), ts) k =
+fun eta_expand (c as (_, (_, tys)), ts) k =
   let
     val j = length ts;
     val l = k - j;
-    val tys = (curry Library.take l o curry Library.drop j o fst o unfold_fun) ty;
     val ctxt = (fold o fold_varnames) Name.declare ts Name.context;
-    val vs_tys = Name.names ctxt "a" tys;
+    val vs_tys = Name.names ctxt "a" ((curry Library.take l o curry Library.drop j) tys);
   in vs_tys `|--> IConst c `$$ ts @ map (fn (v, _) => IVar v) vs_tys end;
 
 
@@ -410,22 +409,15 @@
     code
     |> (if can (get_def code) name
         then
-          tracing (fn _ => "asserting definition " ^ labelled_name name)
-          #> add_dp dep
+          add_dp dep
         else
-          tracing (fn _ => "allocating definition " ^ labelled_name name
-            ^ (if strict then " (strict)" else " (non-strict)"))
-          #> ensure_bot name
+          ensure_bot name
           #> add_dp dep
-          #> tracing (fn _ => "creating definition " ^ labelled_name name)
           #> invoke_generator name defgen
           #-> (fn def => prep_def def)
           #-> (fn def =>
-             tracing (fn _ => "adding")
-          #> add_def_incr strict (name, def)
-          #> tracing (fn _ => "postprocessing")
+             add_def_incr strict (name, def)
           #> postprocess_def (name, def)
-          #> tracing (fn _ => "adding done")
        ))
     |> pair dep
   end;