# HG changeset patch # User haftmann # Date 1284543032 -7200 # Node ID fdbb2c55ffc24b1b064a6f45a5d466f1bcc2a862 # Parent 6608c4838ff957ca17ccb39870de102a48df440c replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references diff -r 6608c4838ff9 -r fdbb2c55ffc2 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Wed Sep 15 11:30:31 2010 +0200 +++ b/src/HOL/HOL.thy Wed Sep 15 11:30:32 2010 +0200 @@ -1966,12 +1966,10 @@ *} ML {* -structure Eval_Method = -struct - -val eval_ref : (unit -> bool) option Unsynchronized.ref = Unsynchronized.ref NONE; - -end; +structure Eval_Method = Proof_Data( + type T = unit -> bool + fun init thy () = error "Eval_Method" +) *} oracle eval_oracle = {* fn ct => @@ -1981,7 +1979,7 @@ val dummy = @{cprop True}; in case try HOLogic.dest_Trueprop t of SOME t' => if Code_Eval.eval NONE - ("Eval_Method.eval_ref", Eval_Method.eval_ref) (K I) thy t' [] + (Eval_Method.get, Eval_Method.put, "Eval_Method.put") (K I) thy t' [] then Thm.capply (Thm.capply @{cterm "op \ \ prop \ prop \ prop"} ct) dummy else dummy | NONE => dummy diff -r 6608c4838ff9 -r fdbb2c55ffc2 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Sep 15 11:30:31 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Sep 15 11:30:32 2010 +0200 @@ -43,18 +43,20 @@ val print_stored_rules : Proof.context -> unit val print_all_modes : compilation -> Proof.context -> unit val mk_casesrule : Proof.context -> term -> thm list -> term - val eval_ref : (unit -> term Predicate.pred) option Unsynchronized.ref - val random_eval_ref : (unit -> int * int -> term Predicate.pred * (int * int)) - option Unsynchronized.ref - val dseq_eval_ref : (unit -> term DSequence.dseq) option Unsynchronized.ref - val random_dseq_eval_ref : (unit -> int -> int -> int * int -> term DSequence.dseq * (int * int)) - option Unsynchronized.ref - val new_random_dseq_eval_ref : - (unit -> int -> int -> int * int -> int -> term Lazy_Sequence.lazy_sequence) - option Unsynchronized.ref - val new_random_dseq_stats_eval_ref : - (unit -> int -> int -> int * int -> int -> (term * int) Lazy_Sequence.lazy_sequence) - option Unsynchronized.ref + + val put_pred_result : (unit -> term Predicate.pred) -> Proof.context -> Proof.context + val put_pred_random_result : (unit -> int * int -> term Predicate.pred * (int * int)) -> + Proof.context -> Proof.context + val put_dseq_result : (unit -> term DSequence.dseq) -> Proof.context -> Proof.context + val put_dseq_random_result : (unit -> int -> int -> int * int -> term DSequence.dseq * (int * int)) -> + Proof.context -> Proof.context + val put_lseq_random_result : + (unit -> int -> int -> int * int -> int -> term Lazy_Sequence.lazy_sequence) -> + Proof.context -> Proof.context + val put_lseq_random_stats_result : + (unit -> int -> int -> int * int -> int -> (term * int) Lazy_Sequence.lazy_sequence) -> + Proof.context -> Proof.context + val code_pred_intro_attrib : attribute (* used by Quickcheck_Generator *) (* temporary for testing of the compilation *) @@ -3105,17 +3107,41 @@ (* transformation for code generation *) -val eval_ref = Unsynchronized.ref (NONE : (unit -> term Predicate.pred) option); -val random_eval_ref = - Unsynchronized.ref (NONE : (unit -> int * int -> term Predicate.pred * (int * int)) option); -val dseq_eval_ref = Unsynchronized.ref (NONE : (unit -> term DSequence.dseq) option); -val random_dseq_eval_ref = - Unsynchronized.ref (NONE : (unit -> int -> int -> int * int -> term DSequence.dseq * (int * int)) option); -val new_random_dseq_eval_ref = - Unsynchronized.ref (NONE : (unit -> int -> int -> int * int -> int -> term Lazy_Sequence.lazy_sequence) option) -val new_random_dseq_stats_eval_ref = - Unsynchronized.ref (NONE : - (unit -> int -> int -> int * int -> int -> (term * int) Lazy_Sequence.lazy_sequence) option) +structure Pred_Result = Proof_Data ( + type T = unit -> term Predicate.pred + fun init _ () = error "Pred_Result" +); +val put_pred_result = Pred_Result.put; + +structure Pred_Random_Result = Proof_Data ( + type T = unit -> int * int -> term Predicate.pred * (int * int) + fun init _ () = error "Pred_Random_Result" +); +val put_pred_random_result = Pred_Random_Result.put; + +structure Dseq_Result = Proof_Data ( + type T = unit -> term DSequence.dseq + fun init _ () = error "Dseq_Result" +); +val put_dseq_result = Dseq_Result.put; + +structure Dseq_Random_Result = Proof_Data ( + type T = unit -> int -> int -> int * int -> term DSequence.dseq * (int * int) + fun init _ () = error "Dseq_Random_Result" +); +val put_dseq_random_result = Dseq_Random_Result.put; + +structure Lseq_Random_Result = Proof_Data ( + type T = unit -> int -> int -> int * int -> int -> term Lazy_Sequence.lazy_sequence + fun init _ () = error "Lseq_Random_Result" +); +val put_lseq_random_result = Lseq_Random_Result.put; + +structure Lseq_Random_Stats_Result = Proof_Data ( + type T = unit -> int -> int -> int * int -> int -> (term * int) Lazy_Sequence.lazy_sequence + fun init _ () = error "Lseq_Random_Stats_Result" +); +val put_lseq_random_stats_result = Lseq_Random_Stats_Result.put; (*FIXME turn this into an LCF-guarded preprocessor for comprehensions*) fun analyze_compr ctxt compfuns param_user_modes (compilation, arguments) t_compr = @@ -3251,7 +3277,7 @@ val [nrandom, size, depth] = arguments in rpair NONE (fst (DSequence.yieldn k - (Code_Eval.eval NONE ("Predicate_Compile_Core.random_dseq_eval_ref", random_dseq_eval_ref) + (Code_Eval.eval 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 |> Random_Engine.run) @@ -3259,7 +3285,7 @@ end | DSeq => rpair NONE (fst (DSequence.yieldn k - (Code_Eval.eval NONE ("Predicate_Compile_Core.dseq_eval_ref", dseq_eval_ref) + (Code_Eval.eval NONE (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Core.put_dseq_result") DSequence.map thy t' []) (the_single arguments) true)) | New_Pos_Random_DSeq => let @@ -3270,21 +3296,21 @@ apsnd (SOME o accumulate) (split_list (fst (Lazy_Sequence.yieldn k (Code_Eval.eval NONE - ("Predicate_Compile_Core.new_random_dseq_stats_eval_ref", new_random_dseq_stats_eval_ref) + (Lseq_Random_Stats_Result.get, put_lseq_random_stats_result, "Predicate_Compile_Core.put_lseq_random_stats_result") (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)))) else rpair NONE (fst (Lazy_Sequence.yieldn k (Code_Eval.eval NONE - ("Predicate_Compile_Core.new_random_dseq_eval_ref", new_random_dseq_eval_ref) + (Lseq_Random_Result.get, put_lseq_random_result, "Predicate_Compile_Core.put_lseq_random_result") (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))) end | _ => rpair NONE (fst (Predicate.yieldn k - (Code_Eval.eval NONE ("Predicate_Compile_Core.eval_ref", eval_ref) + (Code_Eval.eval NONE (Pred_Result.get, put_pred_result, "Predicate_Compile_Core.put_pred_result") Predicate.map thy t' []))) in ((T, ts), statistics) end; diff -r 6608c4838ff9 -r fdbb2c55ffc2 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Wed Sep 15 11:30:31 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Wed Sep 15 11:30:32 2010 +0200 @@ -7,12 +7,15 @@ signature PREDICATE_COMPILE_QUICKCHECK = sig (*val quickcheck : Proof.context -> term -> int -> term list option*) - val test_ref : - ((unit -> int -> int -> int * int -> term list DSequence.dseq * (int * int)) option) Unsynchronized.ref - val new_test_ref : - ((unit -> int -> int -> int * int -> int -> term list Lazy_Sequence.lazy_sequence) option) Unsynchronized.ref; - val eval_random_ref : - ((unit -> int -> int -> int -> int * int -> term list Predicate.pred) option) Unsynchronized.ref; + val put_pred_result : + (unit -> int -> int -> int -> int * int -> term list Predicate.pred) -> + Proof.context -> Proof.context; + val put_dseq_result : + (unit -> int -> int -> int * int -> term list DSequence.dseq * (int * int)) -> + Proof.context -> Proof.context; + val put_lseq_result : + (unit -> int -> int -> int * int -> int -> term list Lazy_Sequence.lazy_sequence) -> + Proof.context -> Proof.context; val tracing : bool Unsynchronized.ref; val quiet : bool Unsynchronized.ref; @@ -30,15 +33,23 @@ open Predicate_Compile_Aux; -val test_ref = - Unsynchronized.ref (NONE : (unit -> int -> int -> int * int -> term list DSequence.dseq * (int * int)) option); +structure Pred_Result = Proof_Data ( + type T = unit -> int -> int -> int -> int * int -> term list Predicate.pred + fun init _ () = error "Pred_Result" +); +val put_pred_result = Pred_Result.put; -val new_test_ref = - Unsynchronized.ref (NONE : (unit -> int -> int -> int * int -> int -> term list Lazy_Sequence.lazy_sequence) option) +structure Dseq_Result = Proof_Data ( + type T = unit -> int -> int -> int * int -> term list DSequence.dseq * (int * int) + fun init _ () = error "Dseq_Result" +); +val put_dseq_result = Dseq_Result.put; -val eval_random_ref = - Unsynchronized.ref (NONE : (unit -> int -> int -> int -> int * int -> term list Predicate.pred) option); - +structure Lseq_Result = Proof_Data ( + type T = unit -> int -> int -> int * int -> int -> term list Lazy_Sequence.lazy_sequence + fun init _ () = error "Lseq_Result" +); +val put_lseq_result = Lseq_Result.put; val tracing = Unsynchronized.ref false; @@ -253,7 +264,7 @@ Pos_Random_DSeq => let val compiled_term = - Code_Eval.eval (SOME target) ("Predicate_Compile_Quickcheck.test_ref", test_ref) + Code_Eval.eval (SOME target) (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Quickcheck.put_dseq_result") (fn proc => fn g => fn n => fn size => fn s => g n size s |>> (DSequence.map o map) proc) thy4 qc_term [] in @@ -265,7 +276,7 @@ let val compiled_term = Code_Eval.eval (SOME target) - ("Predicate_Compile_Quickcheck.new_test_ref", new_test_ref) + (Lseq_Result.get, put_lseq_result, "Predicate_Compile_Quickcheck.put_lseq_result") (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 [] @@ -279,7 +290,7 @@ | Depth_Limited_Random => let val compiled_term = Code_Eval.eval (SOME target) - ("Predicate_Compile_Quickcheck.eval_random_ref", eval_random_ref) + (Pred_Result.get, put_pred_result, "Predicate_Compile_Quickcheck.put_pred_result") (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 [] diff -r 6608c4838ff9 -r fdbb2c55ffc2 src/HOL/Tools/quickcheck_generators.ML --- a/src/HOL/Tools/quickcheck_generators.ML Wed Sep 15 11:30:31 2010 +0200 +++ b/src/HOL/Tools/quickcheck_generators.ML Wed Sep 15 11:30:32 2010 +0200 @@ -15,9 +15,10 @@ val ensure_random_datatype: Datatype.config -> string list -> theory -> theory val compile_generator_expr: Proof.context -> term -> int -> term list option * (bool list * bool) - val eval_ref: (unit -> int -> seed -> term list option * seed) option Unsynchronized.ref - val eval_report_ref: - (unit -> int -> seed -> (term list option * (bool list * bool)) * seed) option Unsynchronized.ref + val put_counterexample: (unit -> int -> seed -> term list option * seed) + -> Proof.context -> Proof.context + val put_counterexample_report: (unit -> int -> seed -> (term list option * (bool list * bool)) * seed) + -> Proof.context -> Proof.context val setup: theory -> theory end; @@ -304,13 +305,17 @@ (** building and compiling generator expressions **) -val eval_ref : - (unit -> int -> int * int -> term list option * (int * int)) option Unsynchronized.ref = - Unsynchronized.ref NONE; +structure Counterexample = Proof_Data ( + type T = unit -> int -> int * int -> term list option * (int * int) + fun init _ () = error "Counterexample" +); +val put_counterexample = Counterexample.put; -val eval_report_ref : - (unit -> int -> seed -> (term list option * (bool list * bool)) * seed) option Unsynchronized.ref = - Unsynchronized.ref NONE; +structure Counterexample_Report = Proof_Data ( + type T = unit -> int -> seed -> (term list option * (bool list * bool)) * seed + fun init _ () = error "Counterexample_Report" +); +val put_counterexample_report = Counterexample_Report.put; val target = "Quickcheck"; @@ -387,13 +392,15 @@ in if Quickcheck.report ctxt then let val t' = mk_reporting_generator_expr thy t Ts; - val compile = Code_Eval.eval (SOME target) ("Quickcheck_Generators.eval_report_ref", eval_report_ref) + val compile = Code_Eval.eval (SOME target) + (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' []; in compile #> Random_Engine.run end else let val t' = mk_generator_expr thy t Ts; - val compile = Code_Eval.eval (SOME target) ("Quickcheck_Generators.eval_ref", eval_ref) + val compile = Code_Eval.eval (SOME target) + (Counterexample.get, put_counterexample, "Quickcheck_Generators.put_counterexample") (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' []; val dummy_report = ([], false) in compile #> Random_Engine.run #> rpair dummy_report end diff -r 6608c4838ff9 -r fdbb2c55ffc2 src/Pure/ML/ml_context.ML --- a/src/Pure/ML/ml_context.ML Wed Sep 15 11:30:31 2010 +0200 +++ b/src/Pure/ML/ml_context.ML Wed Sep 15 11:30:32 2010 +0200 @@ -36,8 +36,9 @@ val eval_text_in: Proof.context option -> bool -> Position.T -> Symbol_Pos.text -> unit val expression: Position.T -> string -> string -> ML_Lex.token Antiquote.antiquote list -> Context.generic -> Context.generic - val evaluate: Proof.context -> bool -> - string * (unit -> 'a) option Unsynchronized.ref -> string * string -> 'a + val value: Proof.context -> + (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string -> + string * string -> 'a end structure ML_Context: ML_CONTEXT = @@ -213,17 +214,15 @@ (ML_Lex.read Position.none ("Context.set_thread_data (SOME (let " ^ bind ^ " = ") @ ants @ ML_Lex.read Position.none (" in " ^ body ^ " end (ML_Context.the_generic_context ())));"))); - -(* FIXME not thread-safe -- reference can be accessed directly *) -fun evaluate ctxt verbose (ref_name, r) (prelude, txt) = NAMED_CRITICAL "ML" (fn () => +fun value ctxt (get, put, put_ml) (prelude, value) = let - val s = prelude ^ "val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ txt ^ "))" - val ants = ML_Lex.read Position.none s; - val _ = r := NONE; - val _ = - Context.setmp_thread_data (SOME (Context.Proof ctxt)) - (fn () => eval verbose Position.none ants) (); - in (case ! r of NONE => error ("Bad evaluation for " ^ ref_name) | SOME e => e) end) (); + val read = ML_Lex.read Position.none; + val ants = read prelude @ read ("val _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml + ^ " (fn () => " ^ value ^ ")) (ML_Context.the_generic_context ())))"); + val ctxt' = ctxt + |> put (fn () => error ("Bad evaluation for " ^ quote put_ml)) + |> Context.proof_map (exec (fn () => eval false Position.none ants)); + in get ctxt' () end; end; diff -r 6608c4838ff9 -r fdbb2c55ffc2 src/Tools/Code/code_eval.ML --- a/src/Tools/Code/code_eval.ML Wed Sep 15 11:30:31 2010 +0200 +++ b/src/Tools/Code/code_eval.ML Wed Sep 15 11:30:32 2010 +0200 @@ -7,7 +7,8 @@ signature CODE_EVAL = sig val target: string - val eval: string option -> string * (unit -> 'a) option Unsynchronized.ref + val eval: string option + -> (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string -> ((term -> term) -> 'a -> 'a) -> theory -> term -> string list -> 'a val setup: theory -> theory end; @@ -39,7 +40,7 @@ (** evaluation **) -fun eval some_target reff postproc thy t args = +fun eval some_target cookie postproc thy t args = let val ctxt = ProofContext.init_global thy; fun evaluator naming program ((_, (_, ty)), t) deps = @@ -55,7 +56,7 @@ (the_default target some_target) NONE "Code" [] naming program' [value_name]; val value_code = space_implode " " (value_name' :: map (enclose "(" ")") args); - in ML_Context.evaluate ctxt false reff (program_code, value_code) end; + in ML_Context.value ctxt cookie (program_code, value_code) end; in Code_Thingol.dynamic_eval_value thy postproc evaluator t end; diff -r 6608c4838ff9 -r fdbb2c55ffc2 src/Tools/nbe.ML --- a/src/Tools/nbe.ML Wed Sep 15 11:30:31 2010 +0200 +++ b/src/Tools/nbe.ML Wed Sep 15 11:30:32 2010 +0200 @@ -19,7 +19,7 @@ (*abstractions as closures*) val same: Univ -> Univ -> bool - val univs_ref: (unit -> Univ list -> Univ list) option Unsynchronized.ref + val put_result: (unit -> Univ list -> Univ list) -> Proof.context -> Proof.context val trace: bool Unsynchronized.ref val setup: theory -> theory @@ -228,10 +228,15 @@ (* nbe specific syntax and sandbox communication *) -val univs_ref = Unsynchronized.ref (NONE : (unit -> Univ list -> Univ list) option); +structure Univs = Proof_Data( + type T = unit -> Univ list -> Univ list + fun init thy () = error "Univs" +); +val put_result = Univs.put; local val prefix = "Nbe."; + val name_put = prefix ^ "put_result"; val name_ref = prefix ^ "univs_ref"; val name_const = prefix ^ "Const"; val name_abss = prefix ^ "abss"; @@ -239,7 +244,7 @@ val name_same = prefix ^ "same"; in -val univs_cookie = (name_ref, univs_ref); +val univs_cookie = (Univs.get, put_result, name_put); fun nbe_fun 0 "" = "nbe_value" | nbe_fun i c = "c_" ^ translate_string (fn "." => "_" | c => c) c ^ "_" ^ string_of_int i; @@ -389,7 +394,7 @@ s |> traced (fn s => "\n--- code to be evaluated:\n" ^ s) |> pair "" - |> ML_Context.evaluate ctxt (!trace) univs_cookie + |> ML_Context.value ctxt univs_cookie |> (fn f => f deps_vals) |> (fn univs => cs ~~ univs) end;