src/Tools/code/code_package.ML

 Code generator interfaces and Isar setup.
 *)
 
 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;
 
 structure CodePackage : CODE_PACKAGE =
 struct

     val code = Program.get thy;
     val seris' = map (fn (((target, module), file), args) =>
       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 =
-  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;
-
-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 evaluate eval_kind term_of thy eval = eval_kind thy (fn funcgr => fn ct =>
+  let
+    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 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
     val (consts', funcgr) = CodeFuncgr.make_consts thy consts;
     val (consts'', _) = generate thy funcgr (fold_map ooo perhaps_const) consts';