# HG changeset patch
# User haftmann
# Date 1284648693 -7200
# Node ID 55e0ff582fa4c47c28016b5077903ebd59e85e0e
# Parent  4a7d09da2b9c02b567724669e27117a5c6da971c
adjusted to changes in Code_Runtime

diff -r 4a7d09da2b9c -r 55e0ff582fa4 src/HOL/Code_Evaluation.thy
--- a/src/HOL/Code_Evaluation.thy	Thu Sep 16 08:18:34 2010 +0200
+++ b/src/HOL/Code_Evaluation.thy	Thu Sep 16 16:51:33 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 4a7d09da2b9c -r 55e0ff582fa4 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Sep 16 08:18:34 2010 +0200
+++ b/src/HOL/HOL.thy	Thu Sep 16 16:51:33 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 4a7d09da2b9c -r 55e0ff582fa4 src/HOL/Library/Eval_Witness.thy
--- a/src/HOL/Library/Eval_Witness.thy	Thu Sep 16 08:18:34 2010 +0200
+++ b/src/HOL/Library/Eval_Witness.thy	Thu Sep 16 16:51:33 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 4a7d09da2b9c -r 55e0ff582fa4 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Sep 16 08:18:34 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Sep 16 16:51:33 2010 +0200
@@ -3277,16 +3277,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
@@ -3295,23 +3295,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 4a7d09da2b9c -r 55e0ff582fa4 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Thu Sep 16 08:18:34 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Thu Sep 16 16:51:33 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 4a7d09da2b9c -r 55e0ff582fa4 src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Thu Sep 16 08:18:34 2010 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML	Thu Sep 16 16:51:33 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;