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