cleaned up evaluation interfaces

--- a/src/HOL/Library/Eval.thy	Tue Jan 29 10:19:58 2008 +0100
+++ b/src/HOL/Library/Eval.thy	Tue Jan 29 10:20:00 2008 +0100
@@ -362,12 +362,9 @@
 
 val eval_ref = ref (NONE : (unit -> term) option);
 
-fun eval_invoke thy code ((_, ty), t) deps _ =
-  CodeTarget.eval_invoke thy ("Eval.eval_ref", eval_ref) code (t, ty) [];
-
 fun eval_term thy =
   Eval_Aux.mk_term_of
-  #> CodePackage.eval_term thy (eval_invoke thy)
+  #> (fn t => CodePackage.eval_term ("Eval.eval_ref", eval_ref) thy t [])
   #> Code.postprocess_term thy;
 
 val evaluators = [

--- a/src/Tools/code/code_package.ML	Tue Jan 29 10:19:58 2008 +0100
+++ b/src/Tools/code/code_package.ML	Tue Jan 29 10:20:00 2008 +0100
@@ -7,16 +7,20 @@
 
 signature CODE_PACKAGE =
 sig
-  val eval_conv: theory
+  val evaluate_conv: theory
     -> (CodeThingol.code -> CodeThingol.typscheme * CodeThingol.iterm
        -> string list -> cterm -> thm)
     -> cterm -> thm;
-  val eval_term: theory
+  val evaluate_term: theory
     -> (CodeThingol.code -> CodeThingol.typscheme * CodeThingol.iterm
        -> string list -> term -> 'a)
     -> term -> 'a;
+  val eval_conv: string * (unit -> thm) option ref
+    -> theory -> cterm -> string list -> thm;
+  val eval_term: string * (unit -> 'a) option ref
+    -> theory -> term -> string list -> 'a;
+  val satisfies: theory -> term -> string list -> bool;
   val satisfies_ref: (unit -> bool) option ref;
-  val satisfies: theory -> term -> string list -> bool;
   val codegen_shell_command: string (*theory name*) -> string (*cg expr*) -> unit;
 end;
 
@@ -95,36 +99,31 @@
       CodeTarget.get_serializer thy target permissive module file args cs) seris;
   in (map (fn f => f code) seris' : unit list; ()) end;
 
-fun raw_eval evaluate term_of thy g =
+fun evaluate eval_kind term_of thy eval = eval_kind thy (fn funcgr => fn ct =>
   let
-    fun result (_, code) =
-      let
-        val CodeThingol.Fun ((vs, ty), [(([], t), _)]) =
-          Graph.get_node code CodeName.value_name;
-        val deps = Graph.imm_succs code CodeName.value_name;
-        val code' = Graph.del_nodes [CodeName.value_name] code;
-        val code'' = CodeThingol.project_code false [] (SOME deps) code';
-      in ((code'', ((vs, ty), t), deps), code') end;
-    fun h funcgr ct =
-      let
-        val ((code, vs_ty_t, deps), _) = term_of ct
-          |> generate thy funcgr CodeThingol.ensure_value
-          |> result
-          ||> `(fn code' => Program.change thy (K code'));
-      in g code vs_ty_t deps ct end;
-  in evaluate thy h end;
+    val ((code, (vs_ty_t, deps)), _) = generate thy funcgr
+      CodeThingol.ensure_value (term_of ct)
+  in eval code vs_ty_t deps ct end);
+
+fun evaluate_conv thy = evaluate CodeFuncgr.eval_conv Thm.term_of thy;
+fun evaluate_term thy = evaluate CodeFuncgr.eval_term I thy;
+
+fun eval_ml reff args thy code ((vs, ty), t) deps _ =
+  CodeTarget.eval thy reff code (t, ty) args;
 
-fun eval_conv thy = raw_eval CodeFuncgr.eval_conv Thm.term_of thy;
-fun eval_term thy = raw_eval CodeFuncgr.eval_term I thy;
+fun eval evaluate term_of reff thy ct args =
+  let
+    val _ = if null (term_frees (term_of ct)) then () else error ("Term "
+      ^ quote (Sign.string_of_term thy (term_of ct))
+      ^ " to be evaluated containts free variables");
+  in evaluate thy (eval_ml reff args thy) ct end;
+
+fun eval_conv reff = eval evaluate_conv Thm.term_of reff;
+fun eval_term reff = eval evaluate_term I reff;
 
 val satisfies_ref : (unit -> bool) option ref = ref NONE;
 
-fun satisfies thy t witnesses =
-  let
-    fun evl code ((vs, ty), t) deps _ =
-      CodeTarget.eval_invoke thy ("CodePackage.satisfies_ref", satisfies_ref)
-        code (t, ty) witnesses;
-  in eval_term thy evl t end;
+val satisfies = eval_term ("CodePackage.satisfies_ref", satisfies_ref);
 
 fun filter_generatable thy consts =
   let

--- a/src/Tools/code/code_thingol.ML	Tue Jan 29 10:19:58 2008 +0100
+++ b/src/Tools/code/code_thingol.ML	Tue Jan 29 10:20:00 2008 +0100
@@ -85,11 +85,12 @@
   val ensure_const: theory -> ((sort -> sort) * Sorts.algebra) * Consts.T
     -> CodeFuncgr.T -> string -> transact -> string * transact;
   val ensure_value: theory -> ((sort -> sort) * Sorts.algebra) * Consts.T
-    -> CodeFuncgr.T -> term -> transact -> string * transact;
-  val add_value_stmt: iterm * itype -> code -> code;
+    -> CodeFuncgr.T -> term
+      -> transact -> (code * ((typscheme * iterm) * string list)) * transact;
   val transact: theory -> CodeFuncgr.T
     -> (theory -> ((sort -> sort) * Sorts.algebra) * Consts.T -> CodeFuncgr.T
       -> transact -> 'a * transact) -> code -> 'a * code;
+  val add_value_stmt: iterm * itype -> code -> code;
 end;
 
 structure CodeThingol: CODE_THINGOL =
@@ -642,41 +643,19 @@
       ##>> exprgen_typ thy algbr funcgr ty
       ##>> exprgen_term thy algbr funcgr t
       #>> (fn ((vs, ty), t) => Fun ((vs, ty), [(([], t), Drule.dummy_thm)]));
-  in
-    ensure_stmt stmt_value CodeName.value_name
-  end;
-
-fun eval evaluate term_of thy g code0 =
-  let
-    fun result (_, code) =
+    fun term_value (dep, code1) =
       let
         val Fun ((vs, ty), [(([], t), _)]) =
-          Graph.get_node code CodeName.value_name;
-        val deps = Graph.imm_succs code CodeName.value_name;
-        val code' = Graph.del_nodes [CodeName.value_name] code;
-        val code'' = project_code false [] (SOME deps) code';
-      in ((code'', ((vs, ty), t), deps), code') end;
-    fun h funcgr ct =
-      let
-        val ((code, vs_ty_t, deps), _) =
-          code0
-          |> transact thy funcgr (fn thy => fn algbr => fn funcgr =>
-               ensure_value thy algbr funcgr (term_of ct))
-          |> result
-          ||> `(fn code' => code');
-      in g code vs_ty_t deps ct end;
-  in evaluate thy h end;
-
-val _ : (theory -> (CodeFuncgr.T -> 'Z -> 'Y) -> 'X)
-                  -> ('Z -> term)
-                     -> theory
-                        -> (stmt Graph.T
-                            -> ((vname * sort) list * itype) * iterm
-                               -> Graph.key list -> 'Z -> 'Y)
-                           -> stmt Graph.T -> 'X = eval;
-
-fun eval_conv thy = eval CodeFuncgr.eval_conv Thm.term_of thy;
-fun eval_term thy = eval CodeFuncgr.eval_term I thy;
+          Graph.get_node code1 CodeName.value_name;
+        val deps = Graph.imm_succs code1 CodeName.value_name;
+        val code2 = Graph.del_nodes [CodeName.value_name] code1;
+        val code3 = project_code false [] (SOME deps) code2;
+      in ((code3, (((vs, ty), t), deps)), (dep, code2)) end;
+  in
+    ensure_stmt stmt_value CodeName.value_name
+    #> snd
+    #> term_value
+  end;
 
 end; (*struct*)
 

--- a/src/Tools/nbe.ML	Tue Jan 29 10:19:58 2008 +0100
+++ b/src/Tools/nbe.ML	Tue Jan 29 10:20:00 2008 +0100
@@ -405,13 +405,13 @@
       let
         val t = Thm.term_of ct;
       in norm_invoke thy code t vs_ty_t deps end;
-  in CodePackage.eval_conv thy conv ct end;
+  in CodePackage.evaluate_conv thy conv ct end;
 
 fun norm_term thy =
   let
     fun invoke code vs_ty_t deps t =
       eval thy code t vs_ty_t deps;
-  in CodePackage.eval_term thy invoke #> Code.postprocess_term thy end;
+  in CodePackage.evaluate_term thy invoke #> Code.postprocess_term thy end;
 
 (* evaluation command *)