# HG changeset patch # User wenzelm # Date 1119298443 -7200 # Node ID f66ab8a4e98f4c22bfc2cda79950dd286b03d00d # Parent 38bc902946b2dfbe358fe416addba8d48ca8bcc2 improved treatment of intermediate checkpoints: actual copy instead of extend, purge after end; tuned; diff -r 38bc902946b2 -r f66ab8a4e98f src/Pure/context.ML --- a/src/Pure/context.ML Mon Jun 20 22:14:02 2005 +0200 +++ b/src/Pure/context.ML Mon Jun 20 22:14:03 2005 +0200 @@ -3,7 +3,7 @@ Author: Markus Wenzel, TU Muenchen Generic theory contexts with unique identity, arbitrarily typed data, -linear and graph development. Implicit ML theory context. +graph-based development. Implicit theory context in ML. *) signature BASIC_CONTEXT = @@ -18,7 +18,9 @@ signature CONTEXT = sig include BASIC_CONTEXT + exception DATA_FAIL of exn * string (*theory context*) + val theory_name: theory -> string val parents_of: theory -> theory list val ancestors_of: theory -> theory list val is_stale: theory -> bool @@ -26,7 +28,6 @@ val PureN: string val CPureN: string val draftN: string - val is_draft: theory -> bool val exists_name: string -> theory -> bool val names_of: theory -> string list val pretty_thy: theory -> Pretty.T @@ -37,21 +38,17 @@ val check_thy: string -> theory -> theory val eq_thy: theory * theory -> bool val subthy: theory * theory -> bool + val merge: theory * theory -> theory (*exception TERM*) + val merge_refs: theory_ref * theory_ref -> theory_ref (*exception TERM*) val self_ref: theory -> theory_ref val deref: theory_ref -> theory - exception DATA_FAIL of exn * string - val theory_data: theory -> string list - val print_all_data: theory -> unit val copy_thy: theory -> theory val checkpoint_thy: theory -> theory - val pre_pure: theory - val merge: theory * theory -> theory (*exception TERM*) - val merge_refs: theory_ref * theory_ref -> theory_ref (*exception TERM*) - val theory_name: theory -> string - val begin_theory: (theory -> Pretty.pp) -> string -> theory list -> theory - val end_theory: theory -> theory - - (*ML context*) + val finish_thy: theory -> theory + val theory_data: theory -> string list + val pre_pure_thy: theory + val begin_thy: (theory -> Pretty.pp) -> string -> theory list -> theory + (*ML theory context*) val get_context: unit -> theory option val set_context: theory option -> unit val reset_context: unit -> unit @@ -73,14 +70,12 @@ include CONTEXT structure TheoryData: sig - val declare: string -> Object.T -> (Object.T -> Object.T) -> - (Object.T -> Object.T) -> (Pretty.pp -> Object.T * Object.T -> Object.T) -> - (theory -> Object.T -> unit) -> serial + val declare: string -> Object.T -> (Object.T -> Object.T) -> (Object.T -> Object.T) -> + (Pretty.pp -> Object.T * Object.T -> Object.T) -> serial val init: serial -> theory -> theory - val print: serial -> theory -> unit val get: serial -> (Object.T -> 'a) -> theory -> 'a val put: serial -> ('a -> Object.T) -> 'a -> theory -> theory - end; + end end; structure Context: PRIVATE_CONTEXT = @@ -88,21 +83,72 @@ (*** theory context ***) +(** theory data **) + +(* data kinds and access methods *) + +exception DATA_FAIL of exn * string; + +local + +type kind = + {name: string, + empty: Object.T, + copy: Object.T -> Object.T, + extend: Object.T -> Object.T, + merge: Pretty.pp -> Object.T * Object.T -> Object.T}; + +val kinds = ref (Inttab.empty: kind Inttab.table); + +fun invoke meth_name meth_fn k = + (case Inttab.lookup (! kinds, k) of + SOME kind => meth_fn kind |> transform_failure (fn exn => + DATA_FAIL (exn, "Theory data method " ^ #name kind ^ "." ^ meth_name ^ " failed")) + | NONE => sys_error ("Invalid theory data identifier " ^ string_of_int k)); + +in + +fun invoke_name k = invoke "name" (K o #name) k (); +fun invoke_empty k = invoke "empty" (K o #empty) k (); +val invoke_copy = invoke "copy" #copy; +val invoke_extend = invoke "extend" #extend; +fun invoke_merge pp = invoke "merge" (fn kind => #merge kind pp); + +fun declare_theory_data name e cp ext mrg = + let + val k = serial (); + val kind = {name = name, empty = e, copy = cp, extend = ext, merge = mrg}; + val _ = conditional (Inttab.exists (equal name o #name o #2) (! kinds)) (fn () => + warning ("Duplicate declaration of theory data " ^ quote name)); + val _ = kinds := Inttab.update ((k, kind), ! kinds); + in k end; + +val copy_data = Inttab.map' invoke_copy; +val extend_data = Inttab.map' invoke_extend; +fun merge_data pp = Inttab.join (SOME oo invoke_merge pp) o pairself extend_data; + +end; + + + +(** datatype theory **) + datatype theory = Theory of (*identity*) - {self: theory ref option, - id: serial * string, - ids: string Inttab.table} * + {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*) (*data*) - Object.T Inttab.table * + Object.T Inttab.table * (*record of arbitrarily typed data*) + (*ancestry of graph development*) + {parents: theory list, (*immediate predecessors*) + ancestors: theory list} * (*all predecessors*) (*history of linear development*) - {name: string, - version: int, - intermediates: theory list} * - (*ancestry of graph development*) - {parents: theory list, - ancestors: theory list}; + {name: string, (*prospective name of finished theory*) + version: int, (*checkpoint counter*) + intermediates: theory list}; (*intermediate checkpoints*) exception THEORY of string * theory list; @@ -110,20 +156,18 @@ val identity_of = #1 o rep_theory; val data_of = #2 o rep_theory; -val history_of = #3 o rep_theory; -val ancestry_of = #4 o rep_theory; +val ancestry_of = #3 o rep_theory; +val history_of = #4 o rep_theory; -fun make_identity self id ids = {self = self, id = id, ids = ids}; +fun make_identity self id ids iids = {self = self, id = id, ids = ids, iids = iids}; +fun make_ancestry parents ancestors = {parents = parents, ancestors = ancestors}; fun make_history name vers ints = {name = name, version = vers, intermediates = ints}; -fun make_ancestry parents ancestors = {parents = parents, ancestors = ancestors}; val parents_of = #parents o ancestry_of; val ancestors_of = #ancestors o ancestry_of; - +val theory_name = #name o history_of; -(** theory identity **) - (* staleness *) fun eq_id ((i: int, _), (j, _)) = i = j; @@ -134,10 +178,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}, data, history, ancestry)) = + | vitalize (thy as Theory ({self = NONE, id, ids, iids}, data, ancestry, history)) = let val r = ref thy; - val thy' = Theory (make_identity (SOME r) id ids, data, history, ancestry); + val thy' = Theory (make_identity (SOME r) id ids iids, data, ancestry, history); in r := thy'; thy' end; @@ -151,11 +195,13 @@ fun draft_id (_, name) = (name = draftN); val is_draft = draft_id o #id o identity_of; -fun exists_name name (Theory ({id, ids, ...}, _, _, _)) = - name = #2 id orelse Inttab.exists (equal name o #2) ids; +fun exists_name name (Theory ({id, ids, iids, ...}, _, _, _)) = + name = #2 id orelse + Inttab.exists (equal name o #2) ids orelse + Inttab.exists (equal name o #2) iids; -fun names_of (Theory ({id, ids, ...}, _, _, _)) = - map #2 (Inttab.dest ids @ [id]); +fun names_of (Theory ({id, ids, iids, ...}, _, _, _)) = + rev (#2 id :: Inttab.fold (cons o #2) iids (Inttab.fold (cons o #2) ids [])); fun pretty_thy thy = Pretty.str_list "{" "}" (names_of thy @ (if is_stale thy then ["!"] else [])); @@ -177,33 +223,54 @@ fun check_thy pos thy = if is_stale thy then - raise TERM ("Stale theory encountered (see " ^ pos ^ "):\n" ^ string_of_thy thy, []) + raise TERM ("Stale theory encountered (in " ^ pos ^ "):\n" ^ string_of_thy thy, []) else thy; -fun check_insert id ids = +fun check_ins id ids = if draft_id id orelse is_some (Inttab.lookup (ids, #1 id)) then ids else if Inttab.exists (equal (#2 id) o #2) ids then raise TERM ("Different versions of theory component " ^ quote (#2 id), []) else Inttab.update (id, ids); -fun check_merge thy1 thy2 = - let - val {id = id1, ids = ids1, ...} = identity_of thy1; - val {id = id2, ids = ids2, ...} = identity_of thy2; - in check_insert id2 (Inttab.fold check_insert ids2 (check_insert id1 ids1)) end; +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; -(* equality and inclusion *) +(* theory references *) + +(*theory_ref provides a safe way to store dynamic references to a + theory -- 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 o #self o identity_of o check_thy "Context.self_ref"; +fun deref (TheoryRef (ref thy)) = thy; + + +(* equality and inclusion *) (* FIXME proper_subthy; no subthy_internal *) local -fun exists_ids (Theory ({id, ids, ...}, _, _, _)) (i, _) = - i = #1 id orelse is_some (Inttab.lookup (ids, i)); +fun exists_ids (Theory ({id, ids, iids, ...}, _, _, _)) (i, _) = + i = #1 id orelse + is_some (Inttab.lookup (ids, i)) orelse + is_some (Inttab.lookup (iids, i)); fun member_ids (Theory ({id, ...}, _, _, _), thy) = exists_ids thy id; -fun subset_ids (Theory ({id, ids, ...}, _, _, _), thy) = - exists_ids thy id andalso Inttab.forall (exists_ids thy) ids; +fun subset_ids (Theory ({id, ids, iids, ...}, _, _, _), thy) = + exists_ids thy id andalso + Inttab.forall (exists_ids thy) ids andalso + Inttab.forall (exists_ids thy) iids; in @@ -214,139 +281,6 @@ end; -(* external references *) - -datatype theory_ref = TheoryRef of theory ref; - -val self_ref = TheoryRef o the o #self o identity_of o check_thy "Context.self_ref"; -fun deref (TheoryRef (ref thy)) = thy; - - - -(** theory data **) - -(* data kinds and access methods *) - -exception DATA_FAIL of exn * string; - -local - -type kind = - {name: string, - empty: Object.T, - copy: Object.T -> Object.T, - extend: Object.T -> Object.T, - merge: Pretty.pp -> Object.T * Object.T -> Object.T, - print: theory -> Object.T -> unit}; - -val kinds = ref (Inttab.empty: kind Inttab.table); - -fun invoke meth_name meth_fn k = - (case Inttab.lookup (! kinds, k) of - SOME kind => meth_fn kind |> transform_failure (fn exn => - DATA_FAIL (exn, "Theory data method " ^ #name kind ^ "." ^ meth_name ^ " failed")) - | NONE => sys_error ("Invalid theory data identifier " ^ string_of_int k)); - -in - -fun invoke_name k = invoke "name" (K o #name) k (); -fun invoke_empty k = invoke "empty" (K o #empty) k (); -val invoke_copy = invoke "copy" #copy; -val invoke_extend = invoke "extend" #extend; -fun invoke_merge pp = invoke "merge" (fn kind => #merge kind pp); -fun invoke_print thy = invoke "print" (fn kind => #print kind thy); - -fun declare name e cp ext mrg prt = - let - val k = serial (); - val kind = {name = name, empty = e, copy = cp, extend = ext, merge = mrg, print = prt}; - val _ = conditional (Inttab.exists (equal name o #name o #2) (! kinds)) (fn () => - warning ("Duplicate declaration of theory data " ^ quote name)); - val _ = kinds := Inttab.update ((k, kind), ! kinds); - in k end; - -val copy_data = Inttab.map' invoke_copy; -val extend_data = Inttab.map' invoke_extend; -fun merge_data pp = Inttab.join (SOME oo invoke_merge pp) o pairself extend_data; - -fun theory_data thy = - map invoke_name (Inttab.keys (data_of thy)) - |> map (rpair ()) |> Symtab.make_multi |> Symtab.dest - |> map (apsnd length) - |> map (fn (name, 1) => name | (name, n) => name ^ enclose "[" "]" (string_of_int n)); - -fun print_all_data thy = - List.app (uncurry (invoke_print thy)) (Inttab.dest (data_of thy)); - -end; - - - -(** build theories **) - -(* primitives *) - -fun create_thy name self id ids data history ancestry = - let - val ids' = check_insert id ids; - val id' = (serial (), name); - val _ = check_insert id' ids'; - val identity' = make_identity self id' ids'; - in vitalize (Theory (identity', data, history, ancestry)) end; - -fun copy_thy (thy as Theory ({id, ids, ...}, data, history, ancestry)) = - let val _ = check_thy "Context.copy_thy" thy; - in create_thy draftN NONE id ids (copy_data data) history ancestry end; - -fun change_thy name f (thy as Theory ({self, id, ids}, data, history, ancestry)) = - let - val _ = check_thy "Context.change_thy" thy; - val (self', data', ancestry') = - if is_draft thy then (self, data, ancestry) - else (NONE, extend_data data, make_ancestry [thy] (thy :: #ancestors ancestry)); - in create_thy name self' id ids (f data') history ancestry' end; - -fun name_thy name = change_thy name I; -val map_thy = change_thy draftN; -val extend_thy = map_thy I; - -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); - in vitalize (Theory (identity', data', history', ancestry')) end; - - -(* theory data *) - -structure TheoryData = -struct - -val declare = declare; - -fun get k dest thy = - (case Inttab.lookup (data_of thy, k) of - SOME x => (dest x handle Match => - error ("Failed to access theory data " ^ quote (invoke_name k))) - | NONE => error ("Uninitialized theory data " ^ quote (invoke_name k))); - -fun print k thy = invoke_print thy k (get k I thy); -fun put k mk x = map_thy (curry Inttab.update (k, mk x)); -fun init k = put k I (invoke_empty k); - -end; - - -(* pre_pure *) - -val pre_pure = create_thy draftN NONE (serial (), draftN) Inttab.empty - Inttab.empty (make_history ProtoPureN 0 []) (make_ancestry [] []); - - (* trivial merge *) fun merge (thy1, thy2) = @@ -359,52 +293,123 @@ fun merge_refs (ref1, ref2) = self_ref (merge (deref ref1, deref ref2)); -(* non-trivial merge *) + +(** build theories **) + +(* primitives *) + +fun create_thy name self id ids iids data ancestry history = + let + val intermediate = #version history > 0; + val (ids', iids') = check_insert intermediate id (ids, iids); + val id' = (serial (), name); + val _ = check_insert intermediate id' (ids', iids'); + val identity' = make_identity self id' ids' iids'; + in vitalize (Theory (identity', data, ancestry, history)) end; -fun merge_internal pp (thy1, thy2) = +fun change_thy name f (thy as Theory ({self, id, ids, iids}, data, ancestry, history)) = + let + val _ = check_thy "Context.change_thy" thy; + val (self', data', ancestry') = + if is_draft thy then (self, data, ancestry) (*destructive change!*) + else if #version history > 0 + then (NONE, copy_data data, ancestry) + 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; + +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 "Context.copy_thy" thy; + create_thy draftN NONE id ids iids (copy_data data) ancestry history); + +val pre_pure_thy = create_thy draftN NONE (serial (), draftN) Inttab.empty Inttab.empty + Inttab.empty (make_ancestry [] []) (make_history ProtoPureN 0 []); + + +(* named theory nodes *) + +fun merge_thys pp (thy1, thy2) = if subthy_internal (thy2, thy1) then thy1 else if subthy_internal (thy1, thy2) then thy2 else if exists_name CPureN thy1 <> exists_name CPureN thy2 then error "Cannot merge Pure and CPure developments" else let - val ids = check_merge thy1 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 []; - val ancestry = make_ancestry [] []; - in create_thy draftN NONE (serial (), draftN) ids data history ancestry end; + in create_thy draftN NONE (serial (), draftN) ids iids data ancestry history end; + +fun begin_thy pp name imports = + if name = draftN then error ("Illegal theory name: " ^ quote draftN) + else + let + val parents = gen_distinct eq_thy imports; (* FIXME maximals *) + val ancestors = gen_distinct eq_thy (parents @ List.concat (map ancestors_of parents)); + val Theory ({id, ids, iids, ...}, data, _, _) = + (case parents of + [] => error "No parent theories" + | thy :: thys => extend_thy (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; -(* named theory nodes *) - -val theory_name = #name o history_of; +(* undoable checkpoints *) -fun begin_theory pp name imports = - if name = draftN then - error ("Illegal theory name: " ^ quote draftN) - else if exists is_draft imports then - error "Attempt to import draft theories" +fun checkpoint_thy thy = + if not (is_draft thy) then thy else let - val parents = gen_distinct eq_thy imports; - val ancestors = gen_distinct eq_thy (parents @ List.concat (map ancestors_of parents)); - val Theory ({id, ids, ...}, data, _, _) = - (case parents of - [] => error "No parent theories" - | thy :: thys => extend_thy (Library.foldl (merge_internal pp) (thy, thys))); - val history = make_history name 0 []; - val ancestry = make_ancestry parents ancestors; - in create_thy draftN NONE id ids data history ancestry end; + 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; + +fun finish_thy thy = + let + val {name, version, intermediates} = history_of thy; + val rs = map (the o #self o identity_of o check_thy "Context.finish_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')); + in List.app (fn r => r := thy'') rs; thy'' end; + + +(* theory data *) -fun end_theory thy = - thy -(*|> purge_thy FIXME *) - |> name_thy (theory_name thy); +fun theory_data thy = + map invoke_name (Inttab.keys (data_of thy)) + |> map (rpair ()) |> Symtab.make_multi |> Symtab.dest + |> map (apsnd length) + |> map (fn (name, 1) => name | (name, n) => name ^ enclose "[" "]" (string_of_int n)); + +structure TheoryData = +struct + +val declare = declare_theory_data; + +fun get k dest thy = + (case Inttab.lookup (data_of thy, k) of + SOME x => (dest x handle Match => + error ("Failed to access theory data " ^ quote (invoke_name k))) + | NONE => error ("Uninitialized theory data " ^ quote (invoke_name k))); + +fun put k mk x = modify_thy (curry Inttab.update (k, mk x)); +fun init k = put k I (invoke_empty k); + +end; - -(*** ML theory context ***) +(** ML theory context **) local val current_theory = ref (NONE: theory option); @@ -489,6 +494,7 @@ val init: theory -> theory val print: theory -> unit val get: theory -> T + val get_sg: theory -> T (*obsolete*) val put: T -> theory -> theory val map: (T -> T) -> theory -> theory end; @@ -505,13 +511,12 @@ (Data Data.empty) (fn Data x => Data (Data.copy x)) (fn Data x => Data (Data.extend x)) - (fn pp => fn (Data x1, Data x2) => Data (Data.merge pp (x1, x2))) - (fn thy => fn Data x => Data.print thy x); + (fn pp => fn (Data x1, Data x2) => Data (Data.merge pp (x1, x2))); val init = TheoryData.init kind; -val print = TheoryData.print kind; val get = TheoryData.get kind (fn Data x => x); -val get_sg = get; (*obsolete*) +val get_sg = get; +fun print thy = Data.print thy (get thy); val put = TheoryData.put kind Data; fun map f thy = put (f (get thy)) thy;