# HG changeset patch
# User haftmann
# Date 1284652276 -7200
# Node ID fd1032c23cdfff714328e7686e05cb50bfd37bfc
# Parent  d7caf48c46769d67b9e1bb7fd2511ca7a2680d0e# Parent  8bc560df99eacf5eb94667c8fb324f9c51b886bd
merged

diff -r d7caf48c4676 -r fd1032c23cdf src/HOL/Code_Evaluation.thy
--- a/src/HOL/Code_Evaluation.thy	Thu Sep 16 17:42:49 2010 +0200
+++ b/src/HOL/Code_Evaluation.thy	Thu Sep 16 17:51:16 2010 +0200
@@ -315,8 +315,8 @@
 
 fun tracing s x = (Output.tracing s; x);
 
-fun eval_term thy t = Code_Runtime.value NONE (Evaluation.get, put_term, "Code_Evaluation.put_term")
-  I thy (HOLogic.mk_term_of (fastype_of t) t) [];
+fun eval_term thy t = Code_Runtime.dynamic_value_strict (Evaluation.get, put_term, "Code_Evaluation.put_term")
+  thy NONE I (HOLogic.mk_term_of (fastype_of t) t) [];
 
 end
 *}
diff -r d7caf48c4676 -r fd1032c23cdf src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Sep 16 17:42:49 2010 +0200
+++ b/src/HOL/HOL.thy	Thu Sep 16 17:51:16 2010 +0200
@@ -1958,42 +1958,17 @@
 
 subsubsection {* Evaluation and normalization by evaluation *}
 
-text {* Avoid some named infixes in evaluation environment *}
-
-code_reserved Eval oo ooo oooo upto downto orf andf
-
 setup {*
   Value.add_evaluator ("SML", Codegen.eval_term o ProofContext.theory_of)
 *}
 
 ML {*
-structure Eval_Method = Proof_Data(
-  type T = unit -> bool
-  fun init thy () = error "Eval_Method"
-)
-*}
-
-oracle eval_oracle = {* fn ct =>
-  let
-    val thy = Thm.theory_of_cterm ct;
-    val t = Thm.term_of ct;
-    val dummy = @{cprop True};
-  in case try HOLogic.dest_Trueprop t
-   of SOME t' => if Code_Runtime.value NONE
-         (Eval_Method.get, Eval_Method.put, "Eval_Method.put") (K I) thy t' [] 
-       then Thm.capply (Thm.capply @{cterm "op \<equiv> \<Colon> prop \<Rightarrow> prop \<Rightarrow> prop"} ct) dummy
-       else dummy
-    | NONE => dummy
-  end
-*}
-
-ML {*
 fun gen_eval_method conv ctxt = SIMPLE_METHOD'
   (CONVERSION (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt)
     THEN' rtac TrueI)
 *}
 
-method_setup eval = {* Scan.succeed (gen_eval_method eval_oracle) *}
+method_setup eval = {* Scan.succeed (gen_eval_method Code_Runtime.dynamic_holds_conv) *}
   "solve goal by evaluation"
 
 method_setup evaluation = {* Scan.succeed (gen_eval_method Codegen.evaluation_conv) *}
diff -r d7caf48c4676 -r fd1032c23cdf src/HOL/Library/Eval_Witness.thy
--- a/src/HOL/Library/Eval_Witness.thy	Thu Sep 16 17:42:49 2010 +0200
+++ b/src/HOL/Library/Eval_Witness.thy	Thu Sep 16 17:51:16 2010 +0200
@@ -44,6 +44,13 @@
 instance bool :: ml_equiv ..
 instance list :: (ml_equiv) ml_equiv ..
 
+ML {*
+structure Eval_Method = Proof_Data (
+  type T = unit -> bool
+  fun init _ () = error "Eval_Method"
+)
+*}
+
 oracle eval_witness_oracle = {* fn (cgoal, ws) =>
 let
   val thy = Thm.theory_of_cterm cgoal;
@@ -59,7 +66,7 @@
     | dest_exs _ _ = sys_error "dest_exs";
   val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal);
 in
-  if Code_Runtime.value NONE (Eval_Method.get, Eval_Method.put, "Eval_Method.put") (K I) thy t ws
+  if Code_Runtime.dynamic_value_strict (Eval_Method.get, Eval_Method.put, "Eval_Method.put") thy NONE (K I) t ws
   then Thm.cterm_of thy goal
   else @{cprop True} (*dummy*)
 end
diff -r d7caf48c4676 -r fd1032c23cdf src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Sep 16 17:42:49 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Sep 16 17:51:16 2010 +0200
@@ -3278,16 +3278,16 @@
             val [nrandom, size, depth] = arguments
           in
             rpair NONE (fst (DSequence.yieldn k
-              (Code_Runtime.value NONE (Dseq_Random_Result.get, put_dseq_random_result, "Predicate_Compile_Core.put_dseq_random_result")
-                (fn proc => fn g => fn nrandom => fn size => fn s => g nrandom size s |>> DSequence.map proc)
-                  thy t' [] nrandom size
+              (Code_Runtime.dynamic_value_strict (Dseq_Random_Result.get, put_dseq_random_result, "Predicate_Compile_Core.put_dseq_random_result")
+                thy NONE (fn proc => fn g => fn nrandom => fn size => fn s => g nrandom size s |>> DSequence.map proc)
+                  t' [] nrandom size
                 |> Random_Engine.run)
               depth true))
           end
       | DSeq =>
           rpair NONE (fst (DSequence.yieldn k
-            (Code_Runtime.value NONE (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Core.put_dseq_result")
-              DSequence.map thy t' []) (the_single arguments) true))
+            (Code_Runtime.dynamic_value_strict (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Core.put_dseq_result")
+              thy NONE DSequence.map t' []) (the_single arguments) true))
       | New_Pos_Random_DSeq =>
           let
             val [nrandom, size, depth] = arguments
@@ -3296,23 +3296,25 @@
             if stats then
               apsnd (SOME o accumulate) (split_list
               (fst (Lazy_Sequence.yieldn k
-                (Code_Runtime.value NONE
+                (Code_Runtime.dynamic_value_strict
                   (Lseq_Random_Stats_Result.get, put_lseq_random_stats_result, "Predicate_Compile_Core.put_lseq_random_stats_result")
+                  thy NONE
                   (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
                     |> Lazy_Sequence.mapa (apfst proc))
-                    thy t' [] nrandom size seed depth))))
+                    t' [] nrandom size seed depth))))
             else rpair NONE
               (fst (Lazy_Sequence.yieldn k
-                (Code_Runtime.value NONE
+                (Code_Runtime.dynamic_value_strict
                   (Lseq_Random_Result.get, put_lseq_random_result, "Predicate_Compile_Core.put_lseq_random_result")
+                  thy NONE 
                   (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
                     |> Lazy_Sequence.mapa proc)
-                    thy t' [] nrandom size seed depth)))
+                    t' [] nrandom size seed depth)))
           end
       | _ =>
           rpair NONE (fst (Predicate.yieldn k
-            (Code_Runtime.value NONE (Pred_Result.get, put_pred_result, "Predicate_Compile_Core.put_pred_result")
-              Predicate.map thy t' [])))
+            (Code_Runtime.dynamic_value_strict (Pred_Result.get, put_pred_result, "Predicate_Compile_Core.put_pred_result")
+              thy NONE Predicate.map t' [])))
   in ((T, ts), statistics) end;
 
 fun values ctxt param_user_modes ((raw_expected, stats), comp_options) k t_compr =
diff -r d7caf48c4676 -r fd1032c23cdf src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Thu Sep 16 17:42:49 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Thu Sep 16 17:51:16 2010 +0200
@@ -272,9 +272,10 @@
         Pos_Random_DSeq =>
           let
             val compiled_term =
-              Code_Runtime.value (SOME target) (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Quickcheck.put_dseq_result")
+              Code_Runtime.dynamic_value_strict (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Quickcheck.put_dseq_result")
+                thy4 (SOME target)
                 (fn proc => fn g => fn n => fn size => fn s => g n size s |>> (DSequence.map o map) proc)
-                thy4 qc_term []
+                qc_term []
           in
             (fn size => fn nrandom => fn depth =>
               Option.map fst (DSequence.yield
@@ -283,11 +284,12 @@
       | New_Pos_Random_DSeq =>
           let
             val compiled_term =
-              Code_Runtime.value (SOME target)
+              Code_Runtime.dynamic_value_strict
                 (Lseq_Result.get, put_lseq_result, "Predicate_Compile_Quickcheck.put_lseq_result")
+                thy4 (SOME target)
                 (fn proc => fn g => fn nrandom => fn size => fn s => fn depth =>
                   g nrandom size s depth |> (Lazy_Sequence.mapa o map) proc)
-                  thy4 qc_term []
+                  qc_term []
           in
             fn size => fn nrandom => fn depth => Option.map fst (Lazy_Sequence.yield 
                (
@@ -297,11 +299,11 @@
           end
       | Depth_Limited_Random =>
           let
-            val compiled_term = Code_Runtime.value (SOME target)
+            val compiled_term = Code_Runtime.dynamic_value_strict
               (Pred_Result.get, put_pred_result, "Predicate_Compile_Quickcheck.put_pred_result")
-                (fn proc => fn g => fn depth => fn nrandom => fn size => fn seed =>
+                thy4 (SOME target) (fn proc => fn g => fn depth => fn nrandom => fn size => fn seed =>
                   g depth nrandom size seed |> (Predicate.map o map) proc)
-                thy4 qc_term []
+                qc_term []
           in
             fn size => fn nrandom => fn depth => Option.map fst (Predicate.yield 
               (compiled_term depth nrandom size (Random_Engine.run (fn s => (s, s)))))
diff -r d7caf48c4676 -r fd1032c23cdf src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Thu Sep 16 17:42:49 2010 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML	Thu Sep 16 17:51:16 2010 +0200
@@ -392,16 +392,16 @@
   in if Quickcheck.report ctxt then
     let
       val t' = mk_reporting_generator_expr thy t Ts;
-      val compile = Code_Runtime.value (SOME target)
+      val compile = Code_Runtime.dynamic_value_strict
         (Counterexample_Report.get, put_counterexample_report, "Quickcheck_Generators.put_counterexample_report")
-        (fn proc => fn g => fn s => g s #>> (apfst o Option.map o map) proc) thy t' [];
+        thy (SOME target) (fn proc => fn g => fn s => g s #>> (apfst o Option.map o map) proc) t' [];
     in compile #> Random_Engine.run end
   else
     let
       val t' = mk_generator_expr thy t Ts;
-      val compile = Code_Runtime.value (SOME target)
+      val compile = Code_Runtime.dynamic_value_strict
         (Counterexample.get, put_counterexample, "Quickcheck_Generators.put_counterexample")
-        (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' [];
+        thy (SOME target) (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) t' [];
       val dummy_report = ([], false)
     in compile #> Random_Engine.run #> rpair dummy_report end
   end;
diff -r d7caf48c4676 -r fd1032c23cdf src/Pure/General/exn.ML
--- a/src/Pure/General/exn.ML	Thu Sep 16 17:42:49 2010 +0200
+++ b/src/Pure/General/exn.ML	Thu Sep 16 17:51:16 2010 +0200
@@ -11,6 +11,7 @@
   val get_exn: 'a result -> exn option
   val capture: ('a -> 'b) -> 'a -> 'b result
   val release: 'a result -> 'a
+  val map_result: ('a -> 'a) -> 'a result -> 'a result
   exception Interrupt
   val interrupt: unit -> 'a
   val is_interrupt: exn -> bool
@@ -43,6 +44,9 @@
 fun release (Result y) = y
   | release (Exn e) = reraise e;
 
+fun map_result f (Result x) = Result (f x)
+  | map_result f e = e;
+
 
 (* interrupts *)
 
diff -r d7caf48c4676 -r fd1032c23cdf src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Thu Sep 16 17:42:49 2010 +0200
+++ b/src/Tools/Code/code_preproc.ML	Thu Sep 16 17:51:16 2010 +0200
@@ -29,7 +29,9 @@
   val dynamic_eval_value: theory -> ((term -> term) -> 'a -> 'a)
     -> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a
   val static_eval_conv: theory -> string list
-    -> (code_algebra -> code_graph -> (string * sort) list -> term -> conv) -> conv
+    -> (code_algebra -> code_graph -> theory -> (string * sort) list -> term -> conv) -> conv
+  val static_eval_value: theory -> ((term -> term) -> 'a -> 'a) -> string list
+    -> (code_algebra -> code_graph -> theory -> (string * sort) list -> term -> 'a) -> term -> 'a
 
   val setup: theory -> theory
 end
@@ -138,6 +140,8 @@
 
 fun preprocess_conv thy ct =
   let
+    val ctxt = ProofContext.init_global thy;
+    val _ = (Sign.no_frees ctxt o map_types (K dummyT) o Sign.no_vars ctxt) (Thm.term_of ct);
     val pre = (Simplifier.global_context thy o #pre o the_thmproc) thy;
   in
     ct
@@ -145,6 +149,8 @@
     |> trans_conv_rule (AxClass.unoverload_conv thy)
   end;
 
+fun preprocess_term thy = term_of_conv thy (preprocess_conv thy);
+
 fun postprocess_conv thy ct =
   let
     val post = (Simplifier.global_context thy o #post o the_thmproc) thy;
@@ -427,43 +433,56 @@
 
 fun dest_cterm ct = let val t = Thm.term_of ct in (Term.add_tfrees t [], t) end;
 
-fun dynamic_eval thy cterm_of conclude_evaluation evaluator proto_ct =
+fun dynamic_eval_conv thy conv ct =
   let
-    val ctxt = Syntax.init_pretty_global thy;
-    val ct = cterm_of proto_ct;
-    val _ = (Sign.no_frees ctxt o map_types (K dummyT) o Sign.no_vars ctxt) (Thm.term_of ct);
-    val thm = preprocess_conv thy ct;
-    val ct' = Thm.rhs_of thm;
+    val thm1 = preprocess_conv thy ct;
+    val ct' = Thm.rhs_of thm1;
     val (vs', t') = dest_cterm ct';
     val consts = fold_aterms
       (fn Const (c, _) => insert (op =) c | _ => I) t' [];
     val (algebra', eqngr') = obtain false thy consts [t'];
-  in conclude_evaluation (evaluator algebra' eqngr' vs' t' ct') thm end;
+    val thm2 = conv algebra' eqngr' vs' t' ct';
+    val thm3 = postprocess_conv thy (Thm.rhs_of thm2);
+  in
+    Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
+      error ("could not construct evaluation proof:\n"
+      ^ (cat_lines o map (Display.string_of_thm_global thy)) [thm1, thm2, thm3])
+  end;
 
-fun dynamic_eval_conv thy =
+fun dynamic_eval_value thy postproc evaluator t =
   let
-    fun conclude_evaluation thm2 thm1 =
-      let
-        val thm3 = postprocess_conv thy (Thm.rhs_of thm2);
-      in
-        Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
-          error ("could not construct evaluation proof:\n"
-          ^ (cat_lines o map (Display.string_of_thm_global thy)) [thm1, thm2, thm3])
-      end;
-  in dynamic_eval thy I conclude_evaluation end;
-
-fun dynamic_eval_value thy postproc evaluator = dynamic_eval thy (Thm.cterm_of thy)
-  (K o postproc (postprocess_term thy)) (K oooo evaluator);
+    val t' = preprocess_term thy t;
+    val vs' = Term.add_tfrees t' [];
+    val consts = fold_aterms
+      (fn Const (c, _) => insert (op =) c | _ => I) t' [];
+    val (algebra', eqngr') = obtain false thy consts [t'];
+    val result = evaluator algebra' eqngr' vs' t';
+  in
+    evaluator algebra' eqngr' vs' t'
+    |> postproc (postprocess_term thy)
+  end;
 
 fun static_eval_conv thy consts conv =
   let
     val (algebra, eqngr) = obtain true thy consts [];
+    val conv' = conv algebra eqngr;
   in
     Conv.tap_thy (fn thy => (preprocess_conv thy)
-      then_conv (fn ct => uncurry (conv algebra eqngr) (dest_cterm ct) ct)
+      then_conv (fn ct => uncurry (conv' thy) (dest_cterm ct) ct)
       then_conv (postprocess_conv thy))
   end;
 
+fun static_eval_value thy postproc consts evaluator =
+  let
+    val (algebra, eqngr) = obtain true thy consts [];
+    val evaluator' = evaluator algebra eqngr;
+  in fn t =>
+    t
+    |> preprocess_term thy
+    |> (fn t => evaluator' thy (Term.add_tfrees t [])  t)
+    |> postproc (postprocess_term thy)
+  end;
+
 
 (** setup **)
 
diff -r d7caf48c4676 -r fd1032c23cdf src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Thu Sep 16 17:42:49 2010 +0200
+++ b/src/Tools/Code/code_runtime.ML	Thu Sep 16 17:51:16 2010 +0200
@@ -7,41 +7,139 @@
 signature CODE_RUNTIME =
 sig
   val target: string
-  val value: string option
-    -> (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string
-    -> ((term -> term) -> 'a -> 'a) -> theory -> term -> string list -> 'a
+  type 'a cookie = (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string
+  val dynamic_value: 'a cookie -> theory -> string option
+    -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a option
+  val dynamic_value_strict: 'a cookie -> theory -> string option
+    -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a
+  val dynamic_value_exn: 'a cookie -> theory -> string option
+    -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a Exn.result
+  val static_value: 'a cookie -> theory -> string option
+    -> ((term -> term) -> 'a -> 'a) -> string list -> term -> 'a option
+  val static_value_strict: 'a cookie -> theory -> string option
+    -> ((term -> term) -> 'a -> 'a) -> string list -> term -> 'a
+  val static_value_exn: 'a cookie -> theory -> string option
+    -> ((term -> term) -> 'a -> 'a) -> string list -> term -> 'a Exn.result
+  val dynamic_holds_conv: conv
+  val static_holds_conv: theory -> string list -> conv
   val code_reflect: (string * string list) list -> string list -> string -> string option
     -> theory -> theory
-  val setup: theory -> theory
+  datatype truth = Holds
+  val put_truth: (unit -> truth) -> Proof.context -> Proof.context
 end;
 
 structure Code_Runtime : CODE_RUNTIME =
 struct
 
+open Basic_Code_Thingol;
+
 (** evaluation **)
 
+(* technical prerequisites *)
+
+val this = "Code_Runtime";
+val s_truth = Long_Name.append this "truth";
+val s_Holds = Long_Name.append this "Holds";
+
 val target = "Eval";
 
-val truth_struct = "Code_Truth";
+datatype truth = Holds;
 
-fun value some_target cookie postproc thy t args =
+val _ = Context.>> (Context.map_theory
+  (Code_Target.extend_target (target, (Code_ML.target_SML, K I))
+  #> Code_Target.add_tyco_syntax target @{type_name prop} (SOME (0, (K o K o K) (Code_Printer.str s_truth)))
+  #> Code_Target.add_const_syntax target @{const_name Code_Generator.holds} (SOME (Code_Printer.plain_const_syntax s_Holds))
+  #> Code_Target.add_reserved target this
+  #> fold (Code_Target.add_reserved target) ["oo", "ooo", "oooo", "upto", "downto", "orf", "andf"])); (*avoid further pervasive infix names*)
+
+
+(* evaluation into target language values *)
+
+type 'a cookie = (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string;
+
+fun base_evaluator cookie thy some_target naming program ((_, (vs, ty)), t) deps args =
   let
     val ctxt = ProofContext.init_global thy;
-    fun evaluator naming program ((_, (_, ty)), t) deps =
-      let
-        val _ = if Code_Thingol.contains_dictvar t then
-          error "Term to be evaluated contains free dictionaries" else ();
-        val value_name = "Value.VALUE.value"
-        val program' = program
-          |> Graph.new_node (value_name,
-              Code_Thingol.Fun (Term.dummy_patternN, ((([], ty), [(([], t), (NONE, true))]), NONE)))
-          |> fold (curry Graph.add_edge value_name) deps;
-        val (program_code, [SOME value_name']) = Code_Target.produce_code_for thy
-          (the_default target some_target) NONE "Code" [] naming program' [value_name];
-        val value_code = space_implode " "
-          (value_name' :: map (enclose "(" ")") args);
-      in ML_Context.value ctxt cookie (program_code, value_code) end;
-  in Code_Thingol.dynamic_eval_value thy postproc evaluator t end;
+    val _ = if Code_Thingol.contains_dictvar t then
+      error "Term to be evaluated contains free dictionaries" else ();
+    val v' = Name.variant (map fst vs) "a";
+    val vs' = (v', []) :: vs
+    val ty' = Code_Thingol.fun_tyco `%% [ITyVar v', ty];
+    val value_name = "Value.value.value"
+    val program' = program
+      |> Graph.new_node (value_name,
+          Code_Thingol.Fun (Term.dummy_patternN, (((vs', ty'), [(([IVar NONE], t), (NONE, true))]), NONE)))
+      |> fold (curry Graph.add_edge value_name) deps;
+    val (program_code, [SOME value_name']) = Code_Target.produce_code_for thy
+      (the_default target some_target) NONE "Code" [] naming program' [value_name];
+    val value_code = space_implode " "
+      (value_name' :: "()" :: map (enclose "(" ")") args);
+  in Exn.capture (ML_Context.value ctxt cookie) (program_code, value_code) end;
+
+fun partiality_as_none e = SOME (Exn.release e)
+  handle General.Match => NONE
+    | General.Bind => NONE
+    | General.Fail _ => NONE;
+
+fun dynamic_value_exn cookie thy some_target postproc t args =
+  let
+    fun evaluator naming program expr deps =
+      base_evaluator cookie thy some_target naming program expr deps args;
+  in Code_Thingol.dynamic_eval_value thy (Exn.map_result o postproc) evaluator t end;
+
+fun dynamic_value_strict cookie thy some_target postproc t args =
+  Exn.release (dynamic_value_exn cookie thy some_target postproc t args);
+
+fun dynamic_value cookie thy some_target postproc t args =
+  partiality_as_none (dynamic_value_exn cookie thy some_target postproc t args);
+
+fun static_value_exn cookie thy some_target postproc consts =
+  let
+    fun evaluator naming program thy expr deps =
+      base_evaluator cookie thy some_target naming program expr deps [];
+  in Code_Thingol.static_eval_value thy (Exn.map_result o postproc) consts evaluator end;
+
+fun static_value_strict cookie thy some_target postproc consts t =
+  Exn.release (static_value_exn cookie thy some_target postproc consts t);
+
+fun static_value cookie thy some_target postproc consts t =
+  partiality_as_none (static_value_exn cookie thy some_target postproc consts t);
+
+
+(* evaluation for truth or nothing *)
+
+structure Truth_Result = Proof_Data (
+  type T = unit -> truth
+  fun init _ () = error "Truth_Result"
+);
+val put_truth = Truth_Result.put;
+val truth_cookie = (Truth_Result.get, put_truth, Long_Name.append this "put_truth");
+
+fun check_holds thy naming program expr 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 (base_evaluator truth_cookie thy NONE naming program expr deps [])
+     of SOME Holds => true
+      | _ => false;
+  in
+    Thm.mk_binop iff ct (if result then @{cprop "PROP Code_Generator.holds"} else ct)
+  end;
+
+val (_, raw_check_holds_oracle) = Context.>>> (Context.map_theory_result
+  (Thm.add_oracle (Binding.name "holds_by_evaluation",
+  fn (thy, naming, program, expr, deps, ct) => check_holds thy naming program expr deps ct)));
+
+fun check_holds_oracle thy naming program expr deps ct =
+  raw_check_holds_oracle (thy, naming, program, expr, deps, ct);
+
+val dynamic_holds_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_eval_conv thy (check_holds_oracle thy));
+
+fun static_holds_conv thy consts = Code_Thingol.static_eval_conv thy consts
+  (fn naming => fn program => fn thy => check_holds_oracle thy naming program);
 
 
 (** instrumentalization **)
@@ -221,6 +319,4 @@
 
 end; (*local*)
 
-val setup = Code_Target.extend_target (target, (Code_ML.target_SML, K I));
-
 end; (*struct*)
diff -r d7caf48c4676 -r fd1032c23cdf src/Tools/Code/code_simp.ML
--- a/src/Tools/Code/code_simp.ML	Thu Sep 16 17:42:49 2010 +0200
+++ b/src/Tools/Code/code_simp.ML	Thu Sep 16 17:51:16 2010 +0200
@@ -84,7 +84,8 @@
 (* evaluation with freezed code context *)
 
 fun static_eval_conv thy some_ss consts = no_frees_conv
-  (Code_Thingol.static_eval_conv_simple thy consts (rewrite_modulo thy some_ss));
+  (Code_Thingol.static_eval_conv_simple thy consts
+    (fn program => fn thy => rewrite_modulo thy some_ss program));
 
 fun static_eval_tac thy some_ss consts = CONVERSION (static_eval_conv thy some_ss consts)
   THEN' conclude_tac thy some_ss;
diff -r d7caf48c4676 -r fd1032c23cdf src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Thu Sep 16 17:42:49 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML	Thu Sep 16 17:51:16 2010 +0200
@@ -99,10 +99,13 @@
     -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
     -> term -> 'a
   val static_eval_conv: theory -> string list
-    -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> conv)
+    -> (naming -> program -> theory -> ((string * sort) list * typscheme) * iterm -> string list -> conv)
     -> conv
   val static_eval_conv_simple: theory -> string list
-    -> (program -> conv) -> conv
+    -> (program -> theory -> conv) -> conv
+  val static_eval_value: theory -> ((term -> term) -> 'a -> 'a) -> string list
+    -> (naming -> program -> theory -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
+    -> term -> 'a
 end;
 
 structure Code_Thingol: CODE_THINGOL =
@@ -884,25 +887,34 @@
     #> term_value
   end;
 
-fun base_evaluator thy evaluator algebra eqngr vs t =
+fun base_evaluator evaluator algebra eqngr thy vs t =
   let
     val (((naming, program), (((vs', ty'), t'), deps)), _) =
       invoke_generation false thy (algebra, eqngr) ensure_value t;
     val vs'' = map (fn (v, _) => (v, (the o AList.lookup (op =) vs o prefix "'") v)) vs';
-  in evaluator naming program ((vs'', (vs', ty')), t') deps end;
+  in evaluator naming program thy ((vs'', (vs', ty')), t') deps end;
+
+fun dynamic_evaluator thy evaluator algebra eqngr vs t =
+  base_evaluator (fn naming => fn program => fn _ => evaluator naming program) algebra eqngr thy vs t;
 
-fun dynamic_eval_conv thy = Code_Preproc.dynamic_eval_conv thy o base_evaluator thy;
-fun dynamic_eval_value thy postproc = Code_Preproc.dynamic_eval_value thy postproc o base_evaluator thy;
+fun dynamic_eval_conv thy evaluator =
+  Code_Preproc.dynamic_eval_conv thy (dynamic_evaluator thy evaluator);
+
+fun dynamic_eval_value thy postproc evaluator =
+  Code_Preproc.dynamic_eval_value thy postproc (dynamic_evaluator thy evaluator);
 
 fun static_eval_conv thy consts conv =
-  Code_Preproc.static_eval_conv thy consts (base_evaluator thy conv); (*FIXME avoid re-generation*)
+  Code_Preproc.static_eval_conv thy consts (base_evaluator conv); (*FIXME avoid re-generation*)
 
 fun static_eval_conv_simple thy consts conv =
-  Code_Preproc.static_eval_conv thy consts (fn algebra => fn eqngr => fn _ => fn _ => fn ct =>
+  Code_Preproc.static_eval_conv thy consts (fn algebra => fn eqngr => fn thy => fn _ => fn _ => fn ct =>
     conv ((NONE, (empty_naming, Graph.empty)) (*FIXME provide abstraction for this kind of invocation*)
       |> fold_map (ensure_const thy algebra eqngr false) consts
-      |> (snd o snd o snd)) ct);
+      |> (snd o snd o snd)) thy ct);
 
+fun static_eval_value thy postproc consts conv =
+  Code_Preproc.static_eval_value thy postproc consts (base_evaluator conv); (*FIXME avoid re-generation*)
+  
 
 (** diagnostic commands **)
 
diff -r d7caf48c4676 -r fd1032c23cdf src/Tools/Code_Generator.thy
--- a/src/Tools/Code_Generator.thy	Thu Sep 16 17:42:49 2010 +0200
+++ b/src/Tools/Code_Generator.thy	Thu Sep 16 17:51:16 2010 +0200
@@ -21,8 +21,8 @@
   "~~/src/Tools/Code/code_ml.ML"
   "~~/src/Tools/Code/code_haskell.ML"
   "~~/src/Tools/Code/code_scala.ML"
-  "~~/src/Tools/Code/code_runtime.ML"
   "~~/src/Tools/nbe.ML"
+  ("~~/src/Tools/Code/code_runtime.ML")
 begin
 
 setup {*
@@ -32,7 +32,6 @@
   #> Code_ML.setup
   #> Code_Haskell.setup
   #> Code_Scala.setup
-  #> Code_Runtime.setup
   #> Nbe.setup
   #> Quickcheck.setup
 *}
@@ -64,6 +63,8 @@
     by rule (rule holds)+
 qed  
 
+use "~~/src/Tools/Code/code_runtime.ML"
+
 hide_const (open) holds
 
 end
diff -r d7caf48c4676 -r fd1032c23cdf src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Thu Sep 16 17:42:49 2010 +0200
+++ b/src/Tools/nbe.ML	Thu Sep 16 17:51:16 2010 +0200
@@ -609,7 +609,8 @@
 
 fun static_eval_conv thy consts = Code_Simp.no_frees_conv
   (lift_triv_classes_conv thy (Code_Thingol.static_eval_conv thy consts
-    (K (fn program => oracle thy program (compile true thy program)))));
+    (K (fn program => let val nbe_program = compile true thy program
+      in fn thy => oracle thy program nbe_program end))));
 
 
 (** setup **)