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,12 +226,25 @@
1.33 val str_of_thy = Pretty.str_of o pretty_abbrev_thy;
1.34
1.35
1.36 +(* theory references *)
1.37 +
1.38 +(*theory_ref provides a safe way to store dynamic references to a
1.39 + theory in external data structures -- a plain theory value would
1.40 + become stale as the self reference moves on*)
1.41 +
1.42 +datatype theory_ref = TheoryRef of theory ref;
1.43 +
1.44 +fun deref (TheoryRef (ref thy)) = thy;
1.45 +
1.46 +fun check_thy thy = (*thread-safe version*)
1.47 + let val thy_ref = TheoryRef (the_self thy) in
1.48 + if is_stale thy then error ("Stale theory encountered:\n" ^ string_of_thy thy)
1.49 + else thy_ref
1.50 + end;
1.51 +
1.52 +
1.53 (* consistency *)
1.54
1.55 -fun check_thy thy =
1.56 - if is_stale thy then error ("Stale theory encountered:\n" ^ string_of_thy thy)
1.57 - else thy;
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 else if Inttab.exists (equal (#2 id) o #2) ids then
1.62 @@ -253,7 +265,7 @@
1.63
1.64 (* equality and inclusion *)
1.65
1.66 -val eq_thy = eq_id o pairself (#id o identity_of o check_thy);
1.67 +val eq_thy = eq_id o pairself (#id o identity_of);
1.68 val thy_ord = int_ord o pairself (#1 o #id o identity_of);
1.69
1.70 fun proper_subthy
1.71 @@ -265,18 +277,6 @@
1.72 fun joinable (thy1, thy2) = subthy (thy1, thy2) orelse subthy (thy2, thy1);
1.73
1.74
1.75 -(* theory references *)
1.76 -
1.77 -(*theory_ref provides a safe way to store dynamic references to a
1.78 - theory in external data structures -- a plain theory value would
1.79 - become stale as the self reference moves on*)
1.80 -
1.81 -datatype theory_ref = TheoryRef of theory ref;
1.82 -
1.83 -val self_ref = TheoryRef o the_self o check_thy;
1.84 -fun deref (TheoryRef (ref thy)) = thy;
1.85 -
1.86 -
1.87 (* trivial merge *)
1.88
1.89 fun merge (thy1, thy2) =
1.90 @@ -289,7 +289,7 @@
1.91
1.92 fun merge_refs (ref1, ref2) =
1.93 if ref1 = ref2 then ref1
1.94 - else self_ref (merge (deref ref1, deref ref2));
1.95 + else check_thy (merge (deref ref1, deref ref2));
1.96
1.97
1.98
1.99 @@ -307,9 +307,10 @@
1.100 val identity' = make_identity self id' ids' iids';
1.101 in vitalize (Theory (identity', data, ancestry, history)) end;
1.102
1.103 -fun change_thy name f (thy as Theory ({self, id, ids, iids}, data, ancestry, history)) =
1.104 +fun change_thy name f thy = NAMED_CRITICAL "theory" (fn () =>
1.105 let
1.106 val _ = check_thy thy;
1.107 + val Theory ({self, id, ids, iids}, data, ancestry, history) = thy;
1.108 val (self', data', ancestry') =
1.109 if is_draft thy then (self, data, ancestry) (*destructive change!*)
1.110 else if #version history > 0
1.111 @@ -317,14 +318,17 @@
1.112 else (NONE, extend_data data,
1.113 make_ancestry [thy] (thy :: #ancestors ancestry));
1.114 val data'' = f data';
1.115 - in create_thy name self' id ids iids data'' ancestry' history end;
1.116 + in create_thy name self' id ids iids data'' ancestry' history end);
1.117
1.118 fun name_thy name = change_thy name I;
1.119 val modify_thy = change_thy draftN;
1.120 val extend_thy = modify_thy I;
1.121
1.122 -fun copy_thy (thy as Theory ({id, ids, iids, ...}, data, ancestry, history)) =
1.123 - (check_thy thy; create_thy draftN NONE id ids iids (copy_data data) ancestry history);
1.124 +fun copy_thy thy = NAMED_CRITICAL "theory" (fn () =>
1.125 + let
1.126 + val _ = check_thy thy;
1.127 + val Theory ({id, ids, iids, ...}, data, ancestry, history) = thy;
1.128 + in create_thy draftN NONE id ids iids (copy_data data) ancestry history end);
1.129
1.130 val pre_pure_thy = create_thy draftN NONE (serial (), draftN) Inttab.empty Inttab.empty
1.131 Datatab.empty (make_ancestry [] []) (make_history ProtoPureN 0 []);
1.132 @@ -335,23 +339,25 @@
1.133 fun merge_thys pp (thy1, thy2) =
1.134 if exists_name CPureN thy1 <> exists_name CPureN thy2 then
1.135 error "Cannot merge Pure and CPure developments"
1.136 - else
1.137 + else NAMED_CRITICAL "theory" (fn () =>
1.138 let
1.139 + val _ = check_thy thy1;
1.140 + val _ = check_thy thy2;
1.141 val (ids, iids) = check_merge thy1 thy2;
1.142 val data = merge_data (pp thy1) (data_of thy1, data_of thy2);
1.143 val ancestry = make_ancestry [] [];
1.144 val history = make_history "" 0 [];
1.145 - in create_thy draftN NONE (serial (), draftN) ids iids data ancestry history end;
1.146 + in create_thy draftN NONE (serial (), draftN) ids iids data ancestry history end);
1.147
1.148 fun maximal_thys thys =
1.149 thys |> filter (fn thy => not (exists (fn thy' => proper_subthy (thy, thy')) thys));
1.150
1.151 fun begin_thy pp name imports =
1.152 if name = draftN then error ("Illegal theory name: " ^ quote draftN)
1.153 - else
1.154 + else NAMED_CRITICAL "theory" (fn () =>
1.155 let
1.156 - val parents =
1.157 - maximal_thys (distinct eq_thy (map check_thy imports));
1.158 + val _ = map check_thy imports;
1.159 + val parents = maximal_thys (distinct eq_thy imports);
1.160 val ancestors = distinct eq_thy (parents @ maps ancestors_of parents);
1.161 val Theory ({id, ids, iids, ...}, data, _, _) =
1.162 (case parents of
1.163 @@ -360,31 +366,31 @@
1.164 | thy :: thys => Library.foldl (merge_thys pp) (thy, thys));
1.165 val ancestry = make_ancestry parents ancestors;
1.166 val history = make_history name 0 [];
1.167 - in create_thy draftN NONE id ids iids data ancestry history end;
1.168 + in create_thy draftN NONE id ids iids data ancestry history end);
1.169
1.170
1.171 (* undoable checkpoints *)
1.172
1.173 fun checkpoint_thy thy =
1.174 if not (is_draft thy) then thy
1.175 - else
1.176 + else NAMED_CRITICAL "theory" (fn () =>
1.177 let
1.178 val {name, version, intermediates} = history_of thy;
1.179 val thy' as Theory (identity', data', ancestry', _) =
1.180 name_thy (name ^ ":" ^ string_of_int version) thy;
1.181 val history' = make_history name (version + 1) (thy' :: intermediates);
1.182 - in vitalize (Theory (identity', data', ancestry', history')) end;
1.183 + in vitalize (Theory (identity', data', ancestry', history')) end);
1.184
1.185 -fun finish_thy thy =
1.186 +fun finish_thy thy = NAMED_CRITICAL "theory" (fn () =>
1.187 let
1.188 val {name, version, intermediates} = history_of thy;
1.189 - val rs = map (the_self o check_thy) intermediates;
1.190 + val rs = map ((fn TheoryRef r => r) o check_thy) intermediates;
1.191 val thy' as Theory ({self, id, ids, ...}, data', ancestry', _) = name_thy name thy;
1.192 val identity' = make_identity self id ids Inttab.empty;
1.193 val history' = make_history name 0 [];
1.194 val thy'' = vitalize (Theory (identity', data', ancestry', history'));
1.195 val _ = List.app (fn r => r := thy'') rs;
1.196 - in thy'' end;
1.197 + in thy'' end);
1.198
1.199
1.200 (* theory data *)
1.201 @@ -435,12 +441,15 @@
1.202
1.203 in
1.204
1.205 -fun init_proof thy = Proof (self_ref thy, init_data thy);
1.206 +fun init_proof thy = Proof (check_thy thy, init_data thy);
1.207
1.208 fun transfer_proof thy' (prf as Proof (thy_ref, data)) =
1.209 - if not (subthy (deref thy_ref, thy')) then
1.210 - error "transfer proof context: not a super theory"
1.211 - else Proof (self_ref thy', init_new_data data thy');
1.212 + let
1.213 + val thy = deref thy_ref;
1.214 + val _ = subthy (thy, thy') orelse error "transfer proof context: not a super theory";
1.215 + val _ = check_thy thy;
1.216 + val thy_ref' = check_thy thy';
1.217 + in Proof (thy_ref', init_new_data data thy') end;
1.218
1.219
1.220 structure ProofData =