# HG changeset patch # User wenzelm # Date 1186151300 -7200 # Node ID 73baca9860873c86c1fdd896bb899d33061b8efc # Parent 0683a2fc40418118064285eccd1ebc8d8ed42e49 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; diff -r 0683a2fc4041 -r 73baca986087 src/Pure/context.ML --- a/src/Pure/context.ML Fri Aug 03 16:28:19 2007 +0200 +++ b/src/Pure/context.ML Fri Aug 03 16:28:20 2007 +0200 @@ -3,8 +3,8 @@ Author: Markus Wenzel, TU Muenchen Generic theory contexts with unique identity, arbitrarily typed data, -development graph and history support. Generic proof contexts with -arbitrarily typed data. +monotonic development graph and history support. Generic proof +contexts with arbitrarily typed data. *) signature BASIC_CONTEXT = @@ -33,15 +33,14 @@ val pprint_thy: theory -> pprint_args -> unit val pretty_abbrev_thy: theory -> Pretty.T val str_of_thy: theory -> string - val check_thy: theory -> theory + val deref: theory_ref -> theory + val check_thy: theory -> theory_ref val eq_thy: theory * theory -> bool val thy_ord: theory * theory -> order val subthy: theory * theory -> bool val joinable: theory * theory -> bool val merge: theory * theory -> theory val merge_refs: theory_ref * theory_ref -> theory_ref - val self_ref: theory -> theory_ref - val deref: theory_ref -> theory val copy_thy: theory -> theory val checkpoint_thy: theory -> theory val finish_thy: theory -> theory @@ -227,11 +226,24 @@ val str_of_thy = Pretty.str_of o pretty_abbrev_thy; -(* consistency *) +(* theory references *) + +(*theory_ref provides a safe way to store dynamic references to a + theory in external data structures -- a plain theory value would + become stale as the self reference moves on*) + +datatype theory_ref = TheoryRef of theory ref; -fun check_thy thy = - if is_stale thy then error ("Stale theory encountered:\n" ^ string_of_thy thy) - else thy; +fun deref (TheoryRef (ref thy)) = thy; + +fun check_thy thy = (*thread-safe version*) + let val thy_ref = TheoryRef (the_self thy) in + if is_stale thy then error ("Stale theory encountered:\n" ^ string_of_thy thy) + else thy_ref + end; + + +(* consistency *) fun check_ins id ids = if draft_id id orelse Inttab.defined ids (#1 id) then ids @@ -253,7 +265,7 @@ (* equality and inclusion *) -val eq_thy = eq_id o pairself (#id o identity_of o check_thy); +val eq_thy = eq_id o pairself (#id o identity_of); val thy_ord = int_ord o pairself (#1 o #id o identity_of); fun proper_subthy @@ -265,18 +277,6 @@ fun joinable (thy1, thy2) = subthy (thy1, thy2) orelse subthy (thy2, thy1); -(* theory references *) - -(*theory_ref provides a safe way to store dynamic references to a - theory in external data structures -- a plain theory value would - become stale as the self reference moves on*) - -datatype theory_ref = TheoryRef of theory ref; - -val self_ref = TheoryRef o the_self o check_thy; -fun deref (TheoryRef (ref thy)) = thy; - - (* trivial merge *) fun merge (thy1, thy2) = @@ -289,7 +289,7 @@ fun merge_refs (ref1, ref2) = if ref1 = ref2 then ref1 - else self_ref (merge (deref ref1, deref ref2)); + else check_thy (merge (deref ref1, deref ref2)); @@ -307,9 +307,10 @@ val identity' = make_identity self id' ids' iids'; in vitalize (Theory (identity', data, ancestry, history)) end; -fun change_thy name f (thy as Theory ({self, id, ids, iids}, data, ancestry, history)) = +fun change_thy name f thy = NAMED_CRITICAL "theory" (fn () => let val _ = check_thy thy; + val Theory ({self, id, ids, iids}, data, ancestry, history) = thy; val (self', data', ancestry') = if is_draft thy then (self, data, ancestry) (*destructive change!*) else if #version history > 0 @@ -317,14 +318,17 @@ else (NONE, extend_data data, make_ancestry [thy] (thy :: #ancestors ancestry)); val data'' = f data'; - in create_thy name self' id ids iids data'' ancestry' history end; + in create_thy name self' id ids iids data'' ancestry' history end); fun name_thy name = change_thy name I; val modify_thy = change_thy draftN; val extend_thy = modify_thy I; -fun copy_thy (thy as Theory ({id, ids, iids, ...}, data, ancestry, history)) = - (check_thy thy; create_thy draftN NONE id ids iids (copy_data data) ancestry history); +fun copy_thy thy = NAMED_CRITICAL "theory" (fn () => + let + val _ = check_thy thy; + val Theory ({id, ids, iids, ...}, data, ancestry, history) = thy; + in create_thy draftN NONE id ids iids (copy_data data) ancestry history end); val pre_pure_thy = create_thy draftN NONE (serial (), draftN) Inttab.empty Inttab.empty Datatab.empty (make_ancestry [] []) (make_history ProtoPureN 0 []); @@ -335,23 +339,25 @@ fun merge_thys pp (thy1, thy2) = if exists_name CPureN thy1 <> exists_name CPureN thy2 then error "Cannot merge Pure and CPure developments" - else + else NAMED_CRITICAL "theory" (fn () => let + val _ = check_thy thy1; + val _ = check_thy thy2; val (ids, iids) = check_merge thy1 thy2; val data = merge_data (pp thy1) (data_of thy1, data_of thy2); val ancestry = make_ancestry [] []; val history = make_history "" 0 []; - in create_thy draftN NONE (serial (), draftN) ids iids data ancestry history end; + in create_thy draftN NONE (serial (), draftN) ids iids data ancestry history end); fun maximal_thys thys = thys |> filter (fn thy => not (exists (fn thy' => proper_subthy (thy, thy')) thys)); fun begin_thy pp name imports = if name = draftN then error ("Illegal theory name: " ^ quote draftN) - else + else NAMED_CRITICAL "theory" (fn () => let - val parents = - maximal_thys (distinct eq_thy (map check_thy imports)); + val _ = map check_thy imports; + val parents = maximal_thys (distinct eq_thy imports); val ancestors = distinct eq_thy (parents @ maps ancestors_of parents); val Theory ({id, ids, iids, ...}, data, _, _) = (case parents of @@ -360,31 +366,31 @@ | thy :: thys => Library.foldl (merge_thys pp) (thy, thys)); val ancestry = make_ancestry parents ancestors; val history = make_history name 0 []; - in create_thy draftN NONE id ids iids data ancestry history end; + in create_thy draftN NONE id ids iids data ancestry history end); (* undoable checkpoints *) fun checkpoint_thy thy = if not (is_draft thy) then thy - else + else NAMED_CRITICAL "theory" (fn () => let val {name, version, intermediates} = history_of thy; val thy' as Theory (identity', data', ancestry', _) = name_thy (name ^ ":" ^ string_of_int version) thy; val history' = make_history name (version + 1) (thy' :: intermediates); - in vitalize (Theory (identity', data', ancestry', history')) end; + in vitalize (Theory (identity', data', ancestry', history')) end); -fun finish_thy thy = +fun finish_thy thy = NAMED_CRITICAL "theory" (fn () => let val {name, version, intermediates} = history_of thy; - val rs = map (the_self o check_thy) intermediates; + val rs = map ((fn TheoryRef r => r) o check_thy) intermediates; val thy' as Theory ({self, id, ids, ...}, data', ancestry', _) = name_thy name thy; val identity' = make_identity self id ids Inttab.empty; val history' = make_history name 0 []; val thy'' = vitalize (Theory (identity', data', ancestry', history')); val _ = List.app (fn r => r := thy'') rs; - in thy'' end; + in thy'' end); (* theory data *) @@ -435,12 +441,15 @@ in -fun init_proof thy = Proof (self_ref thy, init_data thy); +fun init_proof thy = Proof (check_thy thy, init_data thy); fun transfer_proof thy' (prf as Proof (thy_ref, data)) = - if not (subthy (deref thy_ref, thy')) then - error "transfer proof context: not a super theory" - else Proof (self_ref thy', init_new_data data thy'); + let + val thy = deref thy_ref; + val _ = subthy (thy, thy') orelse error "transfer proof context: not a super theory"; + val _ = check_thy thy; + val thy_ref' = check_thy thy'; + in Proof (thy_ref', init_new_data data thy') end; structure ProofData =