--- a/src/CCL/ROOT.ML Tue Sep 29 14:59:24 2009 +0200
+++ b/src/CCL/ROOT.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/FOLP/IFOLP.thy Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/FOLP/simp.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Code_Evaluation.thy Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Fun.thy Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/HOL.thy Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Import/hol4rews.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Import/import.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Import/import_syntax.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Import/importrecorder.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Import/lazy_seq.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Import/proof_kernel.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Import/shuffler.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Library/Eval_Witness.thy Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Library/positivstellensatz.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Matrix/cplex/Cplex_tools.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Modelcheck/EindhovenSyn.thy Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Prolog/prolog.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Random.thy Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/SMT/Tools/smt_normalize.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Statespace/DistinctTreeProver.thy Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Tools/Function/fundef_common.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Tools/Function/scnp_solve.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Tools/TFL/rules.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Tools/lin_arith.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Tools/meson.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Tools/polyhash.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Tools/prop_logic.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Tools/record.ML Tue Sep 29 16:24:36 2009 +0200
@@ -15,15 +15,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
@@ -118,7 +118,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 ();
@@ -671,8 +671,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)))
@@ -864,7 +864,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:59:24 2009 +0200
+++ b/src/HOL/Tools/res_axioms.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Tools/sat_funcs.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/Tools/sat_solver.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/ex/SVC_Oracle.thy Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOL/ex/svc_funcs.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/Provers/blast.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/Provers/classical.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/Provers/order.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/Provers/quasi.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/Provers/trancl.ML Tue Sep 29 16:24:36 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/Sequents/prover.ML Tue Sep 29 14:59:24 2009 +0200
+++ b/src/Sequents/prover.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/Tools/Code/code_ml.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/Tools/Code/code_target.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/Tools/Compute_Oracle/am_compiler.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/Tools/Compute_Oracle/am_ghc.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/Tools/Compute_Oracle/am_interpreter.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/Tools/Compute_Oracle/am_sml.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/Tools/Compute_Oracle/compute.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/Tools/Compute_Oracle/linker.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/Tools/Compute_Oracle/report.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/Tools/Metis/make-metis Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/Tools/Metis/metis.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/Tools/auto_solve.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/Tools/coherent.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/Tools/eqsubst.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/Tools/more_conv.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/Tools/nbe.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/Tools/quickcheck.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/Tools/random_word.ML Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/ZF/Datatype_ZF.thy Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/ZF/ZF.thy Tue Sep 29 16:24:36 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:59:24 2009 +0200
+++ b/src/ZF/ind_syntax.ML Tue Sep 29 16:24:36 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)