improved check_thy: produce a checked theory_ref (thread-safe version);
authorwenzelm
Fri Aug 03 16:28:20 2007 +0200 (2007-08-03)
changeset 2414173baca986087
parent 24140 0683a2fc4041
child 24142 6f6b698b9def
improved check_thy: produce a checked theory_ref (thread-safe version);
removed obsolete self_ref (cf. check_thy);
thread-safeness: when creating certified items, perform Theory.check_thy *last*;
eq_thy: no check here;
marked some critical sections;
src/Pure/context.ML
     1.1 --- a/src/Pure/context.ML	Fri Aug 03 16:28:19 2007 +0200
     1.2 +++ b/src/Pure/context.ML	Fri Aug 03 16:28:20 2007 +0200
     1.3 @@ -3,8 +3,8 @@
     1.4      Author:     Markus Wenzel, TU Muenchen
     1.5  
     1.6  Generic theory contexts with unique identity, arbitrarily typed data,
     1.7 -development graph and history support.  Generic proof contexts with
     1.8 -arbitrarily typed data.
     1.9 +monotonic development graph and history support.  Generic proof
    1.10 +contexts with arbitrarily typed data.
    1.11  *)
    1.12  
    1.13  signature BASIC_CONTEXT =
    1.14 @@ -33,15 +33,14 @@
    1.15    val pprint_thy: theory -> pprint_args -> unit
    1.16    val pretty_abbrev_thy: theory -> Pretty.T
    1.17    val str_of_thy: theory -> string
    1.18 -  val check_thy: theory -> theory
    1.19 +  val deref: theory_ref -> theory
    1.20 +  val check_thy: theory -> theory_ref
    1.21    val eq_thy: theory * theory -> bool
    1.22    val thy_ord: theory * theory -> order
    1.23    val subthy: theory * theory -> bool
    1.24    val joinable: theory * theory -> bool
    1.25    val merge: theory * theory -> theory
    1.26    val merge_refs: theory_ref * theory_ref -> theory_ref
    1.27 -  val self_ref: theory -> theory_ref
    1.28 -  val deref: theory_ref -> theory
    1.29    val copy_thy: theory -> theory
    1.30    val checkpoint_thy: theory -> theory
    1.31    val finish_thy: theory -> theory
    1.32 @@ -227,11 +226,24 @@
    1.33  val str_of_thy = Pretty.str_of o pretty_abbrev_thy;
    1.34  
    1.35  
    1.36 -(* consistency *)
    1.37 +(* theory references *)
    1.38 +
    1.39 +(*theory_ref provides a safe way to store dynamic references to a
    1.40 +  theory in external data structures -- a plain theory value would
    1.41 +  become stale as the self reference moves on*)
    1.42 +
    1.43 +datatype theory_ref = TheoryRef of theory ref;
    1.44  
    1.45 -fun check_thy thy =
    1.46 -  if is_stale thy then error ("Stale theory encountered:\n" ^ string_of_thy thy)
    1.47 -  else thy;
    1.48 +fun deref (TheoryRef (ref thy)) = thy;
    1.49 +
    1.50 +fun check_thy thy =  (*thread-safe version*)
    1.51 +  let val thy_ref = TheoryRef (the_self thy) in
    1.52 +    if is_stale thy then error ("Stale theory encountered:\n" ^ string_of_thy thy)
    1.53 +    else thy_ref
    1.54 +  end;
    1.55 +
    1.56 +
    1.57 +(* consistency *)
    1.58  
    1.59  fun check_ins id ids =
    1.60    if draft_id id orelse Inttab.defined ids (#1 id) then ids
    1.61 @@ -253,7 +265,7 @@
    1.62  
    1.63  (* equality and inclusion *)
    1.64  
    1.65 -val eq_thy = eq_id o pairself (#id o identity_of o check_thy);
    1.66 +val eq_thy = eq_id o pairself (#id o identity_of);
    1.67  val thy_ord = int_ord o pairself (#1 o #id o identity_of);
    1.68  
    1.69  fun proper_subthy
    1.70 @@ -265,18 +277,6 @@
    1.71  fun joinable (thy1, thy2) = subthy (thy1, thy2) orelse subthy (thy2, thy1);
    1.72  
    1.73  
    1.74 -(* theory references *)
    1.75 -
    1.76 -(*theory_ref provides a safe way to store dynamic references to a
    1.77 -  theory in external data structures -- a plain theory value would
    1.78 -  become stale as the self reference moves on*)
    1.79 -
    1.80 -datatype theory_ref = TheoryRef of theory ref;
    1.81 -
    1.82 -val self_ref = TheoryRef o the_self o check_thy;
    1.83 -fun deref (TheoryRef (ref thy)) = thy;
    1.84 -
    1.85 -
    1.86  (* trivial merge *)
    1.87  
    1.88  fun merge (thy1, thy2) =
    1.89 @@ -289,7 +289,7 @@
    1.90  
    1.91  fun merge_refs (ref1, ref2) =
    1.92    if ref1 = ref2 then ref1
    1.93 -  else self_ref (merge (deref ref1, deref ref2));
    1.94 +  else check_thy (merge (deref ref1, deref ref2));
    1.95  
    1.96  
    1.97  
    1.98 @@ -307,9 +307,10 @@
    1.99      val identity' = make_identity self id' ids' iids';
   1.100    in vitalize (Theory (identity', data, ancestry, history)) end;
   1.101  
   1.102 -fun change_thy name f (thy as Theory ({self, id, ids, iids}, data, ancestry, history)) =
   1.103 +fun change_thy name f thy = NAMED_CRITICAL "theory" (fn () =>
   1.104    let
   1.105      val _ = check_thy thy;
   1.106 +    val Theory ({self, id, ids, iids}, data, ancestry, history) = thy;
   1.107      val (self', data', ancestry') =
   1.108        if is_draft thy then (self, data, ancestry)    (*destructive change!*)
   1.109        else if #version history > 0
   1.110 @@ -317,14 +318,17 @@
   1.111        else (NONE, extend_data data,
   1.112          make_ancestry [thy] (thy :: #ancestors ancestry));
   1.113      val data'' = f data';
   1.114 -  in create_thy name self' id ids iids data'' ancestry' history end;
   1.115 +  in create_thy name self' id ids iids data'' ancestry' history end);
   1.116  
   1.117  fun name_thy name = change_thy name I;
   1.118  val modify_thy = change_thy draftN;
   1.119  val extend_thy = modify_thy I;
   1.120  
   1.121 -fun copy_thy (thy as Theory ({id, ids, iids, ...}, data, ancestry, history)) =
   1.122 -  (check_thy thy; create_thy draftN NONE id ids iids (copy_data data) ancestry history);
   1.123 +fun copy_thy thy = NAMED_CRITICAL "theory" (fn () =>
   1.124 +  let
   1.125 +    val _ = check_thy thy;
   1.126 +    val Theory ({id, ids, iids, ...}, data, ancestry, history) = thy;
   1.127 +  in create_thy draftN NONE id ids iids (copy_data data) ancestry history end);
   1.128  
   1.129  val pre_pure_thy = create_thy draftN NONE (serial (), draftN) Inttab.empty Inttab.empty
   1.130    Datatab.empty (make_ancestry [] []) (make_history ProtoPureN 0 []);
   1.131 @@ -335,23 +339,25 @@
   1.132  fun merge_thys pp (thy1, thy2) =
   1.133    if exists_name CPureN thy1 <> exists_name CPureN thy2 then
   1.134      error "Cannot merge Pure and CPure developments"
   1.135 -  else
   1.136 +  else NAMED_CRITICAL "theory" (fn () =>
   1.137      let
   1.138 +      val _ = check_thy thy1;
   1.139 +      val _ = check_thy thy2;
   1.140        val (ids, iids) = check_merge thy1 thy2;
   1.141        val data = merge_data (pp thy1) (data_of thy1, data_of thy2);
   1.142        val ancestry = make_ancestry [] [];
   1.143        val history = make_history "" 0 [];
   1.144 -    in create_thy draftN NONE (serial (), draftN) ids iids data ancestry history end;
   1.145 +    in create_thy draftN NONE (serial (), draftN) ids iids data ancestry history end);
   1.146  
   1.147  fun maximal_thys thys =
   1.148    thys |> filter (fn thy => not (exists (fn thy' => proper_subthy (thy, thy')) thys));
   1.149  
   1.150  fun begin_thy pp name imports =
   1.151    if name = draftN then error ("Illegal theory name: " ^ quote draftN)
   1.152 -  else
   1.153 +  else NAMED_CRITICAL "theory" (fn () =>
   1.154      let
   1.155 -      val parents =
   1.156 -        maximal_thys (distinct eq_thy (map check_thy imports));
   1.157 +      val _ = map check_thy imports;
   1.158 +      val parents = maximal_thys (distinct eq_thy imports);
   1.159        val ancestors = distinct eq_thy (parents @ maps ancestors_of parents);
   1.160        val Theory ({id, ids, iids, ...}, data, _, _) =
   1.161          (case parents of
   1.162 @@ -360,31 +366,31 @@
   1.163          | thy :: thys => Library.foldl (merge_thys pp) (thy, thys));
   1.164        val ancestry = make_ancestry parents ancestors;
   1.165        val history = make_history name 0 [];
   1.166 -    in create_thy draftN NONE id ids iids data ancestry history end;
   1.167 +    in create_thy draftN NONE id ids iids data ancestry history end);
   1.168  
   1.169  
   1.170  (* undoable checkpoints *)
   1.171  
   1.172  fun checkpoint_thy thy =
   1.173    if not (is_draft thy) then thy
   1.174 -  else
   1.175 +  else NAMED_CRITICAL "theory" (fn () =>
   1.176      let
   1.177        val {name, version, intermediates} = history_of thy;
   1.178        val thy' as Theory (identity', data', ancestry', _) =
   1.179          name_thy (name ^ ":" ^ string_of_int version) thy;
   1.180        val history' = make_history name (version + 1) (thy' :: intermediates);
   1.181 -    in vitalize (Theory (identity', data', ancestry', history')) end;
   1.182 +    in vitalize (Theory (identity', data', ancestry', history')) end);
   1.183  
   1.184 -fun finish_thy thy =
   1.185 +fun finish_thy thy = NAMED_CRITICAL "theory" (fn () =>
   1.186    let
   1.187      val {name, version, intermediates} = history_of thy;
   1.188 -    val rs = map (the_self o check_thy) intermediates;
   1.189 +    val rs = map ((fn TheoryRef r => r) o check_thy) intermediates;
   1.190      val thy' as Theory ({self, id, ids, ...}, data', ancestry', _) = name_thy name thy;
   1.191      val identity' = make_identity self id ids Inttab.empty;
   1.192      val history' = make_history name 0 [];
   1.193      val thy'' = vitalize (Theory (identity', data', ancestry', history'));
   1.194      val _ = List.app (fn r => r := thy'') rs;
   1.195 -  in thy'' end;
   1.196 +  in thy'' end);
   1.197  
   1.198  
   1.199  (* theory data *)
   1.200 @@ -435,12 +441,15 @@
   1.201  
   1.202  in
   1.203  
   1.204 -fun init_proof thy = Proof (self_ref thy, init_data thy);
   1.205 +fun init_proof thy = Proof (check_thy thy, init_data thy);
   1.206  
   1.207  fun transfer_proof thy' (prf as Proof (thy_ref, data)) =
   1.208 -  if not (subthy (deref thy_ref, thy')) then
   1.209 -    error "transfer proof context: not a super theory"
   1.210 -  else Proof (self_ref thy', init_new_data data thy');
   1.211 +  let
   1.212 +    val thy = deref thy_ref;
   1.213 +    val _ = subthy (thy, thy') orelse error "transfer proof context: not a super theory";
   1.214 +    val _ = check_thy thy;
   1.215 +    val thy_ref' = check_thy thy';
   1.216 +  in Proof (thy_ref', init_new_data data thy') end;
   1.217  
   1.218  
   1.219  structure ProofData =