34 val pretty_thy: theory -> Pretty.T |
34 val pretty_thy: theory -> Pretty.T |
35 val string_of_thy: theory -> string |
35 val string_of_thy: theory -> string |
36 val pprint_thy: theory -> pprint_args -> unit |
36 val pprint_thy: theory -> pprint_args -> unit |
37 val pretty_abbrev_thy: theory -> Pretty.T |
37 val pretty_abbrev_thy: theory -> Pretty.T |
38 val str_of_thy: theory -> string |
38 val str_of_thy: theory -> string |
39 val check_thy: string -> theory -> theory |
39 val check_thy: theory -> theory |
40 val eq_thy: theory * theory -> bool |
40 val eq_thy: theory * theory -> bool |
41 val subthy: theory * theory -> bool |
41 val subthy: theory * theory -> bool |
42 val joinable: theory * theory -> bool |
42 val joinable: theory * theory -> bool |
43 val merge: theory * theory -> theory (*exception TERM*) |
43 val merge: theory * theory -> theory (*exception TERM*) |
44 val merge_refs: theory_ref * theory_ref -> theory_ref (*exception TERM*) |
44 val merge_refs: theory_ref * theory_ref -> theory_ref (*exception TERM*) |
243 val str_of_thy = Pretty.str_of o pretty_abbrev_thy; |
243 val str_of_thy = Pretty.str_of o pretty_abbrev_thy; |
244 |
244 |
245 |
245 |
246 (* consistency *) (*exception TERM*) |
246 (* consistency *) (*exception TERM*) |
247 |
247 |
248 fun check_thy pos thy = |
248 fun check_thy thy = |
249 if is_stale thy then |
249 if is_stale thy then |
250 raise TERM ("Stale theory encountered (in " ^ pos ^ "):\n" ^ string_of_thy thy, []) |
250 raise TERM ("Stale theory encountered:\n" ^ string_of_thy thy, []) |
251 else thy; |
251 else thy; |
252 |
252 |
253 fun check_ins id ids = |
253 fun check_ins id ids = |
254 if draft_id id orelse is_some (Inttab.lookup (ids, #1 id)) then ids |
254 if draft_id id orelse is_some (Inttab.lookup (ids, #1 id)) then ids |
255 else if Inttab.exists (equal (#2 id) o #2) ids then |
255 else if Inttab.exists (equal (#2 id) o #2) ids then |
268 |> check_insert (#version history2 > 0) id2; |
268 |> check_insert (#version history2 > 0) id2; |
269 |
269 |
270 |
270 |
271 (* equality and inclusion *) |
271 (* equality and inclusion *) |
272 |
272 |
273 val eq_thy = eq_id o pairself (#id o identity_of o check_thy "Context.eq_thy"); |
273 val eq_thy = eq_id o pairself (#id o identity_of o check_thy); |
274 |
274 |
275 fun proper_subthy |
275 fun proper_subthy |
276 (thy1 as Theory ({id = (i, _), ...}, _, _, _), |
276 (Theory ({id = (i, _), ...}, _, _, _), Theory ({ids, iids, ...}, _, _, _)) = |
277 thy2 as Theory ({ids, iids, ...}, _, _, _)) = |
277 is_some (Inttab.lookup (ids, i)) orelse is_some (Inttab.lookup (iids, i)); |
278 (pairself (check_thy "Context.proper_subthy") (thy1, thy2); |
|
279 is_some (Inttab.lookup (ids, i)) orelse is_some (Inttab.lookup (iids, i))); |
|
280 |
278 |
281 fun subthy thys = eq_thy thys orelse proper_subthy thys; |
279 fun subthy thys = eq_thy thys orelse proper_subthy thys; |
282 |
280 |
283 fun joinable (thy1, thy2) = subthy (thy1, thy2) orelse subthy (thy2, thy1); |
281 fun joinable (thy1, thy2) = subthy (thy1, thy2) orelse subthy (thy2, thy1); |
284 |
282 |
289 theory in external data structures -- a plain theory value would |
287 theory in external data structures -- a plain theory value would |
290 become stale as the self reference moves on*) |
288 become stale as the self reference moves on*) |
291 |
289 |
292 datatype theory_ref = TheoryRef of theory ref; |
290 datatype theory_ref = TheoryRef of theory ref; |
293 |
291 |
294 val self_ref = TheoryRef o the_self o check_thy "Context.self_ref"; |
292 val self_ref = TheoryRef o the_self o check_thy; |
295 fun deref (TheoryRef (ref thy)) = thy; |
293 fun deref (TheoryRef (ref thy)) = thy; |
296 |
294 |
297 |
295 |
298 (* trivial merge *) (*exception TERM*) |
296 (* trivial merge *) (*exception TERM*) |
299 |
297 |
300 fun merge (thy1, thy2) = |
298 fun merge (thy1, thy2) = |
301 if subthy (thy2, thy1) then thy1 |
299 if eq_thy (thy1, thy2) then thy1 |
302 else if subthy (thy1, thy2) then thy2 |
300 else if proper_subthy (thy2, thy1) then thy1 |
|
301 else if proper_subthy (thy1, thy2) then thy2 |
303 else (check_merge thy1 thy2; |
302 else (check_merge thy1 thy2; |
304 raise TERM (cat_lines ["Attempt to perform non-trivial merge of theories:", |
303 raise TERM (cat_lines ["Attempt to perform non-trivial merge of theories:", |
305 str_of_thy thy1, str_of_thy thy2], [])); |
304 str_of_thy thy1, str_of_thy thy2], [])); |
306 |
305 |
307 fun merge_refs (ref1, ref2) = self_ref (merge (deref ref1, deref ref2)); |
306 fun merge_refs (ref1, ref2) = |
|
307 if ref1 = ref2 then ref1 |
|
308 else self_ref (merge (deref ref1, deref ref2)); |
308 |
309 |
309 |
310 |
310 |
311 |
311 (** build theories **) |
312 (** build theories **) |
312 |
313 |
321 val identity' = make_identity self id' ids' iids'; |
322 val identity' = make_identity self id' ids' iids'; |
322 in vitalize (Theory (identity', data, ancestry, history)) end; |
323 in vitalize (Theory (identity', data, ancestry, history)) end; |
323 |
324 |
324 fun change_thy name f (thy as Theory ({self, id, ids, iids}, data, ancestry, history)) = |
325 fun change_thy name f (thy as Theory ({self, id, ids, iids}, data, ancestry, history)) = |
325 let |
326 let |
326 val _ = check_thy "Context.change_thy" thy; |
327 val _ = check_thy thy; |
327 val (self', data', ancestry') = |
328 val (self', data', ancestry') = |
328 if is_draft thy then (self, data, ancestry) (*destructive change!*) |
329 if is_draft thy then (self, data, ancestry) (*destructive change!*) |
329 else if #version history > 0 |
330 else if #version history > 0 |
330 then (NONE, map_theory copy_data data, ancestry) |
331 then (NONE, map_theory copy_data data, ancestry) |
331 else (NONE, map_theory extend_data data, make_ancestry [thy] (thy :: #ancestors ancestry)); |
332 else (NONE, map_theory extend_data data, make_ancestry [thy] (thy :: #ancestors ancestry)); |
335 fun name_thy name = change_thy name I; |
336 fun name_thy name = change_thy name I; |
336 val modify_thy = change_thy draftN; |
337 val modify_thy = change_thy draftN; |
337 val extend_thy = modify_thy I; |
338 val extend_thy = modify_thy I; |
338 |
339 |
339 fun copy_thy (thy as Theory ({id, ids, iids, ...}, data, ancestry, history)) = |
340 fun copy_thy (thy as Theory ({id, ids, iids, ...}, data, ancestry, history)) = |
340 (check_thy "Context.copy_thy" thy; |
341 (check_thy thy; |
341 create_thy draftN NONE id ids iids (map_theory copy_data data) ancestry history); |
342 create_thy draftN NONE id ids iids (map_theory copy_data data) ancestry history); |
342 |
343 |
343 val pre_pure_thy = create_thy draftN NONE (serial (), draftN) Inttab.empty Inttab.empty |
344 val pre_pure_thy = create_thy draftN NONE (serial (), draftN) Inttab.empty Inttab.empty |
344 (make_data Inttab.empty Inttab.empty) (make_ancestry [] []) (make_history ProtoPureN 0 []); |
345 (make_data Inttab.empty Inttab.empty) (make_ancestry [] []) (make_history ProtoPureN 0 []); |
345 |
346 |
366 fun begin_thy pp name imports = |
367 fun begin_thy pp name imports = |
367 if name = draftN then error ("Illegal theory name: " ^ quote draftN) |
368 if name = draftN then error ("Illegal theory name: " ^ quote draftN) |
368 else |
369 else |
369 let |
370 let |
370 val parents = |
371 val parents = |
371 maximal_thys (gen_distinct eq_thy (map (check_thy "Context.begin_thy") imports)); |
372 maximal_thys (gen_distinct eq_thy (map check_thy imports)); |
372 val ancestors = gen_distinct eq_thy (parents @ List.concat (map ancestors_of parents)); |
373 val ancestors = gen_distinct eq_thy (parents @ List.concat (map ancestors_of parents)); |
373 val Theory ({id, ids, iids, ...}, data, _, _) = |
374 val Theory ({id, ids, iids, ...}, data, _, _) = |
374 (case parents of |
375 (case parents of |
375 [] => error "No parent theories" |
376 [] => error "No parent theories" |
376 | [thy] => extend_thy thy |
377 | [thy] => extend_thy thy |
393 in vitalize (Theory (identity', data', ancestry', history')) end; |
394 in vitalize (Theory (identity', data', ancestry', history')) end; |
394 |
395 |
395 fun finish_thy thy = |
396 fun finish_thy thy = |
396 let |
397 let |
397 val {name, version, intermediates} = history_of thy; |
398 val {name, version, intermediates} = history_of thy; |
398 val rs = map (the_self o check_thy "Context.finish_thy") intermediates; |
399 val rs = map (the_self o check_thy) intermediates; |
399 val thy' as Theory ({self, id, ids, ...}, data', ancestry', _) = name_thy name thy; |
400 val thy' as Theory ({self, id, ids, ...}, data', ancestry', _) = name_thy name thy; |
400 val identity' = make_identity self id ids Inttab.empty; |
401 val identity' = make_identity self id ids Inttab.empty; |
401 val history' = make_history name 0 []; |
402 val history' = make_history name 0 []; |
402 val thy'' = vitalize (Theory (identity', data', ancestry', history')); |
403 val thy'' = vitalize (Theory (identity', data', ancestry', history')); |
403 val _ = List.app (fn r => r := thy'') rs; |
404 val _ = List.app (fn r => r := thy'') rs; |