# HG changeset patch # User haftmann # Date 1190094360 -7200 # Node ID 85eceef2edc7141654debacafb2d1f91b9c2c39a # Parent 0398a5e802d33c6f99428bc0face9c454ebbb11a introduced generic concepts for theory interpretators diff -r 0398a5e802d3 -r 85eceef2edc7 src/HOL/Inductive.thy --- a/src/HOL/Inductive.thy Tue Sep 18 07:36:38 2007 +0200 +++ b/src/HOL/Inductive.thy Tue Sep 18 07:46:00 2007 +0200 @@ -18,7 +18,6 @@ ("Tools/datatype_rep_proofs.ML") ("Tools/datatype_abs_proofs.ML") ("Tools/datatype_realizer.ML") - ("Tools/datatype_hooks.ML") ("Tools/datatype_case.ML") ("Tools/datatype_package.ML") ("Tools/datatype_codegen.ML") @@ -111,8 +110,6 @@ use "Tools/datatype_case.ML" use "Tools/datatype_realizer.ML" -use "Tools/datatype_hooks.ML" - use "Tools/datatype_package.ML" setup DatatypePackage.setup diff -r 0398a5e802d3 -r 85eceef2edc7 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Sep 18 07:36:38 2007 +0200 +++ b/src/HOL/IsaMakefile Tue Sep 18 07:46:00 2007 +0200 @@ -110,7 +110,7 @@ Tools/TFL/usyntax.ML Tools/TFL/utils.ML Tools/cnf_funcs.ML \ Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \ Tools/datatype_case.ML Tools/datatype_codegen.ML \ - Tools/datatype_hooks.ML Tools/datatype_package.ML \ + Tools/datatype_package.ML \ Tools/datatype_prop.ML Tools/datatype_realizer.ML \ Tools/datatype_rep_proofs.ML Tools/dseq.ML \ Tools/function_package/auto_term.ML \ diff -r 0398a5e802d3 -r 85eceef2edc7 src/HOL/Library/Eval.thy --- a/src/HOL/Library/Eval.thy Tue Sep 18 07:36:38 2007 +0200 +++ b/src/HOL/Library/Eval.thy Tue Sep 18 07:46:00 2007 +0200 @@ -56,7 +56,7 @@ DatatypeCodegen.prove_codetypes_arities (Class.intro_classes_tac []) (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs) [TypOf.class_typ_of] mk ((K o K) (fold Code.add_default_func)) -in DatatypeCodegen.add_codetypes_hook_bootstrap hook end +in DatatypeCodegen.add_codetypes_hook hook end *} @@ -118,7 +118,7 @@ DatatypeCodegen.prove_codetypes_arities (Class.intro_classes_tac []) (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs) [TermOf.class_term_of] ((K o K o pair) []) mk -in DatatypeCodegen.add_codetypes_hook_bootstrap hook end +in DatatypeCodegen.add_codetypes_hook hook end *} abbreviation diff -r 0398a5e802d3 -r 85eceef2edc7 src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Tue Sep 18 07:36:38 2007 +0200 +++ b/src/HOL/Library/Library.thy Tue Sep 18 07:46:00 2007 +0200 @@ -12,7 +12,7 @@ Commutative_Ring Continuity Efficient_Nat - Eval + (*Eval*) Eval_Witness Executable_Set FuncSet diff -r 0398a5e802d3 -r 85eceef2edc7 src/HOL/Tools/datatype_codegen.ML --- a/src/HOL/Tools/datatype_codegen.ML Tue Sep 18 07:36:38 2007 +0200 +++ b/src/HOL/Tools/datatype_codegen.ML Tue Sep 18 07:46:00 2007 +0200 @@ -17,12 +17,11 @@ -> theory -> theory val codetype_hook: hook val eq_hook: hook - val codetypes_dependency: theory -> (string * bool) list list - val add_codetypes_hook_bootstrap: hook -> theory -> theory + val add_codetypes_hook: hook -> theory -> theory val the_codetypes_mut_specs: theory -> (string * bool) list -> ((string * sort) list * (string * (bool * (string * typ list) list)) list) val get_codetypes_arities: theory -> (string * bool) list -> sort - -> (string * (arity * term list)) list option + -> (string * (arity * term list)) list val prove_codetypes_arities: tactic -> (string * bool) list -> sort -> (arity list -> (string * term list) list -> theory -> ((bstring * Attrib.src list) * term) list * theory) @@ -443,6 +442,11 @@ (* abstraction over datatypes vs. type copies *) +fun get_spec thy (dtco, true) = + (the o DatatypePackage.get_datatype_spec thy) dtco + | get_spec thy (tyco, false) = + TypecopyPackage.get_spec thy tyco; + fun codetypes_dependency thy = let val names = @@ -472,11 +476,6 @@ |> map (AList.make (the o AList.lookup (op =) names)) end; -fun get_spec thy (dtco, true) = - (the o DatatypePackage.get_datatype_spec thy) dtco - | get_spec thy (tyco, false) = - TypecopyPackage.get_spec thy tyco; - local fun get_eq_thms thy tyco = case DatatypePackage.get_datatype thy tyco of SOME _ => get_eq_datatype thy tyco @@ -506,7 +505,7 @@ type hook = (string * (bool * ((string * sort) list * (string * typ list) list))) list -> theory -> theory; -fun add_codetypes_hook_bootstrap hook thy = +fun add_codetypes_hook hook thy = let fun add_spec thy (tyco, is_dt) = (tyco, (is_dt, get_spec thy (tyco, is_dt))); @@ -517,8 +516,8 @@ in thy |> fold hook ((map o map) (add_spec thy) (codetypes_dependency thy)) - |> DatatypeHooks.add datatype_hook - |> TypecopyPackage.add_hook typecopy_hook + |> DatatypePackage.add_interpretator datatype_hook + |> TypecopyPackage.add_interpretator typecopy_hook end; fun the_codetypes_mut_specs thy ([(tyco, is_dt)]) = @@ -572,11 +571,11 @@ val ty = (tys' ---> Type (tyco, map TFree vs')); in list_comb (Const (c, ty), map Free ts) end; in - map (fn (tyco, cs) => (tyco, (mk_arity tyco, map (mk_cons tyco) cs))) css |> SOME - end handle Class_Error => NONE; + map (fn (tyco, cs) => (tyco, (mk_arity tyco, map (mk_cons tyco) cs))) css + end; fun prove_codetypes_arities tac tycos sort f after_qed thy = - case get_codetypes_arities thy tycos sort + case try (get_codetypes_arities thy tycos) sort of NONE => thy | SOME insts => let fun proven (tyco, asorts, sort) = @@ -634,13 +633,13 @@ val setup = add_codegen "datatype" datatype_codegen - #> add_tycodegen "datatype" datatype_tycodegen - #> DatatypeHooks.add (fold add_datatype_case_const) - #> DatatypeHooks.add (fold add_datatype_case_defs) + #> add_tycodegen "datatype" datatype_tycodegen + #> DatatypePackage.add_interpretator (fold add_datatype_case_const) + #> DatatypePackage.add_interpretator (fold add_datatype_case_defs) val setup_hooks = - add_codetypes_hook_bootstrap codetype_hook - #> add_codetypes_hook_bootstrap eq_hook + add_codetypes_hook codetype_hook + #> add_codetypes_hook eq_hook end; diff -r 0398a5e802d3 -r 85eceef2edc7 src/HOL/Tools/datatype_hooks.ML --- a/src/HOL/Tools/datatype_hooks.ML Tue Sep 18 07:36:38 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,35 +0,0 @@ -(* Title: HOL/Tools/datatype_hooks.ML - ID: $Id$ - Author: Florian Haftmann, TU Muenchen - -Hooks for datatype introduction. -*) - -signature DATATYPE_HOOKS = -sig - type hook = string list -> theory -> theory - val add: hook -> theory -> theory - val all: hook -end; - -structure DatatypeHooks : DATATYPE_HOOKS = -struct - -type hook = string list -> theory -> theory; - -structure DatatypeHooksData = TheoryDataFun -( - type T = (serial * hook) list; - val empty = []; - val copy = I; - val extend = I; - fun merge _ hooks : T = AList.merge (op =) (K true) hooks; -); - -fun add hook = - DatatypeHooksData.map (cons (serial (), hook)); - -fun all dtcos thy = - fold_rev (fn (_, f) => f dtcos) (DatatypeHooksData.get thy) thy; - -end; diff -r 0398a5e802d3 -r 85eceef2edc7 src/HOL/Tools/datatype_package.ML --- a/src/HOL/Tools/datatype_package.ML Tue Sep 18 07:36:38 2007 +0200 +++ b/src/HOL/Tools/datatype_package.ML Tue Sep 18 07:46:00 2007 +0200 @@ -69,6 +69,7 @@ val datatype_of_case : theory -> string -> DatatypeAux.datatype_info option val get_datatype_spec : theory -> string -> ((string * sort) list * (string * typ list) list) option val get_datatype_constrs : theory -> string -> (string * typ) list option + val add_interpretator: (string list -> theory -> theory) -> theory -> theory val print_datatypes : theory -> unit val make_case : Proof.context -> bool -> string list -> term -> (term * term) list -> term * (term * (int * bool)) list @@ -521,6 +522,10 @@ val specify_consts = gen_specify_consts Sign.add_consts_i; val specify_consts_authentic = gen_specify_consts Sign.add_consts_authentic; +structure DatatypeInterpretator = TheoryInterpretatorFun(struct type T = string; val eq = op = end); + +fun add_interpretator interpretator = DatatypeInterpretator.add_interpretator interpretator; + fun add_datatype_axm flat_names new_type_names descr sorts types_syntax constr_syntax dt_info case_names_induct case_names_exhausts thy = let @@ -666,7 +671,7 @@ |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd |> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos) - |> DatatypeHooks.all (map fst dt_infos); + |> DatatypeInterpretator.add_those (map fst dt_infos); in ({distinct = distinct, inject = inject, @@ -726,7 +731,7 @@ |> Theory.parent_path |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd |> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos) - |> DatatypeHooks.all (map fst dt_infos); + |> DatatypeInterpretator.add_those (map fst dt_infos); in ({distinct = distinct, inject = inject, @@ -831,7 +836,7 @@ |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd |> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos) - |> DatatypeHooks.all (map fst dt_infos); + |> DatatypeInterpretator.add_those (map fst dt_infos); in ({distinct = distinct, inject = inject, @@ -934,7 +939,8 @@ DatatypeProp.distinctness_limit_setup #> Method.add_methods tactic_emulations #> simproc_setup #> - trfun_setup; + trfun_setup #> + DatatypeInterpretator.init; (* outer syntax *) diff -r 0398a5e802d3 -r 85eceef2edc7 src/HOL/Tools/function_package/fundef_package.ML --- a/src/HOL/Tools/function_package/fundef_package.ML Tue Sep 18 07:36:38 2007 +0200 +++ b/src/HOL/Tools/function_package/fundef_package.ML Tue Sep 18 07:46:00 2007 +0200 @@ -26,7 +26,6 @@ val setup_termination_proof : string option -> local_theory -> Proof.state val setup : theory -> theory - val setup_case_cong_hook : theory -> theory val get_congs : theory -> thm list end @@ -176,11 +175,10 @@ |> safe_mk_meta_eq))) thy -val case_cong_hook = fold add_case_cong +val case_cong = fold add_case_cong -val setup_case_cong_hook = - DatatypeHooks.add case_cong_hook - #> (fn thy => case_cong_hook (Symtab.keys (DatatypePackage.get_datatypes thy)) thy) +val setup_case_cong = DatatypePackage.add_interpretator case_cong + (* ad-hoc method to convert elimination-style goals to existential statements *) @@ -259,7 +257,7 @@ Attrib.add_attributes [("fundef_cong", Attrib.add_del_args FundefCtxTree.cong_add FundefCtxTree.cong_del, "declaration of congruence rule for function definitions")] - #> setup_case_cong_hook + #> setup_case_cong #> FundefRelation.setup #> elim_to_cases_setup diff -r 0398a5e802d3 -r 85eceef2edc7 src/HOL/Tools/typecopy_package.ML --- a/src/HOL/Tools/typecopy_package.ML Tue Sep 18 07:36:38 2007 +0200 +++ b/src/HOL/Tools/typecopy_package.ML Tue Sep 18 07:46:00 2007 +0200 @@ -19,8 +19,8 @@ -> theory -> (string * info) * theory val get_typecopies: theory -> string list val get_typecopy_info: theory -> string -> info option - type hook = string * info -> theory -> theory - val add_hook: hook -> theory -> theory + type interpretator = string * info -> theory -> theory + val add_interpretator: interpretator -> theory -> theory val get_spec: theory -> string -> (string * sort) list * (string * typ list) list val get_eq: theory -> string -> thm val print_typecopies: theory -> unit @@ -41,21 +41,20 @@ proj_def: thm }; -type hook = string * info -> theory -> theory; +structure TypecopyInterpretator = TheoryInterpretatorFun(struct type T = string; val eq = op = end); structure TypecopyData = TheoryDataFun ( - type T = info Symtab.table * (serial * hook) list; - val empty = (Symtab.empty, []); + type T = info Symtab.table; + val empty = Symtab.empty; val copy = I; val extend = I; - fun merge _ ((tab1, hooks1), (tab2, hooks2) : T) = - (Symtab.merge (K true) (tab1, tab2), AList.merge (op =) (K true) (hooks1, hooks2)); + fun merge _ = Symtab.merge (K true); ); fun print_typecopies thy = let - val (tab, _) = TypecopyData.get thy; + val tab = TypecopyData.get thy; fun mk (tyco, { vs, constr, typ, proj = (proj, _), ... } : info) = (Pretty.block o Pretty.breaks) [ Sign.pretty_typ thy (Type (tyco, map TFree vs)), @@ -68,17 +67,16 @@ (Pretty.str "type copies:" :: map mk (Symtab.dest tab)) end; -val get_typecopies = Symtab.keys o fst o TypecopyData.get; -val get_typecopy_info = Symtab.lookup o fst o TypecopyData.get; +val get_typecopies = Symtab.keys o TypecopyData.get; +val get_typecopy_info = Symtab.lookup o TypecopyData.get; -(* hook management *) +(* interpretator management *) -fun add_hook hook = - (TypecopyData.map o apsnd o cons) (serial (), hook); +type interpretator = string * info -> theory -> theory; -fun invoke_hooks tyco_info thy = - fold_rev (fn (_, f) => f tyco_info) ((snd o TypecopyData.get) thy) thy; +fun add_interpretator interp = TypecopyInterpretator.add_interpretator + (fold (fn tyco => fn thy => interp (tyco, (the o get_typecopy_info thy) tyco) thy)); (* add a type copy *) @@ -109,8 +107,8 @@ }; in thy - |> (TypecopyData.map o apfst o Symtab.update_new) (tyco, info) - |> invoke_hooks (tyco, info) + |> (TypecopyData.map o Symtab.update_new) (tyco, info) + |> TypecopyInterpretator.add_those [tyco] |> pair (tyco, info) end in @@ -139,10 +137,10 @@ in (vs, [(constr, [typ])]) end; -(* hook for projection function code *) +(* interpretator for projection function code *) fun add_project (_ , {proj_def, ...} : info) = Code.add_default_func proj_def; -val setup = add_hook add_project; +val setup = TypecopyInterpretator.init #> add_interpretator add_project; end; diff -r 0398a5e802d3 -r 85eceef2edc7 src/HOL/ex/ExecutableContent.thy --- a/src/HOL/ex/ExecutableContent.thy Tue Sep 18 07:36:38 2007 +0200 +++ b/src/HOL/ex/ExecutableContent.thy Tue Sep 18 07:46:00 2007 +0200 @@ -7,7 +7,7 @@ theory ExecutableContent imports Main - Eval + (*Eval*) "~~/src/HOL/ex/Records" AssocList Binomial 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;