--- a/src/Pure/Tools/codegen_package.ML Tue Jul 24 15:20:52 2007 +0200
+++ b/src/Pure/Tools/codegen_package.ML Tue Jul 24 15:20:53 2007 +0200
@@ -7,6 +7,7 @@
signature CODEGEN_PACKAGE =
sig
+ val compile_term: theory -> term -> CodegenThingol.code * CodegenThingol.iterm;
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;
@@ -532,6 +533,17 @@
val t' = Thm.term_of ct';
in generate thy funcgr exprgen_term' t' end;
+fun compile_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';
+ val t'' = generate thy funcgr exprgen_term' t';
+ val consts = CodegenThingol.fold_constnames (insert (op =)) t'' [];
+ val code = Code.get thy
+ |> CodegenThingol.project_code true [] (SOME consts)
+ in (code, t'') end;
+
fun raw_eval_term thy (ref_spec, t) args =
let
val _ = (Term.map_types o Term.map_atyps) (fn _ =>