# HG changeset patch # User wenzelm # Date 1119026001 -7200 # Node ID 7eb6b6cbd166778774626d885d6e66d05706c92b # Parent 3b17850023f12dbf8de930c8389182a4e5675760 added type theory: generic theory contexts with unique identity, arbitrarily typed data, linear and graph development -- a complete rewrite of code that used to be spread over in sign.ML, theory.ML, theory_data.ML, pure_thy.ML; diff -r 3b17850023f1 -r 7eb6b6cbd166 src/Pure/context.ML --- a/src/Pure/context.ML Fri Jun 17 18:33:20 2005 +0200 +++ b/src/Pure/context.ML Fri Jun 17 18:33:21 2005 +0200 @@ -2,11 +2,15 @@ ID: $Id$ Author: Markus Wenzel, TU Muenchen -Theory contexts. +Generic theory contexts with unique identity, arbitrarily typed data, +linear and graph development. Implicit ML theory context. *) signature BASIC_CONTEXT = sig + type theory + type theory_ref + exception THEORY of string * theory list val context: theory -> unit val the_context: unit -> theory end; @@ -14,6 +18,40 @@ signature CONTEXT = sig include BASIC_CONTEXT + (*theory context*) + val parents_of: theory -> theory list + val ancestors_of: theory -> theory list + val is_stale: theory -> bool + val ProtoPureN: string + 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 + val string_of_thy: theory -> string + val pprint_thy: theory -> pprint_args -> unit + val pretty_abbrev_thy: theory -> Pretty.T + val str_of_thy: theory -> string + val check_thy: string -> theory -> theory + val eq_thy: theory * theory -> bool + val subthy: theory * theory -> bool + 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 get_context: unit -> theory option val set_context: theory option -> unit val reset_context: unit -> unit @@ -30,11 +68,343 @@ val setup: unit -> (theory -> theory) list end; -structure Context: CONTEXT = +signature PRIVATE_CONTEXT = +sig + 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 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; + +structure Context: PRIVATE_CONTEXT = struct +(*** theory context ***) -(** implicit theory context in ML **) +datatype theory = + Theory of + (*identity*) + {self: theory ref option, + id: serial * string, + ids: string Inttab.table} * + (*data*) + Object.T Inttab.table * + (*history of linear development*) + {name: string, + version: int, + intermediates: theory list} * + (*ancestry of graph development*) + {parents: theory list, + ancestors: theory list}; + +exception THEORY of string * theory list; + +fun rep_theory (Theory args) = args; + +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; + +fun make_identity self id ids = {self = self, id = id, ids = ids}; +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; + + + +(** theory identity **) + +(* staleness *) + +fun eq_id ((i: int, _), (j, _)) = i = j; + +fun is_stale + (Theory ({self = SOME (ref (Theory ({id = id', ...}, _, _, _))), id, ...}, _, _, _)) = + not (eq_id (id, id')) + | 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)) = + let + val r = ref thy; + val thy' = Theory (make_identity (SOME r) id ids, data, history, ancestry); + in r := thy'; thy' end; + + +(* names *) + +val ProtoPureN = "ProtoPure"; +val PureN = "Pure"; +val CPureN = "CPure"; + +val draftN = "#"; +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 names_of (Theory ({id, ids, ...}, _, _, _)) = + map #2 (Inttab.dest ids @ [id]); + +fun pretty_thy thy = + Pretty.str_list "{" "}" (names_of thy @ (if is_stale thy then ["!"] else [])); + +val string_of_thy = Pretty.string_of o pretty_thy; +val pprint_thy = Pretty.pprint o pretty_thy; + +fun pretty_abbrev_thy thy = + let + val names = names_of thy; + val n = length names; + val abbrev = if n > 5 then "..." :: List.drop (names, n - 5) else names; + in Pretty.str_list "{" "}" abbrev end; + +val str_of_thy = Pretty.str_of o pretty_abbrev_thy; + + +(* consistency *) + +fun check_thy pos thy = + if is_stale thy then + raise TERM ("Stale theory encountered (see " ^ pos ^ "):\n" ^ string_of_thy thy, []) + else thy; + +fun check_insert 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; + + +(* equality and inclusion *) + +local + +fun exists_ids (Theory ({id, ids, ...}, _, _, _)) (i, _) = + i = #1 id orelse is_some (Inttab.lookup (ids, 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; + +in + +val eq_thy = eq_id o pairself (#id o identity_of o check_thy "Context.eq_thy"); +fun subthy thys = eq_thy thys orelse member_ids thys; +fun subthy_internal thys = eq_thy thys orelse subset_ids thys; + +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) = + if subthy (thy2, thy1) then thy1 + else if subthy (thy1, thy2) then thy2 + else (check_merge thy1 thy2; + raise TERM (cat_lines ["Attempt to perform non-trivial merge of theories:", + str_of_thy thy1, str_of_thy thy2], [])); + +fun merge_refs (ref1, ref2) = self_ref (merge (deref ref1, deref ref2)); + + +(* non-trivial merge *) + +fun merge_internal 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 data = merge_data (pp thy1) (data_of thy1, data_of thy2); + val history = make_history "" 0 []; + val ancestry = make_ancestry [] []; + in create_thy draftN NONE (serial (), draftN) ids data history ancestry end; + + +(* named theory nodes *) + +val theory_name = #name o history_of; + +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" + 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; + +fun end_theory thy = + thy +(*|> purge_thy FIXME *) + |> name_thy (theory_name thy); + + + + +(*** ML theory context ***) local val current_theory = ref (NONE: theory option); @@ -71,7 +441,7 @@ (* use ML text *) -val ml_output = (writeln, error_msg: string -> unit); +val ml_output = (writeln, error_msg); fun use_output verb txt = use_text ml_output verb (Symbol.escape txt); @@ -84,8 +454,7 @@ use_context ("let " ^ bind ^ " = " ^ txt ^ " in\n" ^ body ^ " end"); - -(** delayed theory setup **) +(* delayed theory setup *) local val setup_fns = ref ([]: (theory -> theory) list); @@ -94,8 +463,59 @@ fun setup () = let val fns = ! setup_fns in setup_fns := []; fns end; end; - end; structure BasicContext: BASIC_CONTEXT = Context; open BasicContext; + + + +(*** type-safe interface for theory data ***) + +signature THEORY_DATA_ARGS = +sig + val name: string + type T + val empty: T + val copy: T -> T + val extend: T -> T + val merge: Pretty.pp -> T * T -> T + val print: theory -> T -> unit +end; + +signature THEORY_DATA = +sig + type T + val init: theory -> theory + val print: theory -> unit + val get: theory -> T + val put: T -> theory -> theory + val map: (T -> T) -> theory -> theory +end; + +functor TheoryDataFun(Data: THEORY_DATA_ARGS): THEORY_DATA = +struct + +structure TheoryData = Context.TheoryData; + +type T = Data.T; +exception Data of T; + +val kind = TheoryData.declare Data.name + (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); + +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 put = TheoryData.put kind Data; +fun map f thy = put (f (get thy)) thy; + +end; + +(*hide private interface!*) +structure Context: CONTEXT = Context;