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;
authorwenzelm
Thu Jul 18 13:12:54 2013 +0200 (2013-07-18)
changeset 5269638466f4f3483
parent 52695 b24d11ab44ff
child 52697 6fb98a20c349
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;
src/HOL/Tools/Nitpick/nitpick_model.ML
src/Pure/Isar/toplevel.ML
src/Pure/context.ML
src/Pure/goal.ML
src/Pure/proofterm.ML
src/Pure/theory.ML
src/Pure/thm.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Jul 17 23:51:10 2013 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Jul 18 13:12:54 2013 +0200
     1.3 @@ -94,7 +94,7 @@
     1.4  fun add_wacky_syntax ctxt =
     1.5    let
     1.6      val name_of = fst o dest_Const
     1.7 -    val thy = Proof_Context.theory_of ctxt |> Context.reject_draft
     1.8 +    val thy = Proof_Context.theory_of ctxt
     1.9      val (maybe_t, thy) =
    1.10        Sign.declare_const_global ((@{binding nitpick_maybe}, @{typ "'a => 'a"}),
    1.11                            Mixfix (maybe_mixfix (), [1000], 1000)) thy
     2.1 --- a/src/Pure/Isar/toplevel.ML	Wed Jul 17 23:51:10 2013 +0200
     2.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Jul 18 13:12:54 2013 +0200
     2.3 @@ -255,14 +255,6 @@
     2.4  fun reset_presentation (Theory (gthy, _)) = Theory (gthy, NONE)
     2.5    | reset_presentation node = node;
     2.6  
     2.7 -fun is_draft_theory (Theory (gthy, _)) = Context.is_draft (Context.theory_of gthy)
     2.8 -  | is_draft_theory _ = false;
     2.9 -
    2.10 -fun is_stale state = Context.is_stale (theory_of state) handle Runtime.UNDEF => false;
    2.11 -
    2.12 -fun stale_error NONE = SOME (ERROR "Stale theory encountered after successful execution!")
    2.13 -  | stale_error some = some;
    2.14 -
    2.15  fun map_theory f (Theory (gthy, ctxt)) =
    2.16        Theory (Context.mapping f (Local_Theory.raw_theory f) gthy, ctxt)
    2.17    | map_theory _ node = node;
    2.18 @@ -271,9 +263,7 @@
    2.19  
    2.20  fun apply_transaction f g node =
    2.21    let
    2.22 -    val _ = is_draft_theory node andalso error "Illegal draft theory in toplevel state";
    2.23      val cont_node = reset_presentation node;
    2.24 -    val back_node = map_theory (Theory.checkpoint o Theory.copy) cont_node;
    2.25      fun state_error e nd = (State (SOME nd, SOME node), e);
    2.26  
    2.27      val (result, err) =
    2.28 @@ -282,14 +272,10 @@
    2.29        |> map_theory Theory.checkpoint
    2.30        |> state_error NONE
    2.31        handle exn => state_error (SOME exn) cont_node;
    2.32 -
    2.33 -    val (result', err') =
    2.34 -      if is_stale result then state_error (stale_error err) back_node
    2.35 -      else (result, err);
    2.36    in
    2.37 -    (case err' of
    2.38 -      NONE => tap g result'
    2.39 -    | SOME exn => raise FAILURE (result', exn))
    2.40 +    (case err of
    2.41 +      NONE => tap g result
    2.42 +    | SOME exn => raise FAILURE (result, exn))
    2.43    end;
    2.44  
    2.45  val exit_transaction =
     3.1 --- a/src/Pure/context.ML	Wed Jul 17 23:51:10 2013 +0200
     3.2 +++ b/src/Pure/context.ML	Thu Jul 18 13:12:54 2013 +0200
     3.3 @@ -34,9 +34,6 @@
     3.4    val parents_of: theory -> theory list
     3.5    val ancestors_of: theory -> theory list
     3.6    val theory_name: theory -> string
     3.7 -  val is_stale: theory -> bool
     3.8 -  val is_draft: theory -> bool
     3.9 -  val reject_draft: theory -> theory
    3.10    val PureN: string
    3.11    val display_names: theory -> string list
    3.12    val pretty_thy: theory -> Pretty.T
    3.13 @@ -52,8 +49,6 @@
    3.14    val joinable: theory * theory -> bool
    3.15    val merge: theory * theory -> theory
    3.16    val merge_refs: theory_ref * theory_ref -> theory_ref
    3.17 -  val copy_thy: theory -> theory
    3.18 -  val checkpoint_thy: theory -> theory
    3.19    val finish_thy: theory -> theory
    3.20    val begin_thy: (theory -> pretty) -> string -> theory list -> theory
    3.21    (*proof context*)
    3.22 @@ -166,18 +161,16 @@
    3.23  datatype theory =
    3.24    Theory of
    3.25     (*identity*)
    3.26 -   {self: theory Unsynchronized.ref option,  (*dynamic self reference -- follows theory changes*)
    3.27 -    draft: bool,                  (*draft mode -- linear destructive changes*)
    3.28 -    id: serial,                   (*identifier*)
    3.29 -    ids: unit Inttab.table} *     (*cumulative identifiers of non-drafts -- symbolic body content*)
    3.30 +   {id: serial,                   (*identifier*)
    3.31 +    ids: Inttab.set} *            (*cumulative identifiers -- symbolic body content*)
    3.32     (*data*)
    3.33 -   Any.T Datatab.table *       (*body content*)
    3.34 +   Any.T Datatab.table *          (*body content*)
    3.35     (*ancestry*)
    3.36     {parents: theory list,         (*immediate predecessors*)
    3.37      ancestors: theory list} *     (*all predecessors -- canonical reverse order*)
    3.38     (*history*)
    3.39     {name: string,                 (*official theory name*)
    3.40 -    stage: int};                  (*checkpoint counter*)
    3.41 +    stage: int};                  (*counter for anonymous updates*)
    3.42  
    3.43  exception THEORY of string * theory list;
    3.44  
    3.45 @@ -188,60 +181,28 @@
    3.46  val ancestry_of = #3 o rep_theory;
    3.47  val history_of = #4 o rep_theory;
    3.48  
    3.49 -fun make_identity self draft id ids = {self = self, draft = draft, id = id, ids = ids};
    3.50 +fun make_identity id ids = {id = id, ids = ids};
    3.51  fun make_ancestry parents ancestors = {parents = parents, ancestors = ancestors};
    3.52  fun make_history name stage = {name = name, stage = stage};
    3.53  
    3.54 -val the_self = the o #self o identity_of;
    3.55  val parents_of = #parents o ancestry_of;
    3.56  val ancestors_of = #ancestors o ancestry_of;
    3.57  val theory_name = #name o history_of;
    3.58  
    3.59  
    3.60 -(* staleness *)
    3.61 -
    3.62 -fun eq_id (i: int, j) = i = j;
    3.63 -
    3.64 -fun is_stale
    3.65 -    (Theory ({self =
    3.66 -        SOME (Unsynchronized.ref (Theory ({id = id', ...}, _, _, _))), id, ...}, _, _, _)) =
    3.67 -      not (eq_id (id, id'))
    3.68 -  | is_stale (Theory ({self = NONE, ...}, _, _, _)) = true;
    3.69 -
    3.70 -fun vitalize (thy as Theory ({self = SOME r, ...}, _, _, _)) = (r := thy; thy)
    3.71 -  | vitalize (thy as Theory ({self = NONE, draft, id, ids}, data, ancestry, history)) =
    3.72 -      let
    3.73 -        val r = Unsynchronized.ref thy;
    3.74 -        val thy' = Theory (make_identity (SOME r) draft id ids, data, ancestry, history);
    3.75 -      in r := thy'; thy' end;
    3.76 -
    3.77 -
    3.78 -(* draft mode *)
    3.79 -
    3.80 -val is_draft = #draft o identity_of;
    3.81 -
    3.82 -fun reject_draft thy =
    3.83 -  if is_draft thy then
    3.84 -    raise THEORY ("Illegal draft theory -- stable checkpoint required", [thy])
    3.85 -  else thy;
    3.86 -
    3.87 -
    3.88  (* names *)
    3.89  
    3.90  val PureN = "Pure";
    3.91 -val draftN = "#";
    3.92  val finished = ~1;
    3.93  
    3.94  fun display_names thy =
    3.95    let
    3.96 -    val draft = if is_draft thy then [draftN] else [];
    3.97 -    val {stage, ...} = history_of thy;
    3.98 -    val name =
    3.99 -      if stage = finished then theory_name thy
   3.100 -      else theory_name thy ^ ":" ^ string_of_int stage;
   3.101 +    val {name, stage} = history_of thy;
   3.102 +    val name' =
   3.103 +      if stage = finished then name
   3.104 +      else name ^ ":" ^ string_of_int stage;
   3.105      val ancestor_names = map theory_name (ancestors_of thy);
   3.106 -    val stale = if is_stale thy then ["!"] else [];
   3.107 -  in rev (stale @ draft @ [name] @ ancestor_names) end;
   3.108 +  in rev (name' :: ancestor_names) end;
   3.109  
   3.110  val pretty_thy = Pretty.str_list "{" "}" o display_names;
   3.111  val string_of_thy = Pretty.string_of o pretty_thy;
   3.112 @@ -268,40 +229,29 @@
   3.113    else get_theory thy name;
   3.114  
   3.115  
   3.116 -(* theory references *)
   3.117 -
   3.118 -(*theory_ref provides a safe way to store dynamic references to a
   3.119 -  theory in external data structures -- a plain theory value would
   3.120 -  become stale as the self reference moves on*)
   3.121 -
   3.122 -datatype theory_ref = Theory_Ref of theory Unsynchronized.ref;
   3.123 +(* theory references *)  (* FIXME dummy *)
   3.124  
   3.125 -fun deref (Theory_Ref (Unsynchronized.ref thy)) = thy;
   3.126 +datatype theory_ref = Theory_Ref of theory;
   3.127  
   3.128 -fun check_thy thy =  (*thread-safe version*)
   3.129 -  let val thy_ref = Theory_Ref (the_self thy) in
   3.130 -    if is_stale thy then error ("Stale theory encountered:\n" ^ string_of_thy thy)
   3.131 -    else thy_ref
   3.132 -  end;
   3.133 +fun deref (Theory_Ref thy) = thy;
   3.134 +fun check_thy thy = Theory_Ref thy;
   3.135  
   3.136  
   3.137  (* build ids *)
   3.138  
   3.139 -fun insert_id draft id ids =
   3.140 -  if draft then ids
   3.141 -  else Inttab.update (id, ()) ids;
   3.142 +fun insert_id id ids = Inttab.update (id, ()) ids;
   3.143  
   3.144  fun merge_ids
   3.145 -    (Theory ({draft = draft1, id = id1, ids = ids1, ...}, _, _, _))
   3.146 -    (Theory ({draft = draft2, id = id2, ids = ids2, ...}, _, _, _)) =
   3.147 +    (Theory ({id = id1, ids = ids1, ...}, _, _, _))
   3.148 +    (Theory ({id = id2, ids = ids2, ...}, _, _, _)) =
   3.149    Inttab.merge (K true) (ids1, ids2)
   3.150 -  |> insert_id draft1 id1
   3.151 -  |> insert_id draft2 id2;
   3.152 +  |> insert_id id1
   3.153 +  |> insert_id id2;
   3.154  
   3.155  
   3.156  (* equality and inclusion *)
   3.157  
   3.158 -val eq_thy = eq_id o pairself (#id o identity_of);
   3.159 +val eq_thy = op = o pairself (#id o identity_of);
   3.160  
   3.161  fun proper_subthy (Theory ({id, ...}, _, _, _), Theory ({ids, ...}, _, _, _)) =
   3.162    Inttab.defined ids id;
   3.163 @@ -335,9 +285,7 @@
   3.164    else error (cat_lines ["Attempt to perform non-trivial merge of theories:",
   3.165      str_of_thy thy1, str_of_thy thy2]);
   3.166  
   3.167 -fun merge_refs (ref1, ref2) =
   3.168 -  if ref1 = ref2 then ref1
   3.169 -  else check_thy (merge (deref ref1, deref ref2));
   3.170 +fun merge_refs (ref1, ref2) = check_thy (merge (deref ref1, deref ref2));
   3.171  
   3.172  
   3.173  
   3.174 @@ -345,44 +293,33 @@
   3.175  
   3.176  (* primitives *)
   3.177  
   3.178 -local
   3.179 -  val lock = Mutex.mutex ();
   3.180 -in
   3.181 -  fun SYNCHRONIZED e = Simple_Thread.synchronized "theory" lock e;
   3.182 -end;
   3.183 +fun create_thy ids data ancestry history =
   3.184 +  Theory (make_identity (serial ()) ids, data, ancestry, history);
   3.185  
   3.186 -fun create_thy self draft ids data ancestry history =
   3.187 -  let val identity = make_identity self draft (serial ()) ids;
   3.188 -  in vitalize (Theory (identity, data, ancestry, history)) end;
   3.189 +val pre_pure_thy =
   3.190 +  create_thy Inttab.empty Datatab.empty (make_ancestry [] []) (make_history PureN 0);
   3.191  
   3.192 -fun change_thy draft' f thy =
   3.193 +local
   3.194 +
   3.195 +fun change_thy finish f thy =
   3.196    let
   3.197 -    val Theory ({self, draft, id, ids}, data, ancestry, history) = thy;
   3.198 -    val (self', data', ancestry') =
   3.199 -      if draft then (self, data, ancestry)    (*destructive change!*)
   3.200 -      else if #stage history > 0
   3.201 -      then (NONE, data, ancestry)
   3.202 -      else (NONE, extend_data data, make_ancestry [thy] (extend_ancestors thy (ancestors_of thy)));
   3.203 -    val ids' = insert_id draft id ids;
   3.204 +    val Theory ({id, ids}, data, ancestry, {name, stage}) = thy;
   3.205 +    val (data', ancestry') =
   3.206 +      if stage = finished then
   3.207 +        (extend_data data, make_ancestry [thy] (extend_ancestors thy (ancestors_of thy)))
   3.208 +      else (data, ancestry);
   3.209 +    val history' = {name = name, stage = if finish then finished else stage + 1};
   3.210 +    val ids' = insert_id id ids;
   3.211      val data'' = f data';
   3.212 -    val thy' = SYNCHRONIZED (fn () =>
   3.213 -      (check_thy thy; create_thy self' draft' ids' data'' ancestry' history));
   3.214 -  in thy' end;
   3.215 +  in create_thy ids' data'' ancestry' history' end;
   3.216  
   3.217 -val name_thy = change_thy false I;
   3.218 -val extend_thy = change_thy true I;
   3.219 -val modify_thy = change_thy true;
   3.220 +in
   3.221  
   3.222 -fun copy_thy thy =
   3.223 -  let
   3.224 -    val Theory ({draft, id, ids, ...}, data, ancestry, history) = thy;
   3.225 -    val ids' = insert_id draft id ids;
   3.226 -    val thy' = SYNCHRONIZED (fn () =>
   3.227 -      (check_thy thy; create_thy NONE true ids' data ancestry history));
   3.228 -  in thy' end;
   3.229 +val update_thy = change_thy false;
   3.230 +val extend_thy = update_thy I;
   3.231 +val finish_thy = change_thy true I;
   3.232  
   3.233 -val pre_pure_thy = create_thy NONE true Inttab.empty
   3.234 -  Datatab.empty (make_ancestry [] []) (make_history PureN 0);
   3.235 +end;
   3.236  
   3.237  
   3.238  (* named theory nodes *)
   3.239 @@ -393,15 +330,13 @@
   3.240      val data = merge_data (pp thy1) (data_of thy1, data_of thy2);
   3.241      val ancestry = make_ancestry [] [];
   3.242      val history = make_history "" 0;
   3.243 -    val thy' = SYNCHRONIZED (fn () =>
   3.244 -     (check_thy thy1; check_thy thy2; create_thy NONE true ids data ancestry history));
   3.245 -  in thy' end;
   3.246 +  in create_thy ids data ancestry history end;
   3.247  
   3.248  fun maximal_thys thys =
   3.249    thys |> filter_out (fn thy => exists (fn thy' => proper_subthy (thy, thy')) thys);
   3.250  
   3.251  fun begin_thy pp name imports =
   3.252 -  if name = "" orelse name = draftN then error ("Bad theory name: " ^ quote name)
   3.253 +  if name = "" then error ("Bad theory name: " ^ quote name)
   3.254    else
   3.255      let
   3.256        val parents = maximal_thys (distinct eq_thy imports);
   3.257 @@ -417,28 +352,7 @@
   3.258  
   3.259        val ancestry = make_ancestry parents ancestors;
   3.260        val history = make_history name 0;
   3.261 -      val thy' = SYNCHRONIZED (fn () =>
   3.262 -        (map check_thy imports; create_thy NONE true ids data ancestry history));
   3.263 -    in thy' end;
   3.264 -
   3.265 -
   3.266 -(* history stages *)
   3.267 -
   3.268 -fun history_stage f thy =
   3.269 -  let
   3.270 -    val {name, stage} = history_of thy;
   3.271 -    val _ = stage = finished andalso raise THEORY ("Theory already finished", [thy]);
   3.272 -    val history' = make_history name (f stage);
   3.273 -    val thy' as Theory (identity', data', ancestry', _) = name_thy thy;
   3.274 -    val thy'' = SYNCHRONIZED (fn () =>
   3.275 -      (check_thy thy'; vitalize (Theory (identity', data', ancestry', history'))));
   3.276 -  in thy'' end;
   3.277 -
   3.278 -fun checkpoint_thy thy =
   3.279 -  if is_draft thy then history_stage (fn stage => stage + 1) thy
   3.280 -  else thy;
   3.281 -
   3.282 -val finish_thy = history_stage (fn _ => finished);
   3.283 +    in create_thy ids data ancestry history end;
   3.284  
   3.285  
   3.286  (* theory data *)
   3.287 @@ -453,7 +367,7 @@
   3.288      SOME x => x
   3.289    | NONE => invoke_empty k) |> dest;
   3.290  
   3.291 -fun put k mk x = modify_thy (Datatab.update (k, mk x));
   3.292 +fun put k mk x = update_thy (Datatab.update (k, mk x));
   3.293  
   3.294  end;
   3.295  
     4.1 --- a/src/Pure/goal.ML	Wed Jul 17 23:51:10 2013 +0200
     4.2 +++ b/src/Pure/goal.ML	Thu Jul 18 13:12:54 2013 +0200
     4.3 @@ -232,7 +232,6 @@
     4.4  fun future_result ctxt result prop =
     4.5    let
     4.6      val thy = Proof_Context.theory_of ctxt;
     4.7 -    val _ = Context.reject_draft thy;
     4.8      val cert = Thm.cterm_of thy;
     4.9      val certT = Thm.ctyp_of thy;
    4.10  
     5.1 --- a/src/Pure/proofterm.ML	Wed Jul 17 23:51:10 2013 +0200
     5.2 +++ b/src/Pure/proofterm.ML	Thu Jul 18 13:12:54 2013 +0200
     5.3 @@ -1491,7 +1491,6 @@
     5.4        postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) (Future.join body));
     5.5    in
     5.6      if null promises then Future.map postproc body
     5.7 -    else if Context.is_draft thy then Future.value (fulfill ())
     5.8      else if Future.is_finished body andalso length promises = 1 then
     5.9        Future.map (fn _ => fulfill ()) (snd (hd promises))
    5.10      else
    5.11 @@ -1546,18 +1545,16 @@
    5.12          (Type.strip_sorts o atyp_map) args;
    5.13      val argsP = map OfClass outer_constraints @ map Hyp hyps;
    5.14  
    5.15 -    fun full_proof0 () =
    5.16 -      #4 (shrink_proof thy [] 0 (rew_proof thy (fold_rev implies_intr_proof hyps prf)));
    5.17 -
    5.18      fun make_body0 proof0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};
    5.19      val body0 =
    5.20        if not (proofs_enabled ()) then Future.value (make_body0 MinProof)
    5.21 -      else if Context.is_draft thy then Future.value (make_body0 (full_proof0 ()))
    5.22        else
    5.23          (singleton o Future.cond_forks)
    5.24            {name = "Proofterm.prepare_thm_proof", group = NONE,
    5.25              deps = [], pri = 0, interrupts = true}
    5.26 -          (make_body0 o full_proof0);
    5.27 +          (fn () =>
    5.28 +            make_body0
    5.29 +              (#4 (shrink_proof thy [] 0 (rew_proof thy (fold_rev implies_intr_proof hyps prf)))));
    5.30  
    5.31      fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);
    5.32      val (i, body') =
     6.1 --- a/src/Pure/theory.ML	Wed Jul 17 23:51:10 2013 +0200
     6.2 +++ b/src/Pure/theory.ML	Thu Jul 18 13:12:54 2013 +0200
     6.3 @@ -64,8 +64,8 @@
     6.4  fun merge_list [] = raise THEORY ("Empty merge of theories", [])
     6.5    | merge_list (thy :: thys) = Library.foldl merge (thy, thys);
     6.6  
     6.7 -val checkpoint = Context.checkpoint_thy;
     6.8 -val copy = Context.copy_thy;
     6.9 +val checkpoint : theory -> theory = I;  (* FIXME dummy *)
    6.10 +val copy : theory -> theory = I;  (* FIXME dummy *)
    6.11  
    6.12  fun requires thy name what =
    6.13    if exists (fn thy' => Context.theory_name thy' = name) (nodes_of thy) then ()
     7.1 --- a/src/Pure/thm.ML	Wed Jul 17 23:51:10 2013 +0200
     7.2 +++ b/src/Pure/thm.ML	Thu Jul 18 13:12:54 2013 +0200
     7.3 @@ -569,7 +569,7 @@
     7.4  fun future future_thm ct =
     7.5    let
     7.6      val Cterm {thy_ref = thy_ref, t = prop, T, maxidx, sorts} = ct;
     7.7 -    val thy = Context.reject_draft (Theory.deref thy_ref);
     7.8 +    val thy = Theory.deref thy_ref;
     7.9      val _ = T <> propT andalso raise CTERM ("future: prop expected", [ct]);
    7.10  
    7.11      val i = serial ();