finish_thy: to not collapse checkpoints -- allows future proofs to be deferred indefinitely (performance tradeoff: 5-15% slowdown in sequential batch jobs);
1 (* Title: Pure/context.ML
2 Author: Markus Wenzel, TU Muenchen
4 Generic theory contexts with unique identity, arbitrarily typed data,
5 monotonic development graph and history support. Generic proof
6 contexts with arbitrarily typed data.
9 signature BASIC_CONTEXT =
13 exception THEORY of string * theory list
20 val theory_name: theory -> string
21 val parents_of: theory -> theory list
22 val ancestors_of: theory -> theory list
23 val is_stale: theory -> bool
25 val is_draft: theory -> bool
26 val reject_draft: theory -> theory
27 val exists_name: string -> theory -> bool
28 val names_of: theory -> string list
29 val pretty_thy: theory -> Pretty.T
30 val string_of_thy: theory -> string
31 val pprint_thy: theory -> pprint_args -> unit
32 val pprint_thy_ref: theory_ref -> pprint_args -> unit
33 val pretty_abbrev_thy: theory -> Pretty.T
34 val str_of_thy: theory -> string
35 val deref: theory_ref -> theory
36 val check_thy: theory -> theory_ref
37 val eq_thy: theory * theory -> bool
38 val subthy: theory * theory -> bool
39 val joinable: theory * theory -> bool
40 val merge: theory * theory -> theory
41 val merge_refs: theory_ref * theory_ref -> theory_ref
42 val copy_thy: theory -> theory
43 val checkpoint_thy: theory -> theory
44 val finish_thy: theory -> theory
45 val begin_thy: (theory -> Pretty.pp) -> string -> theory list -> theory
48 val theory_of_proof: proof -> theory
49 val transfer_proof: theory -> proof -> proof
50 val init_proof: theory -> proof
52 datatype generic = Theory of theory | Proof of proof
53 val cases: (theory -> 'a) -> (proof -> 'a) -> generic -> 'a
54 val mapping: (theory -> theory) -> (proof -> proof) -> generic -> generic
55 val mapping_result: (theory -> 'a * theory) -> (proof -> 'a * proof) -> generic -> 'a * generic
56 val the_theory: generic -> theory
57 val the_proof: generic -> proof
58 val map_theory: (theory -> theory) -> generic -> generic
59 val map_proof: (proof -> proof) -> generic -> generic
60 val map_theory_result: (theory -> 'a * theory) -> generic -> 'a * generic
61 val map_proof_result: (proof -> 'a * proof) -> generic -> 'a * generic
62 val theory_map: (generic -> generic) -> theory -> theory
63 val proof_map: (generic -> generic) -> proof -> proof
64 val theory_of: generic -> theory (*total*)
65 val proof_of: generic -> proof (*total*)
67 val thread_data: unit -> generic option
68 val the_thread_data: unit -> generic
69 val set_thread_data: generic option -> unit
70 val setmp_thread_data: generic option -> ('a -> 'b) -> 'a -> 'b
71 val >> : (generic -> generic) -> unit
72 val >>> : (generic -> 'a * generic) -> 'a
75 signature PRIVATE_CONTEXT =
80 val declare: Object.T -> (Object.T -> Object.T) -> (Object.T -> Object.T) ->
81 (Pretty.pp -> Object.T * Object.T -> Object.T) -> serial
82 val get: serial -> (Object.T -> 'a) -> theory -> 'a
83 val put: serial -> ('a -> Object.T) -> 'a -> theory -> theory
87 val declare: (theory -> Object.T) -> serial
88 val get: serial -> (Object.T -> 'a) -> proof -> 'a
89 val put: serial -> ('a -> Object.T) -> 'a -> proof -> proof
93 structure Context: PRIVATE_CONTEXT =
96 (*** theory context ***)
100 (* data kinds and access methods *)
102 (*private copy avoids potential conflict of table exceptions*)
103 structure Datatab = TableFun(type key = int val ord = int_ord);
109 copy: Object.T -> Object.T,
110 extend: Object.T -> Object.T,
111 merge: Pretty.pp -> Object.T * Object.T -> Object.T};
113 val kinds = ref (Datatab.empty: kind Datatab.table);
116 (case Datatab.lookup (! kinds) k of
118 | NONE => sys_error "Invalid theory data identifier");
122 fun invoke_empty k = invoke (K o #empty) k ();
123 val invoke_copy = invoke #copy;
124 val invoke_extend = invoke #extend;
125 fun invoke_merge pp = invoke (fn kind => #merge kind pp);
127 fun declare_theory_data empty copy extend merge =
130 val kind = {empty = empty, copy = copy, extend = extend, merge = merge};
131 val _ = CRITICAL (fn () => change kinds (Datatab.update (k, kind)));
134 val copy_data = Datatab.map' invoke_copy;
135 val extend_data = Datatab.map' invoke_extend;
136 fun merge_data pp = Datatab.join (invoke_merge pp) o pairself extend_data;
142 (** datatype theory **)
147 {self: theory ref option, (*dynamic self reference -- follows theory changes*)
148 id: serial * string, (*identifier of this theory*)
149 ids: string Inttab.table, (*identifiers of ancestors*)
150 iids: string Inttab.table} * (*identifiers of intermediate checkpoints*)
152 Object.T Datatab.table *
154 {parents: theory list, (*immediate predecessors*)
155 ancestors: theory list} * (*all predecessors*)
157 {name: string, (*prospective name of finished theory*)
158 version: int, (*checkpoint counter*)
159 intermediates: theory list}; (*intermediate checkpoints*)
161 exception THEORY of string * theory list;
163 fun rep_theory (Theory args) = args;
165 val identity_of = #1 o rep_theory;
166 val data_of = #2 o rep_theory;
167 val ancestry_of = #3 o rep_theory;
168 val history_of = #4 o rep_theory;
170 fun make_identity self id ids iids = {self = self, id = id, ids = ids, iids = iids};
171 fun make_ancestry parents ancestors = {parents = parents, ancestors = ancestors};
172 fun make_history name vers ints = {name = name, version = vers, intermediates = ints};
174 val the_self = the o #self o identity_of;
175 val parents_of = #parents o ancestry_of;
176 val ancestors_of = #ancestors o ancestry_of;
177 val theory_name = #name o history_of;
182 fun eq_id ((i: int, _), (j, _)) = (i = j);
185 (Theory ({self = SOME (ref (Theory ({id = id', ...}, _, _, _))), id, ...}, _, _, _)) =
186 not (eq_id (id, id'))
187 | is_stale (Theory ({self = NONE, ...}, _, _, _)) = true;
189 fun vitalize (thy as Theory ({self = SOME r, ...}, _, _, _)) = (r := thy; thy)
190 | vitalize (thy as Theory ({self = NONE, id, ids, iids}, data, ancestry, history)) =
193 val thy' = Theory (make_identity (SOME r) id ids iids, data, ancestry, history);
194 in r := thy'; thy' end;
202 fun draft_id (_, name) = (name = draftN);
203 val is_draft = draft_id o #id o identity_of;
205 fun reject_draft thy =
206 if is_draft thy then raise THEORY ("Illegal draft theory -- stable checkpoint required", [thy])
209 fun exists_name name (thy as Theory ({id, ids, iids, ...}, _, _, _)) =
210 name = theory_name thy orelse
212 Inttab.exists (fn (_, a) => a = name) ids orelse
213 Inttab.exists (fn (_, a) => a = name) iids;
215 fun names_of (Theory ({id, ids, ...}, _, _, _)) =
216 rev (#2 id :: Inttab.fold (cons o #2) ids []);
219 Pretty.str_list "{" "}" (names_of thy @ (if is_stale thy then ["!"] else []));
221 val string_of_thy = Pretty.string_of o pretty_thy;
222 val pprint_thy = Pretty.pprint o pretty_thy;
224 fun pretty_abbrev_thy thy =
226 val names = names_of thy;
227 val n = length names;
228 val abbrev = if n > 5 then "..." :: List.drop (names, n - 5) else names;
229 in Pretty.str_list "{" "}" abbrev end;
231 val str_of_thy = Pretty.str_of o pretty_abbrev_thy;
234 (* theory references *)
236 (*theory_ref provides a safe way to store dynamic references to a
237 theory in external data structures -- a plain theory value would
238 become stale as the self reference moves on*)
240 datatype theory_ref = TheoryRef of theory ref;
242 fun deref (TheoryRef (ref thy)) = thy;
244 fun check_thy thy = (*thread-safe version*)
245 let val thy_ref = TheoryRef (the_self thy) in
246 if is_stale thy then error ("Stale theory encountered:\n" ^ string_of_thy thy)
250 val pprint_thy_ref = Pretty.pprint o pretty_thy o deref;
255 fun check_ins id ids =
256 if draft_id id orelse Inttab.defined ids (#1 id) then ids
257 else if Inttab.exists (fn (_, a) => a = #2 id) ids then
258 error ("Different versions of theory component " ^ quote (#2 id))
259 else Inttab.update id ids;
261 fun check_insert intermediate id (ids, iids) =
262 let val ids' = check_ins id ids and iids' = check_ins id iids
263 in if intermediate then (ids, iids') else (ids', iids) end;
266 (Theory ({id = id1, ids = ids1, iids = iids1, ...}, _, _, history1))
267 (Theory ({id = id2, ids = ids2, iids = iids2, ...}, _, _, history2)) =
268 (Inttab.fold check_ins ids2 ids1, Inttab.fold check_ins iids2 iids1)
269 |> check_insert (#version history1 > 0) id1
270 |> check_insert (#version history2 > 0) id2;
273 (* equality and inclusion *)
275 val eq_thy = eq_id o pairself (#id o identity_of);
277 fun proper_subthy (Theory ({id = (i, _), ...}, _, _, _), Theory ({ids, iids, ...}, _, _, _)) =
278 Inttab.defined ids i orelse Inttab.defined iids i;
280 fun subthy thys = eq_thy thys orelse proper_subthy thys;
282 fun joinable (thy1, thy2) = subthy (thy1, thy2) orelse subthy (thy2, thy1);
287 fun merge (thy1, thy2) =
288 if eq_thy (thy1, thy2) then thy1
289 else if proper_subthy (thy2, thy1) then thy1
290 else if proper_subthy (thy1, thy2) then thy2
291 else (check_merge thy1 thy2;
292 error (cat_lines ["Attempt to perform non-trivial merge of theories:",
293 str_of_thy thy1, str_of_thy thy2]));
295 fun merge_refs (ref1, ref2) =
296 if ref1 = ref2 then ref1
297 else check_thy (merge (deref ref1, deref ref2));
301 (** build theories **)
305 fun create_thy name self id ids iids data ancestry history =
307 val {version, name = _, intermediates = _} = history;
308 val intermediate = version > 0;
309 val (ids', iids') = check_insert intermediate id (ids, iids);
310 val id' = (serial (), name);
311 val _ = check_insert intermediate id' (ids', iids');
312 val identity' = make_identity self id' ids' iids';
313 in vitalize (Theory (identity', data, ancestry, history)) end;
315 fun change_thy name f thy =
317 val Theory ({self, id, ids, iids}, data, ancestry, history) = thy;
318 val (self', data', ancestry') =
319 if is_draft thy then (self, data, ancestry) (*destructive change!*)
320 else if #version history > 0
321 then (NONE, copy_data data, ancestry)
322 else (NONE, extend_data data, make_ancestry [thy] (thy :: #ancestors ancestry));
323 val data'' = f data';
324 val thy' = NAMED_CRITICAL "theory" (fn () =>
325 (check_thy thy; create_thy name self' id ids iids data'' ancestry' history));
328 fun name_thy name = change_thy name I;
329 val modify_thy = change_thy draftN;
330 val extend_thy = modify_thy I;
334 val Theory ({id, ids, iids, ...}, data, ancestry, history) = thy;
335 val data' = copy_data data;
336 val thy' = NAMED_CRITICAL "theory" (fn () =>
337 (check_thy thy; create_thy draftN NONE id ids iids data' ancestry history));
340 val pre_pure_thy = create_thy draftN NONE (serial (), draftN) Inttab.empty Inttab.empty
341 Datatab.empty (make_ancestry [] []) (make_history PureN 0 []);
344 (* named theory nodes *)
346 fun merge_thys pp (thy1, thy2) =
348 val (ids, iids) = check_merge thy1 thy2;
349 val data = merge_data (pp thy1) (data_of thy1, data_of thy2);
350 val ancestry = make_ancestry [] [];
351 val history = make_history "" 0 [];
352 val thy' = NAMED_CRITICAL "theory" (fn () =>
353 (check_thy thy1; check_thy thy2;
354 create_thy draftN NONE (serial (), draftN) ids iids data ancestry history))
357 fun maximal_thys thys =
358 thys |> filter_out (fn thy => exists (fn thy' => proper_subthy (thy, thy')) thys);
360 fun begin_thy pp name imports =
361 if name = draftN then error ("Illegal theory name: " ^ quote draftN)
364 val parents = maximal_thys (distinct eq_thy imports);
365 val ancestors = distinct eq_thy (parents @ maps ancestors_of parents);
366 val Theory ({id, ids, iids, ...}, data, _, _) =
368 [] => error "No parent theories"
369 | [thy] => extend_thy thy
370 | thy :: thys => Library.foldl (merge_thys pp) (thy, thys));
371 val ancestry = make_ancestry parents ancestors;
372 val history = make_history name 0 [];
373 val thy' = NAMED_CRITICAL "theory" (fn () =>
374 (map check_thy imports; create_thy draftN NONE id ids iids data ancestry history));
378 (* undoable checkpoints *)
380 fun checkpoint_thy thy =
381 if not (is_draft thy) then thy
384 val {name, version, intermediates} = history_of thy;
385 val thy' as Theory (identity', data', ancestry', _) =
386 name_thy (name ^ ":" ^ string_of_int version) thy;
387 val history' = make_history name (version + 1) (thy' :: intermediates);
388 val thy'' = NAMED_CRITICAL "theory" (fn () =>
389 (check_thy thy'; vitalize (Theory (identity', data', ancestry', history'))));
392 fun finish_thy thy = NAMED_CRITICAL "theory" (fn () =>
394 val {name, ...} = history_of thy;
395 val Theory (identity', data', ancestry', _) = name_thy name thy;
396 val history' = make_history name 0 [];
397 val thy' = vitalize (Theory (identity', data', ancestry', history'));
403 structure TheoryData =
406 val declare = declare_theory_data;
409 dest ((case Datatab.lookup (data_of thy) k of
411 | NONE => invoke_copy k (invoke_empty k))); (*adhoc value*)
413 fun put k mk x = modify_thy (Datatab.update (k, mk x));
419 (*** proof context ***)
423 datatype proof = Prf of Object.T Datatab.table * theory_ref;
425 fun theory_of_proof (Prf (_, thy_ref)) = deref thy_ref;
426 fun data_of_proof (Prf (data, _)) = data;
427 fun map_prf f (Prf (data, thy_ref)) = Prf (f data, thy_ref);
430 (* proof data kinds *)
434 val kinds = ref (Datatab.empty: (theory -> Object.T) Datatab.table);
437 (case Datatab.lookup (! kinds) k of
439 | NONE => sys_error "Invalid proof data identifier");
442 Datatab.map' (fn k => fn _ => invoke_init k thy) (! kinds);
444 fun init_new_data data thy =
445 Datatab.merge (K true) (data, init_data thy);
449 fun init_proof thy = Prf (init_data thy, check_thy thy);
451 fun transfer_proof thy' (prf as Prf (data, thy_ref)) =
453 val thy = deref thy_ref;
454 val _ = subthy (thy, thy') orelse error "transfer proof context: not a super theory";
455 val _ = check_thy thy;
456 val data' = init_new_data data thy';
457 val thy_ref' = check_thy thy';
458 in Prf (data', thy_ref') end;
461 structure ProofData =
467 val _ = CRITICAL (fn () => change kinds (Datatab.update (k, init)));
471 dest (case Datatab.lookup (data_of_proof prf) k of
473 | NONE => invoke_init k (theory_of_proof prf)); (*adhoc value*)
475 fun put k mk x = map_prf (Datatab.update (k, mk x));
483 (*** generic context ***)
485 datatype generic = Theory of theory | Proof of proof;
487 fun cases f _ (Theory thy) = f thy
488 | cases _ g (Proof prf) = g prf;
490 fun mapping f g = cases (Theory o f) (Proof o g);
491 fun mapping_result f g = cases (apsnd Theory o f) (apsnd Proof o g);
493 val the_theory = cases I (fn _ => error "Ill-typed context: theory expected");
494 val the_proof = cases (fn _ => error "Ill-typed context: proof expected") I;
496 fun map_theory f = Theory o f o the_theory;
497 fun map_proof f = Proof o f o the_proof;
499 fun map_theory_result f = apsnd Theory o f o the_theory;
500 fun map_proof_result f = apsnd Proof o f o the_proof;
502 fun theory_map f = the_theory o f o Theory;
503 fun proof_map f = the_proof o f o Proof;
505 val theory_of = cases I theory_of_proof;
506 val proof_of = cases init_proof I;
512 local val tag = Universal.tag () : generic option Universal.tag in
515 (case Thread.getLocal tag of
516 SOME (SOME context) => SOME context
519 fun the_thread_data () =
520 (case thread_data () of
521 SOME context => context
522 | _ => error "Unknown context");
524 fun set_thread_data context = Thread.setLocal (tag, context);
525 fun setmp_thread_data context = Library.setmp_thread_data tag (thread_data ()) context;
531 val (res, context') = f (the_thread_data ());
532 val _ = set_thread_data (SOME context');
536 fun >> f = >>> (fn context => ((), f context));
538 val _ = set_thread_data (SOME (Theory pre_pure_thy));
542 structure BasicContext: BASIC_CONTEXT = Context;
547 (*** type-safe interfaces for data declarations ***)
551 signature THEORY_DATA_ARGS =
557 val merge: Pretty.pp -> T * T -> T
560 signature THEORY_DATA =
564 val put: T -> theory -> theory
565 val map: (T -> T) -> theory -> theory
566 val init: theory -> theory
569 functor TheoryDataFun(Data: THEORY_DATA_ARGS): THEORY_DATA =
572 structure TheoryData = Context.TheoryData;
577 val kind = TheoryData.declare
579 (fn Data x => Data (Data.copy x))
580 (fn Data x => Data (Data.extend x))
581 (fn pp => fn (Data x1, Data x2) => Data (Data.merge pp (x1, x2)));
583 val get = TheoryData.get kind (fn Data x => x);
584 val put = TheoryData.put kind Data;
585 fun map f thy = put (f (get thy)) thy;
587 fun init thy = map I thy;
595 signature PROOF_DATA_ARGS =
598 val init: theory -> T
601 signature PROOF_DATA =
604 val get: Context.proof -> T
605 val put: T -> Context.proof -> Context.proof
606 val map: (T -> T) -> Context.proof -> Context.proof
609 functor ProofDataFun(Data: PROOF_DATA_ARGS): PROOF_DATA =
612 structure ProofData = Context.ProofData;
617 val kind = ProofData.declare (Data o Data.init);
619 val get = ProofData.get kind (fn Data x => x);
620 val put = ProofData.put kind Data;
621 fun map f prf = put (f (get prf)) prf;
629 signature GENERIC_DATA_ARGS =
634 val merge: Pretty.pp -> T * T -> T
637 signature GENERIC_DATA =
640 val get: Context.generic -> T
641 val put: T -> Context.generic -> Context.generic
642 val map: (T -> T) -> Context.generic -> Context.generic
645 functor GenericDataFun(Data: GENERIC_DATA_ARGS): GENERIC_DATA =
648 structure ThyData = TheoryDataFun(open Data val copy = I);
649 structure PrfData = ProofDataFun(type T = Data.T val init = ThyData.get);
653 fun get (Context.Theory thy) = ThyData.get thy
654 | get (Context.Proof prf) = PrfData.get prf;
656 fun put x (Context.Theory thy) = Context.Theory (ThyData.put x thy)
657 | put x (Context.Proof prf) = Context.Proof (PrfData.put x prf);
659 fun map f ctxt = put (f (get ctxt)) ctxt;
663 (*hide private interface*)
664 structure Context: CONTEXT = Context;
666 (*fake predeclarations*)
667 structure Proof = struct type context = Context.proof end;
668 structure ProofContext =
669 struct val theory_of = Context.theory_of_proof val init = Context.init_proof end;