# HG changeset patch # User wenzelm # Date 1190314594 -7200 # Node ID 9885a86f14a812869f707acb7268a8d495bd3d26 # Parent e5bea50b9b89476cbc77a992d8b8c3e1d73a0500 tuned signature; moved generic interpretation to interpretation.ML; added abstract at_begin/end wrappers; diff -r e5bea50b9b89 -r 9885a86f14a8 src/Pure/theory.ML --- a/src/Pure/theory.ML Thu Sep 20 20:56:33 2007 +0200 +++ b/src/Pure/theory.ML Thu Sep 20 20:56:34 2007 +0200 @@ -15,30 +15,28 @@ sig include BASIC_THEORY include SIGN_THEORY + val assert_super: theory -> theory -> theory val parents_of: theory -> theory list val ancestors_of: theory -> theory list - val begin_theory: string -> theory list -> theory - val end_theory: theory -> theory + val check_thy: theory -> theory_ref + val deref: theory_ref -> theory + val merge: theory * theory -> theory + val merge_refs: theory_ref * theory_ref -> theory_ref + val merge_list: theory list -> theory val checkpoint: theory -> theory val copy: theory -> theory - val rep_theory: theory -> - {axioms: term NameSpace.table, - defs: Defs.T, - oracles: ((theory * Object.T -> term) * stamp) NameSpace.table} + val requires: theory -> string -> string -> unit val axiom_space: theory -> NameSpace.T val axiom_table: theory -> term Symtab.table val oracle_space: theory -> NameSpace.T val oracle_table: theory -> ((theory * Object.T -> term) * stamp) Symtab.table val axioms_of: theory -> (string * term) list val all_axioms_of: theory -> (string * term) list - val defs_of : theory -> Defs.T - val check_thy: theory -> theory_ref - val deref: theory_ref -> theory - val merge: theory * theory -> theory - val merge_refs: theory_ref * theory_ref -> theory_ref - val merge_list: theory list -> theory - val requires: theory -> string -> string -> unit - val assert_super: theory -> theory -> theory + val defs_of: theory -> Defs.T + val at_begin: (theory -> theory option) -> theory -> theory + val at_end: (theory -> theory option) -> theory -> theory + val begin_theory: string -> theory list -> theory + val end_theory: theory -> theory val cert_axm: theory -> string * term -> string * term val read_axm: theory -> string * string -> string * term val add_axioms: (bstring * string) list -> theory -> theory @@ -51,111 +49,11 @@ val add_oracle: bstring * (theory * Object.T -> term) -> theory -> theory end -signature THEORY_INTERPRETATOR = -sig - type T - type interpretator = T list -> theory -> theory - val add_those: T list -> theory -> theory - val all_those: theory -> T list - val add_interpretator: interpretator -> theory -> theory - val init: theory -> theory -end; - -signature THEORY_INTERPRETATOR_KEY = -sig - type T - val eq: T * T -> bool -end; - -structure Theory = +structure Theory: THEORY = struct -(** datatype thy **) - -datatype thy = Thy of - {axioms: term NameSpace.table, - defs: Defs.T, - oracles: ((theory * Object.T -> term) * stamp) NameSpace.table, - consolidate: theory -> theory}; - -fun make_thy (axioms, defs, oracles, consolidate) = - Thy {axioms = axioms, defs = defs, oracles = oracles, consolidate = consolidate}; - -fun err_dup_axm dup = error ("Duplicate axiom: " ^ quote dup); -fun err_dup_ora dup = error ("Duplicate oracle: " ^ quote dup); - -structure ThyData = TheoryDataFun -( - type T = thy; - val empty = make_thy (NameSpace.empty_table, Defs.empty, NameSpace.empty_table, I); - val copy = I; - - fun extend (Thy {axioms, defs, oracles, consolidate}) = - make_thy (NameSpace.empty_table, defs, oracles, consolidate); - - fun merge pp (thy1, thy2) = - let - val Thy {axioms = _, defs = defs1, oracles = oracles1, - consolidate = consolidate1} = thy1; - val Thy {axioms = _, defs = defs2, oracles = oracles2, - consolidate = consolidate2} = thy2; - - val axioms = NameSpace.empty_table; - val defs = Defs.merge pp (defs1, defs2); - val oracles = NameSpace.merge_tables (eq_snd (op =)) (oracles1, oracles2) - handle Symtab.DUP dup => err_dup_ora dup; - val consolidate = consolidate1 #> consolidate2; - in make_thy (axioms, defs, oracles, consolidate) end; -); - -fun rep_theory thy = ThyData.get thy |> (fn Thy {axioms, defs, oracles, ...} => - {axioms = axioms, defs = defs, oracles = oracles}); - -fun map_thy f = ThyData.map (fn (Thy {axioms, defs, oracles, consolidate}) => - make_thy (f (axioms, defs, oracles, consolidate))); - -fun map_axioms f = map_thy - (fn (axioms, defs, oracles, consolidate) => (f axioms, defs, oracles, consolidate)); -fun map_defs f = map_thy - (fn (axioms, defs, oracles, consolidate) => (axioms, f defs, oracles, consolidate)); -fun map_oracles f = map_thy - (fn (axioms, defs, oracles, consolidate) => (axioms, defs, f oracles, consolidate)); - - -(* basic operations *) - -val axiom_space = #1 o #axioms o rep_theory; -val axiom_table = #2 o #axioms o rep_theory; - -val oracle_space = #1 o #oracles o rep_theory; -val oracle_table = #2 o #oracles o rep_theory; - -val axioms_of = Symtab.dest o #2 o #axioms o rep_theory; - -val defs_of = #defs o rep_theory; - -fun requires thy name what = - if Context.exists_name name thy then () - else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what); - - -(* interpretators *) - -fun add_consolidate f = map_thy - (fn (axioms, defs, oracles, consolidate) => (axioms, defs, oracles, consolidate #> f)); - -fun consolidate thy = - let - val Thy {consolidate, ...} = ThyData.get thy; - in - thy |> consolidate - end; - - -(** type theory **) - -(* context operations *) +(** theory context operations **) val eq_thy = Context.eq_thy; val subthy = Context.subthy; @@ -169,17 +67,128 @@ val check_thy = Context.check_thy; val deref = Context.deref; + val merge = Context.merge; val merge_refs = Context.merge_refs; fun merge_list [] = raise THEORY ("Empty merge of theories", []) | merge_list (thy :: thys) = Library.foldl merge (thy, thys); -val begin_theory = Sign.local_path o consolidate oo Context.begin_thy Sign.pp; -val end_theory = Context.finish_thy; val checkpoint = Context.checkpoint_thy; val copy = Context.copy_thy; +fun requires thy name what = + if Context.exists_name name thy then () + else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what); + + + +(** theory wrappers **) + +type wrapper = (theory -> theory option) * stamp; + +fun apply_wrappers (wrappers: wrapper list) = + let + fun app [] res = res + | app ((f, _) :: fs) (changed, thy) = + (case f thy of + NONE => app fs (changed, thy) + | SOME thy' => app fs (true, thy')); + fun app_fixpoint thy = + (case app wrappers (false, thy) of + (false, _) => thy + | (true, thy') => app_fixpoint thy'); + in app_fixpoint end; + + + +(** datatype thy **) + +datatype thy = Thy of + {axioms: term NameSpace.table, + defs: Defs.T, + oracles: ((theory * Object.T -> term) * stamp) NameSpace.table, + wrappers: wrapper list * wrapper list}; + +fun make_thy (axioms, defs, oracles, wrappers) = + Thy {axioms = axioms, defs = defs, oracles = oracles, wrappers = wrappers}; + +fun err_dup_axm dup = error ("Duplicate axiom: " ^ quote dup); +fun err_dup_ora dup = error ("Duplicate oracle: " ^ quote dup); + +structure ThyData = TheoryDataFun +( + type T = thy; + val empty = make_thy (NameSpace.empty_table, Defs.empty, NameSpace.empty_table, ([], [])); + val copy = I; + + fun extend (Thy {axioms, defs, oracles, wrappers}) = + make_thy (NameSpace.empty_table, defs, oracles, wrappers); + + fun merge pp (thy1, thy2) = + let + val Thy {axioms = _, defs = defs1, oracles = oracles1, wrappers = (bgs1, ens1)} = thy1; + val Thy {axioms = _, defs = defs2, oracles = oracles2, wrappers = (bgs2, ens2)} = thy2; + + val axioms' = NameSpace.empty_table; + val defs' = Defs.merge pp (defs1, defs2); + val oracles' = NameSpace.merge_tables (eq_snd (op =)) (oracles1, oracles2) + handle Symtab.DUP dup => err_dup_ora dup; + val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2); + val ens' = Library.merge (eq_snd op =) (ens1, ens2); + in make_thy (axioms', defs', oracles', (bgs', ens')) end; +); + +fun rep_theory thy = ThyData.get thy |> (fn Thy args => args); + +fun map_thy f = ThyData.map (fn (Thy {axioms, defs, oracles, wrappers}) => + make_thy (f (axioms, defs, oracles, wrappers))); + + +fun map_axioms f = map_thy + (fn (axioms, defs, oracles, wrappers) => (f axioms, defs, oracles, wrappers)); + +fun map_defs f = map_thy + (fn (axioms, defs, oracles, wrappers) => (axioms, f defs, oracles, wrappers)); + +fun map_oracles f = map_thy + (fn (axioms, defs, oracles, wrappers) => (axioms, defs, f oracles, wrappers)); + +fun map_wrappers f = map_thy + (fn (axioms, defs, oracles, wrappers) => (axioms, defs, oracles, f wrappers)); + + +(* basic operations *) + +val axiom_space = #1 o #axioms o rep_theory; +val axiom_table = #2 o #axioms o rep_theory; + +val oracle_space = #1 o #oracles o rep_theory; +val oracle_table = #2 o #oracles o rep_theory; + +val axioms_of = Symtab.dest o #2 o #axioms o rep_theory; +fun all_axioms_of thy = maps axioms_of (thy :: ancestors_of thy); + +val defs_of = #defs o rep_theory; + + +(* begin/end theory *) + +val begin_wrappers = rev o #1 o #wrappers o rep_theory; +val end_wrappers = rev o #2 o #wrappers o rep_theory; + +fun at_begin f = map_wrappers (apfst (cons (f, stamp ()))); +fun at_end f = map_wrappers (apsnd (cons (f, stamp ()))); + +fun begin_theory name imports = + let + val thy = Context.begin_thy Sign.pp name imports; + val wrappers = begin_wrappers thy; + in thy |> Sign.local_path |> apply_wrappers wrappers end; + +fun end_theory thy = + thy |> apply_wrappers (end_wrappers thy) |> Context.finish_thy; + (* signature operations *) @@ -188,10 +197,7 @@ -(** axioms **) - -fun all_axioms_of thy = maps axioms_of (thy :: ancestors_of thy); - +(** add axioms **) (* prepare axioms *) @@ -350,66 +356,5 @@ end; -functor TheoryInterpretatorFun(Key: THEORY_INTERPRETATOR_KEY) : THEORY_INTERPRETATOR = -struct - -open Key; - -type interpretator = T list -> theory -> theory; - -fun apply ips x = fold_rev (fn (_, f) => f x) ips; - -structure InterpretatorData = TheoryDataFun ( - type T = ((serial * interpretator) list * T list) * (theory -> theory); - val empty = (([], []), I); - val extend = I; - val copy = I; - fun merge pp (((interpretators1, done1), upd1), ((interpretators2, done2), upd2)) = - let - fun diff (interpretators1 : (serial * interpretator) list, done1) - (interpretators2, done2) = let - val interpretators = subtract (eq_fst (op =)) interpretators1 interpretators2; - val undone = subtract eq done2 done1; - in apply interpretators undone end; - val interpretators = AList.merge (op =) (K true) (interpretators1, interpretators2); - val done = Library.merge eq (done1, done2); - val upd_new = diff (interpretators2, done2) (interpretators1, done1) - #> diff (interpretators1, done1) (interpretators2, done2); - val upd = upd1 #> upd2 #> upd_new; - in ((interpretators, done), upd) end; -); - -fun consolidate thy = - let - val (_, upd) = InterpretatorData.get thy; - in - thy |> upd |> (InterpretatorData.map o apsnd) (K I) - end; - -val init = Theory.add_consolidate consolidate; - -fun add_those xs thy = - let - val ((interpretators, _), _) = InterpretatorData.get thy; - in - thy - |> apply interpretators xs - |> (InterpretatorData.map o apfst o apsnd) (append xs) - end; - -val all_those = snd o fst o InterpretatorData.get; - -fun add_interpretator interpretator thy = - let - val ((interpretators, xs), _) = InterpretatorData.get thy; - in - thy - |> interpretator (rev xs) - |> (InterpretatorData.map o apfst o apfst) (cons (serial (), interpretator)) - end; - -end; - -structure Theory: THEORY = Theory; structure BasicTheory: BASIC_THEORY = Theory; open BasicTheory;