added eval_term

--- a/src/Pure/Tools/codegen_package.ML	Wed Jul 26 11:32:55 2006 +0200
+++ b/src/Pure/Tools/codegen_package.ML	Wed Jul 26 13:31:07 2006 +0200
@@ -64,7 +64,7 @@
 fun alias_get name = (fst o !) alias_ref name;
 fun alias_rev name = (snd o !) alias_ref name;
 
-val nsp_module = ""; (* a dummy by convention *)
+val nsp_module = ""; (*a dummy by convention*)
 val nsp_class = "class";
 val nsp_tyco = "tyco";
 val nsp_const = "const";
@@ -73,6 +73,7 @@
 val nsp_mem = "mem";
 val nsp_inst = "inst";
 val nsp_instmem = "instmem";
+val nsp_eval = "EVAL"; (*only for evaluation*)
 
 fun add_nsp shallow name =
   name
@@ -1040,24 +1041,11 @@
   |> CodegenTheorems.notify_dirty
   |> `(#modl o CodegenData.get);
 
-fun serialize_module module (target_data : target_data) cs seri =
-  let
-    val s_class = #syntax_class target_data
-    val s_tyco = #syntax_tyco target_data
-    val s_const = #syntax_const target_data
-  in
-    (seri (
-      Symtab.lookup s_class,
-      (Option.map fst oo Symtab.lookup) s_tyco,
-      (Option.map fst oo Symtab.lookup) s_const
-    ) (Symtab.keys s_class @ Symtab.keys s_tyco @ Symtab.keys s_const, cs) module : unit)
-  end;
-
 fun eval_term (ref_spec, t) thy =
   let
     val target_data =
       ((fn data => (the o Symtab.lookup data) "ml") o #target_data o CodegenData.get) thy;
-    val eval = CodegenSerializer.eval_term nsp_dtcon [[nsp_module], [nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_class, nsp_mem, nsp_inst, nsp_instmem]]
+    val eval = CodegenSerializer.eval_term nsp_eval nsp_dtcon [[nsp_module], [nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_class, nsp_mem, nsp_inst, nsp_instmem], [nsp_eval]]
       ((Option.map fst oo Symtab.lookup) (#syntax_tyco target_data),
        (Option.map fst oo Symtab.lookup) (#syntax_const target_data))
       (Symtab.keys (#syntax_tyco target_data) @ Symtab.keys (#syntax_const target_data))
@@ -1240,8 +1228,15 @@
           |> CodegenData.get
           |> #target_data
           |> (fn data => (the oo Symtab.lookup) data target);
+        val s_class = #syntax_class target_data
+        val s_tyco = #syntax_tyco target_data
+        val s_const = #syntax_const target_data
       in
-        (serialize_module module target_data cs; thy)
+        (seri (
+          Symtab.lookup s_class,
+          (Option.map fst oo Symtab.lookup) s_tyco,
+          (Option.map fst oo Symtab.lookup) s_const
+        ) (Symtab.keys s_class @ Symtab.keys s_tyco @ Symtab.keys s_const, cs) module : unit; thy)
       end;
   in
     thy

--- a/src/Pure/Tools/codegen_serializer.ML	Wed Jul 26 11:32:55 2006 +0200
+++ b/src/Pure/Tools/codegen_serializer.ML	Wed Jul 26 13:31:07 2006 +0200
@@ -26,7 +26,7 @@
     haskell: string * (string * string list -> serializer)
   };
   val mk_flat_ml_resolver: string list -> string -> string;
-  val eval_term: string -> string list list
+  val eval_term: string -> string -> string list list
       -> (string -> CodegenThingol.itype pretty_syntax option)
             * (string -> CodegenThingol.iterm pretty_syntax option)
       -> string list
@@ -797,16 +797,16 @@
     || parse_single_file serializer
   end;
 
-fun eval_term nsp_dtcon nspgrp (syntax_tyco, syntax_const) hidden ((ref_name, reff), e) modl =
+fun eval_term nsp_eval nsp_dtcon nspgrp (syntax_tyco, syntax_const) hidden ((ref_name, reff), e) modl =
   let
-    val (val_name, modl') = CodegenThingol.add_eval_def e modl;
+    val (val_name, modl') = CodegenThingol.add_eval_def (nsp_eval, e) modl;
     val struct_name = "EVAL";
     val serializer = ml_serializer struct_name "ml" nsp_dtcon nspgrp
       (fn "" => (fn p => (use_text Context.ml_output false (Pretty.output p); NONE))
-        | _ => SOME) (K NONE, syntax_tyco, syntax_const) (hidden, SOME [val_name]);
+        | _ => SOME) (K NONE, syntax_tyco, syntax_const) (hidden, SOME [NameSpace.pack [nsp_eval, val_name]]);
     val _ = serializer modl';
     val val_name_struct = NameSpace.append struct_name val_name;
-    val _ = use_text Context.ml_output false ("val _ = (" ^ ref_name ^ " := " ^ val_name_struct ^ ")");
+    val _ = use_text Context.ml_output false ("val _ = (" ^ ref_name ^ " := " ^ val_name_struct ^ "())");
     val value = ! reff;
   in value end;
 

--- a/src/Pure/Tools/codegen_thingol.ML	Wed Jul 26 11:32:55 2006 +0200
+++ b/src/Pure/Tools/codegen_thingol.ML	Wed Jul 26 13:31:07 2006 +0200
@@ -88,7 +88,7 @@
   val diff_module: module * module -> (string * def) list;
   val project_module: string list -> module -> module;
   val purge_module: string list -> module -> module;
-  val add_eval_def: iterm -> module -> string * module;
+  val add_eval_def: string (*shallow name space*) * iterm -> module -> string * module;
   val delete_garbage: string list (*hidden definitions*) -> module -> module;
   val has_nsp: string -> string -> bool;
   val ensure_def: (string -> transact -> def transact_fin) -> bool -> string
@@ -833,7 +833,7 @@
     empty_module
     |> fold (fn name => add_def (name, get_def modl name)) selected
 (*     |> fold ensure_bot (hidden @ bots')  *)
-    |> fold (fn (x, y) => (writeln ("adding " ^ x ^ " -> " ^ y); add_dep (x, y))) adddeps
+    |> fold (fn (x, y) => ((*writeln ("adding " ^ x ^ " -> " ^ y);*) add_dep (x, y))) adddeps
   end;
 
 fun allimports_of modl =
@@ -1028,13 +1028,14 @@
     |-> (fn x => fn (_, modl) => (x, modl))
   end;
 
-fun add_eval_def e modl =
+fun add_eval_def (shallow, e) modl =
   let
-    val name = hd (Name.invent_list (Graph.keys modl) "VALUE" 1);
+    val name = "VALUE";
+    val sname = NameSpace.pack [shallow, name];
   in
     modl
-    |> add_def (name, Fun ([([], e)], ([], "" `%% [])))
-    |> fold (curry add_dep name) (add_deps_of_term e [])
+    |> add_def (sname, Fun ([([], e)], ([("a", [])], ITyVar "a")))
+    |> fold (curry add_dep sname) (add_deps_of_term e [])
     |> pair name
   end;