# HG changeset patch # User wenzelm # Date 1229023905 -3600 # Node ID c7ba485581ae79e02abe2fdf49ac818f65500ea0 # Parent b92443a701de7d7a80afc45880a2dd796db15b3b unified ids for ancestors and checkpoints, removed obsolete history of checkpoints; tuned representation of internal node names -- avoid string copies; tuned signature; diff -r b92443a701de -r c7ba485581ae src/Pure/context.ML --- a/src/Pure/context.ML Thu Dec 11 20:17:57 2008 +0100 +++ b/src/Pure/context.ML Thu Dec 11 20:31:45 2008 +0100 @@ -17,9 +17,9 @@ sig include BASIC_CONTEXT (*theory context*) - val theory_name: theory -> string val parents_of: theory -> theory list val ancestors_of: theory -> theory list + val theory_name: theory -> string val is_stale: theory -> bool val PureN: string val is_draft: theory -> bool @@ -145,9 +145,8 @@ Theory of (*identity*) {self: theory ref option, (*dynamic self reference -- follows theory changes*) - id: serial * string, (*identifier of this theory*) - ids: string Inttab.table, (*identifiers of ancestors*) - iids: string Inttab.table} * (*identifiers of intermediate checkpoints*) + id: serial * (string * int), (*identifier/name of this theory node*) + ids: (string * int) Inttab.table} * (*ancestors and checkpoints*) (*data*) Object.T Datatab.table * (*ancestry*) @@ -155,8 +154,7 @@ ancestors: theory list} * (*all predecessors*) (*history*) {name: string, (*prospective name of finished theory*) - version: int, (*checkpoint counter*) - intermediates: theory list}; (*intermediate checkpoints*) + version: int}; (*checkpoint counter*) exception THEORY of string * theory list; @@ -167,9 +165,9 @@ val ancestry_of = #3 o rep_theory; val history_of = #4 o rep_theory; -fun make_identity self id ids iids = {self = self, id = id, ids = ids, iids = iids}; +fun make_identity self id ids = {self = self, id = id, ids = ids}; fun make_ancestry parents ancestors = {parents = parents, ancestors = ancestors}; -fun make_history name vers ints = {name = name, version = vers, intermediates = ints}; +fun make_history name version = {name = name, version = version}; val the_self = the o #self o identity_of; val parents_of = #parents o ancestry_of; @@ -187,10 +185,10 @@ | is_stale (Theory ({self = NONE, ...}, _, _, _)) = true; fun vitalize (thy as Theory ({self = SOME r, ...}, _, _, _)) = (r := thy; thy) - | vitalize (thy as Theory ({self = NONE, id, ids, iids}, data, ancestry, history)) = + | vitalize (thy as Theory ({self = NONE, id, ids}, data, ancestry, history)) = let val r = ref thy; - val thy' = Theory (make_identity (SOME r) id ids iids, data, ancestry, history); + val thy' = Theory (make_identity (SOME r) id ids, data, ancestry, history); in r := thy'; thy' end; @@ -199,21 +197,25 @@ val PureN = "Pure"; val draftN = "#"; -fun draft_id (_, name) = (name = draftN); +val draft_name = (draftN, ~1); + +fun draft_id (_, (name, _)) = (name = draftN); val is_draft = draft_id o #id o identity_of; fun reject_draft thy = if is_draft thy then raise THEORY ("Illegal draft theory -- stable checkpoint required", [thy]) else thy; -fun exists_name name (thy as Theory ({id, ids, iids, ...}, _, _, _)) = +fun exists_name name (thy as Theory ({id = (_, (a, _)), ids, ...}, _, _, _)) = name = theory_name thy orelse - name = #2 id orelse - Inttab.exists (fn (_, a) => a = name) ids orelse - Inttab.exists (fn (_, a) => a = name) iids; + name = a orelse + Inttab.exists (fn (_, (b, _)) => b = name) ids; -fun names_of (Theory ({id, ids, ...}, _, _, _)) = - rev (#2 id :: Inttab.fold (cons o #2) ids []); +fun name_of (a, ~1) = a + | name_of (a, i) = a ^ ":" ^ string_of_int i; + +fun names_of (Theory ({id = (_, a), ids, ...}, _, _, _)) = + rev (name_of a :: Inttab.fold (fn (_, (b, ~1)) => cons b | _ => I) ids []); fun pretty_thy thy = Pretty.str_list "{" "}" (names_of thy @ (if is_stale thy then ["!"] else [])); @@ -252,30 +254,26 @@ (* consistency *) -fun check_ins id ids = +fun check_insert id ids = if draft_id id orelse Inttab.defined ids (#1 id) then ids else if Inttab.exists (fn (_, a) => a = #2 id) ids then - error ("Different versions of theory component " ^ quote (#2 id)) + error ("Different versions of theory component " ^ quote (name_of (#2 id))) else Inttab.update id ids; -fun check_insert intermediate id (ids, iids) = - let val ids' = check_ins id ids and iids' = check_ins id iids - in if intermediate then (ids, iids') else (ids', iids) end; - fun check_merge - (Theory ({id = id1, ids = ids1, iids = iids1, ...}, _, _, history1)) - (Theory ({id = id2, ids = ids2, iids = iids2, ...}, _, _, history2)) = - (Inttab.fold check_ins ids2 ids1, Inttab.fold check_ins iids2 iids1) - |> check_insert (#version history1 > 0) id1 - |> check_insert (#version history2 > 0) id2; + (Theory ({id = id1, ids = ids1, ...}, _, _, _)) + (Theory ({id = id2, ids = ids2, ...}, _, _, _)) = + Inttab.fold check_insert ids2 ids1 + |> check_insert id1 + |> check_insert id2; (* equality and inclusion *) val eq_thy = eq_id o pairself (#id o identity_of); -fun proper_subthy (Theory ({id = (i, _), ...}, _, _, _), Theory ({ids, iids, ...}, _, _, _)) = - Inttab.defined ids i orelse Inttab.defined iids i; +fun proper_subthy (Theory ({id, ...}, _, _, _), Theory ({ids, ...}, _, _, _)) = + Inttab.defined ids (#1 id); fun subthy thys = eq_thy thys orelse proper_subthy thys; @@ -302,19 +300,18 @@ (* primitives *) -fun create_thy name self id ids iids data ancestry history = +fun create_thy name self id ids data ancestry history = let - val {version, name = _, intermediates = _} = history; - val intermediate = version > 0; - val (ids', iids') = check_insert intermediate id (ids, iids); + val {version, ...} = history; + val ids' = check_insert id ids; val id' = (serial (), name); - val _ = check_insert intermediate id' (ids', iids'); - val identity' = make_identity self id' ids' iids'; + val _ = check_insert id' ids'; + val identity' = make_identity self id' ids'; in vitalize (Theory (identity', data, ancestry, history)) end; fun change_thy name f thy = let - val Theory ({self, id, ids, iids}, data, ancestry, history) = thy; + val Theory ({self, id, ids}, data, ancestry, history) = thy; val (self', data', ancestry') = if is_draft thy then (self, data, ancestry) (*destructive change!*) else if #version history > 0 @@ -322,36 +319,36 @@ else (NONE, extend_data data, make_ancestry [thy] (thy :: #ancestors ancestry)); val data'' = f data'; val thy' = NAMED_CRITICAL "theory" (fn () => - (check_thy thy; create_thy name self' id ids iids data'' ancestry' history)); + (check_thy thy; create_thy name self' id ids data'' ancestry' history)); in thy' end; fun name_thy name = change_thy name I; -val modify_thy = change_thy draftN; +val modify_thy = change_thy draft_name; val extend_thy = modify_thy I; fun copy_thy thy = let - val Theory ({id, ids, iids, ...}, data, ancestry, history) = thy; + val Theory ({id, ids, ...}, data, ancestry, history) = thy; val data' = copy_data data; val thy' = NAMED_CRITICAL "theory" (fn () => - (check_thy thy; create_thy draftN NONE id ids iids data' ancestry history)); + (check_thy thy; create_thy draft_name NONE id ids data' ancestry history)); in thy' end; -val pre_pure_thy = create_thy draftN NONE (serial (), draftN) Inttab.empty Inttab.empty - Datatab.empty (make_ancestry [] []) (make_history PureN 0 []); +val pre_pure_thy = create_thy draft_name NONE (serial (), draft_name) Inttab.empty + Datatab.empty (make_ancestry [] []) (make_history PureN 0); (* named theory nodes *) fun merge_thys pp (thy1, thy2) = let - val (ids, iids) = check_merge thy1 thy2; + val ids = 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 []; + val history = make_history "" 0; val thy' = NAMED_CRITICAL "theory" (fn () => (check_thy thy1; check_thy thy2; - create_thy draftN NONE (serial (), draftN) ids iids data ancestry history)) + create_thy draft_name NONE (serial (), draft_name) ids data ancestry history)); in thy' end; fun maximal_thys thys = @@ -363,37 +360,36 @@ let val parents = maximal_thys (distinct eq_thy imports); val ancestors = distinct eq_thy (parents @ maps ancestors_of parents); - val Theory ({id, ids, iids, ...}, data, _, _) = + val Theory ({id, ids, ...}, data, _, _) = (case parents of [] => error "No parent theories" | [thy] => extend_thy thy | thy :: thys => Library.foldl (merge_thys pp) (thy, thys)); val ancestry = make_ancestry parents ancestors; - val history = make_history name 0 []; + val history = make_history name 0; val thy' = NAMED_CRITICAL "theory" (fn () => - (map check_thy imports; create_thy draftN NONE id ids iids data ancestry history)); + (map check_thy imports; create_thy draft_name NONE id ids data ancestry history)); in thy' end; -(* undoable checkpoints *) +(* persistent checkpoints *) fun checkpoint_thy thy = if not (is_draft thy) then thy else 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); + val {name, version} = history_of thy; + val thy' as Theory (identity', data', ancestry', _) = name_thy (name, version) thy; + val history' = make_history name (version + 1); val thy'' = NAMED_CRITICAL "theory" (fn () => (check_thy thy'; vitalize (Theory (identity', data', ancestry', history')))); in thy'' end; fun finish_thy thy = NAMED_CRITICAL "theory" (fn () => let - val {name, ...} = history_of thy; - val Theory (identity', data', ancestry', _) = name_thy name thy; - val history' = make_history name 0 []; + val name = theory_name thy; + val Theory (identity', data', ancestry', _) = name_thy (name, ~1) thy; + val history' = make_history name 0; val thy' = vitalize (Theory (identity', data', ancestry', history')); in thy' end);