--- a/src/Tools/Code/code_preproc.ML Wed Sep 15 15:11:39 2010 +0200
+++ b/src/Tools/Code/code_preproc.ML Wed Sep 15 15:11:39 2010 +0200
@@ -23,7 +23,7 @@
val sortargs: code_graph -> string -> sort list
val all: code_graph -> string list
val pretty: theory -> code_graph -> Pretty.T
- val obtain: theory -> string list -> term list -> code_algebra * code_graph
+ val obtain: bool -> theory -> string list -> term list -> code_algebra * code_graph
val dynamic_eval_conv: theory
-> (code_algebra -> code_graph -> (string * sort) list -> term -> conv) -> conv
val dynamic_eval_value: theory -> ((term -> term) -> 'a -> 'a)
@@ -422,8 +422,8 @@
(** retrieval and evaluation interfaces **)
-fun obtain thy consts ts = apsnd snd
- (Wellsorted.change_yield thy (extend_arities_eqngr thy consts ts));
+fun obtain ignore_cache thy consts ts = apsnd snd
+ (Wellsorted.change_yield (if ignore_cache then NONE else SOME thy) (extend_arities_eqngr thy consts ts));
fun dest_cterm ct = let val t = Thm.term_of ct in (Term.add_tfrees t [], t) end;
@@ -437,7 +437,7 @@
val (vs', t') = dest_cterm ct';
val consts = fold_aterms
(fn Const (c, _) => insert (op =) c | _ => I) t' [];
- val (algebra', eqngr') = obtain thy consts [t'];
+ val (algebra', eqngr') = obtain false thy consts [t'];
in conclude_evaluation (evaluator algebra' eqngr' vs' t' ct') thm end;
fun dynamic_eval_conv thy =
@@ -457,15 +457,12 @@
fun static_eval_conv thy consts conv =
let
- val (algebra, eqngr) = obtain thy consts [];
- fun conv' ct =
- let
- val (vs, t) = dest_cterm ct;
- in
- Conv.tap_thy (fn thy => (preprocess_conv thy)
- then_conv (conv algebra eqngr vs t) then_conv (postprocess_conv thy)) ct
- end;
- in conv' end;
+ val (algebra, eqngr) = obtain true thy consts [];
+ in
+ Conv.tap_thy (fn thy => (preprocess_conv thy)
+ then_conv (fn ct => uncurry (conv algebra eqngr) (dest_cterm ct) ct)
+ then_conv (postprocess_conv thy))
+ end;
(** setup **)