diff -r 0398a5e802d3 -r 85eceef2edc7 src/Pure/theory.ML --- a/src/Pure/theory.ML Tue Sep 18 07:36:38 2007 +0200 +++ b/src/Pure/theory.ML Tue Sep 18 07:46:00 2007 +0200 @@ -51,10 +51,108 @@ val add_oracle: bstring * (theory * Object.T -> term) -> theory -> theory end -structure Theory: THEORY = +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 = 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 *) @@ -62,6 +160,10 @@ val eq_thy = Context.eq_thy; val subthy = Context.subthy; +fun assert_super thy1 thy2 = + if subthy (thy1, thy2) then thy2 + else raise THEORY ("Not a super theory", [thy1, thy2]); + val parents_of = Context.parents_of; val ancestors_of = Context.ancestors_of; @@ -73,7 +175,7 @@ fun merge_list [] = raise THEORY ("Empty merge of theories", []) | merge_list (thy :: thys) = Library.foldl merge (thy, thys); -val begin_theory = Sign.local_path oo Context.begin_thy Sign.pp; +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; @@ -86,73 +188,10 @@ -(** datatype thy **) - -datatype thy = Thy of - {axioms: term NameSpace.table, - defs: Defs.T, - oracles: ((theory * Object.T -> term) * stamp) NameSpace.table}; - -fun make_thy (axioms, defs, oracles) = - Thy {axioms = axioms, defs = defs, oracles = oracles}; - -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}) = make_thy (NameSpace.empty_table, defs, oracles); - - fun merge pp (thy1, thy2) = - let - val Thy {axioms = _, defs = defs1, oracles = oracles1} = thy1; - val Thy {axioms = _, defs = defs2, oracles = oracles2} = thy2; +(** axioms **) - 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; - in make_thy (axioms, defs, oracles) end; -); - -fun rep_theory thy = ThyData.get thy |> (fn Thy args => args); - -fun map_thy f = ThyData.map (fn (Thy {axioms, defs, oracles}) => - make_thy (f (axioms, defs, oracles))); - -fun map_axioms f = map_thy (fn (axioms, defs, oracles) => (f axioms, defs, oracles)); -fun map_defs f = map_thy (fn (axioms, defs, oracles) => (axioms, f defs, oracles)); -fun map_oracles f = map_thy (fn (axioms, defs, oracles) => (axioms, defs, f oracles)); - - -(* 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; - -fun requires thy name what = - if Context.exists_name name thy then () - else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what); - -fun assert_super thy1 thy2 = - if subthy (thy1, thy2) then thy2 - else raise THEORY ("Not a super theory", [thy1, thy2]); - - - -(** add axioms **) (* prepare axioms *) @@ -311,5 +350,66 @@ 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;