--- a/NEWS Tue Sep 29 14:26:33 2009 +1000
+++ b/NEWS Tue Sep 29 18:14:08 2009 +0200
@@ -182,6 +182,19 @@
*** ML ***
+* Structure Synchronized (cf. src/Pure/Concurrent/synchronized.ML)
+provides a high-level programming interface to synchronized state
+variables with atomic update. This works via pure function
+application within a critical section -- its runtime should be as
+short as possible; beware of deadlocks if critical code is nested,
+either directly or indirectly via other synchronized variables!
+
+* Structure Unsynchronized (cf. src/Pure/ML-Systems/unsynchronized.ML)
+wraps raw ML references, explicitly indicating their non-thread-safe
+behaviour. The Isar toplevel keeps this structure open, to
+accommodate Proof General as well as quick and dirty interactive
+experiments with references.
+
* PARALLEL_CHOICE and PARALLEL_GOALS provide basic support for
parallel tactical reasoning.
--- a/src/CCL/ROOT.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/CCL/ROOT.ML Tue Sep 29 18:14:08 2009 +0200
@@ -3,12 +3,11 @@
Copyright 1993 University of Cambridge
Classical Computational Logic based on First-Order Logic.
+
+A computational logic for an untyped functional language with
+evaluation to weak head-normal form.
*)
-set eta_contract;
-
-(* CCL - a computational logic for an untyped functional language *)
-(* with evaluation to weak head-normal form *)
+Unsynchronized.set eta_contract;
use_thys ["Wfd", "Fix"];
-
--- a/src/FOLP/IFOLP.thy Tue Sep 29 14:26:33 2009 +1000
+++ b/src/FOLP/IFOLP.thy Tue Sep 29 18:14:08 2009 +0200
@@ -69,7 +69,7 @@
ML {*
(*show_proofs:=true displays the proof terms -- they are ENORMOUS*)
-val show_proofs = ref false;
+val show_proofs = Unsynchronized.ref false;
fun proof_tr [p,P] = Const (@{const_name Proof}, dummyT) $ P $ p;
--- a/src/FOLP/simp.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/FOLP/simp.ML Tue Sep 29 18:14:08 2009 +0200
@@ -49,7 +49,7 @@
(* temporarily disabled:
val extract_free_congs : unit -> thm list
*)
- val tracing : bool ref
+ val tracing : bool Unsynchronized.ref
end;
functor SimpFun (Simp_data: SIMP_DATA) : SIMP =
@@ -366,7 +366,7 @@
(** Tracing **)
-val tracing = ref false;
+val tracing = Unsynchronized.ref false;
(*Replace parameters by Free variables in P*)
fun variants_abs ([],P) = P
--- a/src/HOL/Code_Evaluation.thy Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Code_Evaluation.thy Tue Sep 29 18:14:08 2009 +0200
@@ -249,14 +249,14 @@
ML {*
signature EVAL =
sig
- val eval_ref: (unit -> term) option ref
+ val eval_ref: (unit -> term) option Unsynchronized.ref
val eval_term: theory -> term -> term
end;
structure Eval : EVAL =
struct
-val eval_ref = ref (NONE : (unit -> term) option);
+val eval_ref = Unsynchronized.ref (NONE : (unit -> term) option);
fun eval_term thy t =
Code_ML.eval NONE ("Eval.eval_ref", eval_ref) I thy (HOLogic.mk_term_of (fastype_of t) t) [];
--- a/src/HOL/Decision_Procs/cooper_tac.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Tue Sep 29 18:14:08 2009 +0200
@@ -4,7 +4,7 @@
signature COOPER_TAC =
sig
- val trace: bool ref
+ val trace: bool Unsynchronized.ref
val linz_tac: Proof.context -> bool -> int -> tactic
val setup: theory -> theory
end
@@ -12,7 +12,7 @@
structure Cooper_Tac: COOPER_TAC =
struct
-val trace = ref false;
+val trace = Unsynchronized.ref false;
fun trace_msg s = if !trace then tracing s else ();
val cooper_ss = @{simpset};
--- a/src/HOL/Decision_Procs/ferrack_tac.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML Tue Sep 29 18:14:08 2009 +0200
@@ -4,7 +4,7 @@
signature FERRACK_TAC =
sig
- val trace: bool ref
+ val trace: bool Unsynchronized.ref
val linr_tac: Proof.context -> bool -> int -> tactic
val setup: theory -> theory
end
@@ -12,7 +12,7 @@
structure Ferrack_Tac =
struct
-val trace = ref false;
+val trace = Unsynchronized.ref false;
fun trace_msg s = if !trace then tracing s else ();
val ferrack_ss = let val ths = [@{thm real_of_int_inject}, @{thm real_of_int_less_iff},
--- a/src/HOL/Decision_Procs/mir_tac.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Decision_Procs/mir_tac.ML Tue Sep 29 18:14:08 2009 +0200
@@ -4,7 +4,7 @@
signature MIR_TAC =
sig
- val trace: bool ref
+ val trace: bool Unsynchronized.ref
val mir_tac: Proof.context -> bool -> int -> tactic
val setup: theory -> theory
end
@@ -12,7 +12,7 @@
structure Mir_Tac =
struct
-val trace = ref false;
+val trace = Unsynchronized.ref false;
fun trace_msg s = if !trace then tracing s else ();
val mir_ss =
--- a/src/HOL/Fun.thy Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Fun.thy Tue Sep 29 18:14:08 2009 +0200
@@ -589,7 +589,7 @@
attach (test) {*
fun gen_fun_type aF aT bG bT i =
let
- val tab = ref [];
+ val tab = Unsynchronized.ref [];
fun mk_upd (x, (_, y)) t = Const ("Fun.fun_upd",
(aT --> bT) --> aT --> bT --> aT --> bT) $ t $ aF x $ y ()
in
--- a/src/HOL/HOL.thy Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/HOL.thy Tue Sep 29 18:14:08 2009 +0200
@@ -1970,7 +1970,7 @@
structure Eval_Method =
struct
-val eval_ref : (unit -> bool) option ref = ref NONE;
+val eval_ref : (unit -> bool) option Unsynchronized.ref = Unsynchronized.ref NONE;
end;
*}
--- a/src/HOL/Import/hol4rews.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Import/hol4rews.ML Tue Sep 29 18:14:08 2009 +0200
@@ -168,7 +168,7 @@
fun merge _ = Library.gen_union Thm.eq_thm
)
-val hol4_debug = ref false
+val hol4_debug = Unsynchronized.ref false
fun message s = if !hol4_debug then writeln s else ()
local
--- a/src/HOL/Import/import.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Import/import.ML Tue Sep 29 18:14:08 2009 +0200
@@ -4,7 +4,7 @@
signature IMPORT =
sig
- val debug : bool ref
+ val debug : bool Unsynchronized.ref
val import_tac : Proof.context -> string * string -> tactic
val setup : theory -> theory
end
@@ -21,7 +21,7 @@
structure Import :> IMPORT =
struct
-val debug = ref false
+val debug = Unsynchronized.ref false
fun message s = if !debug then writeln s else ()
fun import_tac ctxt (thyname, thmname) =
--- a/src/HOL/Import/import_syntax.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Import/import_syntax.ML Tue Sep 29 18:14:08 2009 +0200
@@ -157,8 +157,9 @@
val _ = TextIO.closeIn is
val orig_source = Source.of_string inp
val symb_source = Symbol.source {do_recover = false} orig_source
- val lexes = ref (Scan.make_lexicon (map Symbol.explode ["import_segment","ignore_thms","import","end",">","::","const_maps","const_moves","thm_maps","const_renames","type_maps","def_maps"]),
- Scan.empty_lexicon)
+ val lexes = Unsynchronized.ref
+ (Scan.make_lexicon (map Symbol.explode ["import_segment","ignore_thms","import","end",">","::","const_maps","const_moves","thm_maps","const_renames","type_maps","def_maps"]),
+ Scan.empty_lexicon)
val get_lexes = fn () => !lexes
val token_source = OuterLex.source {do_recover = NONE} get_lexes Position.start symb_source
val token_list = filter_out (OuterLex.is_kind OuterLex.Space) (Source.exhaust token_source)
--- a/src/HOL/Import/importrecorder.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Import/importrecorder.ML Tue Sep 29 18:14:08 2009 +0200
@@ -72,9 +72,9 @@
| AbortReplay of string*string
| Delta of deltastate list
-val history = ref ([]:history_entry list)
-val history_dir = ref (SOME "")
-val skip_imports = ref false
+val history = Unsynchronized.ref ([]:history_entry list)
+val history_dir = Unsynchronized.ref (SOME "")
+val skip_imports = Unsynchronized.ref false
fun set_skip_import b = skip_imports := b
fun get_skip_import () = !skip_imports
--- a/src/HOL/Import/lazy_seq.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Import/lazy_seq.ML Tue Sep 29 18:14:08 2009 +0200
@@ -299,7 +299,7 @@
fun cycle seqfn =
let
- val knot = ref (Seq (Lazy.value NONE))
+ val knot = Unsynchronized.ref (Seq (Lazy.value NONE))
in
knot := seqfn (fn () => !knot);
!knot
@@ -350,7 +350,7 @@
fun of_instream is =
let
- val buffer : char list ref = ref []
+ val buffer : char list Unsynchronized.ref = Unsynchronized.ref []
fun get_input () =
case !buffer of
(c::cs) => (buffer:=cs;
--- a/src/HOL/Import/proof_kernel.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Import/proof_kernel.ML Tue Sep 29 18:14:08 2009 +0200
@@ -53,7 +53,7 @@
val get_proof_dir: string -> theory -> string option
val disambiguate_frees : Thm.thm -> Thm.thm
- val debug : bool ref
+ val debug : bool Unsynchronized.ref
val disk_info_of : proof -> (string * string) option
val set_disk_info_of : proof -> string -> string -> unit
val mk_proof : proof_content -> proof
@@ -132,7 +132,7 @@
fun add_dump s thy = (ImportRecorder.add_dump s; replay_add_dump s thy)
datatype proof_info
- = Info of {disk_info: (string * string) option ref}
+ = Info of {disk_info: (string * string) option Unsynchronized.ref}
datatype proof = Proof of proof_info * proof_content
and proof_content
@@ -258,7 +258,7 @@
end
fun disk_info_of (Proof(Info{disk_info,...},_)) = !disk_info
-fun mk_proof p = Proof(Info{disk_info = ref NONE},p)
+fun mk_proof p = Proof(Info{disk_info = Unsynchronized.ref NONE},p)
fun content_of (Proof(_,p)) = p
fun set_disk_info_of (Proof(Info{disk_info,...},_)) thyname thmname =
@@ -463,8 +463,8 @@
s |> no_quest |> beg_prime
end
-val protected_varnames = ref (Symtab.empty:string Symtab.table)
-val invented_isavar = ref 0
+val protected_varnames = Unsynchronized.ref (Symtab.empty:string Symtab.table)
+val invented_isavar = Unsynchronized.ref 0
fun innocent_varname s = Syntax.is_identifier s andalso not (String.isPrefix "u_" s)
@@ -482,7 +482,7 @@
SOME t => t
| NONE =>
let
- val _ = inc invented_isavar
+ val _ = Unsynchronized.inc invented_isavar
val t = "u_" ^ string_of_int (!invented_isavar)
val _ = ImportRecorder.protect_varname s t
val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames)
@@ -497,7 +497,7 @@
SOME t' => raise REPLAY_PROTECT_VARNAME (s, t, t')
| NONE =>
let
- val _ = inc invented_isavar
+ val _ = Unsynchronized.inc invented_isavar
val t = "u_" ^ string_of_int (!invented_isavar)
val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames)
in
@@ -1188,7 +1188,7 @@
end
end
-val debug = ref false
+val debug = Unsynchronized.ref false
fun if_debug f x = if !debug then f x else ()
val message = if_debug writeln
--- a/src/HOL/Import/shuffler.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Import/shuffler.ML Tue Sep 29 18:14:08 2009 +0200
@@ -7,7 +7,7 @@
signature Shuffler =
sig
- val debug : bool ref
+ val debug : bool Unsynchronized.ref
val norm_term : theory -> term -> thm
val make_equal : theory -> term -> term -> thm option
@@ -30,7 +30,7 @@
structure Shuffler :> Shuffler =
struct
-val debug = ref false
+val debug = Unsynchronized.ref false
fun if_debug f x = if !debug then f x else ()
val message = if_debug writeln
--- a/src/HOL/Library/Eval_Witness.thy Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Library/Eval_Witness.thy Tue Sep 29 18:14:08 2009 +0200
@@ -48,7 +48,7 @@
structure Eval_Witness_Method =
struct
-val eval_ref : (unit -> bool) option ref = ref NONE;
+val eval_ref : (unit -> bool) option Unsynchronized.ref = Unsynchronized.ref NONE;
end;
*}
--- a/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML Tue Sep 29 18:14:08 2009 +0200
@@ -10,7 +10,7 @@
datatype prover_result = Success | Failure | Error
val setup: theory -> theory
- val destdir: string ref
+ val destdir: string Unsynchronized.ref
val get_prover_name: unit -> string
val set_prover_name: string -> unit
end
@@ -30,7 +30,7 @@
(*** calling provers ***)
-val destdir = ref ""
+val destdir = Unsynchronized.ref ""
fun filename dir name =
let
@@ -113,7 +113,7 @@
(* default prover *)
-val prover_name = ref "remote_csdp"
+val prover_name = Unsynchronized.ref "remote_csdp"
fun get_prover_name () = CRITICAL (fn () => ! prover_name);
fun set_prover_name str = CRITICAL (fn () => prover_name := str);
--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Tue Sep 29 18:14:08 2009 +0200
@@ -15,7 +15,7 @@
val sos_tac : (RealArith.pss_tree -> unit) ->
proof_method -> Proof.context -> int -> tactic
- val debugging : bool ref;
+ val debugging : bool Unsynchronized.ref;
exception Failure of string;
end
@@ -58,7 +58,7 @@
val pow2 = rat_pow rat_2;
val pow10 = rat_pow rat_10;
-val debugging = ref false;
+val debugging = Unsynchronized.ref false;
exception Sanity;
--- a/src/HOL/Library/positivstellensatz.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Library/positivstellensatz.ML Tue Sep 29 18:14:08 2009 +0200
@@ -190,20 +190,20 @@
thm list * thm list * thm list -> thm * pss_tree
type cert_conv = cterm -> thm * pss_tree
-val my_eqs = ref ([] : thm list);
-val my_les = ref ([] : thm list);
-val my_lts = ref ([] : thm list);
-val my_proof = ref (Axiom_eq 0);
-val my_context = ref @{context};
+val my_eqs = Unsynchronized.ref ([] : thm list);
+val my_les = Unsynchronized.ref ([] : thm list);
+val my_lts = Unsynchronized.ref ([] : thm list);
+val my_proof = Unsynchronized.ref (Axiom_eq 0);
+val my_context = Unsynchronized.ref @{context};
-val my_mk_numeric = ref ((K @{cterm True}) :Rat.rat -> cterm);
-val my_numeric_eq_conv = ref no_conv;
-val my_numeric_ge_conv = ref no_conv;
-val my_numeric_gt_conv = ref no_conv;
-val my_poly_conv = ref no_conv;
-val my_poly_neg_conv = ref no_conv;
-val my_poly_add_conv = ref no_conv;
-val my_poly_mul_conv = ref no_conv;
+val my_mk_numeric = Unsynchronized.ref ((K @{cterm True}) :Rat.rat -> cterm);
+val my_numeric_eq_conv = Unsynchronized.ref no_conv;
+val my_numeric_ge_conv = Unsynchronized.ref no_conv;
+val my_numeric_gt_conv = Unsynchronized.ref no_conv;
+val my_poly_conv = Unsynchronized.ref no_conv;
+val my_poly_neg_conv = Unsynchronized.ref no_conv;
+val my_poly_add_conv = Unsynchronized.ref no_conv;
+val my_poly_mul_conv = Unsynchronized.ref no_conv;
(* Some useful derived rules *)
--- a/src/HOL/Matrix/cplex/Cplex_tools.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Matrix/cplex/Cplex_tools.ML Tue Sep 29 18:14:08 2009 +0200
@@ -62,7 +62,7 @@
datatype cplexSolver = SOLVER_DEFAULT | SOLVER_CPLEX | SOLVER_GLPK
-val cplexsolver = ref SOLVER_DEFAULT;
+val cplexsolver = Unsynchronized.ref SOLVER_DEFAULT;
fun get_solver () = !cplexsolver;
fun set_solver s = (cplexsolver := s);
@@ -305,8 +305,8 @@
fun load_cplexFile name =
let
val f = TextIO.openIn name
- val ignore_NL = ref true
- val rest = ref []
+ val ignore_NL = Unsynchronized.ref true
+ val rest = Unsynchronized.ref []
fun is_symbol s c = (fst c) = TOKEN_SYMBOL andalso (to_upper (snd c)) = s
@@ -612,7 +612,7 @@
fun basic_write s = TextIO.output(f, s)
- val linebuf = ref ""
+ val linebuf = Unsynchronized.ref ""
fun buf_flushline s =
(basic_write (!linebuf);
basic_write "\n";
@@ -860,7 +860,7 @@
val f = TextIO.openIn name
- val rest = ref []
+ val rest = Unsynchronized.ref []
fun readToken_helper () =
if length (!rest) > 0 then
@@ -995,7 +995,7 @@
val f = TextIO.openIn name
- val rest = ref []
+ val rest = Unsynchronized.ref []
fun readToken_helper () =
if length (!rest) > 0 then
--- a/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML Tue Sep 29 18:14:08 2009 +0200
@@ -136,7 +136,7 @@
fun cplexProg c A b =
let
- val ytable = ref Inttab.empty
+ val ytable = Unsynchronized.ref Inttab.empty
fun indexof s =
if String.size s = 0 then raise (No_name s)
else case Int.fromString (String.extract(s, 1, NONE)) of
@@ -145,7 +145,7 @@
fun nameof i =
let
val s = "x"^(Int.toString i)
- val _ = change ytable (Inttab.update (i, s))
+ val _ = Unsynchronized.change ytable (Inttab.update (i, s))
in
s
end
@@ -242,7 +242,7 @@
fun cut_vector size v =
let
- val count = ref 0;
+ val count = Unsynchronized.ref 0;
fun app (i, s) = if (!count < size) then
(count := !count +1 ; Inttab.update (i, s))
else I
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Sep 29 18:14:08 2009 +0200
@@ -202,7 +202,8 @@
fun log_metis_data log tag sh_calls sh_success metis_calls metis_success metis_proofs metis_time
metis_timeout metis_lemmas metis_posns =
(log ("Total number of " ^ tag ^ "metis calls: " ^ str metis_calls);
- log ("Number of successful " ^ tag ^ "metis calls: " ^ str metis_success ^ " (proof: " ^ str metis_proofs ^ ")");
+ log ("Number of successful " ^ tag ^ "metis calls: " ^ str metis_success ^
+ " (proof: " ^ str metis_proofs ^ ")");
log ("Number of " ^ tag ^ "metis timeouts: " ^ str metis_timeout);
log ("Success rate: " ^ percentage metis_success sh_calls ^ "%");
log ("Number of successful " ^ tag ^ "metis lemmas: " ^ str metis_lemmas);
@@ -252,15 +253,15 @@
(* Warning: we implicitly assume single-threaded execution here! *)
-val data = ref ([] : (int * data) list)
+val data = Unsynchronized.ref ([] : (int * data) list)
-fun init id thy = (change data (cons (id, empty_data)); thy)
+fun init id thy = (Unsynchronized.change data (cons (id, empty_data)); thy)
fun done id ({log, ...}: Mirabelle.done_args) =
AList.lookup (op =) (!data) id
|> Option.map (log_data id log)
|> K ()
-fun change_data id f = (change data (AList.map_entry (op =) id f); ())
+fun change_data id f = (Unsynchronized.change data (AList.map_entry (op =) id f); ())
fun get_atp thy args =
@@ -419,7 +420,7 @@
inc_metis_timeout, inc_metis_lemmas, inc_metis_posns)
val metis0_fns = (inc_metis_calls0, inc_metis_success0, inc_metis_proofs0, inc_metis_time0,
inc_metis_timeout0, inc_metis_lemmas0, inc_metis_posns0)
- val named_thms = ref (NONE : (string * thm list) list option)
+ val named_thms = Unsynchronized.ref (NONE : (string * thm list) list option)
val minimize = AList.defined (op =) args minimizeK
in
Mirabelle.catch sh_tag (run_sledgehammer args named_thms) id st;
--- a/src/HOL/Modelcheck/EindhovenSyn.thy Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Modelcheck/EindhovenSyn.thy Tue Sep 29 18:14:08 2009 +0200
@@ -26,7 +26,7 @@
"Nu " :: "[idts, 'a pred] => 'a pred" ("(3[nu _./ _])" 1000)
ML {*
- val trace_eindhoven = ref false;
+ val trace_eindhoven = Unsynchronized.ref false;
*}
oracle mc_eindhoven_oracle =
--- a/src/HOL/Modelcheck/mucke_oracle.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Modelcheck/mucke_oracle.ML Tue Sep 29 18:14:08 2009 +0200
@@ -1,5 +1,5 @@
-val trace_mc = ref false;
+val trace_mc = Unsynchronized.ref false;
(* transform_case post-processes output strings of the syntax "Mucke" *)
--- a/src/HOL/Nominal/nominal_thmdecls.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Nominal/nominal_thmdecls.ML Tue Sep 29 18:14:08 2009 +0200
@@ -18,7 +18,7 @@
val setup: theory -> theory
val get_eqvt_thms: Proof.context -> thm list
- val NOMINAL_EQVT_DEBUG : bool ref
+ val NOMINAL_EQVT_DEBUG : bool Unsynchronized.ref
end;
structure NominalThmDecls: NOMINAL_THMDECLS =
@@ -43,7 +43,7 @@
(* equality-lemma can be derived. *)
exception EQVT_FORM of string
-val NOMINAL_EQVT_DEBUG = ref false
+val NOMINAL_EQVT_DEBUG = Unsynchronized.ref false
fun tactic (msg, tac) =
if !NOMINAL_EQVT_DEBUG
--- a/src/HOL/Prolog/prolog.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Prolog/prolog.ML Tue Sep 29 18:14:08 2009 +0200
@@ -2,7 +2,7 @@
Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
*)
-set Proof.show_main_goal;
+Unsynchronized.set Proof.show_main_goal;
structure Prolog =
struct
--- a/src/HOL/Random.thy Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Random.thy Tue Sep 29 18:14:08 2009 +0200
@@ -154,7 +154,7 @@
local
-val seed = ref
+val seed = Unsynchronized.ref
(let
val now = Time.toMilliseconds (Time.now ());
val (q, s1) = IntInf.divMod (now, 2147483562);
--- a/src/HOL/SMT/Tools/smt_normalize.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/SMT/Tools/smt_normalize.ML Tue Sep 29 18:14:08 2009 +0200
@@ -304,11 +304,11 @@
fun lift_lambdas ctxt thms =
let
val declare_frees = fold (Thm.fold_terms Term.declare_term_frees)
- val names = ref (declare_frees thms (Name.make_context []))
- val fresh_name = change_result names o yield_singleton Name.variants
+ val names = Unsynchronized.ref (declare_frees thms (Name.make_context []))
+ val fresh_name = Unsynchronized.change_result names o yield_singleton Name.variants
- val defs = ref (Termtab.empty : (int * thm) Termtab.table)
- fun add_def t thm = change defs (Termtab.update (t, (serial (), thm)))
+ val defs = Unsynchronized.ref (Termtab.empty : (int * thm) Termtab.table)
+ fun add_def t thm = Unsynchronized.change defs (Termtab.update (t, (serial (), thm)))
fun make_def cvs eq = Thm.symmetric (fold norm_meta_def cvs eq)
fun def_conv cvs ctxt ct =
let
--- a/src/HOL/Statespace/DistinctTreeProver.thy Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Statespace/DistinctTreeProver.thy Tue Sep 29 18:14:08 2009 +0200
@@ -664,7 +664,7 @@
HOLogic.Trueprop$
(Const ("DistinctTreeProver.all_distinct",DistinctTreeProver.treeT (Type ("nat",[])) --> HOLogic.boolT)$t')
-val da = ref refl;
+val da = Unsynchronized.ref refl;
*}
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Sep 29 18:14:08 2009 +0200
@@ -41,10 +41,10 @@
local
-val atps = ref "e remote_vampire";
-val max_atps = ref 5; (* ~1 means infinite number of atps *)
-val timeout = ref 60;
-val full_types = ref false;
+val atps = Unsynchronized.ref "e remote_vampire";
+val max_atps = Unsynchronized.ref 5; (* ~1 means infinite number of atps *)
+val timeout = Unsynchronized.ref 60;
+val full_types = Unsynchronized.ref false;
in
--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Tue Sep 29 18:14:08 2009 +0200
@@ -69,7 +69,7 @@
forall e in v. ~p(v \ e)
*)
fun minimal p s =
- let val c = ref 0
+ let val c = Unsynchronized.ref 0
fun pc xs = (c := !c + 1; p xs)
in
(case min pc [] s of
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Tue Sep 29 18:14:08 2009 +0200
@@ -6,8 +6,8 @@
signature ATP_WRAPPER =
sig
- val destdir: string ref
- val problem_name: string ref
+ val destdir: string Unsynchronized.ref
+ val problem_name: string Unsynchronized.ref
val tptp_prover_opts_full: int -> bool -> bool -> Path.T * string -> AtpManager.prover
val tptp_prover_opts: int -> bool -> Path.T * string -> AtpManager.prover
val tptp_prover: Path.T * string -> AtpManager.prover
@@ -35,8 +35,8 @@
(* global hooks for writing problemfiles *)
-val destdir = ref ""; (*Empty means write files to /tmp*)
-val problem_name = ref "prob";
+val destdir = Unsynchronized.ref ""; (*Empty means write files to /tmp*)
+val problem_name = Unsynchronized.ref "prob";
(* basic template *)
--- a/src/HOL/Tools/Function/fundef_common.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Tools/Function/fundef_common.ML Tue Sep 29 18:14:08 2009 +0200
@@ -11,7 +11,7 @@
local open FundefLib in
(* Profiling *)
-val profile = ref false;
+val profile = Unsynchronized.ref false;
fun PROFILE msg = if !profile then timeap_msg msg else I
--- a/src/HOL/Tools/Function/scnp_solve.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Tools/Function/scnp_solve.ML Tue Sep 29 18:14:08 2009 +0200
@@ -23,7 +23,7 @@
val generate_certificate : bool -> label list -> graph_problem -> certificate option
- val solver : string ref
+ val solver : string Unsynchronized.ref
end
structure ScnpSolve : SCNP_SOLVE =
@@ -71,7 +71,7 @@
fun exactly_one n f = iexists n (the_one f n)
(* SAT solving *)
-val solver = ref "auto";
+val solver = Unsynchronized.ref "auto";
fun sat_solver x =
FundefCommon.PROFILE "sat_solving..." (SatSolver.invoke_solver (!solver)) x
--- a/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML Tue Sep 29 18:14:08 2009 +0200
@@ -16,7 +16,7 @@
(* Oracle for preprocessing *)
-val (oracle : (string * (cterm -> thm)) option ref) = ref NONE;
+val (oracle : (string * (cterm -> thm)) option Unsynchronized.ref) = Unsynchronized.ref NONE;
fun the_oracle () =
case !oracle of
--- a/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML Tue Sep 29 18:14:08 2009 +0200
@@ -6,13 +6,15 @@
signature PRED_COMPILE_QUICKCHECK =
sig
val quickcheck : Proof.context -> term -> int -> term list option
- val test_ref : ((unit -> int -> int * int -> term list Predicate.pred * (int * int)) option) ref
+ val test_ref :
+ ((unit -> int -> int * int -> term list Predicate.pred * (int * int)) option) Unsynchronized.ref
end;
structure Pred_Compile_Quickcheck : PRED_COMPILE_QUICKCHECK =
struct
-val test_ref = ref (NONE : (unit -> int -> int * int -> term list Predicate.pred * (int * int)) option)
+val test_ref =
+ Unsynchronized.ref (NONE : (unit -> int -> int * int -> term list Predicate.pred * (int * int)) option)
val target = "Quickcheck"
fun dest_compfuns (Predicate_Compile_Core.CompilationFuns funs) = funs
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Sep 29 18:14:08 2009 +0200
@@ -35,10 +35,10 @@
val set_nparams : string -> int -> theory -> theory
val print_stored_rules: theory -> unit
val print_all_modes: theory -> unit
- val do_proofs: bool ref
+ val do_proofs: bool Unsynchronized.ref
val mk_casesrule : Proof.context -> int -> thm list -> term
val analyze_compr: theory -> term -> term
- val eval_ref: (unit -> term Predicate.pred) option ref
+ val eval_ref: (unit -> term Predicate.pred) option Unsynchronized.ref
val add_equations : string list -> theory -> theory
val code_pred_intros_attrib : attribute
(* used by Quickcheck_Generator *)
@@ -123,7 +123,7 @@
fun print_tac s = Seq.single; (*Tactical.print_tac s;*) (* (if ! Toplevel.debug then Tactical.print_tac s else Seq.single); *)
fun debug_tac msg = Seq.single; (* (fn st => (Output.tracing msg; Seq.single st)); *)
-val do_proofs = ref true;
+val do_proofs = Unsynchronized.ref true;
(* reference to preprocessing of InductiveSet package *)
@@ -2334,7 +2334,7 @@
(* transformation for code generation *)
-val eval_ref = ref (NONE : (unit -> term Predicate.pred) option);
+val eval_ref = Unsynchronized.ref (NONE : (unit -> term Predicate.pred) option);
(*FIXME turn this into an LCF-guarded preprocessor for comprehensions*)
fun analyze_compr thy t_compr =
--- a/src/HOL/Tools/TFL/rules.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Tools/TFL/rules.ML Tue Sep 29 18:14:08 2009 +0200
@@ -47,10 +47,10 @@
val rbeta: thm -> thm
(* For debugging my isabelle solver in the conditional rewriter *)
- val term_ref: term list ref
- val thm_ref: thm list ref
- val ss_ref: simpset list ref
- val tracing: bool ref
+ val term_ref: term list Unsynchronized.ref
+ val thm_ref: thm list Unsynchronized.ref
+ val ss_ref: simpset list Unsynchronized.ref
+ val tracing: bool Unsynchronized.ref
val CONTEXT_REWRITE_RULE: term * term list * thm * thm list
-> thm -> thm * term list
val RIGHT_ASSOC: thm -> thm
@@ -544,10 +544,10 @@
(*---------------------------------------------------------------------------
* Trace information for the rewriter
*---------------------------------------------------------------------------*)
-val term_ref = ref [] : term list ref
-val ss_ref = ref [] : simpset list ref;
-val thm_ref = ref [] : thm list ref;
-val tracing = ref false;
+val term_ref = Unsynchronized.ref [] : term list Unsynchronized.ref
+val ss_ref = Unsynchronized.ref [] : simpset list Unsynchronized.ref;
+val thm_ref = Unsynchronized.ref [] : thm list Unsynchronized.ref;
+val tracing = Unsynchronized.ref false;
fun say s = if !tracing then writeln s else ();
@@ -666,7 +666,7 @@
let val globals = func::G
val ss0 = Simplifier.theory_context (Thm.theory_of_thm th) empty_ss
val pbeta_reduce = simpl_conv ss0 [split_conv RS eq_reflection];
- val tc_list = ref[]: term list ref
+ val tc_list = Unsynchronized.ref []: term list Unsynchronized.ref
val dummy = term_ref := []
val dummy = thm_ref := []
val dummy = ss_ref := []
--- a/src/HOL/Tools/TFL/tfl.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Tools/TFL/tfl.ML Tue Sep 29 18:14:08 2009 +0200
@@ -6,7 +6,7 @@
signature PRIM =
sig
- val trace: bool ref
+ val trace: bool Unsynchronized.ref
val trace_thms: string -> thm list -> unit
val trace_cterm: string -> cterm -> unit
type pattern
@@ -40,7 +40,7 @@
structure Prim: PRIM =
struct
-val trace = ref false;
+val trace = Unsynchronized.ref false;
structure R = Rules;
structure S = USyntax;
@@ -75,8 +75,8 @@
* function contains embedded refs!
*---------------------------------------------------------------------------*)
fun gvvariant names =
- let val slist = ref names
- val vname = ref "u"
+ let val slist = Unsynchronized.ref names
+ val vname = Unsynchronized.ref "u"
fun new() =
if !vname mem_string (!slist)
then (vname := Symbol.bump_string (!vname); new())
--- a/src/HOL/Tools/cnf_funcs.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Tools/cnf_funcs.ML Tue Sep 29 18:14:08 2009 +0200
@@ -399,12 +399,10 @@
fun make_cnfx_thm thy t =
let
- val var_id = ref 0 (* properly initialized below *)
- (* unit -> Term.term *)
+ val var_id = Unsynchronized.ref 0 (* properly initialized below *)
fun new_free () =
- Free ("cnfx_" ^ string_of_int (inc var_id), HOLogic.boolT)
- (* Term.term -> Thm.thm *)
- fun make_cnfx_thm_from_nnf (Const ("op &", _) $ x $ y) =
+ Free ("cnfx_" ^ string_of_int (Unsynchronized.inc var_id), HOLogic.boolT)
+ fun make_cnfx_thm_from_nnf (Const ("op &", _) $ x $ y) : thm =
let
val thm1 = make_cnfx_thm_from_nnf x
val thm2 = make_cnfx_thm_from_nnf y
--- a/src/HOL/Tools/lin_arith.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Tools/lin_arith.ML Tue Sep 29 18:14:08 2009 +0200
@@ -22,8 +22,8 @@
val global_setup: theory -> theory
val split_limit: int Config.T
val neq_limit: int Config.T
- val warning_count: int ref
- val trace: bool ref
+ val warning_count: int Unsynchronized.ref
+ val trace: bool Unsynchronized.ref
end;
structure Lin_Arith: LIN_ARITH =
--- a/src/HOL/Tools/meson.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Tools/meson.ML Tue Sep 29 18:14:08 2009 +0200
@@ -319,7 +319,7 @@
Strips universal quantifiers and breaks up conjunctions.
Eliminates existential quantifiers using skoths: Skolemization theorems.*)
fun cnf skoths ctxt (th,ths) =
- let val ctxtr = ref ctxt
+ let val ctxtr = Unsynchronized.ref ctxt
fun cnf_aux (th,ths) =
if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
else if not (has_conns ["All","Ex","op &"] (prop_of th))
--- a/src/HOL/Tools/polyhash.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Tools/polyhash.ML Tue Sep 29 18:14:08 2009 +0200
@@ -108,8 +108,8 @@
HT of {hashVal : 'key -> int,
sameKey : 'key * 'key -> bool,
not_found : exn,
- table : ('key, 'data) bucket_t Array.array ref,
- n_items : int ref}
+ table : ('key, 'data) bucket_t Array.array Unsynchronized.ref,
+ n_items : int Unsynchronized.ref}
local
(*
@@ -134,8 +134,8 @@
hashVal=hashVal,
sameKey=sameKey,
not_found = notFound,
- table = ref (Array.array(roundUp sizeHint, NIL)),
- n_items = ref 0
+ table = Unsynchronized.ref (Array.array(roundUp sizeHint, NIL)),
+ n_items = Unsynchronized.ref 0
};
(* conditionally grow a table *)
@@ -174,7 +174,7 @@
val indx = index (hash, sz)
fun look NIL = (
Array.update(arr, indx, B(hash, key, item, Array.sub(arr, indx)));
- inc n_items;
+ Unsynchronized.inc n_items;
growTable tbl;
NIL)
| look (B(h, k, v, r)) = if ((hash = h) andalso sameKey(key, k))
@@ -200,7 +200,7 @@
fun look NIL =
(Array.update(arr, indx, B(hash, key, item,
Array.sub(arr, indx)));
- inc n_items;
+ Unsynchronized.inc n_items;
growTable tbl;
NONE)
| look (B(h, k, v, r)) =
@@ -261,7 +261,7 @@
fun numItems (HT{n_items, ...}) = !n_items
(* return a list of the items in the table *)
- fun listItems (HT{table = ref arr, n_items, ...}) = let
+ fun listItems (HT{table = Unsynchronized.ref arr, n_items, ...}) = let
fun f (_, l, 0) = l
| f (~1, l, _) = l
| f (i, l, n) = let
@@ -306,8 +306,8 @@
mapTbl 0;
HT{hashVal=hashVal,
sameKey=sameKey,
- table = ref newArr,
- n_items = ref(!n_items),
+ table = Unsynchronized.ref newArr,
+ n_items = Unsynchronized.ref(!n_items),
not_found = not_found}
end (* transform *);
@@ -348,8 +348,8 @@
mapTbl 0;
HT{hashVal=hashVal,
sameKey=sameKey,
- table = ref newArr,
- n_items = ref(!n_items),
+ table = Unsynchronized.ref newArr,
+ n_items = Unsynchronized.ref(!n_items),
not_found = not_found}
end (* transform *);
@@ -365,15 +365,15 @@
(mapTbl 0) handle _ => (); (* FIXME avoid handle _ *)
HT{hashVal=hashVal,
sameKey=sameKey,
- table = ref newArr,
- n_items = ref(!n_items),
+ table = Unsynchronized.ref newArr,
+ n_items = Unsynchronized.ref(!n_items),
not_found = not_found}
end (* copy *);
(* returns a list of the sizes of the various buckets. This is to
* allow users to gauge the quality of their hashing function.
*)
- fun bucketSizes (HT{table = ref arr, ...}) = let
+ fun bucketSizes (HT{table = Unsynchronized.ref arr, ...}) = let
fun len (NIL, n) = n
| len (B(_, _, _, r), n) = len(r, n+1)
fun f (~1, l) = l
--- a/src/HOL/Tools/prop_logic.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Tools/prop_logic.ML Tue Sep 29 18:14:08 2009 +0200
@@ -292,7 +292,7 @@
val fm' = nnf fm
(* 'new' specifies the next index that is available to introduce an auxiliary variable *)
(* int ref *)
- val new = ref (maxidx fm' + 1)
+ val new = Unsynchronized.ref (maxidx fm' + 1)
(* unit -> int *)
fun new_idx () = let val idx = !new in new := idx+1; idx end
(* replaces 'And' by an auxiliary variable (and its definition) *)
@@ -381,15 +381,15 @@
(* Term.term -> int Termtab.table -> prop_formula * int Termtab.table *)
fun prop_formula_of_term t table =
let
- val next_idx_is_valid = ref false
- val next_idx = ref 0
+ val next_idx_is_valid = Unsynchronized.ref false
+ val next_idx = Unsynchronized.ref 0
fun get_next_idx () =
if !next_idx_is_valid then
- inc next_idx
+ Unsynchronized.inc next_idx
else (
next_idx := Termtab.fold (curry Int.max o snd) table 0;
next_idx_is_valid := true;
- inc next_idx
+ Unsynchronized.inc next_idx
)
fun aux (Const ("True", _)) table =
(True, table)
--- a/src/HOL/Tools/quickcheck_generators.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Tools/quickcheck_generators.ML Tue Sep 29 18:14:08 2009 +0200
@@ -16,7 +16,7 @@
-> term list * (term * term) list
val ensure_random_datatype: Datatype.config -> string list -> theory -> theory
val compile_generator_expr: theory -> term -> int -> term list option
- val eval_ref: (unit -> int -> seed -> term list option * seed) option ref
+ val eval_ref: (unit -> int -> seed -> term list option * seed) option Unsynchronized.ref
val setup: theory -> theory
end;
@@ -43,7 +43,7 @@
val ((y, t2), seed') = random seed;
val (seed'', seed''') = random_split seed';
- val state = ref (seed'', [], fn () => Abs ("x", T1, t2 ()));
+ val state = Unsynchronized.ref (seed'', [], fn () => Abs ("x", T1, t2 ()));
fun random_fun' x =
let
val (seed, fun_map, f_t) = ! state;
@@ -345,7 +345,9 @@
(** building and compiling generator expressions **)
-val eval_ref : (unit -> int -> int * int -> term list option * (int * int)) option ref = ref NONE;
+val eval_ref :
+ (unit -> int -> int * int -> term list option * (int * int)) option Unsynchronized.ref =
+ Unsynchronized.ref NONE;
val target = "Quickcheck";
--- a/src/HOL/Tools/record.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Tools/record.ML Tue Sep 29 18:14:08 2009 +0200
@@ -16,15 +16,15 @@
val record_split_simp_tac: thm list -> (term -> int) -> int -> tactic
val record_split_name: string
val record_split_wrapper: string * wrapper
- val print_record_type_abbr: bool ref
- val print_record_type_as_fields: bool ref
+ val print_record_type_abbr: bool Unsynchronized.ref
+ val print_record_type_as_fields: bool Unsynchronized.ref
end;
signature RECORD =
sig
include BASIC_RECORD
- val timing: bool ref
- val record_quick_and_dirty_sensitive: bool ref
+ val timing: bool Unsynchronized.ref
+ val record_quick_and_dirty_sensitive: bool Unsynchronized.ref
val updateN: string
val updN: string
val ext_typeN: string
@@ -287,7 +287,7 @@
(* timing *)
-val timing = ref false;
+val timing = Unsynchronized.ref false;
fun timeit_msg s x = if !timing then (warning s; timeit x) else x ();
fun timing_msg s = if !timing then warning s else ();
@@ -879,8 +879,8 @@
(* print translations *)
-val print_record_type_abbr = ref true;
-val print_record_type_as_fields = ref true;
+val print_record_type_abbr = Unsynchronized.ref true;
+val print_record_type_as_fields = Unsynchronized.ref true;
fun gen_field_upds_tr' mark sfx (tm as Const (name_field, _) $ k $ u) =
let val t = (case k of (Abs (_,_,(Abs (_,_,t)$Bound 0)))
@@ -1072,7 +1072,7 @@
(** record simprocs **)
-val record_quick_and_dirty_sensitive = ref false;
+val record_quick_and_dirty_sensitive = Unsynchronized.ref false;
fun quick_and_dirty_prove stndrd thy asms prop tac =
--- a/src/HOL/Tools/res_axioms.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Tools/res_axioms.ML Tue Sep 29 18:14:08 2009 +0200
@@ -16,7 +16,8 @@
val combinators: thm -> thm
val neg_conjecture_clauses: Proof.context -> thm -> int -> thm list * (string * typ) list
val atpset_rules_of: Proof.context -> (string * thm) list
- val suppress_endtheory: bool ref (*for emergency use where endtheory causes problems*)
+ val suppress_endtheory: bool Unsynchronized.ref
+ (*for emergency use where endtheory causes problems*)
val setup: theory -> theory
end;
@@ -66,11 +67,11 @@
prefix for the Skolem constant.*)
fun declare_skofuns s th =
let
- val nref = ref 0
+ val nref = Unsynchronized.ref 0
fun dec_sko (Const ("Ex",_) $ (xtp as Abs (_, T, p))) (axs, thy) =
(*Existential: declare a Skolem function, then insert into body and continue*)
let
- val cname = "sko_" ^ s ^ "_" ^ Int.toString (inc nref)
+ val cname = "sko_" ^ s ^ "_" ^ Int.toString (Unsynchronized.inc nref)
val args0 = OldTerm.term_frees xtp (*get the formal parameter list*)
val Ts = map type_of args0
val extraTs = rhs_extra_types (Ts ---> T) xtp
@@ -97,14 +98,14 @@
(*Traverse a theorem, accumulating Skolem function definitions.*)
fun assume_skofuns s th =
- let val sko_count = ref 0
+ let val sko_count = Unsynchronized.ref 0
fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) defs =
(*Existential: declare a Skolem function, then insert into body and continue*)
let val skos = map (#1 o Logic.dest_equals) defs (*existing sko fns*)
val args = OldTerm.term_frees xtp \\ skos (*the formal parameters*)
val Ts = map type_of args
val cT = Ts ---> T
- val id = "sko_" ^ s ^ "_" ^ Int.toString (inc sko_count)
+ val id = "sko_" ^ s ^ "_" ^ Int.toString (Unsynchronized.inc sko_count)
val c = Free (id, cT)
val rhs = list_abs_free (map dest_Free args,
HOLogic.choice_const T $ xtp)
@@ -449,7 +450,7 @@
end;
-val suppress_endtheory = ref false;
+val suppress_endtheory = Unsynchronized.ref false;
fun clause_cache_endtheory thy =
if ! suppress_endtheory then NONE
--- a/src/HOL/Tools/sat_funcs.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Tools/sat_funcs.ML Tue Sep 29 18:14:08 2009 +0200
@@ -48,9 +48,9 @@
signature SAT =
sig
- val trace_sat: bool ref (* input: print trace messages *)
- val solver: string ref (* input: name of SAT solver to be used *)
- val counter: int ref (* output: number of resolution steps during last proof replay *)
+ val trace_sat: bool Unsynchronized.ref (* input: print trace messages *)
+ val solver: string Unsynchronized.ref (* input: name of SAT solver to be used *)
+ val counter: int Unsynchronized.ref (* output: number of resolution steps during last proof replay *)
val rawsat_thm: Proof.context -> cterm list -> thm
val rawsat_tac: Proof.context -> int -> tactic
val sat_tac: Proof.context -> int -> tactic
@@ -60,11 +60,12 @@
functor SATFunc(cnf : CNF) : SAT =
struct
-val trace_sat = ref false;
+val trace_sat = Unsynchronized.ref false;
-val solver = ref "zchaff_with_proofs"; (* see HOL/Tools/sat_solver.ML for possible values *)
+val solver = Unsynchronized.ref "zchaff_with_proofs";
+ (*see HOL/Tools/sat_solver.ML for possible values*)
-val counter = ref 0;
+val counter = Unsynchronized.ref 0;
val resolution_thm =
@{lemma "(P ==> False) ==> (~ P ==> False) ==> False" by (rule case_split)}
@@ -191,7 +192,7 @@
" (hyps: " ^ ML_Syntax.print_list
(Syntax.string_of_term_global (theory_of_thm c_new)) (#hyps (rep_thm c_new)) ^ ")")
else ()
- val _ = inc counter
+ val _ = Unsynchronized.inc counter
in
(c_new, new_hyps)
end
--- a/src/HOL/Tools/sat_solver.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Tools/sat_solver.ML Tue Sep 29 18:14:08 2009 +0200
@@ -26,7 +26,7 @@
val read_dimacs_cnf_file : Path.T -> PropLogic.prop_formula
(* generic solver interface *)
- val solvers : (string * solver) list ref
+ val solvers : (string * solver) list Unsynchronized.ref
val add_solver : string * solver -> unit
val invoke_solver : string -> solver (* exception Option *)
end;
@@ -363,7 +363,7 @@
(* solvers: a (reference to a) table of all registered SAT solvers *)
(* ------------------------------------------------------------------------- *)
- val solvers = ref ([] : (string * solver) list);
+ val solvers = Unsynchronized.ref ([] : (string * solver) list);
(* ------------------------------------------------------------------------- *)
(* add_solver: updates 'solvers' by adding a new solver *)
@@ -629,7 +629,7 @@
val _ = init_array (cnf, 0)
(* optimization for the common case where MiniSat "R"s clauses in their *)
(* original order: *)
- val last_ref_clause = ref (number_of_clauses - 1)
+ val last_ref_clause = Unsynchronized.ref (number_of_clauses - 1)
(* search the 'clauses' array for the given list of literals 'lits', *)
(* starting at index '!last_ref_clause + 1' *)
(* int list -> int option *)
@@ -661,17 +661,17 @@
| NONE => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).")
)
(* parse the proof file *)
- val clause_table = ref (Inttab.empty : int list Inttab.table)
- val empty_id = ref ~1
+ val clause_table = Unsynchronized.ref (Inttab.empty : int list Inttab.table)
+ val empty_id = Unsynchronized.ref ~1
(* contains a mapping from clause IDs as used by MiniSat to clause IDs in *)
(* our proof format, where original clauses are numbered starting from 0 *)
- val clause_id_map = ref (Inttab.empty : int Inttab.table)
+ val clause_id_map = Unsynchronized.ref (Inttab.empty : int Inttab.table)
fun sat_to_proof id = (
case Inttab.lookup (!clause_id_map) id of
SOME id' => id'
| NONE => raise INVALID_PROOF ("Clause ID " ^ Int.toString id ^ " used, but not defined.")
)
- val next_id = ref (number_of_clauses - 1)
+ val next_id = Unsynchronized.ref (number_of_clauses - 1)
(* string list -> unit *)
fun process_tokens [] =
()
@@ -708,7 +708,7 @@
| unevens (x :: _ :: xs) = x :: unevens xs
val rs = (map sat_to_proof o unevens o map int_from_string) ids
(* extend the mapping of clause IDs with this newly defined ID *)
- val proof_id = inc next_id
+ val proof_id = Unsynchronized.inc next_id
val _ = clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map)
handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"C\").")
in
@@ -821,9 +821,9 @@
| NONE => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).")
)
(* parse the "resolve_trace" file *)
- val clause_offset = ref ~1
- val clause_table = ref (Inttab.empty : int list Inttab.table)
- val empty_id = ref ~1
+ val clause_offset = Unsynchronized.ref ~1
+ val clause_table = Unsynchronized.ref (Inttab.empty : int list Inttab.table)
+ val empty_id = Unsynchronized.ref ~1
(* string list -> unit *)
fun process_tokens [] =
()
--- a/src/HOL/ex/SVC_Oracle.thy Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/ex/SVC_Oracle.thy Tue Sep 29 18:14:08 2009 +0200
@@ -44,8 +44,8 @@
and body = Term.strip_all_body t
val Us = map #2 params
val nPar = length params
- val vname = ref "V_a"
- val pairs = ref ([] : (term*term) list)
+ val vname = Unsynchronized.ref "V_a"
+ val pairs = Unsynchronized.ref ([] : (term*term) list)
fun insert t =
let val T = fastype_of t
val v = Logic.combound (Var ((!vname,0), Us--->T), 0, nPar)
--- a/src/HOL/ex/predicate_compile.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/ex/predicate_compile.ML Tue Sep 29 18:14:08 2009 +0200
@@ -27,10 +27,10 @@
val code_pred_cmd: string -> Proof.context -> Proof.state
val print_stored_rules: theory -> unit
val print_all_modes: theory -> unit
- val do_proofs: bool ref
+ val do_proofs: bool Unsynchronized.ref
val mk_casesrule : Proof.context -> int -> thm list -> term
val analyze_compr: theory -> term -> term
- val eval_ref: (unit -> term Predicate.pred) option ref
+ val eval_ref: (unit -> term Predicate.pred) option Unsynchronized.ref
val add_equations : string list -> theory -> theory
val code_pred_intros_attrib : attribute
(* used by Quickcheck_Generator *)
@@ -111,7 +111,7 @@
fun print_tac s = Seq.single; (* (if ! Toplevel.debug then Tactical.print_tac s else Seq.single); *)
fun debug_tac msg = Seq.single; (* (fn st => (Output.tracing msg; Seq.single st)); *)
-val do_proofs = ref true;
+val do_proofs = Unsynchronized.ref true;
fun mycheat_tac thy i st =
(Tactic.rtac (SkipProof.make_thm thy (Var (("A", 0), propT))) i) st
@@ -2100,7 +2100,7 @@
(* transformation for code generation *)
-val eval_ref = ref (NONE : (unit -> term Predicate.pred) option);
+val eval_ref = Unsynchronized.ref (NONE : (unit -> term Predicate.pred) option);
(*FIXME turn this into an LCF-guarded preprocessor for comprehensions*)
fun analyze_compr thy t_compr =
--- a/src/HOL/ex/svc_funcs.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/ex/svc_funcs.ML Tue Sep 29 18:14:08 2009 +0200
@@ -18,7 +18,7 @@
structure Svc =
struct
- val trace = ref false;
+ val trace = Unsynchronized.ref false;
datatype expr =
Buildin of string * expr list
@@ -127,7 +127,7 @@
let
val params = rev (Term.rename_wrt_term t (Term.strip_all_vars t))
and body = Term.strip_all_body t
- val nat_vars = ref ([] : string list)
+ val nat_vars = Unsynchronized.ref ([] : string list)
(*translation of a variable: record all natural numbers*)
fun trans_var (a,T,is) =
(if T = HOLogic.natT then nat_vars := (insert (op =) a (!nat_vars))
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Tue Sep 29 18:14:08 2009 +0200
@@ -1,6 +1,6 @@
(* Title: HOLCF/Tools/Domain/domain_theorems.ML
Author: David von Oheimb
- New proofs/tactics by Brian Huffman
+ Author: Brian Huffman
Proof generator for domain command.
*)
@@ -11,15 +11,15 @@
sig
val theorems: Domain_Library.eq * Domain_Library.eq list -> theory -> thm list * theory;
val comp_theorems: bstring * Domain_Library.eq list -> theory -> thm list * theory;
- val quiet_mode: bool ref;
- val trace_domain: bool ref;
+ val quiet_mode: bool Unsynchronized.ref;
+ val trace_domain: bool Unsynchronized.ref;
end;
structure Domain_Theorems :> DOMAIN_THEOREMS =
struct
-val quiet_mode = ref false;
-val trace_domain = ref false;
+val quiet_mode = Unsynchronized.ref false;
+val trace_domain = Unsynchronized.ref false;
fun message s = if !quiet_mode then () else writeln s;
fun trace s = if !trace_domain then tracing s else ();
--- a/src/Provers/Arith/fast_lin_arith.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Provers/Arith/fast_lin_arith.ML Tue Sep 29 18:14:08 2009 +0200
@@ -96,8 +96,8 @@
lessD: thm list, neqE: thm list, simpset: Simplifier.simpset,
number_of : serial * (theory -> typ -> int -> cterm)})
-> Context.generic -> Context.generic
- val trace: bool ref
- val warning_count: int ref;
+ val trace: bool Unsynchronized.ref
+ val warning_count: int Unsynchronized.ref;
end;
functor Fast_Lin_Arith
@@ -152,7 +152,7 @@
treat non-negative atoms separately rather than adding 0 <= atom
*)
-val trace = ref false;
+val trace = Unsynchronized.ref false;
datatype lineq_type = Eq | Le | Lt;
@@ -426,7 +426,7 @@
fun trace_msg msg =
if !trace then tracing msg else ();
-val warning_count = ref 0;
+val warning_count = Unsynchronized.ref 0;
val warning_count_max = 10;
val union_term = curry (gen_union Pattern.aeconv);
@@ -533,7 +533,7 @@
val _ =
if LA_Logic.is_False fls then ()
else
- let val count = CRITICAL (fn () => inc warning_count) in
+ let val count = CRITICAL (fn () => Unsynchronized.inc warning_count) in
if count > warning_count_max then ()
else
(tracing (cat_lines
--- a/src/Provers/blast.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Provers/blast.ML Tue Sep 29 18:14:08 2009 +0200
@@ -66,9 +66,9 @@
exception TRANS of string (*reports translation errors*)
datatype term =
Const of string * term list
- | Skolem of string * term option ref list
+ | Skolem of string * term option Unsynchronized.ref list
| Free of string
- | Var of term option ref
+ | Var of term option Unsynchronized.ref
| Bound of int
| Abs of string*term
| $ of term*term;
@@ -78,10 +78,10 @@
val blast_tac : claset -> int -> tactic
val setup : theory -> theory
(*debugging tools*)
- val stats : bool ref
- val trace : bool ref
- val fullTrace : branch list list ref
- val fromType : (indexname * term) list ref -> Term.typ -> term
+ val stats : bool Unsynchronized.ref
+ val trace : bool Unsynchronized.ref
+ val fullTrace : branch list list Unsynchronized.ref
+ val fromType : (indexname * term) list Unsynchronized.ref -> Term.typ -> term
val fromTerm : theory -> Term.term -> term
val fromSubgoal : theory -> Term.term -> term
val instVars : term -> (unit -> unit)
@@ -98,14 +98,14 @@
type claset = Data.claset;
-val trace = ref false
-and stats = ref false; (*for runtime and search statistics*)
+val trace = Unsynchronized.ref false
+and stats = Unsynchronized.ref false; (*for runtime and search statistics*)
datatype term =
Const of string * term list (*typargs constant--as a terms!*)
- | Skolem of string * term option ref list
+ | Skolem of string * term option Unsynchronized.ref list
| Free of string
- | Var of term option ref
+ | Var of term option Unsynchronized.ref
| Bound of int
| Abs of string*term
| op $ of term*term;
@@ -115,7 +115,7 @@
{pairs: ((term*bool) list * (*safe formulae on this level*)
(term*bool) list) list, (*haz formulae on this level*)
lits: term list, (*literals: irreducible formulae*)
- vars: term option ref list, (*variables occurring in branch*)
+ vars: term option Unsynchronized.ref list, (*variables occurring in branch*)
lim: int}; (*resource limit*)
@@ -123,11 +123,11 @@
datatype state = State of
{thy: theory,
- fullTrace: branch list list ref,
- trail: term option ref list ref,
- ntrail: int ref,
- nclosed: int ref,
- ntried: int ref}
+ fullTrace: branch list list Unsynchronized.ref,
+ trail: term option Unsynchronized.ref list Unsynchronized.ref,
+ ntrail: int Unsynchronized.ref,
+ nclosed: int Unsynchronized.ref,
+ ntried: int Unsynchronized.ref}
fun reject_const thy c =
is_some (Sign.const_type thy c) andalso
@@ -138,11 +138,11 @@
reject_const thy "*False*";
State
{thy = thy,
- fullTrace = ref [],
- trail = ref [],
- ntrail = ref 0,
- nclosed = ref 0, (*branches closed: number of branches closed during the search*)
- ntried = ref 1}); (*branches tried: number of branches created by splitting (counting from 1)*)
+ fullTrace = Unsynchronized.ref [],
+ trail = Unsynchronized.ref [],
+ ntrail = Unsynchronized.ref 0,
+ nclosed = Unsynchronized.ref 0, (*branches closed: number of branches closed during the search*)
+ ntried = Unsynchronized.ref 1}); (*branches tried: number of branches created by splitting (counting from 1)*)
@@ -199,7 +199,7 @@
| fromType alist (Term.TFree(a,_)) = Free a
| fromType alist (Term.TVar (ixn,_)) =
(case (AList.lookup (op =) (!alist) ixn) of
- NONE => let val t' = Var(ref NONE)
+ NONE => let val t' = Var (Unsynchronized.ref NONE)
in alist := (ixn, t') :: !alist; t'
end
| SOME v => v)
@@ -209,11 +209,11 @@
(*Tests whether 2 terms are alpha-convertible; chases instantiations*)
-fun (Const (a, ts)) aconv (Const (b, us)) = a=b andalso aconvs (ts, us)
- | (Skolem (a,_)) aconv (Skolem (b,_)) = a=b (*arglists must then be equal*)
- | (Free a) aconv (Free b) = a=b
- | (Var(ref(SOME t))) aconv u = t aconv u
- | t aconv (Var(ref(SOME u))) = t aconv u
+fun (Const (a, ts)) aconv (Const (b, us)) = a = b andalso aconvs (ts, us)
+ | (Skolem (a,_)) aconv (Skolem (b,_)) = a = b (*arglists must then be equal*)
+ | (Free a) aconv (Free b) = a = b
+ | (Var (Unsynchronized.ref(SOME t))) aconv u = t aconv u
+ | t aconv (Var (Unsynchronized.ref (SOME u))) = t aconv u
| (Var v) aconv (Var w) = v=w (*both Vars are un-assigned*)
| (Bound i) aconv (Bound j) = i=j
| (Abs(_,t)) aconv (Abs(_,u)) = t aconv u
@@ -229,7 +229,7 @@
fun ins_term(t,ts) = if mem_term(t,ts) then ts else t :: ts;
-fun mem_var (v: term option ref, []) = false
+fun mem_var (v: term option Unsynchronized.ref, []) = false
| mem_var (v, v'::vs) = v=v' orelse mem_var(v,vs);
fun ins_var(v,vs) = if mem_var(v,vs) then vs else v :: vs;
@@ -238,19 +238,19 @@
(** Vars **)
(*Accumulates the Vars in the term, suppressing duplicates*)
-fun add_term_vars (Skolem(a,args), vars) = add_vars_vars(args,vars)
- | add_term_vars (Var (v as ref NONE), vars) = ins_var (v, vars)
- | add_term_vars (Var (ref (SOME u)), vars) = add_term_vars(u,vars)
- | add_term_vars (Const (_,ts), vars) = add_terms_vars(ts,vars)
- | add_term_vars (Abs (_,body), vars) = add_term_vars(body,vars)
- | add_term_vars (f$t, vars) = add_term_vars (f, add_term_vars(t, vars))
- | add_term_vars (_, vars) = vars
+fun add_term_vars (Skolem(a,args), vars) = add_vars_vars(args,vars)
+ | add_term_vars (Var (v as Unsynchronized.ref NONE), vars) = ins_var (v, vars)
+ | add_term_vars (Var (Unsynchronized.ref (SOME u)), vars) = add_term_vars (u, vars)
+ | add_term_vars (Const (_, ts), vars) = add_terms_vars (ts, vars)
+ | add_term_vars (Abs (_, body), vars) = add_term_vars (body, vars)
+ | add_term_vars (f $ t, vars) = add_term_vars (f, add_term_vars (t, vars))
+ | add_term_vars (_, vars) = vars
(*Term list version. [The fold functionals are slow]*)
and add_terms_vars ([], vars) = vars
| add_terms_vars (t::ts, vars) = add_terms_vars (ts, add_term_vars(t,vars))
(*Var list version.*)
-and add_vars_vars ([], vars) = vars
- | add_vars_vars (ref (SOME u) :: vs, vars) =
+and add_vars_vars ([], vars) = vars
+ | add_vars_vars (Unsynchronized.ref (SOME u) :: vs, vars) =
add_vars_vars (vs, add_term_vars(u,vars))
| add_vars_vars (v::vs, vars) = (*v must be a ref NONE*)
add_vars_vars (vs, ins_var (v, vars));
@@ -297,10 +297,10 @@
(*Normalize...but not the bodies of ABSTRACTIONS*)
fun norm t = case t of
- Skolem (a,args) => Skolem(a, vars_in_vars args)
- | Const(a,ts) => Const(a, map norm ts)
- | (Var (ref NONE)) => t
- | (Var (ref (SOME u))) => norm u
+ Skolem (a, args) => Skolem (a, vars_in_vars args)
+ | Const (a, ts) => Const (a, map norm ts)
+ | (Var (Unsynchronized.ref NONE)) => t
+ | (Var (Unsynchronized.ref (SOME u))) => norm u
| (f $ u) => (case norm f of
Abs(_,body) => norm (subst_bound (u, body))
| nf => nf $ norm u)
@@ -394,14 +394,14 @@
(*Convert from "real" terms to prototerms; eta-contract.
Code is similar to fromSubgoal.*)
fun fromTerm thy t =
- let val alistVar = ref []
- and alistTVar = ref []
+ let val alistVar = Unsynchronized.ref []
+ and alistTVar = Unsynchronized.ref []
fun from (Term.Const aT) = fromConst thy alistTVar aT
| from (Term.Free (a,_)) = Free a
| from (Term.Bound i) = Bound i
| from (Term.Var (ixn,T)) =
(case (AList.lookup (op =) (!alistVar) ixn) of
- NONE => let val t' = Var(ref NONE)
+ NONE => let val t' = Var (Unsynchronized.ref NONE)
in alistVar := (ixn, t') :: !alistVar; t'
end
| SOME v => v)
@@ -417,10 +417,10 @@
(*A debugging function: replaces all Vars by dummy Frees for visual inspection
of whether they are distinct. Function revert undoes the assignments.*)
fun instVars t =
- let val name = ref "a"
- val updated = ref []
+ let val name = Unsynchronized.ref "a"
+ val updated = Unsynchronized.ref []
fun inst (Const(a,ts)) = List.app inst ts
- | inst (Var(v as ref NONE)) = (updated := v :: (!updated);
+ | inst (Var(v as Unsynchronized.ref NONE)) = (updated := v :: (!updated);
v := SOME (Free ("?" ^ !name));
name := Symbol.bump_string (!name))
| inst (Abs(a,t)) = inst t
@@ -450,7 +450,7 @@
fun delete_concl [] = raise ElimBadPrem
| delete_concl (P :: Ps) =
(case P of
- Const (c, _) $ Var (ref (SOME (Const ("*False*", _)))) =>
+ Const (c, _) $ Var (Unsynchronized.ref (SOME (Const ("*False*", _)))) =>
if c = "*Goal*" orelse c = Data.not_name then Ps
else P :: delete_concl Ps
| _ => P :: delete_concl Ps);
@@ -606,10 +606,10 @@
(*Convert from prototerms to ordinary terms with dummy types for tracing*)
fun showTerm d (Const (a,_)) = Term.Const (a,dummyT)
| showTerm d (Skolem(a,_)) = Term.Const (a,dummyT)
- | showTerm d (Free a) = Term.Free (a,dummyT)
- | showTerm d (Bound i) = Term.Bound i
- | showTerm d (Var(ref(SOME u))) = showTerm d u
- | showTerm d (Var(ref NONE)) = dummyVar2
+ | showTerm d (Free a) = Term.Free (a,dummyT)
+ | showTerm d (Bound i) = Term.Bound i
+ | showTerm d (Var (Unsynchronized.ref(SOME u))) = showTerm d u
+ | showTerm d (Var (Unsynchronized.ref NONE)) = dummyVar2
| showTerm d (Abs(a,t)) = if d=0 then dummyVar
else Term.Abs(a, dummyT, showTerm (d-1) t)
| showTerm d (f $ u) = if d=0 then dummyVar
@@ -687,10 +687,10 @@
(*Replace the ATOMIC term "old" by "new" in t*)
fun subst_atomic (old,new) t =
- let fun subst (Var(ref(SOME u))) = subst u
- | subst (Abs(a,body)) = Abs(a, subst body)
- | subst (f$t) = subst f $ subst t
- | subst t = if t aconv old then new else t
+ let fun subst (Var(Unsynchronized.ref(SOME u))) = subst u
+ | subst (Abs(a,body)) = Abs(a, subst body)
+ | subst (f$t) = subst f $ subst t
+ | subst t = if t aconv old then new else t
in subst t end;
(*Eta-contract a term from outside: just enough to reduce it to an atom*)
@@ -723,11 +723,11 @@
Skolem(_,vars) => vars
| _ => []
fun occEq u = (t aconv u) orelse occ u
- and occ (Var(ref(SOME u))) = occEq u
- | occ (Var v) = not (mem_var (v, vars))
- | occ (Abs(_,u)) = occEq u
- | occ (f$u) = occEq u orelse occEq f
- | occ (_) = false;
+ and occ (Var(Unsynchronized.ref(SOME u))) = occEq u
+ | occ (Var v) = not (mem_var (v, vars))
+ | occ (Abs(_,u)) = occEq u
+ | occ (f$u) = occEq u orelse occEq f
+ | occ _ = false;
in occEq end;
exception DEST_EQ;
@@ -1199,8 +1199,8 @@
(*Translation of a subgoal: Skolemize all parameters*)
fun fromSubgoal thy t =
- let val alistVar = ref []
- and alistTVar = ref []
+ let val alistVar = Unsynchronized.ref []
+ and alistTVar = Unsynchronized.ref []
fun hdvar ((ix,(v,is))::_) = v
fun from lev t =
let val (ht,ts) = Term.strip_comb t
@@ -1219,7 +1219,7 @@
| Term.Bound i => apply (Bound i)
| Term.Var (ix,_) =>
(case (AList.lookup (op =) (!alistVar) ix) of
- NONE => (alistVar := (ix, (ref NONE, bounds ts))
+ NONE => (alistVar := (ix, (Unsynchronized.ref NONE, bounds ts))
:: !alistVar;
Var (hdvar(!alistVar)))
| SOME(v,is) => if is=bounds ts then Var v
@@ -1290,7 +1290,7 @@
(*** For debugging: these apply the prover to a subgoal and return
the resulting tactics, trace, etc. ***)
-val fullTrace = ref ([]: branch list list);
+val fullTrace = Unsynchronized.ref ([]: branch list list);
(*Read a string to make an initial, singleton branch*)
fun readGoal thy s = Syntax.read_prop_global thy s |> fromTerm thy |> rand |> mkGoal;
--- a/src/Provers/classical.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Provers/classical.ML Tue Sep 29 18:14:08 2009 +0200
@@ -74,7 +74,7 @@
val fast_tac : claset -> int -> tactic
val slow_tac : claset -> int -> tactic
- val weight_ASTAR : int ref
+ val weight_ASTAR : int Unsynchronized.ref
val astar_tac : claset -> int -> tactic
val slow_astar_tac : claset -> int -> tactic
val best_tac : claset -> int -> tactic
@@ -746,7 +746,7 @@
(***ASTAR with weight weight_ASTAR, by Norbert Voelker*)
-val weight_ASTAR = ref 5;
+val weight_ASTAR = Unsynchronized.ref 5;
fun astar_tac cs =
ObjectLogic.atomize_prems_tac THEN'
--- a/src/Provers/order.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Provers/order.ML Tue Sep 29 18:14:08 2009 +0200
@@ -656,10 +656,10 @@
let
(* Ordered list of the vertices that DFS has finished with;
most recently finished goes at the head. *)
- val finish : term list ref = ref nil
+ val finish : term list Unsynchronized.ref = Unsynchronized.ref []
(* List of vertices which have been visited. *)
- val visited : term list ref = ref nil
+ val visited : term list Unsynchronized.ref = Unsynchronized.ref []
fun been_visited v = exists (fn w => w aconv v) (!visited)
@@ -715,7 +715,7 @@
fun dfs_int_reachable g u =
let
(* List of vertices which have been visited. *)
- val visited : int list ref = ref nil
+ val visited : int list Unsynchronized.ref = Unsynchronized.ref []
fun been_visited v = exists (fn w => w = v) (!visited)
@@ -755,8 +755,8 @@
fun dfs eq_comp g u v =
let
- val pred = ref nil;
- val visited = ref nil;
+ val pred = Unsynchronized.ref [];
+ val visited = Unsynchronized.ref [];
fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
--- a/src/Provers/quasi.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Provers/quasi.ML Tue Sep 29 18:14:08 2009 +0200
@@ -348,8 +348,8 @@
fun dfs eq_comp g u v =
let
- val pred = ref nil;
- val visited = ref nil;
+ val pred = Unsynchronized.ref [];
+ val visited = Unsynchronized.ref [];
fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
--- a/src/Provers/trancl.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Provers/trancl.ML Tue Sep 29 18:14:08 2009 +0200
@@ -275,8 +275,8 @@
fun dfs eq_comp g u v =
let
- val pred = ref nil;
- val visited = ref nil;
+ val pred = Unsynchronized.ref [];
+ val visited = Unsynchronized.ref [];
fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
@@ -349,7 +349,7 @@
fun dfs_reachable eq_comp g u =
let
(* List of vertices which have been visited. *)
- val visited = ref nil;
+ val visited = Unsynchronized.ref nil;
fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
--- a/src/Pure/Concurrent/future.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/Concurrent/future.ML Tue Sep 29 18:14:08 2009 +0200
@@ -99,13 +99,13 @@
(* global state *)
-val queue = ref Task_Queue.empty;
-val next = ref 0;
-val workers = ref ([]: (Thread.thread * bool) list);
-val scheduler = ref (NONE: Thread.thread option);
-val excessive = ref 0;
-val canceled = ref ([]: Task_Queue.group list);
-val do_shutdown = ref false;
+val queue = Unsynchronized.ref Task_Queue.empty;
+val next = Unsynchronized.ref 0;
+val workers = Unsynchronized.ref ([]: (Thread.thread * bool) list);
+val scheduler = Unsynchronized.ref (NONE: Thread.thread option);
+val excessive = Unsynchronized.ref 0;
+val canceled = Unsynchronized.ref ([]: Task_Queue.group list);
+val do_shutdown = Unsynchronized.ref false;
(* synchronization *)
@@ -162,7 +162,8 @@
in (result, job) end;
fun do_cancel group = (*requires SYNCHRONIZED*)
- (change canceled (insert Task_Queue.eq_group group); broadcast scheduler_event);
+ (Unsynchronized.change canceled (insert Task_Queue.eq_group group);
+ broadcast scheduler_event);
fun execute name (task, group, jobs) =
let
@@ -171,7 +172,7 @@
fold (fn job => fn ok => job valid andalso ok) jobs true) ();
val _ = SYNCHRONIZED "finish" (fn () =>
let
- val maximal = change_result queue (Task_Queue.finish task);
+ val maximal = Unsynchronized.change_result queue (Task_Queue.finish task);
val _ =
if ok then ()
else if Task_Queue.cancel (! queue) group then ()
@@ -188,7 +189,8 @@
fold (fn (_, active) => fn i => if active then i + 1 else i) (! workers) 0;
fun change_active active = (*requires SYNCHRONIZED*)
- change workers (AList.update Thread.equal (Thread.self (), active));
+ Unsynchronized.change workers
+ (AList.update Thread.equal (Thread.self (), active));
(* worker threads *)
@@ -198,14 +200,15 @@
fun worker_next () = (*requires SYNCHRONIZED*)
if ! excessive > 0 then
- (dec excessive;
- change workers (filter_out (fn (thread, _) => Thread.equal (thread, Thread.self ())));
+ (Unsynchronized.dec excessive;
+ Unsynchronized.change workers
+ (filter_out (fn (thread, _) => Thread.equal (thread, Thread.self ())));
broadcast scheduler_event;
NONE)
else if count_active () > Multithreading.max_threads_value () then
(worker_wait scheduler_event; worker_next ())
else
- (case change_result queue (Task_Queue.dequeue (Thread.self ())) of
+ (case Unsynchronized.change_result queue (Task_Queue.dequeue (Thread.self ())) of
NONE => (worker_wait work_available; worker_next ())
| some => some);
@@ -215,13 +218,13 @@
| SOME work => (execute name work; worker_loop name));
fun worker_start name = (*requires SYNCHRONIZED*)
- change workers (cons (SimpleThread.fork false (fn () =>
+ Unsynchronized.change workers (cons (SimpleThread.fork false (fn () =>
(broadcast scheduler_event; worker_loop name)), true));
(* scheduler *)
-val last_status = ref Time.zeroTime;
+val last_status = Unsynchronized.ref Time.zeroTime;
val next_status = Time.fromMilliseconds 500;
val next_round = Time.fromMilliseconds 50;
@@ -263,7 +266,8 @@
val _ = excessive := l - mm;
val _ =
if mm > l then
- funpow (mm - l) (fn () => worker_start ("worker " ^ string_of_int (inc next))) ()
+ funpow (mm - l) (fn () =>
+ worker_start ("worker " ^ string_of_int (Unsynchronized.inc next))) ()
else ();
(*canceled groups*)
@@ -272,7 +276,7 @@
else
(Multithreading.tracing 1 (fn () =>
string_of_int (length (! canceled)) ^ " canceled groups");
- change canceled (filter_out (Task_Queue.cancel (! queue)));
+ Unsynchronized.change canceled (filter_out (Task_Queue.cancel (! queue)));
broadcast_work ());
(*delay loop*)
@@ -317,7 +321,8 @@
val (result, job) = future_job group e;
val task = SYNCHRONIZED "enqueue" (fn () =>
let
- val (task, minimal) = change_result queue (Task_Queue.enqueue group deps pri job);
+ val (task, minimal) =
+ Unsynchronized.change_result queue (Task_Queue.enqueue group deps pri job);
val _ = if minimal then signal work_available else ();
val _ = scheduler_check ();
in task end);
@@ -347,7 +352,7 @@
fun join_next deps = (*requires SYNCHRONIZED*)
if null deps then NONE
else
- (case change_result queue (Task_Queue.dequeue_towards (Thread.self ()) deps) of
+ (case Unsynchronized.change_result queue (Task_Queue.dequeue_towards (Thread.self ()) deps) of
(NONE, []) => NONE
| (NONE, deps') => (worker_wait work_finished; join_next deps')
| (SOME work, deps') => SOME (work, deps'));
--- a/src/Pure/Concurrent/synchronized.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/Concurrent/synchronized.ML Tue Sep 29 18:14:08 2009 +0200
@@ -24,13 +24,13 @@
{name: string,
lock: Mutex.mutex,
cond: ConditionVar.conditionVar,
- var: 'a ref};
+ var: 'a Unsynchronized.ref};
fun var name x = Var
{name = name,
lock = Mutex.mutex (),
cond = ConditionVar.conditionVar (),
- var = ref x};
+ var = Unsynchronized.ref x};
fun value (Var {var, ...}) = ! var;
--- a/src/Pure/Concurrent/synchronized_dummy.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/Concurrent/synchronized_dummy.ML Tue Sep 29 18:14:08 2009 +0200
@@ -7,9 +7,9 @@
structure Synchronized: SYNCHRONIZED =
struct
-datatype 'a var = Var of 'a ref;
+datatype 'a var = Var of 'a Unsynchronized.ref;
-fun var _ x = Var (ref x);
+fun var _ x = Var (Unsynchronized.ref x);
fun value (Var var) = ! var;
fun timed_access (Var var) _ f =
--- a/src/Pure/General/file.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/General/file.ML Tue Sep 29 18:14:08 2009 +0200
@@ -85,7 +85,8 @@
(* file identification *)
local
- val ident_cache = ref (Symtab.empty: {time_stamp: string, id: string} Symtab.table);
+ val ident_cache =
+ Unsynchronized.ref (Symtab.empty: {time_stamp: string, id: string} Symtab.table);
in
fun check_cache (path, time) = CRITICAL (fn () =>
@@ -94,7 +95,8 @@
| SOME {time_stamp, id} => if time_stamp = time then SOME id else NONE));
fun update_cache (path, (time, id)) = CRITICAL (fn () =>
- change ident_cache (Symtab.update (path, {time_stamp = time, id = id})));
+ Unsynchronized.change ident_cache
+ (Symtab.update (path, {time_stamp = time, id = id})));
end;
--- a/src/Pure/General/lazy.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/General/lazy.ML Tue Sep 29 18:14:08 2009 +0200
@@ -26,12 +26,12 @@
Lazy of unit -> 'a |
Result of 'a Exn.result;
-type 'a lazy = 'a T ref;
+type 'a lazy = 'a T Unsynchronized.ref;
fun same (r1: 'a lazy, r2) = r1 = r2;
-fun lazy e = ref (Lazy e);
-fun value x = ref (Result (Exn.Result x));
+fun lazy e = Unsynchronized.ref (Lazy e);
+fun value x = Unsynchronized.ref (Result (Exn.Result x));
fun peek r =
(case ! r of
--- a/src/Pure/General/markup.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/General/markup.ML Tue Sep 29 18:14:08 2009 +0200
@@ -323,10 +323,10 @@
local
val default = {output = default_output};
- val modes = ref (Symtab.make [("", default)]);
+ val modes = Unsynchronized.ref (Symtab.make [("", default)]);
in
fun add_mode name output = CRITICAL (fn () =>
- change modes (Symtab.update_new (name, {output = output})));
+ Unsynchronized.change modes (Symtab.update_new (name, {output = output})));
fun get_mode () =
the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
end;
--- a/src/Pure/General/name_space.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/General/name_space.ML Tue Sep 29 18:14:08 2009 +0200
@@ -9,9 +9,9 @@
signature BASIC_NAME_SPACE =
sig
- val long_names: bool ref
- val short_names: bool ref
- val unique_names: bool ref
+ val long_names: bool Unsynchronized.ref
+ val short_names: bool Unsynchronized.ref
+ val unique_names: bool Unsynchronized.ref
end;
signature NAME_SPACE =
@@ -105,9 +105,9 @@
else ext (get_accesses space name)
end;
-val long_names = ref false;
-val short_names = ref false;
-val unique_names = ref true;
+val long_names = Unsynchronized.ref false;
+val short_names = Unsynchronized.ref false;
+val unique_names = Unsynchronized.ref true;
fun extern space name =
extern_flags
@@ -261,6 +261,6 @@
end;
-structure BasicNameSpace: BASIC_NAME_SPACE = NameSpace;
-open BasicNameSpace;
+structure Basic_Name_Space: BASIC_NAME_SPACE = NameSpace;
+open Basic_Name_Space;
--- a/src/Pure/General/output.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/General/output.ML Tue Sep 29 18:14:08 2009 +0200
@@ -11,13 +11,13 @@
val priority: string -> unit
val tracing: string -> unit
val warning: string -> unit
- val tolerate_legacy_features: bool ref
+ val tolerate_legacy_features: bool Unsynchronized.ref
val legacy_feature: string -> unit
val cond_timeit: bool -> string -> (unit -> 'a) -> 'a
val timeit: (unit -> 'a) -> 'a
val timeap: ('a -> 'b) -> 'a -> 'b
val timeap_msg: string -> ('a -> 'b) -> 'a -> 'b
- val timing: bool ref
+ val timing: bool Unsynchronized.ref
end;
signature OUTPUT =
@@ -32,18 +32,18 @@
val std_output: output -> unit
val std_error: output -> unit
val writeln_default: output -> unit
- val writeln_fn: (output -> unit) ref
- val priority_fn: (output -> unit) ref
- val tracing_fn: (output -> unit) ref
- val warning_fn: (output -> unit) ref
- val error_fn: (output -> unit) ref
- val debug_fn: (output -> unit) ref
- val prompt_fn: (output -> unit) ref
- val status_fn: (output -> unit) ref
+ val writeln_fn: (output -> unit) Unsynchronized.ref
+ val priority_fn: (output -> unit) Unsynchronized.ref
+ val tracing_fn: (output -> unit) Unsynchronized.ref
+ val warning_fn: (output -> unit) Unsynchronized.ref
+ val error_fn: (output -> unit) Unsynchronized.ref
+ val debug_fn: (output -> unit) Unsynchronized.ref
+ val prompt_fn: (output -> unit) Unsynchronized.ref
+ val status_fn: (output -> unit) Unsynchronized.ref
val error_msg: string -> unit
val prompt: string -> unit
val status: string -> unit
- val debugging: bool ref
+ val debugging: bool Unsynchronized.ref
val no_warnings: ('a -> 'b) -> 'a -> 'b
val debug: (unit -> string) -> unit
end;
@@ -60,10 +60,10 @@
local
val default = {output = default_output, escape = default_escape};
- val modes = ref (Symtab.make [("", default)]);
+ val modes = Unsynchronized.ref (Symtab.make [("", default)]);
in
fun add_mode name output escape = CRITICAL (fn () =>
- change modes (Symtab.update_new (name, {output = output, escape = escape})));
+ Unsynchronized.change modes (Symtab.update_new (name, {output = output, escape = escape})));
fun get_mode () =
the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
end;
@@ -91,14 +91,14 @@
(* Isabelle output channels *)
-val writeln_fn = ref writeln_default;
-val priority_fn = ref (fn s => ! writeln_fn s);
-val tracing_fn = ref (fn s => ! writeln_fn s);
-val warning_fn = ref (std_output o suffix "\n" o prefix_lines "### ");
-val error_fn = ref (std_output o suffix "\n" o prefix_lines "*** ");
-val debug_fn = ref (std_output o suffix "\n" o prefix_lines "::: ");
-val prompt_fn = ref std_output;
-val status_fn = ref (fn _: string => ());
+val writeln_fn = Unsynchronized.ref writeln_default;
+val priority_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
+val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
+val warning_fn = Unsynchronized.ref (std_output o suffix "\n" o prefix_lines "### ");
+val error_fn = Unsynchronized.ref (std_output o suffix "\n" o prefix_lines "*** ");
+val debug_fn = Unsynchronized.ref (std_output o suffix "\n" o prefix_lines "::: ");
+val prompt_fn = Unsynchronized.ref std_output;
+val status_fn = Unsynchronized.ref (fn _: string => ());
fun writeln s = ! writeln_fn (output s);
fun priority s = ! priority_fn (output s);
@@ -108,13 +108,13 @@
fun prompt s = ! prompt_fn (output s);
fun status s = ! status_fn (output s);
-val tolerate_legacy_features = ref true;
+val tolerate_legacy_features = Unsynchronized.ref true;
fun legacy_feature s =
(if ! tolerate_legacy_features then warning else error) ("Legacy feature! " ^ s);
fun no_warnings f = setmp warning_fn (K ()) f;
-val debugging = ref false;
+val debugging = Unsynchronized.ref false;
fun debug s = if ! debugging then ! debug_fn (output (s ())) else ()
@@ -140,9 +140,9 @@
fun timeap_msg msg f x = cond_timeit true msg (fn () => f x);
(*global timing mode*)
-val timing = ref false;
+val timing = Unsynchronized.ref false;
end;
-structure BasicOutput: BASIC_OUTPUT = Output;
-open BasicOutput;
+structure Basic_Output: BASIC_OUTPUT = Output;
+open Basic_Output;
--- a/src/Pure/General/pretty.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/General/pretty.ML Tue Sep 29 18:14:08 2009 +0200
@@ -86,10 +86,10 @@
local
val default = {indent = default_indent};
- val modes = ref (Symtab.make [("", default)]);
+ val modes = Unsynchronized.ref (Symtab.make [("", default)]);
in
fun add_mode name indent = CRITICAL (fn () =>
- change modes (Symtab.update_new (name, {indent = indent})));
+ Unsynchronized.change modes (Symtab.update_new (name, {indent = indent})));
fun get_mode () =
the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
end;
@@ -186,14 +186,14 @@
breakgain = m div 20, (*minimum added space required of a break*)
emergencypos = m div 2}; (*position too far to right*)
-val margin_info = ref (make_margin_info 76);
+val margin_info = Unsynchronized.ref (make_margin_info 76);
fun setmargin m = margin_info := make_margin_info m;
fun setmp_margin m f = setmp margin_info (make_margin_info m) f;
(* depth limitation *)
-val depth = ref 0; (*maximum depth; 0 means no limit*)
+val depth = Unsynchronized.ref 0; (*maximum depth; 0 means no limit*)
fun setdepth dp = (depth := dp);
local
--- a/src/Pure/General/print_mode.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/General/print_mode.ML Tue Sep 29 18:14:08 2009 +0200
@@ -7,9 +7,9 @@
signature BASIC_PRINT_MODE =
sig
- val print_mode: string list ref (*global template*)
- val print_mode_value: unit -> string list (*thread-local value*)
- val print_mode_active: string -> bool (*thread-local value*)
+ val print_mode: string list Unsynchronized.ref (*global template*)
+ val print_mode_value: unit -> string list (*thread-local value*)
+ val print_mode_active: string -> bool (*thread-local value*)
end;
signature PRINT_MODE =
@@ -28,7 +28,7 @@
val input = "input";
val internal = "internal";
-val print_mode = ref ([]: string list);
+val print_mode = Unsynchronized.ref ([]: string list);
val tag = Universal.tag () : string list option Universal.tag;
fun print_mode_value () =
--- a/src/Pure/General/secure.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/General/secure.ML Tue Sep 29 18:14:08 2009 +0200
@@ -13,6 +13,7 @@
val use_text: use_context -> int * string -> bool -> string -> unit
val use_file: use_context -> bool -> string -> unit
val toplevel_pp: string list -> string -> unit
+ val open_unsynchronized: unit -> unit
val commit: unit -> unit
val system_out: string -> string * int
val system: string -> int
@@ -23,7 +24,7 @@
(** secure flag **)
-val secure = ref false;
+val secure = Unsynchronized.ref false;
fun set_secure () = secure := true;
fun is_secure () = ! secure;
@@ -47,8 +48,13 @@
fun toplevel_pp path pp = (secure_mltext (); raw_toplevel_pp ML_Parse.global_context path pp);
-(*commit is dynamically bound!*)
-fun commit () = raw_use_text ML_Parse.global_context (0, "") false "commit();";
+
+(* global evaluation *)
+
+val use_global = raw_use_text ML_Parse.global_context (0, "") false;
+
+fun commit () = use_global "commit();"; (*commit is dynamically bound!*)
+fun open_unsynchronized () = use_global "open Unsynchronized";
(* shell commands *)
--- a/src/Pure/IsaMakefile Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/IsaMakefile Tue Sep 29 18:14:08 2009 +0200
@@ -32,7 +32,7 @@
ML-Systems/pp_polyml.ML ML-Systems/proper_int.ML ML-Systems/smlnj.ML \
ML-Systems/system_shell.ML ML-Systems/thread_dummy.ML \
ML-Systems/timing.ML ML-Systems/time_limit.ML \
- ML-Systems/universal.ML
+ ML-Systems/universal.ML ML-Systems/unsynchronized.ML
RAW: $(OUT)/RAW
--- a/src/Pure/Isar/code.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/Isar/code.ML Tue Sep 29 18:14:08 2009 +0200
@@ -217,8 +217,8 @@
purge: theory -> string list -> Object.T -> Object.T
};
-val kinds = ref (Datatab.empty: kind Datatab.table);
-val kind_keys = ref ([]: serial list);
+val kinds = Unsynchronized.ref (Datatab.empty: kind Datatab.table);
+val kind_keys = Unsynchronized.ref ([]: serial list);
fun invoke f k = case Datatab.lookup (! kinds) k
of SOME kind => f kind
@@ -230,8 +230,8 @@
let
val k = serial ();
val kind = {empty = empty, purge = purge};
- val _ = change kinds (Datatab.update (k, kind));
- val _ = change kind_keys (cons k);
+ val _ = Unsynchronized.change kinds (Datatab.update (k, kind));
+ val _ = Unsynchronized.change kind_keys (cons k);
in k end;
fun invoke_init k = invoke (fn kind => #empty kind) k;
@@ -252,13 +252,13 @@
structure Code_Data = TheoryDataFun
(
- type T = spec * data ref;
+ type T = spec * data Unsynchronized.ref;
val empty = (make_spec (false,
- (Symtab.empty, (Symtab.empty, (Symtab.empty, Symtab.empty)))), ref empty_data);
- fun copy (spec, data) = (spec, ref (! data));
+ (Symtab.empty, (Symtab.empty, (Symtab.empty, Symtab.empty)))), Unsynchronized.ref empty_data);
+ fun copy (spec, data) = (spec, Unsynchronized.ref (! data));
val extend = copy;
fun merge pp ((spec1, data1), (spec2, data2)) =
- (merge_spec (spec1, spec2), ref empty_data);
+ (merge_spec (spec1, spec2), Unsynchronized.ref empty_data);
);
fun thy_data f thy = f ((snd o Code_Data.get) thy);
@@ -267,7 +267,7 @@
case Datatab.lookup (! data_ref) kind
of SOME x => x
| NONE => let val y = invoke_init kind
- in (change data_ref (Datatab.update (kind, y)); y) end;
+ in (Unsynchronized.change data_ref (Datatab.update (kind, y)); y) end;
in
@@ -281,11 +281,11 @@
| SOME (c', _) => insert (op =) c' #> insert (op =) c) cs [];
fun map_exec_purge touched f thy =
- Code_Data.map (fn (exec, data) => (f exec, ref (case touched
+ Code_Data.map (fn (exec, data) => (f exec, Unsynchronized.ref (case touched
of SOME cs => invoke_purge_all thy (complete_class_params thy cs) (! data)
| NONE => empty_data))) thy;
-val purge_data = (Code_Data.map o apsnd) (K (ref empty_data));
+val purge_data = (Code_Data.map o apsnd) (K (Unsynchronized.ref empty_data));
fun change_eqns delete c f = (map_exec_purge (SOME [c]) o map_eqns
o (if delete then Symtab.map_entry c else Symtab.map_default (c, ((false, (true, Lazy.value [])), [])))
@@ -332,7 +332,7 @@
let
val data = get_ensure_init kind data_ref;
val data' = f (dest data);
- in (change data_ref (Datatab.update (kind, mk data')); data') end;
+ in (Unsynchronized.change data_ref (Datatab.update (kind, mk data')); data') end;
in thy_data chnge end;
fun change_yield_data (kind, mk, dest) =
@@ -341,7 +341,7 @@
let
val data = get_ensure_init kind data_ref;
val (x, data') = f (dest data);
- in (x, (change data_ref (Datatab.update (kind, mk data')); data')) end;
+ in (x, (Unsynchronized.change data_ref (Datatab.update (kind, mk data')); data')) end;
in thy_data chnge end;
end; (*local*)
--- a/src/Pure/Isar/isar_document.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/Isar/isar_document.ML Tue Sep 29 18:14:08 2009 +0200
@@ -112,18 +112,18 @@
(** global configuration **)
local
- val global_states = ref (Symtab.empty: Toplevel.state option future Symtab.table);
- val global_commands = ref (Symtab.empty: Toplevel.transition Symtab.table);
- val global_documents = ref (Symtab.empty: document Symtab.table);
+ val global_states = Unsynchronized.ref (Symtab.empty: Toplevel.state option future Symtab.table);
+ val global_commands = Unsynchronized.ref (Symtab.empty: Toplevel.transition Symtab.table);
+ val global_documents = Unsynchronized.ref (Symtab.empty: document Symtab.table);
in
-fun change_states f = NAMED_CRITICAL "Isar" (fn () => change global_states f);
+fun change_states f = NAMED_CRITICAL "Isar" (fn () => Unsynchronized.change global_states f);
fun get_states () = NAMED_CRITICAL "Isar" (fn () => ! global_states);
-fun change_commands f = NAMED_CRITICAL "Isar" (fn () => change global_commands f);
+fun change_commands f = NAMED_CRITICAL "Isar" (fn () => Unsynchronized.change global_commands f);
fun get_commands () = NAMED_CRITICAL "Isar" (fn () => ! global_commands);
-fun change_documents f = NAMED_CRITICAL "Isar" (fn () => change global_documents f);
+fun change_documents f = NAMED_CRITICAL "Isar" (fn () => Unsynchronized.change global_documents f);
fun get_documents () = NAMED_CRITICAL "Isar" (fn () => ! global_documents);
fun init () = NAMED_CRITICAL "Isar" (fn () =>
--- a/src/Pure/Isar/local_syntax.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/Isar/local_syntax.ML Tue Sep 29 18:14:08 2009 +0200
@@ -4,7 +4,7 @@
Local syntax depending on theory syntax.
*)
-val show_structs = ref false;
+val show_structs = Unsynchronized.ref false;
signature LOCAL_SYNTAX =
sig
--- a/src/Pure/Isar/method.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/Isar/method.ML Tue Sep 29 18:14:08 2009 +0200
@@ -8,7 +8,7 @@
sig
val FINDGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
val HEADGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
- val trace_rules: bool ref
+ val trace_rules: bool Unsynchronized.ref
end;
signature METHOD =
@@ -215,7 +215,7 @@
(* rule etc. -- single-step refinements *)
-val trace_rules = ref false;
+val trace_rules = Unsynchronized.ref false;
fun trace ctxt rules =
if ! trace_rules andalso not (null rules) then
--- a/src/Pure/Isar/outer_keyword.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/Isar/outer_keyword.ML Tue Sep 29 18:14:08 2009 +0200
@@ -116,16 +116,16 @@
local
-val global_commands = ref (Symtab.empty: T Symtab.table);
-val global_lexicons = ref (Scan.empty_lexicon, Scan.empty_lexicon);
+val global_commands = Unsynchronized.ref (Symtab.empty: T Symtab.table);
+val global_lexicons = Unsynchronized.ref (Scan.empty_lexicon, Scan.empty_lexicon);
in
fun get_commands () = CRITICAL (fn () => ! global_commands);
fun get_lexicons () = CRITICAL (fn () => ! global_lexicons);
-fun change_commands f = CRITICAL (fn () => change global_commands f);
-fun change_lexicons f = CRITICAL (fn () => change global_lexicons f);
+fun change_commands f = CRITICAL (fn () => Unsynchronized.change global_commands f);
+fun change_lexicons f = CRITICAL (fn () => Unsynchronized.change global_lexicons f);
end;
--- a/src/Pure/Isar/outer_lex.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/Isar/outer_lex.ML Tue Sep 29 18:14:08 2009 +0200
@@ -83,7 +83,7 @@
datatype slot =
Slot |
Value of value option |
- Assignable of value option ref;
+ Assignable of value option Unsynchronized.ref;
(* datatype token *)
@@ -245,7 +245,7 @@
(* static binding *)
(*1st stage: make empty slots assignable*)
-fun assignable (Token (x, y, Slot)) = Token (x, y, Assignable (ref NONE))
+fun assignable (Token (x, y, Slot)) = Token (x, y, Assignable (Unsynchronized.ref NONE))
| assignable tok = tok;
(*2nd stage: assign values as side-effect of scanning*)
@@ -253,7 +253,7 @@
| assign _ _ = ();
(*3rd stage: static closure of final values*)
-fun closure (Token (x, y, Assignable (ref v))) = Token (x, y, Value v)
+fun closure (Token (x, y, Assignable (Unsynchronized.ref v))) = Token (x, y, Value v)
| closure tok = tok;
--- a/src/Pure/Isar/outer_syntax.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/Isar/outer_syntax.ML Tue Sep 29 18:14:08 2009 +0200
@@ -88,11 +88,11 @@
local
-val global_commands = ref (Symtab.empty: command Symtab.table);
-val global_markups = ref ([]: (string * ThyOutput.markup) list);
+val global_commands = Unsynchronized.ref (Symtab.empty: command Symtab.table);
+val global_markups = Unsynchronized.ref ([]: (string * ThyOutput.markup) list);
fun change_commands f = CRITICAL (fn () =>
- (change global_commands f;
+ (Unsynchronized.change global_commands f;
global_markups :=
Symtab.fold (fn (name, Command {markup = SOME m, ...}) => cons (name, m) | _ => I)
(! global_commands) []));
--- a/src/Pure/Isar/proof.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/Isar/proof.ML Tue Sep 29 18:14:08 2009 +0200
@@ -30,8 +30,8 @@
val enter_forward: state -> state
val goal_message: (unit -> Pretty.T) -> state -> state
val get_goal: state -> context * (thm list * thm)
- val show_main_goal: bool ref
- val verbose: bool ref
+ val show_main_goal: bool Unsynchronized.ref
+ val verbose: bool Unsynchronized.ref
val pretty_state: int -> state -> Pretty.T list
val pretty_goals: bool -> state -> Pretty.T list
val refine: Method.text -> state -> state Seq.seq
@@ -315,7 +315,7 @@
(** pretty_state **)
-val show_main_goal = ref false;
+val show_main_goal = Unsynchronized.ref false;
val verbose = ProofContext.verbose;
fun pretty_facts _ _ NONE = []
@@ -930,8 +930,8 @@
fun gen_show prep_att prepp before_qed after_qed stmt int state =
let
- val testing = ref false;
- val rule = ref (NONE: thm option);
+ val testing = Unsynchronized.ref false;
+ val rule = Unsynchronized.ref (NONE: thm option);
fun fail_msg ctxt =
"Local statement will fail to refine any pending goal" ::
(case ! rule of NONE => [] | SOME th => [ProofDisplay.string_of_rule ctxt "Failed" th])
--- a/src/Pure/Isar/proof_context.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/Isar/proof_context.ML Tue Sep 29 18:14:08 2009 +0200
@@ -123,15 +123,15 @@
val add_abbrev: string -> Properties.T ->
binding * term -> Proof.context -> (term * term) * Proof.context
val revert_abbrev: string -> string -> Proof.context -> Proof.context
- val verbose: bool ref
+ val verbose: bool Unsynchronized.ref
val setmp_verbose: ('a -> 'b) -> 'a -> 'b
val print_syntax: Proof.context -> unit
val print_abbrevs: Proof.context -> unit
val print_binds: Proof.context -> unit
val print_lthms: Proof.context -> unit
val print_cases: Proof.context -> unit
- val debug: bool ref
- val prems_limit: int ref
+ val debug: bool Unsynchronized.ref
+ val prems_limit: int Unsynchronized.ref
val pretty_ctxt: Proof.context -> Pretty.T list
val pretty_context: Proof.context -> Pretty.T list
val query_type: Proof.context -> string -> Properties.T
@@ -1208,9 +1208,9 @@
(** print context information **)
-val debug = ref false;
+val debug = Unsynchronized.ref false;
-val verbose = ref false;
+val verbose = Unsynchronized.ref false;
fun verb f x = if ! verbose then f (x ()) else [];
fun setmp_verbose f x = Library.setmp verbose true f x;
@@ -1320,7 +1320,7 @@
(* core context *)
-val prems_limit = ref ~1;
+val prems_limit = Unsynchronized.ref ~1;
fun pretty_ctxt ctxt =
if ! prems_limit < 0 andalso not (! debug) then []
--- a/src/Pure/Isar/toplevel.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/Isar/toplevel.ML Tue Sep 29 18:14:08 2009 +0200
@@ -24,12 +24,12 @@
val enter_proof_body: state -> Proof.state
val print_state_context: state -> unit
val print_state: bool -> state -> unit
- val quiet: bool ref
- val debug: bool ref
- val interact: bool ref
- val timing: bool ref
- val profiling: int ref
- val skip_proofs: bool ref
+ val quiet: bool Unsynchronized.ref
+ val debug: bool Unsynchronized.ref
+ val interact: bool Unsynchronized.ref
+ val timing: bool Unsynchronized.ref
+ val profiling: int Unsynchronized.ref
+ val skip_proofs: bool Unsynchronized.ref
exception TERMINATE
exception TOPLEVEL_ERROR
val program: (unit -> 'a) -> 'a
@@ -216,12 +216,12 @@
(** toplevel transitions **)
-val quiet = ref false;
+val quiet = Unsynchronized.ref false;
val debug = Output.debugging;
-val interact = ref false;
+val interact = Unsynchronized.ref false;
val timing = Output.timing;
-val profiling = ref 0;
-val skip_proofs = ref false;
+val profiling = Unsynchronized.ref 0;
+val skip_proofs = Unsynchronized.ref false;
exception TERMINATE = Runtime.TERMINATE;
exception EXCURSION_FAIL = Runtime.EXCURSION_FAIL;
@@ -550,9 +550,9 @@
(* post-transition hooks *)
-local val hooks = ref ([]: (transition -> state -> state -> unit) list) in
+local val hooks = Unsynchronized.ref ([]: (transition -> state -> state -> unit) list) in
-fun add_hook f = CRITICAL (fn () => change hooks (cons f));
+fun add_hook f = CRITICAL (fn () => Unsynchronized.change hooks (cons f));
fun get_hooks () = CRITICAL (fn () => ! hooks);
end;
--- a/src/Pure/ML-Systems/compiler_polyml-5.0.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/ML-Systems/compiler_polyml-5.0.ML Tue Sep 29 18:14:08 2009 +0200
@@ -5,11 +5,11 @@
fun use_text ({tune_source, print, error, ...}: use_context) (line, name) verbose txt =
let
- val in_buffer = ref (explode (tune_source txt));
- val out_buffer = ref ([]: string list);
+ val in_buffer = Unsynchronized.ref (explode (tune_source txt));
+ val out_buffer = Unsynchronized.ref ([]: string list);
fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
- val current_line = ref line;
+ val current_line = Unsynchronized.ref line;
fun get () =
(case ! in_buffer of
[] => ""
--- a/src/Pure/ML-Systems/compiler_polyml-5.2.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/ML-Systems/compiler_polyml-5.2.ML Tue Sep 29 18:14:08 2009 +0200
@@ -14,9 +14,9 @@
fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
(start_line, name) verbose txt =
let
- val current_line = ref start_line;
- val in_buffer = ref (String.explode (tune_source txt));
- val out_buffer = ref ([]: string list);
+ val current_line = Unsynchronized.ref start_line;
+ val in_buffer = Unsynchronized.ref (String.explode (tune_source txt));
+ val out_buffer = Unsynchronized.ref ([]: string list);
fun output () = drop_newline (implode (rev (! out_buffer)));
fun get () =
--- a/src/Pure/ML-Systems/compiler_polyml-5.3.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/ML-Systems/compiler_polyml-5.3.ML Tue Sep 29 18:14:08 2009 +0200
@@ -14,9 +14,9 @@
fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
(start_line, name) verbose txt =
let
- val line = ref start_line;
- val in_buffer = ref (String.explode (tune_source txt));
- val out_buffer = ref ([]: string list);
+ val line = Unsynchronized.ref start_line;
+ val in_buffer = Unsynchronized.ref (String.explode (tune_source txt));
+ val out_buffer = Unsynchronized.ref ([]: string list);
fun output () = drop_newline (implode (rev (! out_buffer)));
fun get () =
--- a/src/Pure/ML-Systems/mosml.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/ML-Systems/mosml.ML Tue Sep 29 18:14:08 2009 +0200
@@ -41,6 +41,7 @@
fun reraise exn = raise exn;
use "ML-Systems/exn.ML";
+use "ML-Systems/unsynchronized.ML";
use "ML-Systems/universal.ML";
use "ML-Systems/thread_dummy.ML";
use "ML-Systems/multithreading.ML";
--- a/src/Pure/ML-Systems/multithreading_polyml.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML Tue Sep 29 18:14:08 2009 +0200
@@ -31,7 +31,7 @@
val available = true;
-val max_threads = ref 0;
+val max_threads = Unsynchronized.ref 0;
val tested_platform =
let val ml_platform = getenv "ML_PLATFORM"
@@ -114,7 +114,7 @@
(* tracing *)
-val trace = ref 0;
+val trace = Unsynchronized.ref 0;
fun tracing level msg =
if level > ! trace then ()
@@ -148,7 +148,7 @@
fun timeLimit time f x = uninterruptible (fn restore_attributes => fn () =>
let
val worker = Thread.self ();
- val timeout = ref false;
+ val timeout = Unsynchronized.ref false;
val watchdog = Thread.fork (fn () =>
(OS.Process.sleep time; timeout := true; Thread.interrupt worker), []);
@@ -173,7 +173,7 @@
(*result state*)
datatype result = Wait | Signal | Result of int;
- val result = ref Wait;
+ val result = Unsynchronized.ref Wait;
val lock = Mutex.mutex ();
val cond = ConditionVar.conditionVar ();
fun set_result res =
@@ -231,8 +231,8 @@
local
val critical_lock = Mutex.mutex ();
-val critical_thread = ref (NONE: Thread.thread option);
-val critical_name = ref "";
+val critical_thread = Unsynchronized.ref (NONE: Thread.thread option);
+val critical_name = Unsynchronized.ref "";
in
@@ -274,7 +274,7 @@
local
val serial_lock = Mutex.mutex ();
-val serial_count = ref 0;
+val serial_count = Unsynchronized.ref 0;
in
--- a/src/Pure/ML-Systems/polyml_common.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/ML-Systems/polyml_common.ML Tue Sep 29 18:14:08 2009 +0200
@@ -6,6 +6,7 @@
exception Interrupt = SML90.Interrupt;
use "ML-Systems/exn.ML";
+use "ML-Systems/unsynchronized.ML";
use "ML-Systems/multithreading.ML";
use "ML-Systems/time_limit.ML";
use "ML-Systems/timing.ML";
@@ -19,6 +20,8 @@
val forget_structure = PolyML.Compiler.forgetStructure;
val _ = PolyML.Compiler.forgetValue "print";
+val _ = PolyML.Compiler.forgetValue "ref";
+val _ = PolyML.Compiler.forgetType "ref";
(* Compiler options *)
@@ -50,7 +53,7 @@
(* print depth *)
local
- val depth = ref 10;
+ val depth = Unsynchronized.ref 10;
in
fun get_print_depth () = ! depth;
fun print_depth n = (depth := n; PolyML.print_depth n);
--- a/src/Pure/ML-Systems/smlnj.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/ML-Systems/smlnj.ML Tue Sep 29 18:14:08 2009 +0200
@@ -9,6 +9,7 @@
use "ML-Systems/proper_int.ML";
use "ML-Systems/overloading_smlnj.ML";
use "ML-Systems/exn.ML";
+use "ML-Systems/unsynchronized.ML";
use "ML-Systems/universal.ML";
use "ML-Systems/thread_dummy.ML";
use "ML-Systems/multithreading.ML";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/unsynchronized.ML Tue Sep 29 18:14:08 2009 +0200
@@ -0,0 +1,25 @@
+(* Title: Pure/ML-Systems/unsynchronized.ML
+ Author: Makarius
+
+Raw ML references as unsynchronized state variables.
+*)
+
+structure Unsynchronized =
+struct
+
+datatype ref = datatype ref;
+
+val op := = op :=;
+val ! = !;
+
+fun set flag = (flag := true; true);
+fun reset flag = (flag := false; false);
+fun toggle flag = (flag := not (! flag); ! flag);
+
+fun change r f = r := f (! r);
+fun change_result r f = let val (x, y) = f (! r) in r := y; x end;
+
+fun inc i = (i := ! i + (1: int); ! i);
+fun dec i = (i := ! i - (1: int); ! i);
+
+end;
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML Tue Sep 29 18:14:08 2009 +0200
@@ -91,8 +91,8 @@
if null toks then Position.none
else ML_Lex.end_pos_of (List.last toks);
- val input_buffer = ref (input @ [(offset_of end_pos, #"\n")]);
- val line = ref (the_default 1 (Position.line_of pos));
+ val input_buffer = Unsynchronized.ref (input @ [(offset_of end_pos, #"\n")]);
+ val line = Unsynchronized.ref (the_default 1 (Position.line_of pos));
fun get_offset () = (case ! input_buffer of [] => 0 | (i, _) :: _ => i);
fun get () =
@@ -106,9 +106,9 @@
(* output *)
- val output_buffer = ref Buffer.empty;
+ val output_buffer = Unsynchronized.ref Buffer.empty;
fun output () = Buffer.content (! output_buffer);
- fun put s = change output_buffer (Buffer.add s);
+ fun put s = Unsynchronized.change output_buffer (Buffer.add s);
fun put_message {message, hard, location, context = _} =
(put ((if hard then "Error" else "Warning") ^ Position.str_of (position_of location) ^ ":\n");
--- a/src/Pure/ML/ml_context.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/ML/ml_context.ML Tue Sep 29 18:14:08 2009 +0200
@@ -19,20 +19,21 @@
val the_global_context: unit -> theory
val the_local_context: unit -> Proof.context
val exec: (unit -> unit) -> Context.generic -> Context.generic
- val stored_thms: thm list ref
+ val stored_thms: thm list Unsynchronized.ref
val ml_store_thm: string * thm -> unit
val ml_store_thms: string * thm list -> unit
type antiq =
{struct_name: string, background: Proof.context} ->
(Proof.context -> string * string) * Proof.context
val add_antiq: string -> (Position.T -> antiq context_parser) -> unit
- val trace: bool ref
+ val trace: bool Unsynchronized.ref
val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
Context.generic option -> (ML_Lex.token list * ML_Lex.token list) * Context.generic option
val eval: bool -> Position.T -> Symbol_Pos.text -> unit
val eval_file: Path.T -> unit
val eval_in: Proof.context option -> bool -> Position.T -> Symbol_Pos.text -> unit
- val evaluate: Proof.context -> bool -> string * (unit -> 'a) option ref -> string -> 'a
+ val evaluate: Proof.context -> bool ->
+ string * (unit -> 'a) option Unsynchronized.ref -> string -> 'a
val expression: Position.T -> string -> string -> string -> Context.generic -> Context.generic
end
@@ -53,7 +54,7 @@
(* theorem bindings *)
-val stored_thms: thm list ref = ref [];
+val stored_thms: thm list Unsynchronized.ref = Unsynchronized.ref [];
fun ml_store sel (name, ths) =
let
@@ -89,12 +90,13 @@
local
-val global_parsers = ref (Symtab.empty: (Position.T -> antiq context_parser) Symtab.table);
+val global_parsers =
+ Unsynchronized.ref (Symtab.empty: (Position.T -> antiq context_parser) Symtab.table);
in
fun add_antiq name scan = CRITICAL (fn () =>
- change global_parsers (fn tab =>
+ Unsynchronized.change global_parsers (fn tab =>
(if not (Symtab.defined tab name) then ()
else warning ("Redefined ML antiquotation: " ^ quote name);
Symtab.update (name, scan) tab)));
@@ -162,7 +164,7 @@
in (ml, SOME (Context.Proof ctxt')) end;
in ((begin_env @ ml_env @ end_env, ml_body), opt_ctxt') end;
-val trace = ref false;
+val trace = Unsynchronized.ref false;
fun eval verbose pos txt =
let
--- a/src/Pure/Proof/extraction.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/Proof/extraction.ML Tue Sep 29 18:14:08 2009 +0200
@@ -91,7 +91,7 @@
Pattern.rewrite_term thy [] (condrew' :: procs) tm
and condrew' tm =
let
- val cache = ref ([] : (term * term) list);
+ val cache = Unsynchronized.ref ([] : (term * term) list);
fun lookup f x = (case AList.lookup (op =) (!cache) x of
NONE =>
let val y = f x
--- a/src/Pure/Proof/reconstruct.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/Proof/reconstruct.ML Tue Sep 29 18:14:08 2009 +0200
@@ -6,7 +6,7 @@
signature RECONSTRUCT =
sig
- val quiet_mode : bool ref
+ val quiet_mode : bool Unsynchronized.ref
val reconstruct_proof : theory -> term -> Proofterm.proof -> Proofterm.proof
val prop_of' : term list -> Proofterm.proof -> term
val prop_of : Proofterm.proof -> term
@@ -19,7 +19,7 @@
open Proofterm;
-val quiet_mode = ref true;
+val quiet_mode = Unsynchronized.ref true;
fun message s = if !quiet_mode then () else writeln s;
fun vars_of t = map Var (rev (Term.add_vars t []));
--- a/src/Pure/ProofGeneral/preferences.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/ProofGeneral/preferences.ML Tue Sep 29 18:14:08 2009 +0200
@@ -18,11 +18,11 @@
get: unit -> string,
set: string -> unit}
val generic_pref: ('a -> string) -> (string -> 'a) -> PgipTypes.pgiptype ->
- 'a ref -> string -> string -> preference
- val string_pref: string ref -> string -> string -> preference
- val int_pref: int ref -> string -> string -> preference
- val nat_pref: int ref -> string -> string -> preference
- val bool_pref: bool ref -> string -> string -> preference
+ 'a Unsynchronized.ref -> string -> string -> preference
+ val string_pref: string Unsynchronized.ref -> string -> string -> preference
+ val int_pref: int Unsynchronized.ref -> string -> string -> preference
+ val nat_pref: int Unsynchronized.ref -> string -> string -> preference
+ val bool_pref: bool Unsynchronized.ref -> string -> string -> preference
type T = (string * preference list) list
val pure_preferences: T
val remove: string -> T -> T
@@ -95,8 +95,9 @@
let
fun get () = PgipTypes.bool_to_pgstring (print_mode_active thm_depsN);
fun set s =
- if PgipTypes.read_pgipbool s then change print_mode (insert (op =) thm_depsN)
- else change print_mode (remove (op =) thm_depsN);
+ if PgipTypes.read_pgipbool s
+ then Unsynchronized.change print_mode (insert (op =) thm_depsN)
+ else Unsynchronized.change print_mode (remove (op =) thm_depsN);
in
mkpref get set PgipTypes.Pgipbool "theorem-dependencies"
"Track theorem dependencies within Proof General"
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Tue Sep 29 18:14:08 2009 +0200
@@ -226,7 +226,7 @@
(* init *)
-val initialized = ref false;
+val initialized = Unsynchronized.ref false;
fun init false = panic "No Proof General interface support for Isabelle/classic mode."
| init true =
@@ -239,9 +239,9 @@
ProofGeneralPgip.init_pgip_channel (! Output.priority_fn);
setup_thy_loader ();
setup_present_hook ();
- set initialized);
+ Unsynchronized.set initialized);
sync_thy_loader ();
- change print_mode (update (op =) proof_generalN);
+ Unsynchronized.change print_mode (update (op =) proof_generalN);
Isar.toplevel_loop {init = true, welcome = true, sync = true, secure = Secure.is_secure ()});
end;
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Tue Sep 29 18:14:08 2009 +0200
@@ -32,20 +32,20 @@
(** print mode **)
val proof_generalN = "ProofGeneral";
-val pgmlsymbols_flag = ref true;
+val pgmlsymbols_flag = Unsynchronized.ref true;
(* assembling and issuing PGIP packets *)
-val pgip_refid = ref NONE: string option ref;
-val pgip_refseq = ref NONE: int option ref;
+val pgip_refid = Unsynchronized.ref NONE: string option Unsynchronized.ref;
+val pgip_refseq = Unsynchronized.ref NONE: int option Unsynchronized.ref;
local
val pgip_class = "pg"
val pgip_tag = "Isabelle/Isar"
- val pgip_id = ref ""
- val pgip_seq = ref 0
- fun pgip_serial () = inc pgip_seq
+ val pgip_id = Unsynchronized.ref ""
+ val pgip_seq = Unsynchronized.ref 0
+ fun pgip_serial () = Unsynchronized.inc pgip_seq
fun assemble_pgips pgips =
Pgip { tag = SOME pgip_tag,
@@ -65,7 +65,7 @@
fun matching_pgip_id id = (id = ! pgip_id)
-val output_xml_fn = ref Output.writeln_default
+val output_xml_fn = Unsynchronized.ref Output.writeln_default
fun output_xml s = ! output_xml_fn (XML.string_of s);
val output_pgips = XML.string_of o PgipOutput.output o assemble_pgips o map PgipOutput.output;
@@ -280,7 +280,7 @@
(* theorem dependeny output *)
-val show_theorem_dependencies = ref false;
+val show_theorem_dependencies = Unsynchronized.ref false;
local
@@ -368,13 +368,13 @@
(* Preferences: tweak for PGIP interfaces *)
-val preferences = ref Preferences.pure_preferences;
+val preferences = Unsynchronized.ref Preferences.pure_preferences;
fun add_preference cat pref =
- CRITICAL (fn () => change preferences (Preferences.add cat pref));
+ CRITICAL (fn () => Unsynchronized.change preferences (Preferences.add cat pref));
fun setup_preferences_tweak () =
- CRITICAL (fn () => change preferences
+ CRITICAL (fn () => Unsynchronized.change preferences
(Preferences.set_default ("show-question-marks", "false") #>
Preferences.remove "show-question-marks" #> (* we use markup, not ?s *)
Preferences.remove "theorem-dependencies" #> (* set internally *)
@@ -471,7 +471,7 @@
fun set_proverflag_pgmlsymbols b =
(pgmlsymbols_flag := b;
NAMED_CRITICAL "print_mode" (fn () =>
- change print_mode
+ Unsynchronized.change print_mode
(fn mode =>
remove (op =) Symbol.xsymbolsN mode @ (if b then [Symbol.xsymbolsN] else []))))
@@ -677,7 +677,7 @@
about this special status, but for now we just keep a local reference.
*)
-val currently_open_file = ref (NONE : pgipurl option)
+val currently_open_file = Unsynchronized.ref (NONE : pgipurl option)
fun get_currently_open_file () = ! currently_open_file;
@@ -779,7 +779,7 @@
*)
local
- val current_working_dir = ref (NONE : string option)
+ val current_working_dir = Unsynchronized.ref (NONE : string option)
in
fun changecwd_dir newdirpath =
let
@@ -1021,7 +1021,7 @@
(* init *)
-val initialized = ref false;
+val initialized = Unsynchronized.ref false;
fun init_pgip false = panic "No Proof General interface support for Isabelle/classic mode."
| init_pgip true =
@@ -1035,9 +1035,9 @@
setup_present_hook ();
init_pgip_session_id ();
welcome ();
- set initialized);
+ Unsynchronized.set initialized);
sync_thy_loader ();
- change print_mode (update (op =) proof_generalN);
+ Unsynchronized.change print_mode (update (op =) proof_generalN);
pgip_toplevel tty_src);
@@ -1045,7 +1045,7 @@
(** Out-of-loop PGIP commands (for Emacs hybrid mode) **)
local
- val pgip_output_channel = ref Output.writeln_default
+ val pgip_output_channel = Unsynchronized.ref Output.writeln_default
in
(* Set recipient for PGIP results *)
--- a/src/Pure/ROOT.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/ROOT.ML Tue Sep 29 18:14:08 2009 +0200
@@ -8,7 +8,7 @@
end;
(*if true then some tools will OMIT some proofs*)
-val quick_and_dirty = ref false;
+val quick_and_dirty = Unsynchronized.ref false;
print_depth 10;
--- a/src/Pure/Syntax/ast.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/Syntax/ast.ML Tue Sep 29 18:14:08 2009 +0200
@@ -24,8 +24,8 @@
val fold_ast_p: string -> ast list * ast -> ast
val unfold_ast: string -> ast -> ast list
val unfold_ast_p: string -> ast -> ast list * ast
- val trace_ast: bool ref
- val stat_ast: bool ref
+ val trace_ast: bool Unsynchronized.ref
+ val stat_ast: bool Unsynchronized.ref
end;
signature AST =
@@ -173,9 +173,9 @@
fun normalize trace stat get_rules pre_ast =
let
- val passes = ref 0;
- val failed_matches = ref 0;
- val changes = ref 0;
+ val passes = Unsynchronized.ref 0;
+ val failed_matches = Unsynchronized.ref 0;
+ val changes = Unsynchronized.ref 0;
fun subst _ (ast as Constant _) = ast
| subst env (Variable x) = the (Symtab.lookup env x)
@@ -184,8 +184,8 @@
fun try_rules ((lhs, rhs) :: pats) ast =
(case match ast lhs of
SOME (env, args) =>
- (inc changes; SOME (mk_appl (subst env rhs) args))
- | NONE => (inc failed_matches; try_rules pats ast))
+ (Unsynchronized.inc changes; SOME (mk_appl (subst env rhs) args))
+ | NONE => (Unsynchronized.inc failed_matches; try_rules pats ast))
| try_rules [] _ = NONE;
val try_headless_rules = try_rules (get_rules "");
@@ -226,7 +226,7 @@
val old_changes = ! changes;
val new_ast = norm ast;
in
- inc passes;
+ Unsynchronized.inc passes;
if old_changes = ! changes then new_ast else normal new_ast
end;
@@ -245,8 +245,8 @@
(* normalize_ast *)
-val trace_ast = ref false;
-val stat_ast = ref false;
+val trace_ast = Unsynchronized.ref false;
+val stat_ast = Unsynchronized.ref false;
fun normalize_ast get_rules ast =
normalize (! trace_ast) (! stat_ast) get_rules ast;
--- a/src/Pure/Syntax/parser.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/Syntax/parser.ML Tue Sep 29 18:14:08 2009 +0200
@@ -17,7 +17,7 @@
Tip of Lexicon.token
val parse: gram -> string -> Lexicon.token list -> parsetree list
val guess_infix_lr: gram -> string -> (string * bool * bool * int) option
- val branching_level: int ref
+ val branching_level: int Unsynchronized.ref
end;
structure Parser: PARSER =
@@ -690,7 +690,7 @@
else movedot_lambda (B, j, tss, Nonterminal (A, k) :: sa, id, i) ts;
-val branching_level = ref 600; (*trigger value for warnings*)
+val branching_level = Unsynchronized.ref 600; (*trigger value for warnings*)
(*get all productions of a NT and NTs chained to it which can
be started by specified token*)
@@ -821,7 +821,7 @@
val Estate = Array.array (s, []);
in
Array.update (Estate, 0, S0);
- get_trees (produce (ref false) prods tags chains Estate 0 indata eof)
+ get_trees (produce (Unsynchronized.ref false) prods tags chains Estate 0 indata eof)
end;
--- a/src/Pure/Syntax/printer.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/Syntax/printer.ML Tue Sep 29 18:14:08 2009 +0200
@@ -6,11 +6,11 @@
signature PRINTER0 =
sig
- val show_brackets: bool ref
- val show_sorts: bool ref
- val show_types: bool ref
- val show_no_free_types: bool ref
- val show_all_types: bool ref
+ val show_brackets: bool Unsynchronized.ref
+ val show_sorts: bool Unsynchronized.ref
+ val show_types: bool Unsynchronized.ref
+ val show_no_free_types: bool Unsynchronized.ref
+ val show_all_types: bool Unsynchronized.ref
val pp_show_brackets: Pretty.pp -> Pretty.pp
end;
@@ -42,11 +42,11 @@
(** options for printing **)
-val show_types = ref false;
-val show_sorts = ref false;
-val show_brackets = ref false;
-val show_no_free_types = ref false;
-val show_all_types = ref false;
+val show_types = Unsynchronized.ref false;
+val show_sorts = Unsynchronized.ref false;
+val show_brackets = Unsynchronized.ref false;
+val show_no_free_types = Unsynchronized.ref false;
+val show_all_types = Unsynchronized.ref false;
fun pp_show_brackets pp = Pretty.pp (setmp show_brackets true (Pretty.term pp),
Pretty.typ pp, Pretty.sort pp, Pretty.classrel pp, Pretty.arity pp);
--- a/src/Pure/Syntax/syn_trans.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/Syntax/syn_trans.ML Tue Sep 29 18:14:08 2009 +0200
@@ -6,7 +6,7 @@
signature SYN_TRANS0 =
sig
- val eta_contract: bool ref
+ val eta_contract: bool Unsynchronized.ref
val atomic_abs_tr': string * typ * term -> term * term
val preserve_binder_abs_tr': string -> string -> string * (term list -> term)
val preserve_binder_abs2_tr': string -> string -> string * (term list -> term)
@@ -276,7 +276,7 @@
(*do (partial) eta-contraction before printing*)
-val eta_contract = ref true;
+val eta_contract = Unsynchronized.ref true;
fun eta_contr tm =
let
--- a/src/Pure/Syntax/syntax.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/Syntax/syntax.ML Tue Sep 29 18:14:08 2009 +0200
@@ -36,9 +36,9 @@
val print_syntax: syntax -> unit
val guess_infix: syntax -> string -> mixfix option
val read_token: string -> Symbol_Pos.T list * Position.T
- val ambiguity_is_error: bool ref
- val ambiguity_level: int ref
- val ambiguity_limit: int ref
+ val ambiguity_is_error: bool Unsynchronized.ref
+ val ambiguity_level: int Unsynchronized.ref
+ val ambiguity_limit: int Unsynchronized.ref
val standard_parse_term: Pretty.pp -> (term -> string option) ->
(((string * int) * sort) list -> string * int -> Term.sort) ->
(string -> bool * string) -> (string -> string option) ->
@@ -472,9 +472,9 @@
(* read_ast *)
-val ambiguity_is_error = ref false;
-val ambiguity_level = ref 1;
-val ambiguity_limit = ref 10;
+val ambiguity_is_error = Unsynchronized.ref false;
+val ambiguity_level = Unsynchronized.ref 1;
+val ambiguity_limit = Unsynchronized.ref 10;
fun ambiguity_msg pos = "Parse error: ambiguous syntax" ^ Position.str_of pos;
@@ -711,7 +711,7 @@
unparse_typ: Proof.context -> typ -> Pretty.T,
unparse_term: Proof.context -> term -> Pretty.T};
- val operations = ref (NONE: operations option);
+ val operations = Unsynchronized.ref (NONE: operations option);
fun operation which ctxt x =
(case ! operations of
--- a/src/Pure/System/isabelle_process.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/System/isabelle_process.ML Tue Sep 29 18:14:08 2009 +0200
@@ -130,7 +130,7 @@
(* init *)
fun init out =
- (change print_mode (update (op =) isabelle_processN);
+ (Unsynchronized.change print_mode (update (op =) isabelle_processN);
setup_channels out |> init_message;
OuterKeyword.report ();
Output.status (Markup.markup Markup.ready "");
--- a/src/Pure/System/isar.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/System/isar.ML Tue Sep 29 18:14:08 2009 +0200
@@ -18,7 +18,7 @@
val undo: int -> unit
val kill: unit -> unit
val kill_proof: unit -> unit
- val crashes: exn list ref
+ val crashes: exn list Unsynchronized.ref
val toplevel_loop: {init: bool, welcome: bool, sync: bool, secure: bool} -> unit
val loop: unit -> unit
val main: unit -> unit
@@ -36,9 +36,9 @@
(*previous state, state transition -- regular commands only*)
local
- val global_history = ref ([]: history);
- val global_state = ref Toplevel.toplevel;
- val global_exn = ref (NONE: (exn * string) option);
+ val global_history = Unsynchronized.ref ([]: history);
+ val global_state = Unsynchronized.ref Toplevel.toplevel;
+ val global_exn = Unsynchronized.ref (NONE: (exn * string) option);
in
fun edit_history count f = NAMED_CRITICAL "Isar" (fn () =>
@@ -115,7 +115,7 @@
(* toplevel loop *)
-val crashes = ref ([]: exn list);
+val crashes = Unsynchronized.ref ([]: exn list);
local
@@ -130,7 +130,7 @@
handle exn =>
(Output.error_msg (ML_Compiler.exn_message exn)
handle crash =>
- (CRITICAL (fn () => change crashes (cons crash));
+ (CRITICAL (fn () => Unsynchronized.change crashes (cons crash));
warning "Recovering from Isar toplevel crash -- see also Isar.crashes");
raw_loop secure src)
end;
@@ -139,6 +139,7 @@
fun toplevel_loop {init = do_init, welcome, sync, secure} =
(Context.set_thread_data NONE;
+ Secure.open_unsynchronized ();
if do_init then init () else ();
if welcome then writeln (Session.welcome ()) else ();
uninterruptible (fn _ => fn () => raw_loop secure (OuterSyntax.isar sync)) ());
--- a/src/Pure/System/session.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/System/session.ML Tue Sep 29 18:14:08 2009 +0200
@@ -21,10 +21,10 @@
(* session state *)
-val session = ref ([Context.PureN]: string list);
-val session_path = ref ([]: string list);
-val session_finished = ref false;
-val remote_path = ref (NONE: Url.T option);
+val session = Unsynchronized.ref ([Context.PureN]: string list);
+val session_path = Unsynchronized.ref ([]: string list);
+val session_finished = Unsynchronized.ref false;
+val remote_path = Unsynchronized.ref (NONE: Url.T option);
(* access path *)
--- a/src/Pure/Thy/html.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/Thy/html.ML Tue Sep 29 18:14:08 2009 +0200
@@ -267,8 +267,8 @@
(* document *)
-val charset = ref "ISO-8859-1";
-fun with_charset s = setmp_noncritical charset s;
+val charset = Unsynchronized.ref "ISO-8859-1";
+fun with_charset s = setmp_noncritical charset s; (* FIXME *)
fun begin_document title =
let val cs = ! charset in
--- a/src/Pure/Thy/present.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/Thy/present.ML Tue Sep 29 18:14:08 2009 +0200
@@ -161,10 +161,11 @@
(* state *)
-val browser_info = ref empty_browser_info;
-fun change_browser_info f = CRITICAL (fn () => change browser_info (map_browser_info f));
+val browser_info = Unsynchronized.ref empty_browser_info;
+fun change_browser_info f =
+ CRITICAL (fn () => Unsynchronized.change browser_info (map_browser_info f));
-val suppress_tex_source = ref false;
+val suppress_tex_source = Unsynchronized.ref false;
fun no_document f x = setmp_noncritical suppress_tex_source true f x;
fun init_theory_info name info =
@@ -229,7 +230,7 @@
(* state *)
-val session_info = ref (NONE: session_info option);
+val session_info = Unsynchronized.ref (NONE: session_info option);
fun with_session x f = (case ! session_info of NONE => x | SOME info => f info);
fun with_context f = f (Context.theory_name (ML_Context.the_global_context ()));
@@ -534,5 +535,5 @@
end;
-structure BasicPresent: BASIC_PRESENT = Present;
-open BasicPresent;
+structure Basic_Present: BASIC_PRESENT = Present;
+open Basic_Present;
--- a/src/Pure/Thy/thy_info.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/Thy/thy_info.ML Tue Sep 29 18:14:08 2009 +0200
@@ -50,9 +50,9 @@
val str_of_action = fn Update => "Update" | Outdate => "Outdate" | Remove => "Remove";
local
- val hooks = ref ([]: (action -> string -> unit) list);
+ val hooks = Unsynchronized.ref ([]: (action -> string -> unit) list);
in
- fun add_hook f = CRITICAL (fn () => change hooks (cons f));
+ fun add_hook f = CRITICAL (fn () => Unsynchronized.change hooks (cons f));
fun perform action name = List.app (fn f => (try (fn () => f action name) (); ())) (! hooks);
end;
@@ -111,10 +111,10 @@
type thy = deps option * theory option;
local
- val database = ref (Graph.empty: thy Graph.T);
+ val database = Unsynchronized.ref (Graph.empty: thy Graph.T);
in
fun get_thys () = ! database;
- fun change_thys f = CRITICAL (fn () => Library.change database f);
+ fun change_thys f = CRITICAL (fn () => Unsynchronized.change database f);
end;
--- a/src/Pure/Thy/thy_load.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/Thy/thy_load.ML Tue Sep 29 18:14:08 2009 +0200
@@ -37,14 +37,16 @@
(* maintain load path *)
-local val load_path = ref [Path.current] in
+local val load_path = Unsynchronized.ref [Path.current] in
fun show_path () = map Path.implode (! load_path);
-fun del_path s = CRITICAL (fn () => change load_path (remove (op =) (Path.explode s)));
-fun add_path s = CRITICAL (fn () => (del_path s; change load_path (cons (Path.explode s))));
-fun path_add s =
- CRITICAL (fn () => (del_path s; change load_path (fn path => path @ [Path.explode s])));
+fun del_path s = CRITICAL (fn () =>
+ Unsynchronized.change load_path (remove (op =) (Path.explode s)));
+fun add_path s = CRITICAL (fn () =>
+ (del_path s; Unsynchronized.change load_path (cons (Path.explode s))));
+fun path_add s = CRITICAL (fn () =>
+ (del_path s; Unsynchronized.change load_path (fn path => path @ [Path.explode s])));
fun reset_path () = load_path := [Path.current];
fun with_paths ss f x =
@@ -124,5 +126,5 @@
end;
-structure BasicThyLoad: BASIC_THY_LOAD = ThyLoad;
-open BasicThyLoad;
+structure Basic_Thy_Load: BASIC_THY_LOAD = ThyLoad;
+open Basic_Thy_Load;
--- a/src/Pure/Thy/thy_output.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/Thy/thy_output.ML Tue Sep 29 18:14:08 2009 +0200
@@ -6,11 +6,11 @@
signature THY_OUTPUT =
sig
- val display: bool ref
- val quotes: bool ref
- val indent: int ref
- val source: bool ref
- val break: bool ref
+ val display: bool Unsynchronized.ref
+ val quotes: bool Unsynchronized.ref
+ val indent: int Unsynchronized.ref
+ val source: bool Unsynchronized.ref
+ val break: bool Unsynchronized.ref
val add_commands: (string * (Args.src -> Toplevel.state -> string)) list -> unit
val add_options: (string * (string -> (unit -> string) -> unit -> string)) list -> unit
val defined_command: string -> bool
@@ -21,7 +21,7 @@
val antiquotation: string -> 'a context_parser ->
({state: Toplevel.state, source: Args.src, context: Proof.context} -> 'a -> string) -> unit
datatype markup = Markup | MarkupEnv | Verbatim
- val modes: string list ref
+ val modes: string list Unsynchronized.ref
val eval_antiquote: Scan.lexicon -> Toplevel.state -> Symbol_Pos.text * Position.T -> string
val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
(Toplevel.transition * Toplevel.state) list -> (OuterLex.token, 'a) Source.source -> Buffer.T
@@ -42,11 +42,11 @@
(** global options **)
-val display = ref false;
-val quotes = ref false;
-val indent = ref 0;
-val source = ref false;
-val break = ref false;
+val display = Unsynchronized.ref false;
+val quotes = Unsynchronized.ref false;
+val indent = Unsynchronized.ref 0;
+val source = Unsynchronized.ref false;
+val break = Unsynchronized.ref false;
@@ -55,10 +55,10 @@
local
val global_commands =
- ref (Symtab.empty: (Args.src -> Toplevel.state -> string) Symtab.table);
+ Unsynchronized.ref (Symtab.empty: (Args.src -> Toplevel.state -> string) Symtab.table);
val global_options =
- ref (Symtab.empty: (string -> (unit -> string) -> unit -> string) Symtab.table);
+ Unsynchronized.ref (Symtab.empty: (string -> (unit -> string) -> unit -> string) Symtab.table);
fun add_item kind (name, x) tab =
(if not (Symtab.defined tab name) then ()
@@ -67,8 +67,10 @@
in
-fun add_commands xs = CRITICAL (fn () => change global_commands (fold (add_item "command") xs));
-fun add_options xs = CRITICAL (fn () => change global_options (fold (add_item "option") xs));
+fun add_commands xs =
+ CRITICAL (fn () => Unsynchronized.change global_commands (fold (add_item "command") xs));
+fun add_options xs =
+ CRITICAL (fn () => Unsynchronized.change global_options (fold (add_item "option") xs));
fun defined_command name = Symtab.defined (! global_commands) name;
fun defined_option name = Symtab.defined (! global_options) name;
@@ -143,7 +145,7 @@
(* eval_antiquote *)
-val modes = ref ([]: string list);
+val modes = Unsynchronized.ref ([]: string list);
fun eval_antiquote lex state (txt, pos) =
let
--- a/src/Pure/Tools/find_theorems.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/Tools/find_theorems.ML Tue Sep 29 18:14:08 2009 +0200
@@ -9,8 +9,8 @@
datatype 'term criterion =
Name of string | Intro | IntroIff | Elim | Dest | Solves | Simp of 'term |
Pattern of 'term
- val tac_limit: int ref
- val limit: int ref
+ val tac_limit: int Unsynchronized.ref
+ val limit: int Unsynchronized.ref
val find_theorems: Proof.context -> thm option -> int option -> bool ->
(bool * string criterion) list -> int option * (Facts.ref * thm) list
val pretty_thm: Proof.context -> Facts.ref * thm -> Pretty.T
@@ -186,7 +186,7 @@
end
else NONE
-val tac_limit = ref 5;
+val tac_limit = Unsynchronized.ref 5;
fun filter_solves ctxt goal =
let
@@ -372,7 +372,7 @@
(Facts.dest_static [] (PureThy.facts_of (ProofContext.theory_of ctxt)) @
Facts.dest_static [] (ProofContext.facts_of ctxt));
-val limit = ref 40;
+val limit = Unsynchronized.ref 40;
fun find_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
let
--- a/src/Pure/codegen.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/codegen.ML Tue Sep 29 18:14:08 2009 +0200
@@ -6,10 +6,10 @@
signature CODEGEN =
sig
- val quiet_mode : bool ref
+ val quiet_mode : bool Unsynchronized.ref
val message : string -> unit
- val mode : string list ref
- val margin : int ref
+ val mode : string list Unsynchronized.ref
+ val margin : int Unsynchronized.ref
val string_of : Pretty.T -> string
val str : string -> Pretty.T
@@ -75,9 +75,9 @@
val mk_type: bool -> typ -> Pretty.T
val mk_term_of: codegr -> string -> bool -> typ -> Pretty.T
val mk_gen: codegr -> string -> bool -> string list -> string -> typ -> Pretty.T
- val test_fn: (int -> term list option) ref
+ val test_fn: (int -> term list option) Unsynchronized.ref
val test_term: Proof.context -> term -> int -> term list option
- val eval_result: (unit -> term) ref
+ val eval_result: (unit -> term) Unsynchronized.ref
val eval_term: theory -> term -> term
val evaluation_conv: cterm -> thm
val parse_mixfix: (string -> 'a) -> string -> 'a mixfix list
@@ -102,12 +102,12 @@
structure Codegen : CODEGEN =
struct
-val quiet_mode = ref true;
+val quiet_mode = Unsynchronized.ref true;
fun message s = if !quiet_mode then () else writeln s;
-val mode = ref ([] : string list);
+val mode = Unsynchronized.ref ([] : string list);
-val margin = ref 80;
+val margin = Unsynchronized.ref 80;
fun string_of p = (Pretty.string_of |>
PrintMode.setmp [] |>
@@ -878,7 +878,8 @@
[mk_gen gr module true xs a T, mk_type true T]) Ts) @
(if member (op =) xs s then [str a] else []))));
-val test_fn : (int -> term list option) ref = ref (fn _ => NONE);
+val test_fn : (int -> term list option) Unsynchronized.ref =
+ Unsynchronized.ref (fn _ => NONE);
fun test_term ctxt t =
let
@@ -912,7 +913,7 @@
(**** Evaluator for terms ****)
-val eval_result = ref (fn () => Bound 0);
+val eval_result = Unsynchronized.ref (fn () => Bound 0);
fun eval_term thy t =
let
--- a/src/Pure/context.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/context.ML Tue Sep 29 18:14:08 2009 +0200
@@ -107,7 +107,7 @@
extend: Object.T -> Object.T,
merge: Pretty.pp -> Object.T * Object.T -> Object.T};
-val kinds = ref (Datatab.empty: kind Datatab.table);
+val kinds = Unsynchronized.ref (Datatab.empty: kind Datatab.table);
fun invoke f k =
(case Datatab.lookup (! kinds) k of
@@ -125,7 +125,7 @@
let
val k = serial ();
val kind = {empty = empty, copy = copy, extend = extend, merge = merge};
- val _ = CRITICAL (fn () => change kinds (Datatab.update (k, kind)));
+ val _ = CRITICAL (fn () => Unsynchronized.change kinds (Datatab.update (k, kind)));
in k end;
val copy_data = Datatab.map' invoke_copy;
@@ -149,7 +149,7 @@
datatype theory =
Theory of
(*identity*)
- {self: theory ref option, (*dynamic self reference -- follows theory changes*)
+ {self: theory Unsynchronized.ref option, (*dynamic self reference -- follows theory changes*)
draft: bool, (*draft mode -- linear destructive changes*)
id: serial, (*identifier*)
ids: unit Inttab.table} * (*cumulative identifiers of non-drafts -- symbolic body content*)
@@ -186,14 +186,15 @@
fun eq_id (i: int, j) = i = j;
fun is_stale
- (Theory ({self = SOME (ref (Theory ({id = id', ...}, _, _, _))), id, ...}, _, _, _)) =
+ (Theory ({self =
+ SOME (Unsynchronized.ref (Theory ({id = id', ...}, _, _, _))), id, ...}, _, _, _)) =
not (eq_id (id, id'))
| is_stale (Theory ({self = NONE, ...}, _, _, _)) = true;
fun vitalize (thy as Theory ({self = SOME r, ...}, _, _, _)) = (r := thy; thy)
| vitalize (thy as Theory ({self = NONE, draft, id, ids}, data, ancestry, history)) =
let
- val r = ref thy;
+ val r = Unsynchronized.ref thy;
val thy' = Theory (make_identity (SOME r) draft id ids, data, ancestry, history);
in r := thy'; thy' end;
@@ -243,9 +244,9 @@
theory in external data structures -- a plain theory value would
become stale as the self reference moves on*)
-datatype theory_ref = TheoryRef of theory ref;
+datatype theory_ref = TheoryRef of theory Unsynchronized.ref;
-fun deref (TheoryRef (ref thy)) = thy;
+fun deref (TheoryRef (Unsynchronized.ref thy)) = thy;
fun check_thy thy = (*thread-safe version*)
let val thy_ref = TheoryRef (the_self thy) in
@@ -437,7 +438,7 @@
local
-val kinds = ref (Datatab.empty: (theory -> Object.T) Datatab.table);
+val kinds = Unsynchronized.ref (Datatab.empty: (theory -> Object.T) Datatab.table);
fun invoke_init k =
(case Datatab.lookup (! kinds) k of
@@ -470,7 +471,7 @@
fun declare init =
let
val k = serial ();
- val _ = CRITICAL (fn () => change kinds (Datatab.update (k, init)));
+ val _ = CRITICAL (fn () => Unsynchronized.change kinds (Datatab.update (k, init)));
in k end;
fun get k dest prf =
--- a/src/Pure/display.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/display.ML Tue Sep 29 18:14:08 2009 +0200
@@ -7,10 +7,10 @@
signature BASIC_DISPLAY =
sig
- val goals_limit: int ref
- val show_consts: bool ref
- val show_hyps: bool ref
- val show_tags: bool ref
+ val goals_limit: int Unsynchronized.ref
+ val show_consts: bool Unsynchronized.ref
+ val show_hyps: bool Unsynchronized.ref
+ val show_tags: bool Unsynchronized.ref
end;
signature DISPLAY =
@@ -39,8 +39,8 @@
val goals_limit = Goal_Display.goals_limit;
val show_consts = Goal_Display.show_consts;
-val show_hyps = ref false; (*false: print meta-hypotheses as dots*)
-val show_tags = ref false; (*false: suppress tags*)
+val show_hyps = Unsynchronized.ref false; (*false: print meta-hypotheses as dots*)
+val show_tags = Unsynchronized.ref false; (*false: suppress tags*)
--- a/src/Pure/goal.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/goal.ML Tue Sep 29 18:14:08 2009 +0200
@@ -6,7 +6,7 @@
signature BASIC_GOAL =
sig
- val parallel_proofs: int ref
+ val parallel_proofs: int Unsynchronized.ref
val SELECT_GOAL: tactic -> int -> tactic
val CONJUNCTS: tactic -> int -> tactic
val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
@@ -102,7 +102,7 @@
(* future_enabled *)
-val parallel_proofs = ref 1;
+val parallel_proofs = Unsynchronized.ref 1;
fun future_enabled () =
Multithreading.enabled () andalso Future.is_worker () andalso ! parallel_proofs >= 1;
--- a/src/Pure/goal_display.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/goal_display.ML Tue Sep 29 18:14:08 2009 +0200
@@ -7,8 +7,8 @@
signature GOAL_DISPLAY =
sig
- val goals_limit: int ref
- val show_consts: bool ref
+ val goals_limit: int Unsynchronized.ref
+ val show_consts: bool Unsynchronized.ref
val pretty_flexpair: Proof.context -> term * term -> Pretty.T
val pretty_goals: Proof.context -> {total: bool, main: bool, maxgoals: int} ->
thm -> Pretty.T list
@@ -18,8 +18,8 @@
structure Goal_Display: GOAL_DISPLAY =
struct
-val goals_limit = ref 10; (*max number of goals to print*)
-val show_consts = ref false; (*true: show consts with types in proof state output*)
+val goals_limit = Unsynchronized.ref 10; (*max number of goals to print*)
+val show_consts = Unsynchronized.ref false; (*true: show consts with types in proof state output*)
fun pretty_flexpair ctxt (t, u) = Pretty.block
[Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u];
--- a/src/Pure/library.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/library.ML Tue Sep 29 18:14:08 2009 +0200
@@ -57,13 +57,8 @@
val andf: ('a -> bool) * ('a -> bool) -> 'a -> bool
val exists: ('a -> bool) -> 'a list -> bool
val forall: ('a -> bool) -> 'a list -> bool
- val set: bool ref -> bool
- val reset: bool ref -> bool
- val toggle: bool ref -> bool
- val change: 'a ref -> ('a -> 'a) -> unit
- val change_result: 'a ref -> ('a -> 'b * 'a) -> 'b
- val setmp_noncritical: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
- val setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
+ val setmp_noncritical: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c
+ val setmp: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c
val setmp_thread_data: 'a Universal.tag -> 'a -> 'a -> ('b -> 'c) -> 'b -> 'c
(*lists*)
@@ -123,8 +118,6 @@
val suffixes: 'a list -> 'a list list
(*integers*)
- val inc: int ref -> int
- val dec: int ref -> int
val upto: int * int -> int list
val downto: int * int -> int list
val radixpand: int * int -> int list
@@ -326,13 +319,6 @@
(* flags *)
-fun set flag = (flag := true; true);
-fun reset flag = (flag := false; false);
-fun toggle flag = (flag := not (! flag); ! flag);
-
-fun change r f = r := f (! r);
-fun change_result r f = let val (x, y) = f (! r) in r := y; x end;
-
(*temporarily set flag during execution*)
fun setmp_noncritical flag value f x =
uninterruptible (fn restore_attributes => fn () =>
@@ -643,10 +629,6 @@
(** integers **)
-fun inc i = (i := ! i + (1: int); ! i);
-fun dec i = (i := ! i - (1: int); ! i);
-
-
(* lists of integers *)
(*make the list [from, from + 1, ..., to]*)
@@ -1055,7 +1037,7 @@
local
val a = 16807.0;
val m = 2147483647.0;
- val random_seed = ref 1.0;
+ val random_seed = Unsynchronized.ref 1.0;
in
fun random () = CRITICAL (fn () =>
@@ -1121,17 +1103,18 @@
val char_vec = Vector.tabulate (62, gensym_char);
fun newid n = implode (map (fn i => Vector.sub (char_vec, i)) (radixpand (62, n)));
-val gensym_seed = ref (0: int);
+val gensym_seed = Unsynchronized.ref (0: int);
in
- fun gensym pre = pre ^ newid (NAMED_CRITICAL "gensym" (fn () => inc gensym_seed));
+ fun gensym pre =
+ pre ^ newid (NAMED_CRITICAL "gensym" (fn () => Unsynchronized.inc gensym_seed));
end;
(* stamps and serial numbers *)
-type stamp = unit ref;
-val stamp: unit -> stamp = ref;
+type stamp = unit Unsynchronized.ref;
+val stamp: unit -> stamp = Unsynchronized.ref;
type serial = int;
val serial = Multithreading.serial;
--- a/src/Pure/meta_simplifier.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/meta_simplifier.ML Tue Sep 29 18:14:08 2009 +0200
@@ -11,9 +11,9 @@
signature BASIC_META_SIMPLIFIER =
sig
- val debug_simp: bool ref
- val trace_simp: bool ref
- val trace_simp_depth_limit: int ref
+ val debug_simp: bool Unsynchronized.ref
+ val trace_simp: bool Unsynchronized.ref
+ val trace_simp_depth_limit: int Unsynchronized.ref
type rrule
val eq_rrule: rrule * rrule -> bool
type simpset
@@ -84,7 +84,7 @@
{rules: rrule Net.net,
prems: thm list,
bounds: int * ((string * typ) * string) list,
- depth: int * bool ref,
+ depth: int * bool Unsynchronized.ref,
context: Proof.context option} *
{congs: (string * thm) list * string list,
procs: proc Net.net,
@@ -112,7 +112,7 @@
val the_context: simpset -> Proof.context
val context: Proof.context -> simpset -> simpset
val theory_context: theory -> simpset -> simpset
- val debug_bounds: bool ref
+ val debug_bounds: bool Unsynchronized.ref
val set_reorient: (theory -> term list -> term -> term -> bool) -> simpset -> simpset
val set_solvers: solver list -> simpset -> simpset
val rewrite_cterm: bool * bool * bool -> (simpset -> thm -> thm option) -> simpset -> conv
@@ -190,7 +190,7 @@
{rules: rrule Net.net,
prems: thm list,
bounds: int * ((string * typ) * string) list,
- depth: int * bool ref,
+ depth: int * bool Unsynchronized.ref,
context: Proof.context option} *
{congs: (string * thm) list * string list,
procs: proc Net.net,
@@ -256,7 +256,7 @@
val simp_depth_limit_value = Config.declare false "simp_depth_limit" (Config.Int 100);
val simp_depth_limit = Config.int simp_depth_limit_value;
-val trace_simp_depth_limit = ref 1;
+val trace_simp_depth_limit = Unsynchronized.ref 1;
fun trace_depth (Simpset ({depth = (depth, exceeded), ...}, _)) msg =
if depth > ! trace_simp_depth_limit then
@@ -266,7 +266,8 @@
val inc_simp_depth = map_simpset1 (fn (rules, prems, bounds, (depth, exceeded), context) =>
(rules, prems, bounds,
- (depth + 1, if depth = ! trace_simp_depth_limit then ref false else exceeded), context));
+ (depth + 1,
+ if depth = ! trace_simp_depth_limit then Unsynchronized.ref false else exceeded), context));
fun simp_depth (Simpset ({depth = (depth, _), ...}, _)) = depth;
@@ -275,8 +276,8 @@
exception SIMPLIFIER of string * thm;
-val debug_simp = ref false;
-val trace_simp = ref false;
+val debug_simp = Unsynchronized.ref false;
+val trace_simp = Unsynchronized.ref false;
local
@@ -746,7 +747,7 @@
(* empty *)
fun init_ss mk_rews termless subgoal_tac solvers =
- make_simpset ((Net.empty, [], (0, []), (0, ref false), NONE),
+ make_simpset ((Net.empty, [], (0, []), (0, Unsynchronized.ref false), NONE),
(([], []), Net.empty, mk_rews, termless, subgoal_tac, [], solvers));
fun clear_ss (ss as Simpset (_, {mk_rews, termless, subgoal_tac, solvers, ...})) =
@@ -1209,7 +1210,7 @@
prover: how to solve premises in conditional rewrites and congruences
*)
-val debug_bounds = ref false;
+val debug_bounds = Unsynchronized.ref false;
fun check_bounds ss ct =
if ! debug_bounds then
@@ -1337,5 +1338,5 @@
end;
-structure BasicMetaSimplifier: BASIC_META_SIMPLIFIER = MetaSimplifier;
-open BasicMetaSimplifier;
+structure Basic_Meta_Simplifier: BASIC_META_SIMPLIFIER = MetaSimplifier;
+open Basic_Meta_Simplifier;
--- a/src/Pure/old_goals.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/old_goals.ML Tue Sep 29 18:14:08 2009 +0200
@@ -19,7 +19,7 @@
type proof
val premises: unit -> thm list
val reset_goals: unit -> unit
- val result_error_fn: (thm -> string -> thm) ref
+ val result_error_fn: (thm -> string -> thm) Unsynchronized.ref
val print_sign_exn: theory -> exn -> 'a
val prove_goalw_cterm: thm list->cterm->(thm list->tactic list)->thm
val prove_goalw_cterm_nocheck: thm list->cterm->(thm list->tactic list)->thm
@@ -233,21 +233,21 @@
(*** References ***)
(*Current assumption list -- set by "goal".*)
-val curr_prems = ref([] : thm list);
+val curr_prems = Unsynchronized.ref([] : thm list);
(*Return assumption list -- useful if you didn't save "goal"'s result. *)
fun premises() = !curr_prems;
(*Current result maker -- set by "goal", used by "result". *)
fun init_mkresult _ = error "No goal has been supplied in subgoal module";
-val curr_mkresult = ref (init_mkresult: bool*thm->thm);
+val curr_mkresult = Unsynchronized.ref (init_mkresult: bool*thm->thm);
(*List of previous goal stacks, for the undo operation. Set by setstate.
A list of lists!*)
-val undo_list = ref([[(asm_rl, Seq.empty)]] : gstack list);
+val undo_list = Unsynchronized.ref([[(asm_rl, Seq.empty)]] : gstack list);
(* Stack of proof attempts *)
-val proofstack = ref([]: proof list);
+val proofstack = Unsynchronized.ref([]: proof list);
(*reset all refs*)
fun reset_goals () =
@@ -272,7 +272,7 @@
Goal_Display.pretty_goals_without_context (!goals_limit) state @
[Pretty.str msg, Pretty.str "Proof failed!"] |> Pretty.chunks |> Pretty.string_of |> error;
-val result_error_fn = ref result_error_default;
+val result_error_fn = Unsynchronized.ref result_error_default;
(*Common treatment of "goal" and "prove_goal":
--- a/src/Pure/pattern.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/pattern.ML Tue Sep 29 18:14:08 2009 +0200
@@ -14,7 +14,7 @@
signature PATTERN =
sig
- val trace_unify_fail: bool ref
+ val trace_unify_fail: bool Unsynchronized.ref
val aeconv: term * term -> bool
val eta_long: typ list -> term -> term
val match: theory -> term * term -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
@@ -40,7 +40,7 @@
exception Unif;
exception Pattern;
-val trace_unify_fail = ref false;
+val trace_unify_fail = Unsynchronized.ref false;
fun string_of_term thy env binders t =
Syntax.string_of_term_global thy
--- a/src/Pure/proofterm.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/proofterm.ML Tue Sep 29 18:14:08 2009 +0200
@@ -8,7 +8,7 @@
signature BASIC_PROOFTERM =
sig
- val proofs: int ref
+ val proofs: int Unsynchronized.ref
datatype proof =
MinProof
@@ -885,7 +885,7 @@
(***** axioms and theorems *****)
-val proofs = ref 2;
+val proofs = Unsynchronized.ref 2;
fun vars_of t = map Var (rev (Term.add_vars t []));
fun frees_of t = map Free (rev (Term.add_frees t []));
--- a/src/Pure/search.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/search.ML Tue Sep 29 18:14:08 2009 +0200
@@ -13,23 +13,23 @@
val THEN_MAYBE : tactic * tactic -> tactic
val THEN_MAYBE' : ('a -> tactic) * ('a -> tactic) -> ('a -> tactic)
- val trace_DEPTH_FIRST : bool ref
+ val trace_DEPTH_FIRST : bool Unsynchronized.ref
val DEPTH_FIRST : (thm -> bool) -> tactic -> tactic
val DEPTH_SOLVE : tactic -> tactic
val DEPTH_SOLVE_1 : tactic -> tactic
val ITER_DEEPEN : (thm->bool) -> (int->tactic) -> tactic
val THEN_ITER_DEEPEN : tactic -> (thm->bool) -> (int->tactic) -> tactic
- val iter_deepen_limit : int ref
+ val iter_deepen_limit : int Unsynchronized.ref
val has_fewer_prems : int -> thm -> bool
val IF_UNSOLVED : tactic -> tactic
val SOLVE : tactic -> tactic
val DETERM_UNTIL_SOLVED: tactic -> tactic
- val trace_BEST_FIRST : bool ref
+ val trace_BEST_FIRST : bool Unsynchronized.ref
val BEST_FIRST : (thm -> bool) * (thm -> int) -> tactic -> tactic
val THEN_BEST_FIRST : tactic -> (thm->bool) * (thm->int) -> tactic
-> tactic
- val trace_ASTAR : bool ref
+ val trace_ASTAR : bool Unsynchronized.ref
val ASTAR : (thm -> bool) * (int->thm->int) -> tactic -> tactic
val THEN_ASTAR : tactic -> (thm->bool) * (int->thm->int) -> tactic
-> tactic
@@ -50,7 +50,7 @@
(**** Depth-first search ****)
-val trace_DEPTH_FIRST = ref false;
+val trace_DEPTH_FIRST = Unsynchronized.ref false;
(*Searches until "satp" reports proof tree as satisfied.
Suppresses duplicate solutions to minimize search space.*)
@@ -130,7 +130,7 @@
(*No known example (on 1-5-2007) needs even thirty*)
-val iter_deepen_limit = ref 50;
+val iter_deepen_limit = Unsynchronized.ref 50;
(*Depth-first iterative deepening search for a state that satisfies satp
tactic tac0 sets up the initial goal queue, while tac1 searches it.
@@ -138,7 +138,7 @@
to suppress solutions arising from earlier searches, as the accumulated cost
(k) can be wrong.*)
fun THEN_ITER_DEEPEN tac0 satp tac1 = traced_tac (fn st =>
- let val countr = ref 0
+ let val countr = Unsynchronized.ref 0
and tf = tracify trace_DEPTH_FIRST (tac1 1)
and qs0 = tac0 st
(*bnd = depth bound; inc = estimate of increment required next*)
@@ -156,7 +156,7 @@
| depth (bnd,inc) ((k,np,rgd,q)::qs) =
if k>=bnd then depth (bnd,inc) qs
else
- case (countr := !countr+1;
+ case (Unsynchronized.inc countr;
if !trace_DEPTH_FIRST then
tracing (string_of_int np ^ implode (map (fn _ => "*") qs))
else ();
@@ -199,7 +199,7 @@
(*** Best-first search ***)
-val trace_BEST_FIRST = ref false;
+val trace_BEST_FIRST = Unsynchronized.ref false;
(*For creating output sequence*)
fun some_of_list [] = NONE
@@ -273,7 +273,7 @@
fun some_of_list [] = NONE
| some_of_list (x::l) = SOME (x, Seq.make (fn () => some_of_list l));
-val trace_ASTAR = ref false;
+val trace_ASTAR = Unsynchronized.ref false;
fun THEN_ASTAR tac0 (satp, costf) tac1 =
let val tf = tracify trace_ASTAR tac1;
--- a/src/Pure/simplifier.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/simplifier.ML Tue Sep 29 18:14:08 2009 +0200
@@ -32,7 +32,7 @@
include BASIC_SIMPLIFIER
val pretty_ss: Proof.context -> simpset -> Pretty.T
val clear_ss: simpset -> simpset
- val debug_bounds: bool ref
+ val debug_bounds: bool Unsynchronized.ref
val inherit_context: simpset -> simpset -> simpset
val the_context: simpset -> Proof.context
val context: Proof.context -> simpset -> simpset
@@ -424,5 +424,5 @@
end;
-structure BasicSimplifier: BASIC_SIMPLIFIER = Simplifier;
-open BasicSimplifier;
+structure Basic_Simplifier: BASIC_SIMPLIFIER = Simplifier;
+open Basic_Simplifier;
--- a/src/Pure/tactical.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/tactical.ML Tue Sep 29 18:14:08 2009 +0200
@@ -34,9 +34,9 @@
val RANGE: (int -> tactic) list -> int -> tactic
val print_tac: string -> tactic
val pause_tac: tactic
- val trace_REPEAT: bool ref
- val suppress_tracing: bool ref
- val tracify: bool ref -> tactic -> tactic
+ val trace_REPEAT: bool Unsynchronized.ref
+ val suppress_tracing: bool Unsynchronized.ref
+ val tracify: bool Unsynchronized.ref -> tactic -> tactic
val traced_tac: (thm -> (thm * thm Seq.seq) option) -> tactic
val DETERM_UNTIL: (thm -> bool) -> tactic -> tactic
val REPEAT_DETERM_N: int -> tactic -> tactic
@@ -204,16 +204,16 @@
and TRACE_QUIT;
(*Tracing flags*)
-val trace_REPEAT= ref false
-and suppress_tracing = ref false;
+val trace_REPEAT= Unsynchronized.ref false
+and suppress_tracing = Unsynchronized.ref false;
(*Handle all tracing commands for current state and tactic *)
fun exec_trace_command flag (tac, st) =
case TextIO.inputLine TextIO.stdIn of
SOME "\n" => tac st
| SOME "f\n" => Seq.empty
- | SOME "o\n" => (flag:=false; tac st)
- | SOME "s\n" => (suppress_tracing:=true; tac st)
+ | SOME "o\n" => (flag := false; tac st)
+ | SOME "s\n" => (suppress_tracing := true; tac st)
| SOME "x\n" => (tracing "Exiting now"; raise (TRACE_EXIT st))
| SOME "quit\n" => raise TRACE_QUIT
| _ => (tracing
--- a/src/Pure/term.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/term.ML Tue Sep 29 18:14:08 2009 +0200
@@ -112,7 +112,7 @@
val exists_type: (typ -> bool) -> term -> bool
val exists_subterm: (term -> bool) -> term -> bool
val exists_Const: (string * typ -> bool) -> term -> bool
- val show_question_marks: bool ref
+ val show_question_marks: bool Unsynchronized.ref
end;
signature TERM =
@@ -963,7 +963,7 @@
(* display variables *)
-val show_question_marks = ref true;
+val show_question_marks = Unsynchronized.ref true;
fun string_of_vname (x, i) =
let
--- a/src/Pure/term_subst.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/term_subst.ML Tue Sep 29 18:14:08 2009 +0200
@@ -157,28 +157,32 @@
in
fun instantiateT_maxidx instT ty i =
- let val maxidx = ref i
+ let val maxidx = Unsynchronized.ref i
in (instantiateT_same maxidx instT ty handle Same.SAME => ty, ! maxidx) end;
fun instantiate_maxidx insts tm i =
- let val maxidx = ref i
+ let val maxidx = Unsynchronized.ref i
in (instantiate_same maxidx insts tm handle Same.SAME => tm, ! maxidx) end;
fun instantiateT [] ty = ty
| instantiateT instT ty =
- (instantiateT_same (ref ~1) (no_indexes1 instT) ty handle Same.SAME => ty);
+ (instantiateT_same (Unsynchronized.ref ~1) (no_indexes1 instT) ty
+ handle Same.SAME => ty);
fun instantiate ([], []) tm = tm
| instantiate insts tm =
- (instantiate_same (ref ~1) (no_indexes2 insts) tm handle Same.SAME => tm);
+ (instantiate_same (Unsynchronized.ref ~1) (no_indexes2 insts) tm
+ handle Same.SAME => tm);
fun instantiateT_option [] _ = NONE
| instantiateT_option instT ty =
- (SOME (instantiateT_same (ref ~1) (no_indexes1 instT) ty) handle Same.SAME => NONE);
+ (SOME (instantiateT_same (Unsynchronized.ref ~1) (no_indexes1 instT) ty)
+ handle Same.SAME => NONE);
fun instantiate_option ([], []) _ = NONE
| instantiate_option insts tm =
- (SOME (instantiate_same (ref ~1) (no_indexes2 insts) tm) handle Same.SAME => NONE);
+ (SOME (instantiate_same (Unsynchronized.ref ~1) (no_indexes2 insts) tm)
+ handle Same.SAME => NONE);
end;
--- a/src/Pure/type.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/type.ML Tue Sep 29 18:14:08 2009 +0200
@@ -417,8 +417,8 @@
(*order-sorted unification*)
fun unify (tsig as TSig {classes = (_, classes), ...}) TU (tyenv, maxidx) =
let
- val tyvar_count = ref maxidx;
- fun gen_tyvar S = TVar ((Name.aT, inc tyvar_count), S);
+ val tyvar_count = Unsynchronized.ref maxidx;
+ fun gen_tyvar S = TVar ((Name.aT, Unsynchronized.inc tyvar_count), S);
fun mg_domain a S = Sorts.mg_domain classes a S
handle Sorts.CLASS_ERROR _ => raise TUNIFY;
--- a/src/Pure/unify.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Pure/unify.ML Tue Sep 29 18:14:08 2009 +0200
@@ -106,7 +106,7 @@
the occurs check must ignore the types of variables. This avoids
that ?x::?'a is unified with f(?x::T), which may lead to a cyclic
substitution when ?'a is instantiated with T later. *)
-fun occurs_terms (seen: (indexname list) ref,
+fun occurs_terms (seen: (indexname list) Unsynchronized.ref,
env: Envir.env, v: indexname, ts: term list): bool =
let fun occurs [] = false
| occurs (t::ts) = occur t orelse occurs ts
@@ -160,7 +160,7 @@
Warning: finds a rigid occurrence of ?f in ?f(t).
Should NOT be called in this case: there is a flex-flex unifier
*)
-fun rigid_occurs_term (seen: (indexname list)ref, env, v: indexname, t) =
+fun rigid_occurs_term (seen: (indexname list) Unsynchronized.ref, env, v: indexname, t) =
let fun nonrigid t = if occurs_terms(seen,env,v,[t]) then Nonrigid
else NoOcc
fun occurs [] = NoOcc
@@ -230,7 +230,7 @@
If v occurs nonrigidly then must use full algorithm. *)
fun assignment thy (env, rbinder, t, u) =
let val vT as (v,T) = get_eta_var (rbinder, 0, t)
- in case rigid_occurs_term (ref [], env, v, u) of
+ in case rigid_occurs_term (Unsynchronized.ref [], env, v, u) of
NoOcc => let val env = unify_types thy (body_type env T,
fastype env (rbinder,u),env)
in Envir.update ((vT, Logic.rlist_abs (rbinder, u)), env) end
@@ -429,7 +429,7 @@
Attempts to update t with u, raising ASSIGN if impossible*)
fun ff_assign thy (env, rbinder, t, u) : Envir.env =
let val vT as (v,T) = get_eta_var(rbinder,0,t)
-in if occurs_terms (ref [], env, v, [u]) then raise ASSIGN
+in if occurs_terms (Unsynchronized.ref [], env, v, [u]) then raise ASSIGN
else let val env = unify_types thy (body_type env T,
fastype env (rbinder,u),
env)
--- a/src/Sequents/prover.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Sequents/prover.ML Tue Sep 29 18:14:08 2009 +0200
@@ -10,12 +10,11 @@
infix 4 add_safes add_unsafes;
structure Cla =
-
struct
datatype pack = Pack of thm list * thm list;
-val trace = ref false;
+val trace = Unsynchronized.ref false;
(*A theorem pack has the form (safe rules, unsafe rules)
An unsafe rule is incomplete or introduces variables in subgoals,
--- a/src/Tools/Code/code_ml.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Tools/Code/code_ml.ML Tue Sep 29 18:14:08 2009 +0200
@@ -6,7 +6,7 @@
signature CODE_ML =
sig
- val eval: string option -> string * (unit -> 'a) option ref
+ val eval: string option -> string * (unit -> 'a) option Unsynchronized.ref
-> ((term -> term) -> 'a -> 'a) -> theory -> term -> string list -> 'a
val target_Eval: string
val setup: theory -> theory
--- a/src/Tools/Code/code_target.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Tools/Code/code_target.ML Tue Sep 29 18:14:08 2009 +0200
@@ -38,7 +38,7 @@
val code_of: theory -> string -> string
-> string list -> (Code_Thingol.naming -> string list) -> string
val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit
- val code_width: int ref
+ val code_width: int Unsynchronized.ref
val allow_abort: string -> theory -> theory
val add_syntax_class: string -> class -> string option -> theory -> theory
@@ -59,7 +59,7 @@
datatype destination = Compile | Export | File of Path.T | String of string list;
type serialization = destination -> (string * string option list) option;
-val code_width = ref 80; (*FIXME after Pretty module no longer depends on print mode*)
+val code_width = Unsynchronized.ref 80; (*FIXME after Pretty module no longer depends on print mode*)
fun code_setmp f = PrintMode.setmp [] (Pretty.setmp_margin (!code_width) f);
fun code_of_pretty p = code_setmp Pretty.string_of p ^ "\n";
fun code_writeln p = Pretty.setmp_margin (!code_width) Pretty.writeln p;
--- a/src/Tools/Compute_Oracle/am_compiler.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Tools/Compute_Oracle/am_compiler.ML Tue Sep 29 18:14:08 2009 +0200
@@ -18,7 +18,7 @@
open AbstractMachine;
-val compiled_rewriter = ref (NONE:(term -> term)Option.option)
+val compiled_rewriter = Unsynchronized.ref (NONE:(term -> term)Option.option)
fun set_compiled_rewriter r = (compiled_rewriter := SOME r)
@@ -81,7 +81,7 @@
fun load_rules sname name prog =
let
- val buffer = ref ""
+ val buffer = Unsynchronized.ref ""
fun write s = (buffer := (!buffer)^s)
fun writeln s = (write s; write "\n")
fun writelist [] = ()
@@ -112,7 +112,7 @@
"",
"fun do_reduction reduce p =",
" let",
- " val s = ref (Continue p)",
+ " val s = Unsynchronized.ref (Continue p)",
" val _ = while cont (!s) do (s := reduce (proj_C (!s)))",
" in",
" proj_S (!s)",
--- a/src/Tools/Compute_Oracle/am_ghc.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Tools/Compute_Oracle/am_ghc.ML Tue Sep 29 18:14:08 2009 +0200
@@ -144,7 +144,7 @@
fun haskell_prog name rules =
let
- val buffer = ref ""
+ val buffer = Unsynchronized.ref ""
fun write s = (buffer := (!buffer)^s)
fun writeln s = (write s; write "\n")
fun writelist [] = ()
@@ -200,7 +200,7 @@
(arity, !buffer)
end
-val guid_counter = ref 0
+val guid_counter = Unsynchronized.ref 0
fun get_guid () =
let
val c = !guid_counter
@@ -214,7 +214,7 @@
fun writeTextFile name s = File.write (Path.explode name) s
-val ghc = ref (case getenv "GHC_PATH" of "" => "ghc" | s => s)
+val ghc = Unsynchronized.ref (case getenv "GHC_PATH" of "" => "ghc" | s => s)
fun fileExists name = ((OS.FileSys.fileSize name; true) handle OS.SysErr _ => false)
--- a/src/Tools/Compute_Oracle/am_interpreter.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Tools/Compute_Oracle/am_interpreter.ML Tue Sep 29 18:14:08 2009 +0200
@@ -5,7 +5,7 @@
signature AM_BARRAS =
sig
include ABSTRACT_MACHINE
- val max_reductions : int option ref
+ val max_reductions : int option Unsynchronized.ref
end
structure AM_Interpreter : AM_BARRAS = struct
@@ -129,12 +129,12 @@
fun cont (Continue _) = true
| cont _ = false
-val max_reductions = ref (NONE : int option)
+val max_reductions = Unsynchronized.ref (NONE : int option)
fun do_reduction reduce p =
let
- val s = ref (Continue p)
- val counter = ref 0
+ val s = Unsynchronized.ref (Continue p)
+ val counter = Unsynchronized.ref 0
val _ = case !max_reductions of
NONE => while cont (!s) do (s := reduce (proj_C (!s)))
| SOME m => while cont (!s) andalso (!counter < m) do (s := reduce (proj_C (!s)); counter := (!counter) + 1)
--- a/src/Tools/Compute_Oracle/am_sml.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Tools/Compute_Oracle/am_sml.ML Tue Sep 29 18:14:08 2009 +0200
@@ -12,18 +12,18 @@
val save_result : (string * term) -> unit
val set_compiled_rewriter : (term -> term) -> unit
val list_nth : 'a list * int -> 'a
- val dump_output : (string option) ref
+ val dump_output : (string option) Unsynchronized.ref
end
structure AM_SML : AM_SML = struct
open AbstractMachine;
-val dump_output = ref (NONE: string option)
+val dump_output = Unsynchronized.ref (NONE: string option)
type program = string * string * (int Inttab.table) * (int Inttab.table) * (term Inttab.table) * (term -> term)
-val saved_result = ref (NONE:(string*term)option)
+val saved_result = Unsynchronized.ref (NONE:(string*term)option)
fun save_result r = (saved_result := SOME r)
fun clear_result () = (saved_result := NONE)
@@ -32,7 +32,7 @@
(*fun list_nth (l,n) = (writeln (makestring ("list_nth", (length l,n))); List.nth (l,n))*)
-val compiled_rewriter = ref (NONE:(term -> term)Option.option)
+val compiled_rewriter = Unsynchronized.ref (NONE:(term -> term)Option.option)
fun set_compiled_rewriter r = (compiled_rewriter := SOME r)
@@ -295,7 +295,7 @@
fun sml_prog name code rules =
let
- val buffer = ref ""
+ val buffer = Unsynchronized.ref ""
fun write s = (buffer := (!buffer)^s)
fun writeln s = (write s; write "\n")
fun writelist [] = ()
@@ -480,7 +480,7 @@
(arity, toplevel_arity, inlinetab, !buffer)
end
-val guid_counter = ref 0
+val guid_counter = Unsynchronized.ref 0
fun get_guid () =
let
val c = !guid_counter
--- a/src/Tools/Compute_Oracle/compute.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Tools/Compute_Oracle/compute.ML Tue Sep 29 18:14:08 2009 +0200
@@ -171,20 +171,21 @@
fun default_naming i = "v_" ^ Int.toString i
-datatype computer = Computer of (theory_ref * Encode.encoding * term list * unit Sorttab.table * prog * unit ref * naming)
- option ref
+datatype computer = Computer of
+ (theory_ref * Encode.encoding * term list * unit Sorttab.table * prog * unit Unsynchronized.ref * naming)
+ option Unsynchronized.ref
-fun theory_of (Computer (ref (SOME (rthy,_,_,_,_,_,_)))) = Theory.deref rthy
-fun hyps_of (Computer (ref (SOME (_,_,hyps,_,_,_,_)))) = hyps
-fun shyps_of (Computer (ref (SOME (_,_,_,shyptable,_,_,_)))) = Sorttab.keys (shyptable)
-fun shyptab_of (Computer (ref (SOME (_,_,_,shyptable,_,_,_)))) = shyptable
-fun stamp_of (Computer (ref (SOME (_,_,_,_,_,stamp,_)))) = stamp
-fun prog_of (Computer (ref (SOME (_,_,_,_,prog,_,_)))) = prog
-fun encoding_of (Computer (ref (SOME (_,encoding,_,_,_,_,_)))) = encoding
-fun set_encoding (Computer (r as ref (SOME (p1,encoding,p2,p3,p4,p5,p6)))) encoding' =
+fun theory_of (Computer (Unsynchronized.ref (SOME (rthy,_,_,_,_,_,_)))) = Theory.deref rthy
+fun hyps_of (Computer (Unsynchronized.ref (SOME (_,_,hyps,_,_,_,_)))) = hyps
+fun shyps_of (Computer (Unsynchronized.ref (SOME (_,_,_,shyptable,_,_,_)))) = Sorttab.keys (shyptable)
+fun shyptab_of (Computer (Unsynchronized.ref (SOME (_,_,_,shyptable,_,_,_)))) = shyptable
+fun stamp_of (Computer (Unsynchronized.ref (SOME (_,_,_,_,_,stamp,_)))) = stamp
+fun prog_of (Computer (Unsynchronized.ref (SOME (_,_,_,_,prog,_,_)))) = prog
+fun encoding_of (Computer (Unsynchronized.ref (SOME (_,encoding,_,_,_,_,_)))) = encoding
+fun set_encoding (Computer (r as Unsynchronized.ref (SOME (p1,encoding,p2,p3,p4,p5,p6)))) encoding' =
(r := SOME (p1,encoding',p2,p3,p4,p5,p6))
-fun naming_of (Computer (ref (SOME (_,_,_,_,_,_,n)))) = n
-fun set_naming (Computer (r as ref (SOME (p1,p2,p3,p4,p5,p6,naming)))) naming'=
+fun naming_of (Computer (Unsynchronized.ref (SOME (_,_,_,_,_,_,n)))) = n
+fun set_naming (Computer (r as Unsynchronized.ref (SOME (p1,p2,p3,p4,p5,p6,naming)))) naming'=
(r := SOME (p1,p2,p3,p4,p5,p6,naming'))
fun ref_of (Computer r) = r
@@ -320,7 +321,8 @@
in (Theory.check_thy thy, encoding, Termtab.keys hyptable, shyptable, prog, stamp, default_naming) end
-fun make_with_cache machine thy cache_patterns raw_thms = Computer (ref (SOME (make_internal machine thy (ref ()) Encode.empty cache_patterns raw_thms)))
+fun make_with_cache machine thy cache_patterns raw_thms =
+ Computer (Unsynchronized.ref (SOME (make_internal machine thy (Unsynchronized.ref ()) Encode.empty cache_patterns raw_thms)))
fun make machine thy raw_thms = make_with_cache machine thy [] raw_thms
@@ -415,7 +417,7 @@
datatype prem = EqPrem of AbstractMachine.term * AbstractMachine.term * Term.typ * int
| Prem of AbstractMachine.term
-datatype theorem = Theorem of theory_ref * unit ref * (int * typ) Symtab.table * (AbstractMachine.term option) Inttab.table
+datatype theorem = Theorem of theory_ref * unit Unsynchronized.ref * (int * typ) Symtab.table * (AbstractMachine.term option) Inttab.table
* prem list * AbstractMachine.term * term list * sort list
--- a/src/Tools/Compute_Oracle/linker.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Tools/Compute_Oracle/linker.ML Tue Sep 29 18:14:08 2009 +0200
@@ -239,7 +239,9 @@
datatype theorem = MonoThm of thm | PolyThm of thm * Linker.instances * thm list
datatype pattern = MonoPattern of term | PolyPattern of term * Linker.instances * term list
-datatype pcomputer = PComputer of theory_ref * Compute.computer * theorem list ref * pattern list ref
+datatype pcomputer =
+ PComputer of theory_ref * Compute.computer * theorem list Unsynchronized.ref *
+ pattern list Unsynchronized.ref
(*fun collect_consts (Var x) = []
| collect_consts (Bound _) = []
@@ -324,7 +326,7 @@
fun add_monos thy monocs pats ths =
let
- val changed = ref false
+ val changed = Unsynchronized.ref false
fun add monocs (th as (MonoThm _)) = ([], th)
| add monocs (PolyThm (th, instances, instanceths)) =
let
@@ -386,9 +388,9 @@
fun remove_duplicates ths =
let
- val counter = ref 0
- val tab = ref (CThmtab.empty : unit CThmtab.table)
- val thstab = ref (Inttab.empty : thm Inttab.table)
+ val counter = Unsynchronized.ref 0
+ val tab = Unsynchronized.ref (CThmtab.empty : unit CThmtab.table)
+ val thstab = Unsynchronized.ref (Inttab.empty : thm Inttab.table)
fun update th =
let
val key = thm2cthm th
@@ -415,7 +417,7 @@
val (_, (pats, ths)) = add_monos thy monocs pats ths
val computer = create_computer machine thy pats ths
in
- PComputer (Theory.check_thy thy, computer, ref ths, ref pats)
+ PComputer (Theory.check_thy thy, computer, Unsynchronized.ref ths, Unsynchronized.ref pats)
end
fun make machine thy ths cs = make_with_cache machine thy [] ths cs
--- a/src/Tools/Compute_Oracle/report.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Tools/Compute_Oracle/report.ML Tue Sep 29 18:14:08 2009 +0200
@@ -3,7 +3,7 @@
local
- val report_depth = ref 0
+ val report_depth = Unsynchronized.ref 0
fun space n = if n <= 0 then "" else (space (n-1))^" "
fun report_space () = space (!report_depth)
--- a/src/Tools/Metis/make-metis Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Tools/Metis/make-metis Tue Sep 29 18:14:08 2009 +0200
@@ -30,16 +30,19 @@
then
echo -e "$FILE (global)" >&2
"$THIS/scripts/mlpp" -c isabelle "src/$FILE" | \
- perl -p -e 's/\b([A-Za-z]+\.[A-Za-z]+)/Metis.\1/g;' -e 's/\bfrag\b/Metis.frag/;'
+ perl -p -e 's/\b([A-Za-z]+\.[A-Za-z]+)/Metis.\1/g;' -e 's/\bfrag\b/Metis.frag/;' | \
+ perl -p -e 's/\bref\b/Unsynchronized.ref/g;'
elif fgrep -q functor "src/$FILE"
then
"$THIS/scripts/mlpp" -c isabelle "src/$FILE" | \
- perl -p -e 's/ union / op union /g;' -e 's/ subset / op subset /g;'
+ perl -p -e 's/ union / op union /g;' -e 's/ subset / op subset /g;' | \
+ perl -p -e 's/\bref\b/Unsynchronized.ref/g;'
else
echo -e "$FILE (local)" >&2
echo "structure Metis = struct open Metis"
cat < "metis_env.ML"
- "$THIS/scripts/mlpp" -c isabelle "src/$FILE"
+ "$THIS/scripts/mlpp" -c isabelle "src/$FILE" | \
+ perl -p -e 's/\bref\b/Unsynchronized.ref/g;'
echo "end;"
fi
done
--- a/src/Tools/Metis/metis.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Tools/Metis/metis.ML Tue Sep 29 18:14:08 2009 +0200
@@ -395,18 +395,18 @@
in
abstype 'a queue = QUEUE of {elems: 'a array, (* the contents *)
- front: int ref,
- back: int ref,
+ front: int Unsynchronized.ref,
+ back: int Unsynchronized.ref,
size: int} (* fixed size of element array *)
with
- fun is_empty (QUEUE{front=ref ~1, back=ref ~1,...}) = true
+ fun is_empty (QUEUE{front=Unsynchronized.ref ~1, back=Unsynchronized.ref ~1,...}) = true
| is_empty _ = false
fun mk_queue n init_val =
if (n < 2)
then raise REQUESTED_QUEUE_SIZE_TOO_SMALL
- else QUEUE{elems=array(n, init_val), front=ref ~1, back=ref ~1, size=n}
+ else QUEUE{elems=array(n, init_val), front=Unsynchronized.ref ~1, back=Unsynchronized.ref ~1, size=n}
fun clear_queue (QUEUE{front,back,...}) = (front := ~1; back := ~1)
@@ -459,9 +459,9 @@
(* Some global values *)
val INFINITY = 999999
-abstype indent_stack = Istack of break_info list ref
+abstype indent_stack = Istack of break_info list Unsynchronized.ref
with
- fun mk_indent_stack() = Istack (ref([]:break_info list))
+ fun mk_indent_stack() = Istack (Unsynchronized.ref([]:break_info list))
fun clear_indent_stack (Istack stk) = (stk := ([]:break_info list))
fun top (Istack stk) =
case !stk
@@ -501,7 +501,7 @@
end
-type block_info = { Block_size : int ref,
+type block_info = { Block_size : int Unsynchronized.ref,
Block_offset : int,
How_to_indent : break_style }
@@ -512,10 +512,10 @@
*)
datatype pp_token
= S of {String : string, Length : int}
- | BB of {Pblocks : block_info list ref, (* Processed *)
- Ublocks : block_info list ref} (* Unprocessed *)
- | E of {Pend : int ref, Uend : int ref}
- | BR of {Distance_to_next_break : int ref,
+ | BB of {Pblocks : block_info list Unsynchronized.ref, (* Processed *)
+ Ublocks : block_info list Unsynchronized.ref} (* Unprocessed *)
+ | E of {Pend : int Unsynchronized.ref, Uend : int Unsynchronized.ref}
+ | BR of {Distance_to_next_break : int Unsynchronized.ref,
Number_of_blanks : int,
Break_offset : int}
@@ -532,12 +532,12 @@
the_token_buffer : pp_token array,
the_delim_stack : delim_stack,
the_indent_stack : indent_stack,
- ++ : int ref -> unit, (* increment circular buffer index *)
- space_left : int ref, (* remaining columns on page *)
- left_index : int ref, (* insertion index *)
- right_index : int ref, (* output index *)
- left_sum : int ref, (* size of strings and spaces inserted *)
- right_sum : int ref} (* size of strings and spaces printed *)
+ ++ : int Unsynchronized.ref -> unit, (* increment circular buffer index *)
+ space_left : int Unsynchronized.ref, (* remaining columns on page *)
+ left_index : int Unsynchronized.ref, (* insertion index *)
+ right_index : int Unsynchronized.ref, (* output index *)
+ left_sum : int Unsynchronized.ref, (* size of strings and spaces inserted *)
+ right_sum : int Unsynchronized.ref} (* size of strings and spaces printed *)
type ppstream = ppstream_
@@ -557,9 +557,9 @@
the_delim_stack = new_delim_stack buf_size,
the_indent_stack = mk_indent_stack (),
++ = fn i => i := ((!i + 1) mod buf_size),
- space_left = ref linewidth,
- left_index = ref 0, right_index = ref 0,
- left_sum = ref 0, right_sum = ref 0}
+ space_left = Unsynchronized.ref linewidth,
+ left_index = Unsynchronized.ref 0, right_index = Unsynchronized.ref 0,
+ left_sum = Unsynchronized.ref 0, right_sum = Unsynchronized.ref 0}
) : ppstream
end
@@ -595,25 +595,25 @@
be printable? Because of what goes on in add_string. See there for details.
*)
-fun print_BB (_,{Pblocks = ref [], Ublocks = ref []}) =
+fun print_BB (_,{Pblocks = Unsynchronized.ref [], Ublocks = Unsynchronized.ref []}) =
raise Fail "PP-error: print_BB"
- | print_BB (PPS{the_indent_stack,linewidth,space_left=ref sp_left,...},
- {Pblocks as ref({How_to_indent=CONSISTENT,Block_size,
+ | print_BB (PPS{the_indent_stack,linewidth,space_left=Unsynchronized.ref sp_left,...},
+ {Pblocks as Unsynchronized.ref({How_to_indent=CONSISTENT,Block_size,
Block_offset}::rst),
- Ublocks=ref[]}) =
+ Ublocks=Unsynchronized.ref[]}) =
(push ((if (!Block_size > sp_left)
then ONE_PER_LINE (linewidth - (sp_left - Block_offset))
else FITS),
the_indent_stack);
Pblocks := rst)
- | print_BB(PPS{the_indent_stack,linewidth,space_left=ref sp_left,...},
- {Pblocks as ref({Block_size,Block_offset,...}::rst),Ublocks=ref[]}) =
+ | print_BB(PPS{the_indent_stack,linewidth,space_left=Unsynchronized.ref sp_left,...},
+ {Pblocks as Unsynchronized.ref({Block_size,Block_offset,...}::rst),Ublocks=Unsynchronized.ref[]}) =
(push ((if (!Block_size > sp_left)
then PACK_ONTO_LINE (linewidth - (sp_left - Block_offset))
else FITS),
the_indent_stack);
Pblocks := rst)
- | print_BB (PPS{the_indent_stack, linewidth, space_left=ref sp_left,...},
+ | print_BB (PPS{the_indent_stack, linewidth, space_left=Unsynchronized.ref sp_left,...},
{Ublocks,...}) =
let fun pr_end_Ublock [{How_to_indent=CONSISTENT,Block_size,Block_offset}] l =
(push ((if (!Block_size > sp_left)
@@ -635,7 +635,7 @@
(* Uend should always be 0 when print_E is called. *)
-fun print_E (_,{Pend = ref 0, Uend = ref 0}) =
+fun print_E (_,{Pend = Unsynchronized.ref 0, Uend = Unsynchronized.ref 0}) =
raise Fail "PP-error: print_E"
| print_E (istack,{Pend, ...}) =
let fun pop_n_times 0 = ()
@@ -710,9 +710,9 @@
fun pointers_coincide(PPS{left_index,right_index,the_token_buffer,...}) =
(!left_index = !right_index) andalso
(case (the_token_buffer sub (!left_index))
- of (BB {Pblocks = ref [], Ublocks = ref []}) => true
+ of (BB {Pblocks = Unsynchronized.ref [], Ublocks = Unsynchronized.ref []}) => true
| (BB _) => false
- | (E {Pend = ref 0, Uend = ref 0}) => true
+ | (E {Pend = Unsynchronized.ref 0, Uend = Unsynchronized.ref 0}) => true
| (E _) => false
| _ => true)
@@ -732,13 +732,13 @@
fun token_size (S{Length, ...}) = Length
| token_size (BB b) =
(case b
- of {Pblocks = ref [], Ublocks = ref []} =>
+ of {Pblocks = Unsynchronized.ref [], Ublocks = Unsynchronized.ref []} =>
raise Fail "PP-error: BB_size"
- | {Pblocks as ref(_::_),Ublocks=ref[]} => POS
+ | {Pblocks as Unsynchronized.ref(_::_),Ublocks=Unsynchronized.ref[]} => POS
| {Ublocks, ...} => last_size (!Ublocks))
- | token_size (E{Pend = ref 0, Uend = ref 0}) =
+ | token_size (E{Pend = Unsynchronized.ref 0, Uend = Unsynchronized.ref 0}) =
raise Fail "PP-error: token_size.E"
- | token_size (E{Pend = ref 0, ...}) = NEG
+ | token_size (E{Pend = Unsynchronized.ref 0, ...}) = NEG
| token_size (E _) = POS
| token_size (BR {Distance_to_next_break, ...}) = !Distance_to_next_break
fun loop (instr) =
@@ -761,12 +761,12 @@
mangled output.)
*)
(case (the_token_buffer sub (!left_index))
- of (BB {Pblocks = ref [], Ublocks = ref []}) =>
+ of (BB {Pblocks = Unsynchronized.ref [], Ublocks = Unsynchronized.ref []}) =>
(update(the_token_buffer,!left_index,
initial_token_value);
++left_index)
| (BB _) => ()
- | (E {Pend = ref 0, Uend = ref 0}) =>
+ | (E {Pend = Unsynchronized.ref 0, Uend = Unsynchronized.ref 0}) =>
(update(the_token_buffer,!left_index,
initial_token_value);
++left_index)
@@ -791,12 +791,12 @@
else BB_inc_right_index ppstrm;
case (the_token_buffer sub (!right_index))
of (BB {Ublocks, ...}) =>
- Ublocks := {Block_size = ref (~(!right_sum)),
+ Ublocks := {Block_size = Unsynchronized.ref (~(!right_sum)),
Block_offset = offset,
How_to_indent = style}::(!Ublocks)
| _ => (update(the_token_buffer, !right_index,
- BB{Pblocks = ref [],
- Ublocks = ref [{Block_size = ref (~(!right_sum)),
+ BB{Pblocks = Unsynchronized.ref [],
+ Ublocks = Unsynchronized.ref [{Block_size = Unsynchronized.ref (~(!right_sum)),
Block_offset = offset,
How_to_indent = style}]});
push_delim_stack (!right_index, the_delim_stack)))
@@ -808,12 +808,12 @@
= ppstrm
in
if (delim_stack_is_empty the_delim_stack)
- then print_token(ppstrm,(E{Pend = ref 1, Uend = ref 0}))
+ then print_token(ppstrm,(E{Pend = Unsynchronized.ref 1, Uend = Unsynchronized.ref 0}))
else (E_inc_right_index ppstrm;
case (the_token_buffer sub (!right_index))
of (E{Uend, ...}) => Uend := !Uend + 1
| _ => (update(the_token_buffer,!right_index,
- E{Uend = ref 1, Pend = ref 0});
+ E{Uend = Unsynchronized.ref 1, Pend = Unsynchronized.ref 0});
push_delim_stack (!right_index, the_delim_stack)))
end
@@ -823,7 +823,7 @@
if (delim_stack_is_empty the_delim_stack)
then ()
else case(the_token_buffer sub (top_delim_stack the_delim_stack))
- of (BB{Ublocks as ref ((b as {Block_size, ...})::rst),
+ of (BB{Ublocks as Unsynchronized.ref ((b as {Block_size, ...})::rst),
Pblocks}) =>
if (k>0)
then (Block_size := !right_sum + !Block_size;
@@ -862,7 +862,7 @@
left_sum := 1; right_sum := 1)
else ++right_index;
update(the_token_buffer, !right_index,
- BR{Distance_to_next_break = ref (~(!right_sum)),
+ BR{Distance_to_next_break = Unsynchronized.ref (~(!right_sum)),
Number_of_blanks = n,
Break_offset = break_offset});
check_delim_stack ppstrm;
@@ -899,10 +899,10 @@
| fnl (_::rst) = fnl rst
| fnl _ = raise Fail "PP-error: fnl: internal error"
- fun set(dstack,BB{Ublocks as ref[{Block_size,...}:block_info],...}) =
+ fun set(dstack,BB{Ublocks as Unsynchronized.ref[{Block_size,...}:block_info],...}) =
(pop_bottom_delim_stack dstack;
Block_size := INFINITY)
- | set (_,BB {Ublocks = ref(_::rst), ...}) = fnl rst
+ | set (_,BB {Ublocks = Unsynchronized.ref(_::rst), ...}) = fnl rst
| set (dstack, E{Pend,Uend}) =
(Pend := (!Pend) + (!Uend);
Uend := 0;
@@ -958,7 +958,7 @@
(TextIO.print (">>>> Pretty-printer failure: " ^ msg ^ "\n"))
fun pp_to_string linewidth ppfn ob =
- let val l = ref ([]:string list)
+ let val l = Unsynchronized.ref ([]:string list)
fun attach s = l := (s::(!l))
in with_pp {consumer = attach, linewidth=linewidth, flush = fn()=>()}
(fn ppstrm => ppfn ppstrm ob);
@@ -995,7 +995,7 @@
(* Tracing. *)
(* ------------------------------------------------------------------------- *)
-val tracePrint : (string -> unit) ref
+val tracePrint : (string -> unit) Unsynchronized.ref
val trace : string -> unit
@@ -1228,7 +1228,7 @@
val newInts : int -> int list
-val withRef : 'r ref * 'r -> ('a -> 'b) -> 'a -> 'b
+val withRef : 'r Unsynchronized.ref * 'r -> ('a -> 'b) -> 'a -> 'b
val cloneArray : 'a Metis.Array.array -> 'a Metis.Array.array
@@ -1305,7 +1305,7 @@
(* Tracing *)
(* ------------------------------------------------------------------------- *)
-val tracePrint = ref print;
+val tracePrint = Unsynchronized.ref print;
fun trace message = !tracePrint message;
@@ -1629,7 +1629,7 @@
fun calcPrimes n = looking [] n (K true) 2
- val primesList = ref (calcPrimes 10);
+ val primesList = Unsynchronized.ref (calcPrimes 10);
in
fun primes n = CRITICAL (fn () =>
if length (!primesList) <= n then List.take (!primesList,n)
@@ -1828,7 +1828,7 @@
(* ------------------------------------------------------------------------- *)
local
- val generator = ref 0
+ val generator = Unsynchronized.ref 0
in
fun newInt () = CRITICAL (fn () =>
let
@@ -1986,12 +1986,12 @@
Value of 'a
| Thunk of unit -> 'a;
-datatype 'a lazy = Lazy of 'a thunk ref;
-
-fun delay f = Lazy (ref (Thunk f));
-
-fun force (Lazy (ref (Value v))) = v
- | force (Lazy (s as ref (Thunk f))) =
+datatype 'a lazy = Lazy of 'a thunk Unsynchronized.ref;
+
+fun delay f = Lazy (Unsynchronized.ref (Thunk f));
+
+fun force (Lazy (Unsynchronized.ref (Value v))) = v
+ | force (Lazy (s as Unsynchronized.ref (Thunk f))) =
let
val v = f ()
val () = s := Value v
@@ -4141,7 +4141,7 @@
fun cache cmp f =
let
- val cache = ref (Map.new cmp)
+ val cache = Unsynchronized.ref (Map.new cmp)
in
fn a =>
case Map.peek (!cache) a of
@@ -4620,7 +4620,7 @@
type 'a pp = ppstream -> 'a -> unit
-val lineLength : int ref
+val lineLength : int Unsynchronized.ref
val beginBlock : ppstream -> breakStyle -> int -> unit
@@ -4797,7 +4797,7 @@
type 'a pp = PP.ppstream -> 'a -> unit;
-val lineLength = ref 75;
+val lineLength = Unsynchronized.ref 75;
fun beginBlock pp Consistent = PP.begin_block pp PP.CONSISTENT
| beginBlock pp Inconsistent = PP.begin_block pp PP.INCONSISTENT;
@@ -5766,19 +5766,19 @@
(* Infix symbols *)
-val infixes : Metis.Parser.infixities ref
+val infixes : Metis.Parser.infixities Unsynchronized.ref
(* The negation symbol *)
-val negation : Metis.Name.name ref
+val negation : Metis.Name.name Unsynchronized.ref
(* Binder symbols *)
-val binders : Metis.Name.name list ref
+val binders : Metis.Name.name list Unsynchronized.ref
(* Bracket symbols *)
-val brackets : (Metis.Name.name * Metis.Name.name) list ref
+val brackets : (Metis.Name.name * Metis.Name.name) list Unsynchronized.ref
(* Pretty printing *)
@@ -6137,7 +6137,7 @@
(* Operators parsed and printed infix *)
-val infixes : Parser.infixities ref = ref
+val infixes : Parser.infixities Unsynchronized.ref = Unsynchronized.ref
[(* ML symbols *)
{token = " / ", precedence = 7, leftAssoc = true},
{token = " div ", precedence = 7, leftAssoc = true},
@@ -6174,15 +6174,15 @@
(* The negation symbol *)
-val negation : Name.name ref = ref "~";
+val negation : Name.name Unsynchronized.ref = Unsynchronized.ref "~";
(* Binder symbols *)
-val binders : Name.name list ref = ref ["\\","!","?","?!"];
+val binders : Name.name list Unsynchronized.ref = Unsynchronized.ref ["\\","!","?","?!"];
(* Bracket symbols *)
-val brackets : (Name.name * Name.name) list ref = ref [("[","]"),("{","}")];
+val brackets : (Name.name * Name.name) list Unsynchronized.ref = Unsynchronized.ref [("[","]"),("{","}")];
(* Pretty printing *)
@@ -11051,11 +11051,11 @@
val newSkolemFunction =
let
- val counter : int NameMap.map ref = ref (NameMap.new ())
+ val counter : int NameMap.map Unsynchronized.ref = Unsynchronized.ref (NameMap.new ())
in
fn n => CRITICAL (fn () =>
let
- val ref m = counter
+ val Unsynchronized.ref m = counter
val i = Option.getOpt (NameMap.peek m n, 0)
val () = counter := NameMap.insert m (n, i + 1)
in
@@ -11249,11 +11249,11 @@
val newDefinitionRelation =
let
- val counter : int ref = ref 0
+ val counter : int Unsynchronized.ref = Unsynchronized.ref 0
in
fn () => CRITICAL (fn () =>
let
- val ref i = counter
+ val Unsynchronized.ref i = counter
val () = counter := i + 1
in
"defCNF_" ^ Int.toString i
@@ -11820,8 +11820,8 @@
Model of
{size : int,
fixed : fixedModel,
- functions : (Term.functionName * int list, int) Map.map ref,
- relations : (Atom.relationName * int list, bool) Map.map ref};
+ functions : (Term.functionName * int list, int) Map.map Unsynchronized.ref,
+ relations : (Atom.relationName * int list, bool) Map.map Unsynchronized.ref};
local
fun cmp ((n1,l1),(n2,l2)) =
@@ -11834,8 +11834,8 @@
Model
{size = N,
fixed = fixed {size = N},
- functions = ref (Map.new cmp),
- relations = ref (Map.new cmp)};
+ functions = Unsynchronized.ref (Map.new cmp),
+ relations = Unsynchronized.ref (Map.new cmp)};
end;
fun size (Model {size = s, ...}) = s;
@@ -11905,7 +11905,7 @@
| (Term.Fn (f,tms), tms') => (f, tms @ tms')
val elts = map interpret tms
val f_elts = (f,elts)
- val ref funcs = functions
+ val Unsynchronized.ref funcs = functions
in
case Map.peek funcs f_elts of
SOME k => k
@@ -11932,7 +11932,7 @@
val elts = map (interpretTerm M V) tms
val r_elts = (r,elts)
- val ref rels = relations
+ val Unsynchronized.ref rels = relations
in
case Map.peek rels r_elts of
SOME b => b
@@ -14717,7 +14717,7 @@
(* Pretty printing. *)
(* ------------------------------------------------------------------------- *)
-val showId : bool ref
+val showId : bool Unsynchronized.ref
val pp : clause Metis.Parser.pp
@@ -14747,10 +14747,10 @@
val newId =
let
- val r = ref 0
+ val r = Unsynchronized.ref 0
in
fn () => CRITICAL (fn () =>
- case r of ref n => let val () = r := n + 1 in n end)
+ case r of Unsynchronized.ref n => let val () = r := n + 1 in n end)
end;
(* ------------------------------------------------------------------------- *)
@@ -14777,7 +14777,7 @@
(* Pretty printing. *)
(* ------------------------------------------------------------------------- *)
-val showId = ref false;
+val showId = Unsynchronized.ref false;
local
val ppIdThm = Parser.ppPair Parser.ppInt Thm.pp;
@@ -16372,9 +16372,9 @@
(* Mapping TPTP functions and relations to different names. *)
(* ------------------------------------------------------------------------- *)
-val functionMapping : {name : string, arity : int, tptp : string} list ref
-
-val relationMapping : {name : string, arity : int, tptp : string} list ref
+val functionMapping : {name : string, arity : int, tptp : string} list Unsynchronized.ref
+
+val relationMapping : {name : string, arity : int, tptp : string} list Unsynchronized.ref
(* ------------------------------------------------------------------------- *)
(* TPTP literals. *)
@@ -16491,7 +16491,7 @@
(* Mapping TPTP functions and relations to different names. *)
(* ------------------------------------------------------------------------- *)
-val functionMapping = ref
+val functionMapping = Unsynchronized.ref
[(* Mapping TPTP functions to infix symbols *)
{name = "*", arity = 2, tptp = "multiply"},
{name = "/", arity = 2, tptp = "divide"},
@@ -16504,7 +16504,7 @@
{name = ".", arity = 2, tptp = "apply"},
{name = "<=", arity = 0, tptp = "less_equal"}];
-val relationMapping = ref
+val relationMapping = Unsynchronized.ref
[(* Mapping TPTP relations to infix symbols *)
{name = "=", arity = 2, tptp = "="},
{name = "==", arity = 2, tptp = "equalish"},
--- a/src/Tools/auto_solve.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Tools/auto_solve.ML Tue Sep 29 18:14:08 2009 +0200
@@ -11,9 +11,9 @@
signature AUTO_SOLVE =
sig
- val auto : bool ref
- val auto_time_limit : int ref
- val limit : int ref
+ val auto : bool Unsynchronized.ref
+ val auto_time_limit : int Unsynchronized.ref
+ val limit : int Unsynchronized.ref
end;
structure AutoSolve : AUTO_SOLVE =
@@ -21,9 +21,9 @@
(* preferences *)
-val auto = ref false;
-val auto_time_limit = ref 2500;
-val limit = ref 5;
+val auto = Unsynchronized.ref false;
+val auto_time_limit = Unsynchronized.ref 2500;
+val limit = Unsynchronized.ref 5;
val _ =
ProofGeneralPgip.add_preference Preferences.category_tracing
--- a/src/Tools/coherent.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Tools/coherent.ML Tue Sep 29 18:14:08 2009 +0200
@@ -20,8 +20,8 @@
signature COHERENT =
sig
- val verbose: bool ref
- val show_facts: bool ref
+ val verbose: bool Unsynchronized.ref
+ val show_facts: bool Unsynchronized.ref
val coherent_tac: Proof.context -> thm list -> int -> tactic
val setup: theory -> theory
end;
@@ -31,7 +31,7 @@
(** misc tools **)
-val verbose = ref false;
+val verbose = Unsynchronized.ref false;
fun message f = if !verbose then tracing (f ()) else ();
@@ -117,7 +117,7 @@
| NONE => is_valid_disj ctxt facts ds
end;
-val show_facts = ref false;
+val show_facts = Unsynchronized.ref false;
fun string_of_facts ctxt s facts = space_implode "\n"
(s :: map (Syntax.string_of_term ctxt)
--- a/src/Tools/eqsubst.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Tools/eqsubst.ML Tue Sep 29 18:14:08 2009 +0200
@@ -278,8 +278,8 @@
* (string * typ) list (* Type abs env *)
* term) (* outer term *);
-val trace_subst_err = (ref NONE : trace_subst_errT option ref);
-val trace_subst_search = ref false;
+val trace_subst_err = (Unsynchronized.ref NONE : trace_subst_errT option Unsynchronized.ref);
+val trace_subst_search = Unsynchronized.ref false;
exception trace_subst_exp of trace_subst_errT;
*)
--- a/src/Tools/more_conv.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Tools/more_conv.ML Tue Sep 29 18:14:08 2009 +0200
@@ -46,11 +46,11 @@
Conv.arg_conv (Conv.abs_conv (fn (_, cx) => cv cx) ctxt)
-fun cache_conv conv =
+fun cache_conv conv = (* FIXME not thread-safe *)
let
- val tab = ref Termtab.empty
+ val tab = Unsynchronized.ref Termtab.empty
fun add_result t thm =
- let val _ = change tab (Termtab.insert Thm.eq_thm (t, thm))
+ let val _ = Unsynchronized.change tab (Termtab.insert Thm.eq_thm (t, thm))
in thm end
fun cconv ct =
(case Termtab.lookup (!tab) (Thm.term_of ct) of
--- a/src/Tools/nbe.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Tools/nbe.ML Tue Sep 29 18:14:08 2009 +0200
@@ -19,8 +19,8 @@
(*abstractions as closures*)
val same: Univ -> Univ -> bool
- val univs_ref: (unit -> Univ list -> Univ list) option ref
- val trace: bool ref
+ val univs_ref: (unit -> Univ list -> Univ list) option Unsynchronized.ref
+ val trace: bool Unsynchronized.ref
val setup: theory -> theory
val add_const_alias: thm -> theory -> theory
@@ -31,7 +31,7 @@
(* generic non-sense *)
-val trace = ref false;
+val trace = Unsynchronized.ref false;
fun traced f x = if !trace then (tracing (f x); x) else x;
@@ -216,7 +216,7 @@
(* nbe specific syntax and sandbox communication *)
-val univs_ref = ref (NONE : (unit -> Univ list -> Univ list) option);
+val univs_ref = Unsynchronized.ref (NONE : (unit -> Univ list -> Univ list) option);
local
val prefix = "Nbe.";
--- a/src/Tools/quickcheck.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Tools/quickcheck.ML Tue Sep 29 18:14:08 2009 +0200
@@ -6,8 +6,8 @@
signature QUICKCHECK =
sig
- val auto: bool ref
- val auto_time_limit: int ref
+ val auto: bool Unsynchronized.ref
+ val auto_time_limit: int Unsynchronized.ref
val test_term: Proof.context -> bool -> string option -> int -> int -> term ->
(string * term) list option
val add_generator: string * (Proof.context -> term -> int -> term list option) -> theory -> theory
@@ -19,8 +19,8 @@
(* preferences *)
-val auto = ref false;
-val auto_time_limit = ref 2500;
+val auto = Unsynchronized.ref false;
+val auto_time_limit = Unsynchronized.ref 2500;
val _ =
ProofGeneralPgip.add_preference Preferences.category_tracing
--- a/src/Tools/random_word.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/Tools/random_word.ML Tue Sep 29 18:14:08 2009 +0200
@@ -35,8 +35,8 @@
val a = 0w777138309;
fun step x = Word.andb (a * x + 0w1, max_word);
-local val rand = ref 0w1
-in fun next_word () = (change rand step; ! rand) end;
+local val rand = Unsynchronized.ref 0w1
+in fun next_word () = (Unsynchronized.change rand step; ! rand) end;
(*NB: higher bits are more random than lower ones*)
fun next_bool () = Word.andb (next_word (), top_bit) = 0w0;
--- a/src/ZF/Datatype_ZF.thy Tue Sep 29 14:26:33 2009 +1000
+++ b/src/ZF/Datatype_ZF.thy Tue Sep 29 18:14:08 2009 +0200
@@ -59,7 +59,7 @@
(*Simproc for freeness reasoning: compare datatype constructors for equality*)
structure DataFree =
struct
- val trace = ref false;
+ val trace = Unsynchronized.ref false;
fun mk_new ([],[]) = Const("True",FOLogic.oT)
| mk_new (largs,rargs) =
--- a/src/ZF/ZF.thy Tue Sep 29 14:26:33 2009 +1000
+++ b/src/ZF/ZF.thy Tue Sep 29 18:14:08 2009 +0200
@@ -8,7 +8,7 @@
theory ZF imports FOL begin
-ML {* reset eta_contract *}
+ML {* Unsynchronized.reset eta_contract *}
global
--- a/src/ZF/ind_syntax.ML Tue Sep 29 14:26:33 2009 +1000
+++ b/src/ZF/ind_syntax.ML Tue Sep 29 18:14:08 2009 +0200
@@ -10,7 +10,7 @@
struct
(*Print tracing messages during processing of "inductive" theory sections*)
-val trace = ref false;
+val trace = Unsynchronized.ref false;
fun traceIt msg thy t =
if !trace then (tracing (msg ^ Syntax.string_of_term_global thy t); t)