replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references
authorhaftmann
Wed Sep 15 11:30:32 2010 +0200 (2010-09-15)
changeset 39388fdbb2c55ffc2
parent 39387 6608c4838ff9
child 39389 20db6db55a6b
child 39392 7a0fcee7a2a3
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references
src/HOL/HOL.thy
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
src/HOL/Tools/quickcheck_generators.ML
src/Pure/ML/ml_context.ML
src/Tools/Code/code_eval.ML
src/Tools/nbe.ML
     1.1 --- a/src/HOL/HOL.thy	Wed Sep 15 11:30:31 2010 +0200
     1.2 +++ b/src/HOL/HOL.thy	Wed Sep 15 11:30:32 2010 +0200
     1.3 @@ -1966,12 +1966,10 @@
     1.4  *}
     1.5  
     1.6  ML {*
     1.7 -structure Eval_Method =
     1.8 -struct
     1.9 -
    1.10 -val eval_ref : (unit -> bool) option Unsynchronized.ref = Unsynchronized.ref NONE;
    1.11 -
    1.12 -end;
    1.13 +structure Eval_Method = Proof_Data(
    1.14 +  type T = unit -> bool
    1.15 +  fun init thy () = error "Eval_Method"
    1.16 +)
    1.17  *}
    1.18  
    1.19  oracle eval_oracle = {* fn ct =>
    1.20 @@ -1981,7 +1979,7 @@
    1.21      val dummy = @{cprop True};
    1.22    in case try HOLogic.dest_Trueprop t
    1.23     of SOME t' => if Code_Eval.eval NONE
    1.24 -         ("Eval_Method.eval_ref", Eval_Method.eval_ref) (K I) thy t' [] 
    1.25 +         (Eval_Method.get, Eval_Method.put, "Eval_Method.put") (K I) thy t' [] 
    1.26         then Thm.capply (Thm.capply @{cterm "op \<equiv> \<Colon> prop \<Rightarrow> prop \<Rightarrow> prop"} ct) dummy
    1.27         else dummy
    1.28      | NONE => dummy
     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Sep 15 11:30:31 2010 +0200
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Sep 15 11:30:32 2010 +0200
     2.3 @@ -43,18 +43,20 @@
     2.4    val print_stored_rules : Proof.context -> unit
     2.5    val print_all_modes : compilation -> Proof.context -> unit
     2.6    val mk_casesrule : Proof.context -> term -> thm list -> term
     2.7 -  val eval_ref : (unit -> term Predicate.pred) option Unsynchronized.ref
     2.8 -  val random_eval_ref : (unit -> int * int -> term Predicate.pred * (int * int))
     2.9 -    option Unsynchronized.ref
    2.10 -  val dseq_eval_ref : (unit -> term DSequence.dseq) option Unsynchronized.ref
    2.11 -  val random_dseq_eval_ref : (unit -> int -> int -> int * int -> term DSequence.dseq * (int * int))
    2.12 -    option Unsynchronized.ref
    2.13 -  val new_random_dseq_eval_ref :
    2.14 -    (unit -> int -> int -> int * int -> int -> term Lazy_Sequence.lazy_sequence)
    2.15 -      option Unsynchronized.ref
    2.16 -  val new_random_dseq_stats_eval_ref :
    2.17 -    (unit -> int -> int -> int * int -> int -> (term * int) Lazy_Sequence.lazy_sequence)
    2.18 -      option Unsynchronized.ref
    2.19 +
    2.20 +  val put_pred_result : (unit -> term Predicate.pred) -> Proof.context -> Proof.context
    2.21 +  val put_pred_random_result : (unit -> int * int -> term Predicate.pred * (int * int)) ->
    2.22 +    Proof.context -> Proof.context
    2.23 +  val put_dseq_result : (unit -> term DSequence.dseq) -> Proof.context -> Proof.context
    2.24 +  val put_dseq_random_result : (unit -> int -> int -> int * int -> term DSequence.dseq * (int * int)) ->
    2.25 +    Proof.context -> Proof.context
    2.26 +  val put_lseq_random_result :
    2.27 +    (unit -> int -> int -> int * int -> int -> term Lazy_Sequence.lazy_sequence) ->
    2.28 +    Proof.context -> Proof.context
    2.29 +  val put_lseq_random_stats_result :
    2.30 +    (unit -> int -> int -> int * int -> int -> (term * int) Lazy_Sequence.lazy_sequence) ->
    2.31 +    Proof.context -> Proof.context
    2.32 +
    2.33    val code_pred_intro_attrib : attribute
    2.34    (* used by Quickcheck_Generator *) 
    2.35    (* temporary for testing of the compilation *)
    2.36 @@ -3105,17 +3107,41 @@
    2.37  
    2.38  (* transformation for code generation *)
    2.39  
    2.40 -val eval_ref = Unsynchronized.ref (NONE : (unit -> term Predicate.pred) option);
    2.41 -val random_eval_ref =
    2.42 -  Unsynchronized.ref (NONE : (unit -> int * int -> term Predicate.pred * (int * int)) option);
    2.43 -val dseq_eval_ref = Unsynchronized.ref (NONE : (unit -> term DSequence.dseq) option);
    2.44 -val random_dseq_eval_ref =
    2.45 -  Unsynchronized.ref (NONE : (unit -> int -> int -> int * int -> term DSequence.dseq * (int * int)) option);
    2.46 -val new_random_dseq_eval_ref =
    2.47 -  Unsynchronized.ref (NONE : (unit -> int -> int -> int * int -> int -> term Lazy_Sequence.lazy_sequence) option)
    2.48 -val new_random_dseq_stats_eval_ref =
    2.49 -    Unsynchronized.ref (NONE :
    2.50 -      (unit -> int -> int -> int * int -> int -> (term * int) Lazy_Sequence.lazy_sequence) option)
    2.51 +structure Pred_Result = Proof_Data (
    2.52 +  type T = unit -> term Predicate.pred
    2.53 +  fun init _ () = error "Pred_Result"
    2.54 +);
    2.55 +val put_pred_result = Pred_Result.put;
    2.56 +
    2.57 +structure Pred_Random_Result = Proof_Data (
    2.58 +  type T = unit -> int * int -> term Predicate.pred * (int * int)
    2.59 +  fun init _ () = error "Pred_Random_Result"
    2.60 +);
    2.61 +val put_pred_random_result = Pred_Random_Result.put;
    2.62 +
    2.63 +structure Dseq_Result = Proof_Data (
    2.64 +  type T = unit -> term DSequence.dseq
    2.65 +  fun init _ () = error "Dseq_Result"
    2.66 +);
    2.67 +val put_dseq_result = Dseq_Result.put;
    2.68 +
    2.69 +structure Dseq_Random_Result = Proof_Data (
    2.70 +  type T = unit -> int -> int -> int * int -> term DSequence.dseq * (int * int)
    2.71 +  fun init _ () = error "Dseq_Random_Result"
    2.72 +);
    2.73 +val put_dseq_random_result = Dseq_Random_Result.put;
    2.74 +
    2.75 +structure Lseq_Random_Result = Proof_Data (
    2.76 +  type T = unit -> int -> int -> int * int -> int -> term Lazy_Sequence.lazy_sequence
    2.77 +  fun init _ () = error "Lseq_Random_Result"
    2.78 +);
    2.79 +val put_lseq_random_result = Lseq_Random_Result.put;
    2.80 +
    2.81 +structure Lseq_Random_Stats_Result = Proof_Data (
    2.82 +  type T = unit -> int -> int -> int * int -> int -> (term * int) Lazy_Sequence.lazy_sequence
    2.83 +  fun init _ () = error "Lseq_Random_Stats_Result"
    2.84 +);
    2.85 +val put_lseq_random_stats_result = Lseq_Random_Stats_Result.put;
    2.86  
    2.87  (*FIXME turn this into an LCF-guarded preprocessor for comprehensions*)
    2.88  fun analyze_compr ctxt compfuns param_user_modes (compilation, arguments) t_compr =
    2.89 @@ -3251,7 +3277,7 @@
    2.90              val [nrandom, size, depth] = arguments
    2.91            in
    2.92              rpair NONE (fst (DSequence.yieldn k
    2.93 -              (Code_Eval.eval NONE ("Predicate_Compile_Core.random_dseq_eval_ref", random_dseq_eval_ref)
    2.94 +              (Code_Eval.eval NONE (Dseq_Random_Result.get, put_dseq_random_result, "Predicate_Compile_Core.put_dseq_random_result")
    2.95                  (fn proc => fn g => fn nrandom => fn size => fn s => g nrandom size s |>> DSequence.map proc)
    2.96                    thy t' [] nrandom size
    2.97                  |> Random_Engine.run)
    2.98 @@ -3259,7 +3285,7 @@
    2.99            end
   2.100        | DSeq =>
   2.101            rpair NONE (fst (DSequence.yieldn k
   2.102 -            (Code_Eval.eval NONE ("Predicate_Compile_Core.dseq_eval_ref", dseq_eval_ref)
   2.103 +            (Code_Eval.eval NONE (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Core.put_dseq_result")
   2.104                DSequence.map thy t' []) (the_single arguments) true))
   2.105        | New_Pos_Random_DSeq =>
   2.106            let
   2.107 @@ -3270,21 +3296,21 @@
   2.108                apsnd (SOME o accumulate) (split_list
   2.109                (fst (Lazy_Sequence.yieldn k
   2.110                  (Code_Eval.eval NONE
   2.111 -                  ("Predicate_Compile_Core.new_random_dseq_stats_eval_ref", new_random_dseq_stats_eval_ref)
   2.112 +                  (Lseq_Random_Stats_Result.get, put_lseq_random_stats_result, "Predicate_Compile_Core.put_lseq_random_stats_result")
   2.113                    (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
   2.114                      |> Lazy_Sequence.mapa (apfst proc))
   2.115                      thy t' [] nrandom size seed depth))))
   2.116              else rpair NONE
   2.117                (fst (Lazy_Sequence.yieldn k
   2.118                  (Code_Eval.eval NONE
   2.119 -                  ("Predicate_Compile_Core.new_random_dseq_eval_ref", new_random_dseq_eval_ref)
   2.120 +                  (Lseq_Random_Result.get, put_lseq_random_result, "Predicate_Compile_Core.put_lseq_random_result")
   2.121                    (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
   2.122                      |> Lazy_Sequence.mapa proc)
   2.123                      thy t' [] nrandom size seed depth)))
   2.124            end
   2.125        | _ =>
   2.126            rpair NONE (fst (Predicate.yieldn k
   2.127 -            (Code_Eval.eval NONE ("Predicate_Compile_Core.eval_ref", eval_ref)
   2.128 +            (Code_Eval.eval NONE (Pred_Result.get, put_pred_result, "Predicate_Compile_Core.put_pred_result")
   2.129                Predicate.map thy t' [])))
   2.130    in ((T, ts), statistics) end;
   2.131  
     3.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Wed Sep 15 11:30:31 2010 +0200
     3.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Wed Sep 15 11:30:32 2010 +0200
     3.3 @@ -7,12 +7,15 @@
     3.4  signature PREDICATE_COMPILE_QUICKCHECK =
     3.5  sig
     3.6    (*val quickcheck : Proof.context -> term -> int -> term list option*)
     3.7 -  val test_ref :
     3.8 -    ((unit -> int -> int -> int * int -> term list DSequence.dseq * (int * int)) option) Unsynchronized.ref
     3.9 -  val new_test_ref :
    3.10 -    ((unit -> int -> int -> int * int -> int -> term list Lazy_Sequence.lazy_sequence) option) Unsynchronized.ref;
    3.11 -  val eval_random_ref :
    3.12 -    ((unit -> int -> int -> int -> int * int -> term list Predicate.pred) option) Unsynchronized.ref;
    3.13 +  val put_pred_result :
    3.14 +    (unit -> int -> int -> int -> int * int -> term list Predicate.pred) ->
    3.15 +      Proof.context -> Proof.context;
    3.16 +  val put_dseq_result :
    3.17 +    (unit -> int -> int -> int * int -> term list DSequence.dseq * (int * int)) ->
    3.18 +      Proof.context -> Proof.context;
    3.19 +  val put_lseq_result :
    3.20 +    (unit -> int -> int -> int * int -> int -> term list Lazy_Sequence.lazy_sequence) ->
    3.21 +      Proof.context -> Proof.context;
    3.22  
    3.23    val tracing : bool Unsynchronized.ref;
    3.24    val quiet : bool Unsynchronized.ref;
    3.25 @@ -30,15 +33,23 @@
    3.26  
    3.27  open Predicate_Compile_Aux;
    3.28  
    3.29 -val test_ref =
    3.30 -  Unsynchronized.ref (NONE : (unit -> int -> int -> int * int -> term list DSequence.dseq * (int * int)) option);
    3.31 +structure Pred_Result = Proof_Data (
    3.32 +  type T = unit -> int -> int -> int -> int * int -> term list Predicate.pred
    3.33 +  fun init _ () = error "Pred_Result"
    3.34 +);
    3.35 +val put_pred_result = Pred_Result.put;
    3.36  
    3.37 -val new_test_ref =
    3.38 -  Unsynchronized.ref (NONE : (unit -> int -> int -> int * int -> int -> term list Lazy_Sequence.lazy_sequence) option)
    3.39 +structure Dseq_Result = Proof_Data (
    3.40 +  type T = unit -> int -> int -> int * int -> term list DSequence.dseq * (int * int)
    3.41 +  fun init _ () = error "Dseq_Result"
    3.42 +);
    3.43 +val put_dseq_result = Dseq_Result.put;
    3.44  
    3.45 -val eval_random_ref =
    3.46 -  Unsynchronized.ref (NONE : (unit -> int -> int -> int -> int * int -> term list Predicate.pred) option);
    3.47 -
    3.48 +structure Lseq_Result = Proof_Data (
    3.49 +  type T = unit -> int -> int -> int * int -> int -> term list Lazy_Sequence.lazy_sequence
    3.50 +  fun init _ () = error "Lseq_Result"
    3.51 +);
    3.52 +val put_lseq_result = Lseq_Result.put;
    3.53  
    3.54  val tracing = Unsynchronized.ref false;
    3.55  
    3.56 @@ -253,7 +264,7 @@
    3.57          Pos_Random_DSeq =>
    3.58            let
    3.59              val compiled_term =
    3.60 -              Code_Eval.eval (SOME target) ("Predicate_Compile_Quickcheck.test_ref", test_ref)
    3.61 +              Code_Eval.eval (SOME target) (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Quickcheck.put_dseq_result")
    3.62                  (fn proc => fn g => fn n => fn size => fn s => g n size s |>> (DSequence.map o map) proc)
    3.63                  thy4 qc_term []
    3.64            in
    3.65 @@ -265,7 +276,7 @@
    3.66            let
    3.67              val compiled_term =
    3.68                Code_Eval.eval (SOME target)
    3.69 -                ("Predicate_Compile_Quickcheck.new_test_ref", new_test_ref)
    3.70 +                (Lseq_Result.get, put_lseq_result, "Predicate_Compile_Quickcheck.put_lseq_result")
    3.71                  (fn proc => fn g => fn nrandom => fn size => fn s => fn depth =>
    3.72                    g nrandom size s depth |> (Lazy_Sequence.mapa o map) proc)
    3.73                    thy4 qc_term []
    3.74 @@ -279,7 +290,7 @@
    3.75        | Depth_Limited_Random =>
    3.76            let
    3.77              val compiled_term = Code_Eval.eval (SOME target)
    3.78 -              ("Predicate_Compile_Quickcheck.eval_random_ref", eval_random_ref)
    3.79 +              (Pred_Result.get, put_pred_result, "Predicate_Compile_Quickcheck.put_pred_result")
    3.80                  (fn proc => fn g => fn depth => fn nrandom => fn size => fn seed =>
    3.81                    g depth nrandom size seed |> (Predicate.map o map) proc)
    3.82                  thy4 qc_term []
     4.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Wed Sep 15 11:30:31 2010 +0200
     4.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Wed Sep 15 11:30:32 2010 +0200
     4.3 @@ -15,9 +15,10 @@
     4.4    val ensure_random_datatype: Datatype.config -> string list -> theory -> theory
     4.5    val compile_generator_expr:
     4.6      Proof.context -> term -> int -> term list option * (bool list * bool)
     4.7 -  val eval_ref: (unit -> int -> seed -> term list option * seed) option Unsynchronized.ref
     4.8 -  val eval_report_ref:
     4.9 -    (unit -> int -> seed -> (term list option * (bool list * bool)) * seed) option Unsynchronized.ref
    4.10 +  val put_counterexample: (unit -> int -> seed -> term list option * seed)
    4.11 +    -> Proof.context -> Proof.context
    4.12 +  val put_counterexample_report: (unit -> int -> seed -> (term list option * (bool list * bool)) * seed)
    4.13 +    -> Proof.context -> Proof.context
    4.14    val setup: theory -> theory
    4.15  end;
    4.16  
    4.17 @@ -304,13 +305,17 @@
    4.18  
    4.19  (** building and compiling generator expressions **)
    4.20  
    4.21 -val eval_ref :
    4.22 -    (unit -> int -> int * int -> term list option * (int * int)) option Unsynchronized.ref =
    4.23 -  Unsynchronized.ref NONE;
    4.24 +structure Counterexample = Proof_Data (
    4.25 +  type T = unit -> int -> int * int -> term list option * (int * int)
    4.26 +  fun init _ () = error "Counterexample"
    4.27 +);
    4.28 +val put_counterexample = Counterexample.put;
    4.29  
    4.30 -val eval_report_ref :
    4.31 -    (unit -> int -> seed -> (term list option * (bool list * bool)) * seed) option Unsynchronized.ref =
    4.32 -  Unsynchronized.ref NONE;
    4.33 +structure Counterexample_Report = Proof_Data (
    4.34 +  type T = unit -> int -> seed -> (term list option * (bool list * bool)) * seed
    4.35 +  fun init _ () = error "Counterexample_Report"
    4.36 +);
    4.37 +val put_counterexample_report = Counterexample_Report.put;
    4.38  
    4.39  val target = "Quickcheck";
    4.40  
    4.41 @@ -387,13 +392,15 @@
    4.42    in if Quickcheck.report ctxt then
    4.43      let
    4.44        val t' = mk_reporting_generator_expr thy t Ts;
    4.45 -      val compile = Code_Eval.eval (SOME target) ("Quickcheck_Generators.eval_report_ref", eval_report_ref)
    4.46 +      val compile = Code_Eval.eval (SOME target)
    4.47 +        (Counterexample_Report.get, put_counterexample_report, "Quickcheck_Generators.put_counterexample_report")
    4.48          (fn proc => fn g => fn s => g s #>> (apfst o Option.map o map) proc) thy t' [];
    4.49      in compile #> Random_Engine.run end
    4.50    else
    4.51      let
    4.52        val t' = mk_generator_expr thy t Ts;
    4.53 -      val compile = Code_Eval.eval (SOME target) ("Quickcheck_Generators.eval_ref", eval_ref)
    4.54 +      val compile = Code_Eval.eval (SOME target)
    4.55 +        (Counterexample.get, put_counterexample, "Quickcheck_Generators.put_counterexample")
    4.56          (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' [];
    4.57        val dummy_report = ([], false)
    4.58      in compile #> Random_Engine.run #> rpair dummy_report end
     5.1 --- a/src/Pure/ML/ml_context.ML	Wed Sep 15 11:30:31 2010 +0200
     5.2 +++ b/src/Pure/ML/ml_context.ML	Wed Sep 15 11:30:32 2010 +0200
     5.3 @@ -36,8 +36,9 @@
     5.4    val eval_text_in: Proof.context option -> bool -> Position.T -> Symbol_Pos.text -> unit
     5.5    val expression: Position.T -> string -> string -> ML_Lex.token Antiquote.antiquote list ->
     5.6      Context.generic -> Context.generic
     5.7 -  val evaluate: Proof.context -> bool ->
     5.8 -    string * (unit -> 'a) option Unsynchronized.ref -> string * string -> 'a
     5.9 +  val value: Proof.context ->
    5.10 +    (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string ->
    5.11 +    string * string -> 'a
    5.12  end
    5.13  
    5.14  structure ML_Context: ML_CONTEXT =
    5.15 @@ -213,17 +214,15 @@
    5.16      (ML_Lex.read Position.none ("Context.set_thread_data (SOME (let " ^ bind ^ " = ") @ ants @
    5.17        ML_Lex.read Position.none (" in " ^ body ^ " end (ML_Context.the_generic_context ())));")));
    5.18  
    5.19 -
    5.20 -(* FIXME not thread-safe -- reference can be accessed directly *)
    5.21 -fun evaluate ctxt verbose (ref_name, r) (prelude, txt) = NAMED_CRITICAL "ML" (fn () =>
    5.22 +fun value ctxt (get, put, put_ml) (prelude, value) =
    5.23    let
    5.24 -    val s = prelude ^ "val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ txt ^ "))"
    5.25 -    val ants = ML_Lex.read Position.none s;
    5.26 -    val _ = r := NONE;
    5.27 -    val _ =
    5.28 -      Context.setmp_thread_data (SOME (Context.Proof ctxt))
    5.29 -        (fn () => eval verbose Position.none ants) ();
    5.30 -  in (case ! r of NONE => error ("Bad evaluation for " ^ ref_name) | SOME e => e) end) ();
    5.31 +    val read = ML_Lex.read Position.none;
    5.32 +    val ants = read prelude @ read ("val _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
    5.33 +      ^ " (fn () => " ^ value ^ ")) (ML_Context.the_generic_context ())))");
    5.34 +    val ctxt' = ctxt
    5.35 +      |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
    5.36 +      |> Context.proof_map (exec (fn () => eval false Position.none ants));
    5.37 +  in get ctxt' () end;
    5.38  
    5.39  end;
    5.40  
     6.1 --- a/src/Tools/Code/code_eval.ML	Wed Sep 15 11:30:31 2010 +0200
     6.2 +++ b/src/Tools/Code/code_eval.ML	Wed Sep 15 11:30:32 2010 +0200
     6.3 @@ -7,7 +7,8 @@
     6.4  signature CODE_EVAL =
     6.5  sig
     6.6    val target: string
     6.7 -  val eval: string option -> string * (unit -> 'a) option Unsynchronized.ref
     6.8 +  val eval: string option
     6.9 +    -> (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string
    6.10      -> ((term -> term) -> 'a -> 'a) -> theory -> term -> string list -> 'a
    6.11    val setup: theory -> theory
    6.12  end;
    6.13 @@ -39,7 +40,7 @@
    6.14  
    6.15  (** evaluation **)
    6.16  
    6.17 -fun eval some_target reff postproc thy t args =
    6.18 +fun eval some_target cookie postproc thy t args =
    6.19    let
    6.20      val ctxt = ProofContext.init_global thy;
    6.21      fun evaluator naming program ((_, (_, ty)), t) deps =
    6.22 @@ -55,7 +56,7 @@
    6.23            (the_default target some_target) NONE "Code" [] naming program' [value_name];
    6.24          val value_code = space_implode " "
    6.25            (value_name' :: map (enclose "(" ")") args);
    6.26 -      in ML_Context.evaluate ctxt false reff (program_code, value_code) end;
    6.27 +      in ML_Context.value ctxt cookie (program_code, value_code) end;
    6.28    in Code_Thingol.dynamic_eval_value thy postproc evaluator t end;
    6.29  
    6.30  
     7.1 --- a/src/Tools/nbe.ML	Wed Sep 15 11:30:31 2010 +0200
     7.2 +++ b/src/Tools/nbe.ML	Wed Sep 15 11:30:32 2010 +0200
     7.3 @@ -19,7 +19,7 @@
     7.4                                               (*abstractions as closures*)
     7.5    val same: Univ -> Univ -> bool
     7.6  
     7.7 -  val univs_ref: (unit -> Univ list -> Univ list) option Unsynchronized.ref
     7.8 +  val put_result: (unit -> Univ list -> Univ list) -> Proof.context -> Proof.context
     7.9    val trace: bool Unsynchronized.ref
    7.10  
    7.11    val setup: theory -> theory
    7.12 @@ -228,10 +228,15 @@
    7.13  
    7.14  (* nbe specific syntax and sandbox communication *)
    7.15  
    7.16 -val univs_ref = Unsynchronized.ref (NONE : (unit -> Univ list -> Univ list) option);
    7.17 +structure Univs = Proof_Data(
    7.18 +  type T = unit -> Univ list -> Univ list
    7.19 +  fun init thy () = error "Univs"
    7.20 +);
    7.21 +val put_result = Univs.put;
    7.22  
    7.23  local
    7.24    val prefix =      "Nbe.";
    7.25 +  val name_put =    prefix ^ "put_result";
    7.26    val name_ref =    prefix ^ "univs_ref";
    7.27    val name_const =  prefix ^ "Const";
    7.28    val name_abss =   prefix ^ "abss";
    7.29 @@ -239,7 +244,7 @@
    7.30    val name_same =   prefix ^ "same";
    7.31  in
    7.32  
    7.33 -val univs_cookie = (name_ref, univs_ref);
    7.34 +val univs_cookie = (Univs.get, put_result, name_put);
    7.35  
    7.36  fun nbe_fun 0 "" = "nbe_value"
    7.37    | nbe_fun i c = "c_" ^ translate_string (fn "." => "_" | c => c) c ^ "_" ^ string_of_int i;
    7.38 @@ -389,7 +394,7 @@
    7.39          s
    7.40          |> traced (fn s => "\n--- code to be evaluated:\n" ^ s)
    7.41          |> pair ""
    7.42 -        |> ML_Context.evaluate ctxt (!trace) univs_cookie
    7.43 +        |> ML_Context.value ctxt univs_cookie
    7.44          |> (fn f => f deps_vals)
    7.45          |> (fn univs => cs ~~ univs)
    7.46        end;