tuned

--- a/src/Pure/Isar/code.ML	Wed Aug 15 08:57:41 2007 +0200
+++ b/src/Pure/Isar/code.ML	Wed Aug 15 08:57:42 2007 +0200
@@ -638,10 +638,8 @@
         | NONE => check_typ_fun (const, thm);
   in check_typ (fst (CodeUnit.head_func thm), thm) end;
 
-val mk_func = CodeUnit.error_thm
-  (assert_func_typ o CodeUnit.mk_func);
-val mk_func_liberal = CodeUnit.warning_thm
-  (assert_func_typ o CodeUnit.mk_func);
+val mk_func = CodeUnit.error_thm (assert_func_typ o CodeUnit.mk_func);
+val mk_func_liberal = CodeUnit.warning_thm (assert_func_typ o CodeUnit.mk_func);
 
 end;
 

--- a/src/Tools/code/code_funcgr.ML	Wed Aug 15 08:57:41 2007 +0200
+++ b/src/Tools/code/code_funcgr.ML	Wed Aug 15 08:57:42 2007 +0200
@@ -12,25 +12,18 @@
   val timing: bool ref
   val funcs: T -> CodeUnit.const -> thm list
   val typ: T -> CodeUnit.const -> typ
-  val deps: T -> CodeUnit.const list -> CodeUnit.const list list
   val all: T -> CodeUnit.const list
   val pretty: theory -> T -> Pretty.T
+  val make: theory -> CodeUnit.const list -> T
+  val make_consts: theory -> CodeUnit.const list -> CodeUnit.const list * T
+  val eval_conv: theory -> (T -> cterm -> thm) -> cterm -> thm
+  val eval_term: theory -> (T -> cterm -> 'a) -> cterm -> 'a
+  val intervene: theory -> T -> T
+    (*FIXME drop intervene as soon as possible*)
   structure Constgraph : GRAPH
 end
 
-signature CODE_FUNCGR_RETRIEVAL =
-sig
-  type T (* = CODE_FUNCGR.T *)
-  val make: theory -> CodeUnit.const list -> T
-  val make_consts: theory -> CodeUnit.const list -> CodeUnit.const list * T
-  val make_term: theory -> (T -> (thm -> thm) -> cterm -> thm -> 'a) -> cterm -> 'a * T
-    (*FIXME drop make_term as soon as possible*)
-  val eval_conv: theory -> (T -> cterm -> thm) -> cterm -> thm
-  val intervene: theory -> T -> T
-    (*FIXME drop intervene as soon as possible*)
-end;
-
-structure CodeFuncgr = (*signature is added later*)
+structure CodeFuncgr : CODE_FUNCGR =
 struct
 
 (** the graph type **)
@@ -48,15 +41,6 @@
 fun typ funcgr =
   fst o Constgraph.get_node funcgr;
 
-fun deps funcgr cs =
-  let
-    val conn = Constgraph.strong_conn funcgr;
-    val order = rev conn;
-  in
-    (map o filter) (member (op =) (Constgraph.all_succs funcgr cs)) order
-    |> filter_out null
-  end;
-
 fun all funcgr = Constgraph.keys funcgr;
 
 fun pretty thy funcgr =
@@ -208,7 +192,7 @@
     |> instances_of thy algebra
   end;
 
-fun ensure_const' rewrites thy algebra funcgr const auxgr =
+fun ensure_const' thy algebra funcgr const auxgr =
   if can (Constgraph.get_node funcgr) const
     then (NONE, auxgr)
   else if can (Constgraph.get_node auxgr) const
@@ -219,26 +203,25 @@
     |> pair (SOME const)
   else let
     val thms = Code.these_funcs thy const
-      |> map (CodeUnit.rewrite_func (rewrites thy))
       |> CodeUnit.norm_args
       |> CodeUnit.norm_varnames CodeName.purify_tvar CodeName.purify_var;
     val rhs = consts_of (const, thms);
   in
     auxgr
     |> Constgraph.new_node (const, thms)
-    |> fold_map (ensure_const rewrites thy algebra funcgr) rhs
+    |> fold_map (ensure_const thy algebra funcgr) rhs
     |-> (fn rhs' => fold (fn SOME const' => Constgraph.add_edge (const, const')
                            | NONE => I) rhs')
     |> pair (SOME const)
   end
-and ensure_const rewrites thy algebra funcgr const =
+and ensure_const thy algebra funcgr const =
   let
     val timeap = if !timing
       then Output.timeap_msg ("time for " ^ CodeUnit.string_of_const thy const)
       else I;
-  in timeap (ensure_const' rewrites thy algebra funcgr const) end;
+  in timeap (ensure_const' thy algebra funcgr const) end;
 
-fun merge_funcss rewrites thy algebra raw_funcss funcgr =
+fun merge_funcss thy algebra raw_funcss funcgr =
   let
     val funcss = raw_funcss
       |> resort_funcss thy algebra funcgr
@@ -267,7 +250,7 @@
           (fold_consts (insert (op =)) thms []);
       in
         funcgr
-        |> ensure_consts' rewrites thy algebra insts
+        |> ensure_consts' thy algebra insts
         |> fold (curry Constgraph.add_edge const) deps
         |> fold (curry Constgraph.add_edge const) insts
        end;
@@ -276,22 +259,22 @@
     |> fold add_funcs funcss
     |> fold add_deps funcss
   end
-and ensure_consts' rewrites thy algebra cs funcgr =
+and ensure_consts' thy algebra cs funcgr =
   let
     val auxgr = Constgraph.empty
-      |> fold (snd oo ensure_const rewrites thy algebra funcgr) cs;
+      |> fold (snd oo ensure_const thy algebra funcgr) cs;
   in
     funcgr
-    |> fold (merge_funcss rewrites thy algebra)
+    |> fold (merge_funcss thy algebra)
          (map (AList.make (Constgraph.get_node auxgr))
          (rev (Constgraph.strong_conn auxgr)))
   end handle INVALID (cs', msg)
     => raise INVALID (fold (insert CodeUnit.eq_const) cs' cs, msg);
 
-fun ensure_consts rewrites thy consts funcgr =
+fun ensure_consts thy consts funcgr =
   let
     val algebra = Code.coregular_algebra thy
-  in ensure_consts' rewrites thy algebra consts funcgr
+  in ensure_consts' thy algebra consts funcgr
     handle INVALID (cs', msg) => error (msg ^ ",\nwhile preprocessing equations for constant(s) "
     ^ commas (map (CodeUnit.string_of_const thy) cs'))
   end;
@@ -302,16 +285,16 @@
 
 val ensure_consts = ensure_consts;
 
-fun check_consts rewrites thy consts funcgr =
+fun check_consts thy consts funcgr =
   let
     val algebra = Code.coregular_algebra thy;
     fun try_const const funcgr =
-      (SOME const, ensure_consts' rewrites thy algebra [const] funcgr)
+      (SOME const, ensure_consts' thy algebra [const] funcgr)
       handle INVALID (cs', msg) => (NONE, funcgr);
     val (consts', funcgr') = fold_map try_const consts funcgr;
   in (map_filter I consts', funcgr') end;
 
-fun ensure_consts_term rewrites thy f ct funcgr =
+fun ensure_consts_term_proto thy f ct funcgr =
   let
     fun consts_of thy t =
       fold_aterms (fn Const c => cons (CodeUnit.const_of_cexpr thy c) | _ => I) t []
@@ -321,11 +304,10 @@
       in Thm.transitive thm thm' end
     val _ = Sign.no_vars (Sign.pp thy) (Thm.term_of ct);
     val _ = Term.fold_types (Type.no_tvars #> K I) (Thm.term_of ct) ();
-    val thm1 = Code.preprocess_conv ct
-      |> fold (rhs_conv o MetaSimplifier.rewrite false o single) (rewrites thy);
+    val thm1 = Code.preprocess_conv ct;
     val ct' = Thm.rhs_of thm1;
     val consts = consts_of thy (Thm.term_of ct');
-    val funcgr' = ensure_consts rewrites thy consts funcgr;
+    val funcgr' = ensure_consts thy consts funcgr;
     val algebra = Code.coregular_algebra thy;
     val (_, thm2) = Thm.varifyT' [] thm1;
     val thm3 = Thm.reflexive (Thm.rhs_of thm2);
@@ -344,10 +326,10 @@
     val cs = fold_aterms (fn Const c => cons c | _ => I) (Thm.term_of ct'') [];
     val drop = drop_classes thy tfrees;
     val instdefs = instances_of_consts thy algebra funcgr' cs;
-    val funcgr'' = ensure_consts rewrites thy instdefs funcgr';
+    val funcgr'' = ensure_consts thy instdefs funcgr';
   in (f funcgr'' drop ct'' thm5, funcgr'') end;
 
-fun ensure_consts_eval rewrites thy conv =
+fun ensure_consts_eval thy conv =
   let
     fun conv' funcgr drop_classes ct thm1 =
       let
@@ -359,49 +341,38 @@
           error ("eval_conv - could not construct proof:\n"
           ^ (cat_lines o map string_of_thm) [thm1, thm2, thm3])
       end;
-  in ensure_consts_term rewrites thy conv' end;
+  in ensure_consts_term_proto thy conv' end;
+
+fun ensure_consts_term thy f =
+  let
+    fun f' funcgr drop_classes ct thm1 = f funcgr ct;
+  in ensure_consts_term_proto thy f' end;
 
 end; (*local*)
 
-end; (*struct*)
-
-functor CodeFuncgrRetrieval (val rewrites: theory -> thm list) : CODE_FUNCGR_RETRIEVAL =
-struct
-
-(** code data **)
-
-type T = CodeFuncgr.T;
-
 structure Funcgr = CodeDataFun
 (struct
   type T = T;
-  val empty = CodeFuncgr.Constgraph.empty;
-  fun merge _ _ = CodeFuncgr.Constgraph.empty;
-  fun purge _ NONE _ = CodeFuncgr.Constgraph.empty
+  val empty = Constgraph.empty;
+  fun merge _ _ = Constgraph.empty;
+  fun purge _ NONE _ = Constgraph.empty
     | purge _ (SOME cs) funcgr =
-        CodeFuncgr.Constgraph.del_nodes ((CodeFuncgr.Constgraph.all_preds funcgr 
-          o filter (can (CodeFuncgr.Constgraph.get_node funcgr))) cs) funcgr;
+        Constgraph.del_nodes ((Constgraph.all_preds funcgr 
+          o filter (can (Constgraph.get_node funcgr))) cs) funcgr;
 end);
 
 fun make thy =
-  Funcgr.change thy o CodeFuncgr.ensure_consts rewrites thy;
+  Funcgr.change thy o ensure_consts thy;
 
 fun make_consts thy =
-  Funcgr.change_yield thy o CodeFuncgr.check_consts rewrites thy;
-
-fun make_term thy f =
-  Funcgr.change_yield thy o CodeFuncgr.ensure_consts_term rewrites thy f;
+  Funcgr.change_yield thy o check_consts thy;
 
 fun eval_conv thy f =
-  fst o Funcgr.change_yield thy o CodeFuncgr.ensure_consts_eval rewrites thy f;
+  fst o Funcgr.change_yield thy o ensure_consts_eval thy f;
+
+fun eval_term thy f =
+  fst o Funcgr.change_yield thy o ensure_consts_term thy f;
 
 fun intervene thy funcgr = Funcgr.change thy (K funcgr);
 
-end; (*functor*)
-
-structure CodeFuncgr : CODE_FUNCGR =
-struct
-
-open CodeFuncgr;
-
 end; (*struct*)

--- a/src/Tools/code/code_package.ML	Wed Aug 15 08:57:41 2007 +0200
+++ b/src/Tools/code/code_package.ML	Wed Aug 15 08:57:42 2007 +0200
@@ -9,14 +9,15 @@
 sig
   (* interfaces *)
   val eval_conv: theory
-    -> (CodeThingol.code -> CodeThingol.iterm -> cterm -> thm) -> cterm -> thm;
+    -> (CodeThingol.code -> CodeThingol.iterm * CodeThingol.itype -> string list -> cterm -> thm)
+    -> cterm -> thm;
+  val eval_term: theory
+    -> (CodeThingol.code -> CodeThingol.iterm * CodeThingol.itype -> string list -> cterm -> 'a)
+    -> cterm -> 'a;
+  val satisfies_ref: bool option ref;
+  val satisfies: theory -> cterm -> string list -> bool;
   val codegen_command: theory -> string -> unit;
 
-  (* primitive interfaces *)
-  val eval_term: theory -> (string (*reference name!*) * 'a option ref) * term -> 'a;
-  val satisfies_ref: bool option ref;
-  val satisfies: theory -> term -> string list -> bool;
-
   (* axiomatic interfaces *)
   type appgen;
   val add_appconst: string * appgen -> theory -> theory;
@@ -63,12 +64,10 @@
     (merge_appgens (appgens1, appgens2), merge_abstypes (abstypes1, abstypes2));
 );
 
-structure Funcgr = CodeFuncgrRetrieval (fun rewrites thy = []);
-
-fun code_depgr thy [] = Funcgr.make thy []
+fun code_depgr thy [] = CodeFuncgr.make thy []
   | code_depgr thy consts =
       let
-        val gr = Funcgr.make thy consts;
+        val gr = CodeFuncgr.make thy consts;
         val select = CodeFuncgr.Constgraph.all_succs gr consts;
       in
         CodeFuncgr.Constgraph.subgraph
@@ -116,7 +115,10 @@
  of SOME ty => SOME ((map_atyps (fn TFree (n, _) => nth tys (the (Int.fromString n)))) ty)
   | NONE => NONE;
 
-fun ensure_def thy = CodeThingol.ensure_def (CodeName.labelled_name thy);
+val value_name = "Isabelle_Eval.EVAL.EVAL";
+
+fun ensure_def thy = CodeThingol.ensure_def
+  (fn s => if s = value_name then "<term>" else CodeName.labelled_name thy s);
 
 fun ensure_def_class thy (algbr as ((_, algebra), _)) funcgr class =
   let
@@ -442,7 +444,7 @@
         orelse is_some (Code.get_datatype_of_constr thy c2)
       then error ("Not a function: " ^ CodeUnit.string_of_const thy c2)
       else ();
-    val funcgr = Funcgr.make thy [c1, c2];
+    val funcgr = CodeFuncgr.make thy [c1, c2];
     val ty1 = (f o CodeFuncgr.typ funcgr) c1;
     val ty2 = CodeFuncgr.typ funcgr c2;
     val _ = if Sign.typ_equiv thy (ty1, ty2) then () else
@@ -513,75 +515,23 @@
 fun generate thy funcgr gen it =
   let
     (*FIXME*)
-    val _ = Funcgr.intervene thy funcgr;
+    val _ = CodeFuncgr.intervene thy funcgr;
     val cs = map_filter (Consttab.lookup ((snd o snd o Translation.get) thy))
       (CodeFuncgr.all funcgr);
-    val funcgr' = Funcgr.make thy cs;
+    val CodeFuncgr' = CodeFuncgr.make thy cs;
     val naming = NameSpace.qualified_names NameSpace.default_naming;
     val consttab = Consts.empty
       |> fold (fn c => Consts.declare naming
-           ((CodeName.const thy c, CodeFuncgr.typ funcgr' c), true))
-           (CodeFuncgr.all funcgr');
+           ((CodeName.const thy c, CodeFuncgr.typ CodeFuncgr' c), true))
+           (CodeFuncgr.all CodeFuncgr');
     val algbr = (Code.operational_algebra thy, consttab);
   in   
     Program.change_yield thy
-      (CodeThingol.start_transact (gen thy algbr funcgr' it))
+      (CodeThingol.start_transact (gen thy algbr CodeFuncgr' it))
+    |> fst
   end;
 
-    (*val val_name = "Isabelle_Eval.EVAL.EVAL";
-    val val_name' = "Isabelle_Eval.EVAL";
-    val val_name'_args = space_implode " " (val_name' :: map (enclose "(" ")") args);
-    val seri = get_serializer thy "SML" false (SOME "Isabelle_Eval") NONE [] labelled_name;
-    fun eval code = (
-      reff := NONE;
-      seri (SOME [val_name]) code;
-      use_text "generated code for evaluation" Output.ml_output (!eval_verbose)
-        ("val _ = (" ^ ref_name ^ " := SOME (" ^ val_name'_args ^ "))");
-      case !reff
-       of NONE => error ("Could not retrieve value of ML reference " ^ quote ref_name
-            ^ " (reference probably has been shadowed)")
-        | SOME value => value
-      );
-
-    fun defgen_fun trns =
-      let
-        val const' = perhaps (Consttab.lookup ((snd o snd o Translation.get) thy)) const;
-        val raw_thms = CodeFuncgr.funcs funcgr const';
-        val ty = (Logic.unvarifyT o CodeFuncgr.typ funcgr) const';
-        val thms = if (null o Term.typ_tfrees) ty orelse (null o fst o strip_type) ty
-          then raw_thms
-          else map (CodeUnit.expand_eta 1) raw_thms;
-        val timeap = if !timing then Output.timeap_msg ("time for " ^ c')
-          else I;
-        val msg = cat_lines ("generating code for theorems " :: map string_of_thm thms);
-        val vs = (map dest_TFree o Consts.typargs consts) (c', ty);
-        val dest_eqthm =
-          apfst (snd o strip_comb) o Logic.dest_equals o Logic.unvarify o prop_of;
-        fun exprgen_eq (args, rhs) trns =
-          trns
-          |> fold_map (exprgen_term thy algbr funcgr) args
-          ||>> exprgen_term thy algbr funcgr rhs;
-      in
-        trns
-        |> CodeThingol.message msg (fn trns => trns
-        |> timeap (fold_map (exprgen_eq o dest_eqthm) thms)
-        ||>> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
-        ||>> exprgen_typ thy algbr funcgr ty
-        |-> (fn ((eqs, vs), ty) => succeed (CodeThingol.Fun (eqs, (vs, ty)))))
-      end;
-    val defgen = if (is_some o Code.get_datatype_of_constr thy) const
-      then defgen_datatypecons
-      else if is_some opt_tyco
-        orelse (not o is_some o AxClass.class_of_param thy) c
-      then defgen_fun
-      else defgen_classop
-  in
-    trns
-    |> ensure_def thy defgen ("generating constant " ^ CodeUnit.string_of_const thy const) c'
-
-*)
-
-(*fun eval_conv thy conv =
+fun raw_eval f thy g =
   let
     val value_name = "Isabelle_Eval.EVAL.EVAL";
     fun ensure_eval thy algbr funcgr t = 
@@ -590,58 +540,46 @@
           exprgen_term' thy algbr funcgr t
           ##>> exprgen_typ thy algbr funcgr (fastype_of t)
           #>> (fn (t, ty) => CodeThingol.Fun ([([], t)], ([], ty)));
+        fun result (dep, code) =
+          let
+            val CodeThingol.Fun ([([], t)], ([], ty)) = Graph.get_node code value_name;
+            val deps = Graph.imm_succs code value_name;
+            val code' = Graph.del_nodes [value_name] code;
+            val code'' = CodeThingol.project_code false [] (SOME deps) code';
+          in ((code'', (t, ty), deps), (dep, code')) end;
       in
         ensure_def thy defgen_eval "evaluation" value_name
-        #> pair value_name
+        #> result
       end;
-    fun conv' funcgr ct =
-      let
-        val (_, code) = generate thy funcgr ensure_eval (Thm.term_of ct);
-        val consts = CodeThingol.fold_constnames (insert (op =)) t [];
-        val code = Program.get thy
-          |> CodeThingol.project_code true [] (SOME consts)
-      in conv code t ct end;
-  in Funcgr.eval_conv thy conv' end;*)
-
-fun eval_conv thy conv =
-  let
-    fun conv' funcgr ct =
+    fun h funcgr ct =
       let
-        val (t, _) = generate thy funcgr exprgen_term' (Thm.term_of ct);
-        val consts = CodeThingol.fold_constnames (insert (op =)) t [];
-        val code = Program.get thy
-          |> CodeThingol.project_code true [] (SOME consts)
-      in conv code t ct end;
-  in Funcgr.eval_conv thy conv' end;
+        val (code, (t, ty), deps) = generate thy funcgr ensure_eval (Thm.term_of ct);
+      in g code (t, ty) deps ct end;
+  in f thy h end;
 
-fun codegen_term thy t =
-  let
-    val ct = Thm.cterm_of thy t;
-    val (ct', funcgr) = Funcgr.make_term thy (K (K K)) ct;
-    val t' = Thm.term_of ct';
-  in generate thy funcgr exprgen_term' t' |> fst end;
-
-fun raw_eval_term thy (ref_spec, t) args =
-  let
-    val _ = (Term.map_types o Term.map_atyps) (fn _ =>
-      error ("Term " ^ Sign.string_of_term thy t ^ " contains polymorphic type"))
-      t;
-    val t' = codegen_term thy t;
-  in
-    CodeTarget.eval_term thy CodeName.labelled_name
-      (Program.get thy) (ref_spec, t') args
-  end;
+fun eval_conv thy = raw_eval CodeFuncgr.eval_conv thy;
+fun eval_term thy = raw_eval CodeFuncgr.eval_term thy;
 
 val satisfies_ref : bool option ref = ref NONE;
 
-fun eval_term thy t = raw_eval_term thy t [];
-fun satisfies thy t witnesses = raw_eval_term thy
-  (("CodePackage.satisfies_ref", satisfies_ref), t) witnesses;
+fun satisfies thy ct witnesses =
+  let
+    fun evl code (t, ty) deps ct =
+      let
+        val t0 = Thm.term_of ct
+        val _ = (Term.map_types o Term.map_atyps) (fn _ =>
+          error ("Term " ^ Sign.string_of_term thy t0 ^ " contains polymorphic type"))
+          t0;
+      in
+        CodeTarget.eval_term thy ("CodePackage.satisfies_ref", satisfies_ref)
+          code (t, ty) witnesses
+      end;
+  in eval_term thy evl ct end;
 
 fun filter_generatable thy consts =
   let
-    val (consts', funcgr) = Funcgr.make_consts thy consts;
-    val (consts'', _) = generate thy funcgr (fold_map ooo perhaps_def_const) consts';
+    val (consts', funcgr) = CodeFuncgr.make_consts thy consts;
+    val consts'' = generate thy funcgr (fold_map ooo perhaps_def_const) consts';
     val consts''' = map_filter (fn (const, SOME _) => SOME const | (_, NONE) => NONE)
       (consts' ~~ consts'');
   in consts''' end;
@@ -658,9 +596,9 @@
   let
     val (perm1, cs) = CodeUnit.read_const_exprs thy
       (filter_generatable thy) raw_cs;
-    val (perm2, cs') = case generate thy (Funcgr.make thy cs) (fold_map ooo ensure_def_const') cs
-     of ([], _) => (true, NONE)
-      | (cs, _) => (false, SOME cs);
+    val (perm2, cs') = case generate thy (CodeFuncgr.make thy cs) (fold_map ooo ensure_def_const') cs
+     of [] => (true, NONE)
+      | cs => (false, SOME cs);
     val code = Program.get thy;
     val seris' = map (fn (((target, module), file), args) =>
       CodeTarget.get_serializer thy target (perm1 orelse perm2) module file args
@@ -670,10 +608,10 @@
   end;
 
 fun code_thms_cmd thy =
-  code_thms thy o snd o CodeUnit.read_const_exprs thy (fst o Funcgr.make_consts thy);
+  code_thms thy o snd o CodeUnit.read_const_exprs thy (fst o CodeFuncgr.make_consts thy);
 
 fun code_deps_cmd thy =
-  code_deps thy o snd o CodeUnit.read_const_exprs thy (fst o Funcgr.make_consts thy);
+  code_deps thy o snd o CodeUnit.read_const_exprs thy (fst o CodeFuncgr.make_consts thy);
 
 val (inK, module_nameK, fileK) = ("in", "module_name", "file");
 

--- a/src/Tools/code/code_thingol.ML	Wed Aug 15 08:57:41 2007 +0200
+++ b/src/Tools/code/code_thingol.ML	Wed Aug 15 08:57:42 2007 +0200
@@ -76,7 +76,7 @@
     -> code -> code;
   val empty_funs: code -> string list;
   val is_cons: code -> string -> bool;
-  val add_eval_def: string (*bind name*) * iterm -> code -> code;
+  val add_eval_def: string (*bind name*) * (iterm * itype) -> code -> code;
 
   val ensure_def: (string -> string) -> (transact -> def * transact) -> string
     -> string -> transact -> transact;
@@ -247,7 +247,6 @@
       * (string * iterm) list);
 
 type code = def Graph.T;
-type transact = Graph.key option * code;
 
 
 (* abstract code *)
@@ -372,6 +371,8 @@
 
 (* transaction protocol *)
 
+type transact = Graph.key option * code;
+
 fun ensure_def labelled_name defgen msg name (dep, code) =
   let
     val msg' = (case dep
@@ -402,9 +403,9 @@
   |> f
   |-> (fn x => fn (_, code) => (x, code));
 
-fun add_eval_def (name, t) code =
+fun add_eval_def (name, (t, ty)) code =
   code
-  |> Graph.new_node (name, Fun ([([], t)], ([("_", [])], ITyVar "_")))
+  |> Graph.new_node (name, Fun ([([], t)], ([], ty)))
   |> fold (curry Graph.add_edge name) (Graph.keys code);
 
 end; (*struct*)

--- a/src/Tools/nbe.ML	Wed Aug 15 08:57:41 2007 +0200
+++ b/src/Tools/nbe.ML	Wed Aug 15 08:57:42 2007 +0200
@@ -60,11 +60,6 @@
    Moreover, to handle functions that are still waiting for some
    arguments we have additionally a list of arguments collected to far
    and the number of arguments we're still waiting for.
-
-   (?) Finally, it might happen, that a function does not get all the
-   arguments it needs.  In this case the function must provide means to
-   present itself as a string. As this might be a heavy-wight
-   operation, we delay it. (?) 
 *)
 
 datatype Univ = 
@@ -233,7 +228,7 @@
         val result = ml_list (map (fn (c, n) => nbe_abss n (nbe_fun c)) num_args);
       in (cs, ml_Let (bind_funs @ [bind_locals]) result) end;
 
-fun assemble_eval thy is_fun t =
+fun assemble_eval thy is_fun (t, deps) =
   let
     val funs = CodeThingol.fold_constnames (insert (op =)) t [];
     val frees = CodeThingol.fold_unbound_varnames (insert (op =)) t [];
@@ -314,7 +309,7 @@
 
 (* evaluation with type reconstruction *)
 
-fun eval thy code t t' =
+fun eval thy code t t' deps =
   let
     fun subst_Frees [] = I
       | subst_Frees inst =
@@ -330,7 +325,7 @@
     fun constrain t =
       singleton (ProofContext.infer_types_pats (ProofContext.init thy)) (TypeInfer.constrain t ty);
   in
-    t'
+    (t', deps)
     |> eval_term thy (Symtab.defined (ensure_funs thy code))
     |> term_of_univ thy
     |> tracing (fn t => "Normalized:\n" ^ setmp show_types true Display.raw_string_of_term t)
@@ -345,22 +340,22 @@
 
 (* evaluation oracle *)
 
-exception Normalization of CodeThingol.code * term * CodeThingol.iterm;
+exception Normalization of CodeThingol.code * term * CodeThingol.iterm * string list;
 
-fun normalization_oracle (thy, Normalization (code, t, t')) =
-  Logic.mk_equals (t, eval thy code t t');
+fun normalization_oracle (thy, Normalization (code, t, t', deps)) =
+  Logic.mk_equals (t, eval thy code t t' deps);
 
-fun normalization_invoke thy code t t' =
-  Thm.invoke_oracle_i thy "HOL.normalization" (thy, Normalization (code, t, t'));
-  (*FIXME get rid of hardwired theory name "HOL"*)
+fun normalization_invoke thy code t t' deps =
+  Thm.invoke_oracle_i thy "Code_Setup.normalization" (thy, Normalization (code, t, t', deps));
+  (*FIXME get rid of hardwired theory name*)
 
 fun normalization_conv ct =
   let
     val thy = Thm.theory_of_cterm ct;
-    fun conv code t' ct =
+    fun conv code (t', ty') deps ct =
       let
         val t = Thm.term_of ct;
-      in normalization_invoke thy code t t' end;
+      in normalization_invoke thy code t t' deps end;
   in CodePackage.eval_conv thy conv ct end;
 
 (* evaluation command *)