# HG changeset patch
# User haftmann
# Date 1292920173 -3600
# Node ID 0e2a3f22f0185de37ef6a7d79230dde462707c47
# Parent  692c3fbde3c9bced8af31629fcd6ccae55ec0d9e
evaluator separating static and dynamic operations

diff -r 692c3fbde3c9 -r 0e2a3f22f018 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Tue Dec 21 09:19:37 2010 +0100
+++ b/src/Tools/Code/code_runtime.ML	Tue Dec 21 09:29:33 2010 +0100
@@ -86,8 +86,7 @@
     val ctxt = ProofContext.init_global thy;
   in ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t) end;
 
-fun obtain_evaluator thy some_target naming program deps =
-  Code_Target.evaluator thy (the_default target some_target) naming program deps;
+fun obtain_evaluator thy some_target = Code_Target.evaluator thy (the_default target some_target);
 
 fun evaluation cookie thy evaluator vs_t args =
   let
@@ -146,15 +145,16 @@
 
 val reject_vars = fn thy => tap (reject_vars thy o Thm.term_of);
 
-fun check_holds some_target naming thy program vs_t deps ct =
+local
+
+fun check_holds thy evaluator vs_t deps ct =
   let
     val t = Thm.term_of ct;
     val _ = if fastype_of t <> propT
       then error ("Not a proposition: " ^ Syntax.string_of_term_global thy t)
       else ();
     val iff = Thm.cterm_of thy (Term.Const ("==", propT --> propT --> propT));
-    val result = case partiality_as_none
-      (evaluation truth_cookie thy (obtain_evaluator thy some_target naming program deps) vs_t [])
+    val result = case partiality_as_none (evaluation truth_cookie thy evaluator vs_t [])
      of SOME Holds => true
       | _ => false;
   in
@@ -163,19 +163,24 @@
 
 val (_, raw_check_holds_oracle) = Context.>>> (Context.map_theory_result
   (Thm.add_oracle (Binding.name "holds_by_evaluation",
-  fn (some_target, naming, thy, program, vs_t, deps, ct) => check_holds some_target naming thy program vs_t deps ct)));
+  fn (thy, evaluator, vs_t, deps, ct) => check_holds thy evaluator vs_t deps ct)));
 
-fun check_holds_oracle some_target naming thy program ((_, vs_ty), t) deps ct =
-  raw_check_holds_oracle (some_target, naming, thy, program, (vs_ty, t), deps, ct);
+fun check_holds_oracle thy evaluator ((_, vs_ty), t) deps ct =
+  raw_check_holds_oracle (thy, evaluator, (vs_ty, t), deps, ct);
+
+in
 
 fun dynamic_holds_conv thy = Code_Thingol.dynamic_conv thy
-    (fn naming => check_holds_oracle NONE naming thy)
-  o reject_vars thy;
+  (fn naming => fn program => fn vs_t => fn deps =>
+    check_holds_oracle thy (obtain_evaluator thy NONE naming program deps) vs_t deps)
+      o reject_vars thy;
 
-fun static_holds_conv thy consts =
-  Code_Thingol.static_conv thy consts
-    (fn naming => fn program => fn consts' => check_holds_oracle NONE naming thy program)
-    o reject_vars thy;
+fun static_holds_conv thy consts = Code_Thingol.static_conv thy consts
+  (fn naming => fn program => fn consts' =>
+    check_holds_oracle thy (obtain_evaluator thy NONE naming program consts'))
+      o reject_vars thy;
+
+end; (*local*)
 
 
 (** instrumentalization **)