# HG changeset patch # User wenzelm # Date 1374145974 -7200 # Node ID 38466f4f348338e461699bb570a31157071b98e8 # Parent b24d11ab44ff1095dfadaae0ceac66f346af6861 immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 -> 100000, JinjaThreads: 65000 -> 300000) -- minimal measurable impact on inference kernel performance; diff -r b24d11ab44ff -r 38466f4f3483 src/HOL/Tools/Nitpick/nitpick_model.ML --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Wed Jul 17 23:51:10 2013 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Jul 18 13:12:54 2013 +0200 @@ -94,7 +94,7 @@ fun add_wacky_syntax ctxt = let val name_of = fst o dest_Const - val thy = Proof_Context.theory_of ctxt |> Context.reject_draft + val thy = Proof_Context.theory_of ctxt val (maybe_t, thy) = Sign.declare_const_global ((@{binding nitpick_maybe}, @{typ "'a => 'a"}), Mixfix (maybe_mixfix (), [1000], 1000)) thy diff -r b24d11ab44ff -r 38466f4f3483 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Wed Jul 17 23:51:10 2013 +0200 +++ b/src/Pure/Isar/toplevel.ML Thu Jul 18 13:12:54 2013 +0200 @@ -255,14 +255,6 @@ fun reset_presentation (Theory (gthy, _)) = Theory (gthy, NONE) | reset_presentation node = node; -fun is_draft_theory (Theory (gthy, _)) = Context.is_draft (Context.theory_of gthy) - | is_draft_theory _ = false; - -fun is_stale state = Context.is_stale (theory_of state) handle Runtime.UNDEF => false; - -fun stale_error NONE = SOME (ERROR "Stale theory encountered after successful execution!") - | stale_error some = some; - fun map_theory f (Theory (gthy, ctxt)) = Theory (Context.mapping f (Local_Theory.raw_theory f) gthy, ctxt) | map_theory _ node = node; @@ -271,9 +263,7 @@ fun apply_transaction f g node = let - val _ = is_draft_theory node andalso error "Illegal draft theory in toplevel state"; val cont_node = reset_presentation node; - val back_node = map_theory (Theory.checkpoint o Theory.copy) cont_node; fun state_error e nd = (State (SOME nd, SOME node), e); val (result, err) = @@ -282,14 +272,10 @@ |> map_theory Theory.checkpoint |> state_error NONE handle exn => state_error (SOME exn) cont_node; - - val (result', err') = - if is_stale result then state_error (stale_error err) back_node - else (result, err); in - (case err' of - NONE => tap g result' - | SOME exn => raise FAILURE (result', exn)) + (case err of + NONE => tap g result + | SOME exn => raise FAILURE (result, exn)) end; val exit_transaction = diff -r b24d11ab44ff -r 38466f4f3483 src/Pure/context.ML --- a/src/Pure/context.ML Wed Jul 17 23:51:10 2013 +0200 +++ b/src/Pure/context.ML Thu Jul 18 13:12:54 2013 +0200 @@ -34,9 +34,6 @@ val parents_of: theory -> theory list val ancestors_of: theory -> theory list val theory_name: theory -> string - val is_stale: theory -> bool - val is_draft: theory -> bool - val reject_draft: theory -> theory val PureN: string val display_names: theory -> string list val pretty_thy: theory -> Pretty.T @@ -52,8 +49,6 @@ val joinable: theory * theory -> bool val merge: theory * theory -> theory val merge_refs: theory_ref * theory_ref -> theory_ref - val copy_thy: theory -> theory - val checkpoint_thy: theory -> theory val finish_thy: theory -> theory val begin_thy: (theory -> pretty) -> string -> theory list -> theory (*proof context*) @@ -166,18 +161,16 @@ datatype theory = Theory of (*identity*) - {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*) + {id: serial, (*identifier*) + ids: Inttab.set} * (*cumulative identifiers -- symbolic body content*) (*data*) - Any.T Datatab.table * (*body content*) + Any.T Datatab.table * (*body content*) (*ancestry*) {parents: theory list, (*immediate predecessors*) ancestors: theory list} * (*all predecessors -- canonical reverse order*) (*history*) {name: string, (*official theory name*) - stage: int}; (*checkpoint counter*) + stage: int}; (*counter for anonymous updates*) exception THEORY of string * theory list; @@ -188,60 +181,28 @@ val ancestry_of = #3 o rep_theory; val history_of = #4 o rep_theory; -fun make_identity self draft id ids = {self = self, draft = draft, id = id, ids = ids}; +fun make_identity id ids = {id = id, ids = ids}; fun make_ancestry parents ancestors = {parents = parents, ancestors = ancestors}; fun make_history name stage = {name = name, stage = stage}; -val the_self = the o #self o identity_of; val parents_of = #parents o ancestry_of; val ancestors_of = #ancestors o ancestry_of; val theory_name = #name o history_of; -(* staleness *) - -fun eq_id (i: int, j) = i = j; - -fun is_stale - (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 = Unsynchronized.ref thy; - val thy' = Theory (make_identity (SOME r) draft id ids, data, ancestry, history); - in r := thy'; thy' end; - - -(* draft mode *) - -val is_draft = #draft o identity_of; - -fun reject_draft thy = - if is_draft thy then - raise THEORY ("Illegal draft theory -- stable checkpoint required", [thy]) - else thy; - - (* names *) val PureN = "Pure"; -val draftN = "#"; val finished = ~1; fun display_names thy = let - val draft = if is_draft thy then [draftN] else []; - val {stage, ...} = history_of thy; - val name = - if stage = finished then theory_name thy - else theory_name thy ^ ":" ^ string_of_int stage; + val {name, stage} = history_of thy; + val name' = + if stage = finished then name + else name ^ ":" ^ string_of_int stage; val ancestor_names = map theory_name (ancestors_of thy); - val stale = if is_stale thy then ["!"] else []; - in rev (stale @ draft @ [name] @ ancestor_names) end; + in rev (name' :: ancestor_names) end; val pretty_thy = Pretty.str_list "{" "}" o display_names; val string_of_thy = Pretty.string_of o pretty_thy; @@ -268,40 +229,29 @@ else get_theory thy name; -(* theory references *) - -(*theory_ref provides a safe way to store dynamic references to a - theory in external data structures -- a plain theory value would - become stale as the self reference moves on*) - -datatype theory_ref = Theory_Ref of theory Unsynchronized.ref; +(* theory references *) (* FIXME dummy *) -fun deref (Theory_Ref (Unsynchronized.ref thy)) = thy; +datatype theory_ref = Theory_Ref of theory; -fun check_thy thy = (*thread-safe version*) - let val thy_ref = Theory_Ref (the_self thy) in - if is_stale thy then error ("Stale theory encountered:\n" ^ string_of_thy thy) - else thy_ref - end; +fun deref (Theory_Ref thy) = thy; +fun check_thy thy = Theory_Ref thy; (* build ids *) -fun insert_id draft id ids = - if draft then ids - else Inttab.update (id, ()) ids; +fun insert_id id ids = Inttab.update (id, ()) ids; fun merge_ids - (Theory ({draft = draft1, id = id1, ids = ids1, ...}, _, _, _)) - (Theory ({draft = draft2, id = id2, ids = ids2, ...}, _, _, _)) = + (Theory ({id = id1, ids = ids1, ...}, _, _, _)) + (Theory ({id = id2, ids = ids2, ...}, _, _, _)) = Inttab.merge (K true) (ids1, ids2) - |> insert_id draft1 id1 - |> insert_id draft2 id2; + |> insert_id id1 + |> insert_id id2; (* equality and inclusion *) -val eq_thy = eq_id o pairself (#id o identity_of); +val eq_thy = op = o pairself (#id o identity_of); fun proper_subthy (Theory ({id, ...}, _, _, _), Theory ({ids, ...}, _, _, _)) = Inttab.defined ids id; @@ -335,9 +285,7 @@ else error (cat_lines ["Attempt to perform non-trivial merge of theories:", str_of_thy thy1, str_of_thy thy2]); -fun merge_refs (ref1, ref2) = - if ref1 = ref2 then ref1 - else check_thy (merge (deref ref1, deref ref2)); +fun merge_refs (ref1, ref2) = check_thy (merge (deref ref1, deref ref2)); @@ -345,44 +293,33 @@ (* primitives *) -local - val lock = Mutex.mutex (); -in - fun SYNCHRONIZED e = Simple_Thread.synchronized "theory" lock e; -end; +fun create_thy ids data ancestry history = + Theory (make_identity (serial ()) ids, data, ancestry, history); -fun create_thy self draft ids data ancestry history = - let val identity = make_identity self draft (serial ()) ids; - in vitalize (Theory (identity, data, ancestry, history)) end; +val pre_pure_thy = + create_thy Inttab.empty Datatab.empty (make_ancestry [] []) (make_history PureN 0); -fun change_thy draft' f thy = +local + +fun change_thy finish f thy = let - val Theory ({self, draft, id, ids}, data, ancestry, history) = thy; - val (self', data', ancestry') = - if draft then (self, data, ancestry) (*destructive change!*) - else if #stage history > 0 - then (NONE, data, ancestry) - else (NONE, extend_data data, make_ancestry [thy] (extend_ancestors thy (ancestors_of thy))); - val ids' = insert_id draft id ids; + val Theory ({id, ids}, data, ancestry, {name, stage}) = thy; + val (data', ancestry') = + if stage = finished then + (extend_data data, make_ancestry [thy] (extend_ancestors thy (ancestors_of thy))) + else (data, ancestry); + val history' = {name = name, stage = if finish then finished else stage + 1}; + val ids' = insert_id id ids; val data'' = f data'; - val thy' = SYNCHRONIZED (fn () => - (check_thy thy; create_thy self' draft' ids' data'' ancestry' history)); - in thy' end; + in create_thy ids' data'' ancestry' history' end; -val name_thy = change_thy false I; -val extend_thy = change_thy true I; -val modify_thy = change_thy true; +in -fun copy_thy thy = - let - val Theory ({draft, id, ids, ...}, data, ancestry, history) = thy; - val ids' = insert_id draft id ids; - val thy' = SYNCHRONIZED (fn () => - (check_thy thy; create_thy NONE true ids' data ancestry history)); - in thy' end; +val update_thy = change_thy false; +val extend_thy = update_thy I; +val finish_thy = change_thy true I; -val pre_pure_thy = create_thy NONE true Inttab.empty - Datatab.empty (make_ancestry [] []) (make_history PureN 0); +end; (* named theory nodes *) @@ -393,15 +330,13 @@ val data = merge_data (pp thy1) (data_of thy1, data_of thy2); val ancestry = make_ancestry [] []; val history = make_history "" 0; - val thy' = SYNCHRONIZED (fn () => - (check_thy thy1; check_thy thy2; create_thy NONE true ids data ancestry history)); - in thy' end; + in create_thy ids data ancestry history end; fun maximal_thys thys = thys |> filter_out (fn thy => exists (fn thy' => proper_subthy (thy, thy')) thys); fun begin_thy pp name imports = - if name = "" orelse name = draftN then error ("Bad theory name: " ^ quote name) + if name = "" then error ("Bad theory name: " ^ quote name) else let val parents = maximal_thys (distinct eq_thy imports); @@ -417,28 +352,7 @@ val ancestry = make_ancestry parents ancestors; val history = make_history name 0; - val thy' = SYNCHRONIZED (fn () => - (map check_thy imports; create_thy NONE true ids data ancestry history)); - in thy' end; - - -(* history stages *) - -fun history_stage f thy = - let - val {name, stage} = history_of thy; - val _ = stage = finished andalso raise THEORY ("Theory already finished", [thy]); - val history' = make_history name (f stage); - val thy' as Theory (identity', data', ancestry', _) = name_thy thy; - val thy'' = SYNCHRONIZED (fn () => - (check_thy thy'; vitalize (Theory (identity', data', ancestry', history')))); - in thy'' end; - -fun checkpoint_thy thy = - if is_draft thy then history_stage (fn stage => stage + 1) thy - else thy; - -val finish_thy = history_stage (fn _ => finished); + in create_thy ids data ancestry history end; (* theory data *) @@ -453,7 +367,7 @@ SOME x => x | NONE => invoke_empty k) |> dest; -fun put k mk x = modify_thy (Datatab.update (k, mk x)); +fun put k mk x = update_thy (Datatab.update (k, mk x)); end; diff -r b24d11ab44ff -r 38466f4f3483 src/Pure/goal.ML --- a/src/Pure/goal.ML Wed Jul 17 23:51:10 2013 +0200 +++ b/src/Pure/goal.ML Thu Jul 18 13:12:54 2013 +0200 @@ -232,7 +232,6 @@ fun future_result ctxt result prop = let val thy = Proof_Context.theory_of ctxt; - val _ = Context.reject_draft thy; val cert = Thm.cterm_of thy; val certT = Thm.ctyp_of thy; diff -r b24d11ab44ff -r 38466f4f3483 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Wed Jul 17 23:51:10 2013 +0200 +++ b/src/Pure/proofterm.ML Thu Jul 18 13:12:54 2013 +0200 @@ -1491,7 +1491,6 @@ postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) (Future.join body)); in if null promises then Future.map postproc body - else if Context.is_draft thy then Future.value (fulfill ()) else if Future.is_finished body andalso length promises = 1 then Future.map (fn _ => fulfill ()) (snd (hd promises)) else @@ -1546,18 +1545,16 @@ (Type.strip_sorts o atyp_map) args; val argsP = map OfClass outer_constraints @ map Hyp hyps; - fun full_proof0 () = - #4 (shrink_proof thy [] 0 (rew_proof thy (fold_rev implies_intr_proof hyps prf))); - fun make_body0 proof0 = PBody {oracles = oracles0, thms = thms0, proof = proof0}; val body0 = if not (proofs_enabled ()) then Future.value (make_body0 MinProof) - else if Context.is_draft thy then Future.value (make_body0 (full_proof0 ())) else (singleton o Future.cond_forks) {name = "Proofterm.prepare_thm_proof", group = NONE, deps = [], pri = 0, interrupts = true} - (make_body0 o full_proof0); + (fn () => + make_body0 + (#4 (shrink_proof thy [] 0 (rew_proof thy (fold_rev implies_intr_proof hyps prf))))); fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0); val (i, body') = diff -r b24d11ab44ff -r 38466f4f3483 src/Pure/theory.ML --- a/src/Pure/theory.ML Wed Jul 17 23:51:10 2013 +0200 +++ b/src/Pure/theory.ML Thu Jul 18 13:12:54 2013 +0200 @@ -64,8 +64,8 @@ fun merge_list [] = raise THEORY ("Empty merge of theories", []) | merge_list (thy :: thys) = Library.foldl merge (thy, thys); -val checkpoint = Context.checkpoint_thy; -val copy = Context.copy_thy; +val checkpoint : theory -> theory = I; (* FIXME dummy *) +val copy : theory -> theory = I; (* FIXME dummy *) fun requires thy name what = if exists (fn thy' => Context.theory_name thy' = name) (nodes_of thy) then () diff -r b24d11ab44ff -r 38466f4f3483 src/Pure/thm.ML --- a/src/Pure/thm.ML Wed Jul 17 23:51:10 2013 +0200 +++ b/src/Pure/thm.ML Thu Jul 18 13:12:54 2013 +0200 @@ -569,7 +569,7 @@ fun future future_thm ct = let val Cterm {thy_ref = thy_ref, t = prop, T, maxidx, sorts} = ct; - val thy = Context.reject_draft (Theory.deref thy_ref); + val thy = Theory.deref thy_ref; val _ = T <> propT andalso raise CTERM ("future: prop expected", [ct]); val i = serial ();