introduced generic concepts for theory interpretators
authorhaftmann
Tue Sep 18 07:46:00 2007 +0200 (2007-09-18)
changeset 2462685eceef2edc7
parent 24625 0398a5e802d3
child 24627 cc6768509ed3
introduced generic concepts for theory interpretators
src/HOL/Inductive.thy
src/HOL/IsaMakefile
src/HOL/Library/Eval.thy
src/HOL/Library/Library.thy
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/datatype_hooks.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/typecopy_package.ML
src/HOL/ex/ExecutableContent.thy
src/Pure/theory.ML
     1.1 --- a/src/HOL/Inductive.thy	Tue Sep 18 07:36:38 2007 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Tue Sep 18 07:46:00 2007 +0200
     1.3 @@ -18,7 +18,6 @@
     1.4    ("Tools/datatype_rep_proofs.ML")
     1.5    ("Tools/datatype_abs_proofs.ML")
     1.6    ("Tools/datatype_realizer.ML")
     1.7 -  ("Tools/datatype_hooks.ML")
     1.8    ("Tools/datatype_case.ML")
     1.9    ("Tools/datatype_package.ML")
    1.10    ("Tools/datatype_codegen.ML")
    1.11 @@ -111,8 +110,6 @@
    1.12  use "Tools/datatype_case.ML"
    1.13  use "Tools/datatype_realizer.ML"
    1.14  
    1.15 -use "Tools/datatype_hooks.ML"
    1.16 -
    1.17  use "Tools/datatype_package.ML"
    1.18  setup DatatypePackage.setup
    1.19  
     2.1 --- a/src/HOL/IsaMakefile	Tue Sep 18 07:36:38 2007 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Tue Sep 18 07:46:00 2007 +0200
     2.3 @@ -110,7 +110,7 @@
     2.4    Tools/TFL/usyntax.ML Tools/TFL/utils.ML Tools/cnf_funcs.ML		\
     2.5    Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML			\
     2.6    Tools/datatype_case.ML Tools/datatype_codegen.ML			\
     2.7 -  Tools/datatype_hooks.ML Tools/datatype_package.ML			\
     2.8 +  Tools/datatype_package.ML			\
     2.9    Tools/datatype_prop.ML Tools/datatype_realizer.ML			\
    2.10    Tools/datatype_rep_proofs.ML Tools/dseq.ML	\
    2.11    Tools/function_package/auto_term.ML	\
     3.1 --- a/src/HOL/Library/Eval.thy	Tue Sep 18 07:36:38 2007 +0200
     3.2 +++ b/src/HOL/Library/Eval.thy	Tue Sep 18 07:46:00 2007 +0200
     3.3 @@ -56,7 +56,7 @@
     3.4      DatatypeCodegen.prove_codetypes_arities (Class.intro_classes_tac [])
     3.5        (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
     3.6        [TypOf.class_typ_of] mk ((K o K) (fold Code.add_default_func))
     3.7 -in DatatypeCodegen.add_codetypes_hook_bootstrap hook end
     3.8 +in DatatypeCodegen.add_codetypes_hook hook end
     3.9  *}
    3.10  
    3.11  
    3.12 @@ -118,7 +118,7 @@
    3.13        DatatypeCodegen.prove_codetypes_arities (Class.intro_classes_tac [])
    3.14        (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
    3.15        [TermOf.class_term_of] ((K o K o pair) []) mk
    3.16 -in DatatypeCodegen.add_codetypes_hook_bootstrap hook end
    3.17 +in DatatypeCodegen.add_codetypes_hook hook end
    3.18  *}
    3.19  
    3.20  abbreviation
     4.1 --- a/src/HOL/Library/Library.thy	Tue Sep 18 07:36:38 2007 +0200
     4.2 +++ b/src/HOL/Library/Library.thy	Tue Sep 18 07:46:00 2007 +0200
     4.3 @@ -12,7 +12,7 @@
     4.4    Commutative_Ring
     4.5    Continuity
     4.6    Efficient_Nat
     4.7 -  Eval
     4.8 +  (*Eval*)
     4.9    Eval_Witness
    4.10    Executable_Set
    4.11    FuncSet
     5.1 --- a/src/HOL/Tools/datatype_codegen.ML	Tue Sep 18 07:36:38 2007 +0200
     5.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Tue Sep 18 07:46:00 2007 +0200
     5.3 @@ -17,12 +17,11 @@
     5.4      -> theory -> theory
     5.5    val codetype_hook: hook
     5.6    val eq_hook: hook
     5.7 -  val codetypes_dependency: theory -> (string * bool) list list
     5.8 -  val add_codetypes_hook_bootstrap: hook -> theory -> theory
     5.9 +  val add_codetypes_hook: hook -> theory -> theory
    5.10    val the_codetypes_mut_specs: theory -> (string * bool) list
    5.11      -> ((string * sort) list * (string * (bool * (string * typ list) list)) list)
    5.12    val get_codetypes_arities: theory -> (string * bool) list -> sort
    5.13 -    -> (string * (arity * term list)) list option
    5.14 +    -> (string * (arity * term list)) list
    5.15    val prove_codetypes_arities: tactic -> (string * bool) list -> sort
    5.16      -> (arity list -> (string * term list) list -> theory
    5.17        -> ((bstring * Attrib.src list) * term) list * theory)
    5.18 @@ -443,6 +442,11 @@
    5.19  
    5.20  (* abstraction over datatypes vs. type copies *)
    5.21  
    5.22 +fun get_spec thy (dtco, true) =
    5.23 +      (the o DatatypePackage.get_datatype_spec thy) dtco
    5.24 +  | get_spec thy (tyco, false) =
    5.25 +      TypecopyPackage.get_spec thy tyco;
    5.26 +
    5.27  fun codetypes_dependency thy =
    5.28    let
    5.29      val names =
    5.30 @@ -472,11 +476,6 @@
    5.31      |> map (AList.make (the o AList.lookup (op =) names))
    5.32    end;
    5.33  
    5.34 -fun get_spec thy (dtco, true) =
    5.35 -      (the o DatatypePackage.get_datatype_spec thy) dtco
    5.36 -  | get_spec thy (tyco, false) =
    5.37 -      TypecopyPackage.get_spec thy tyco;
    5.38 -
    5.39  local
    5.40    fun get_eq_thms thy tyco = case DatatypePackage.get_datatype thy tyco
    5.41     of SOME _ => get_eq_datatype thy tyco
    5.42 @@ -506,7 +505,7 @@
    5.43  type hook = (string * (bool * ((string * sort) list * (string * typ list) list))) list
    5.44    -> theory -> theory;
    5.45  
    5.46 -fun add_codetypes_hook_bootstrap hook thy =
    5.47 +fun add_codetypes_hook hook thy =
    5.48    let
    5.49      fun add_spec thy (tyco, is_dt) =
    5.50        (tyco, (is_dt, get_spec thy (tyco, is_dt)));
    5.51 @@ -517,8 +516,8 @@
    5.52    in
    5.53      thy
    5.54      |> fold hook ((map o map) (add_spec thy) (codetypes_dependency thy))
    5.55 -    |> DatatypeHooks.add datatype_hook
    5.56 -    |> TypecopyPackage.add_hook typecopy_hook
    5.57 +    |> DatatypePackage.add_interpretator datatype_hook
    5.58 +    |> TypecopyPackage.add_interpretator typecopy_hook
    5.59    end;
    5.60  
    5.61  fun the_codetypes_mut_specs thy ([(tyco, is_dt)]) =
    5.62 @@ -572,11 +571,11 @@
    5.63          val ty = (tys' ---> Type (tyco, map TFree vs'));
    5.64        in list_comb (Const (c, ty), map Free ts) end;
    5.65    in
    5.66 -    map (fn (tyco, cs) => (tyco, (mk_arity tyco, map (mk_cons tyco) cs))) css |> SOME
    5.67 -  end handle Class_Error => NONE;
    5.68 +    map (fn (tyco, cs) => (tyco, (mk_arity tyco, map (mk_cons tyco) cs))) css
    5.69 +  end;
    5.70  
    5.71  fun prove_codetypes_arities tac tycos sort f after_qed thy =
    5.72 -  case get_codetypes_arities thy tycos sort
    5.73 +  case try (get_codetypes_arities thy tycos) sort
    5.74     of NONE => thy
    5.75      | SOME insts => let
    5.76          fun proven (tyco, asorts, sort) =
    5.77 @@ -634,13 +633,13 @@
    5.78  
    5.79  val setup = 
    5.80    add_codegen "datatype" datatype_codegen
    5.81 -  #> add_tycodegen "datatype" datatype_tycodegen 
    5.82 -  #> DatatypeHooks.add (fold add_datatype_case_const)
    5.83 -  #> DatatypeHooks.add (fold add_datatype_case_defs)
    5.84 +  #> add_tycodegen "datatype" datatype_tycodegen
    5.85 +  #> DatatypePackage.add_interpretator (fold add_datatype_case_const)
    5.86 +  #> DatatypePackage.add_interpretator (fold add_datatype_case_defs)
    5.87  
    5.88  val setup_hooks =
    5.89 -  add_codetypes_hook_bootstrap codetype_hook
    5.90 -  #> add_codetypes_hook_bootstrap eq_hook
    5.91 +  add_codetypes_hook codetype_hook
    5.92 +  #> add_codetypes_hook eq_hook
    5.93  
    5.94  
    5.95  end;
     6.1 --- a/src/HOL/Tools/datatype_hooks.ML	Tue Sep 18 07:36:38 2007 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,35 +0,0 @@
     6.4 -(*  Title:      HOL/Tools/datatype_hooks.ML
     6.5 -    ID:         $Id$
     6.6 -    Author:     Florian Haftmann, TU Muenchen
     6.7 -
     6.8 -Hooks for datatype introduction.
     6.9 -*)
    6.10 -
    6.11 -signature DATATYPE_HOOKS =
    6.12 -sig
    6.13 -  type hook = string list -> theory -> theory
    6.14 -  val add: hook -> theory -> theory
    6.15 -  val all: hook
    6.16 -end;
    6.17 -
    6.18 -structure DatatypeHooks : DATATYPE_HOOKS =
    6.19 -struct
    6.20 -
    6.21 -type hook = string list -> theory -> theory;
    6.22 -
    6.23 -structure DatatypeHooksData = TheoryDataFun
    6.24 -(
    6.25 -  type T = (serial * hook) list;
    6.26 -  val empty = [];
    6.27 -  val copy = I;
    6.28 -  val extend = I;
    6.29 -  fun merge _ hooks : T = AList.merge (op =) (K true) hooks;
    6.30 -);
    6.31 -
    6.32 -fun add hook =
    6.33 -  DatatypeHooksData.map (cons (serial (), hook));
    6.34 -
    6.35 -fun all dtcos thy =
    6.36 -  fold_rev (fn (_, f) => f dtcos) (DatatypeHooksData.get thy) thy;
    6.37 -
    6.38 -end;
     7.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Sep 18 07:36:38 2007 +0200
     7.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Sep 18 07:46:00 2007 +0200
     7.3 @@ -69,6 +69,7 @@
     7.4    val datatype_of_case : theory -> string -> DatatypeAux.datatype_info option
     7.5    val get_datatype_spec : theory -> string -> ((string * sort) list * (string * typ list) list) option
     7.6    val get_datatype_constrs : theory -> string -> (string * typ) list option
     7.7 +  val add_interpretator: (string list -> theory -> theory) -> theory -> theory
     7.8    val print_datatypes : theory -> unit
     7.9    val make_case :  Proof.context -> bool -> string list -> term ->
    7.10      (term * term) list -> term * (term * (int * bool)) list
    7.11 @@ -521,6 +522,10 @@
    7.12  val specify_consts = gen_specify_consts Sign.add_consts_i;
    7.13  val specify_consts_authentic = gen_specify_consts Sign.add_consts_authentic;
    7.14  
    7.15 +structure DatatypeInterpretator = TheoryInterpretatorFun(struct type T = string; val eq = op = end);
    7.16 +
    7.17 +fun add_interpretator interpretator = DatatypeInterpretator.add_interpretator interpretator;
    7.18 +
    7.19  fun add_datatype_axm flat_names new_type_names descr sorts types_syntax constr_syntax dt_info
    7.20      case_names_induct case_names_exhausts thy =
    7.21    let
    7.22 @@ -666,7 +671,7 @@
    7.23        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
    7.24        |> snd
    7.25        |> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos)
    7.26 -      |> DatatypeHooks.all (map fst dt_infos);
    7.27 +      |> DatatypeInterpretator.add_those (map fst dt_infos);
    7.28    in
    7.29      ({distinct = distinct,
    7.30        inject = inject,
    7.31 @@ -726,7 +731,7 @@
    7.32        |> Theory.parent_path
    7.33        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
    7.34        |> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos)
    7.35 -      |> DatatypeHooks.all (map fst dt_infos);
    7.36 +      |> DatatypeInterpretator.add_those (map fst dt_infos);
    7.37    in
    7.38      ({distinct = distinct,
    7.39        inject = inject,
    7.40 @@ -831,7 +836,7 @@
    7.41        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
    7.42        |> snd
    7.43        |> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos)
    7.44 -      |> DatatypeHooks.all (map fst dt_infos);
    7.45 +      |> DatatypeInterpretator.add_those (map fst dt_infos);
    7.46    in
    7.47      ({distinct = distinct,
    7.48        inject = inject,
    7.49 @@ -934,7 +939,8 @@
    7.50    DatatypeProp.distinctness_limit_setup #>
    7.51    Method.add_methods tactic_emulations #>
    7.52    simproc_setup #>
    7.53 -  trfun_setup;
    7.54 +  trfun_setup #>
    7.55 +  DatatypeInterpretator.init;
    7.56  
    7.57  
    7.58  (* outer syntax *)
     8.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Sep 18 07:36:38 2007 +0200
     8.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Sep 18 07:46:00 2007 +0200
     8.3 @@ -26,7 +26,6 @@
     8.4      val setup_termination_proof : string option -> local_theory -> Proof.state
     8.5  
     8.6      val setup : theory -> theory
     8.7 -    val setup_case_cong_hook : theory -> theory
     8.8      val get_congs : theory -> thm list
     8.9  end
    8.10  
    8.11 @@ -176,11 +175,10 @@
    8.12                             |> safe_mk_meta_eq)))
    8.13                         thy
    8.14  
    8.15 -val case_cong_hook = fold add_case_cong
    8.16 +val case_cong = fold add_case_cong
    8.17  
    8.18 -val setup_case_cong_hook =
    8.19 -    DatatypeHooks.add case_cong_hook
    8.20 -    #> (fn thy => case_cong_hook (Symtab.keys (DatatypePackage.get_datatypes thy)) thy)
    8.21 +val setup_case_cong = DatatypePackage.add_interpretator case_cong
    8.22 +
    8.23  
    8.24  
    8.25  (* ad-hoc method to convert elimination-style goals to existential statements *)
    8.26 @@ -259,7 +257,7 @@
    8.27    Attrib.add_attributes
    8.28      [("fundef_cong", Attrib.add_del_args FundefCtxTree.cong_add FundefCtxTree.cong_del,
    8.29        "declaration of congruence rule for function definitions")]
    8.30 -  #> setup_case_cong_hook
    8.31 +  #> setup_case_cong
    8.32    #> FundefRelation.setup
    8.33    #> elim_to_cases_setup
    8.34  
     9.1 --- a/src/HOL/Tools/typecopy_package.ML	Tue Sep 18 07:36:38 2007 +0200
     9.2 +++ b/src/HOL/Tools/typecopy_package.ML	Tue Sep 18 07:46:00 2007 +0200
     9.3 @@ -19,8 +19,8 @@
     9.4      -> theory -> (string * info) * theory
     9.5    val get_typecopies: theory -> string list
     9.6    val get_typecopy_info: theory -> string -> info option
     9.7 -  type hook = string * info -> theory -> theory
     9.8 -  val add_hook: hook -> theory -> theory
     9.9 +  type interpretator = string * info -> theory -> theory
    9.10 +  val add_interpretator: interpretator -> theory -> theory
    9.11    val get_spec: theory -> string -> (string * sort) list * (string * typ list) list
    9.12    val get_eq: theory -> string -> thm
    9.13    val print_typecopies: theory -> unit
    9.14 @@ -41,21 +41,20 @@
    9.15    proj_def: thm
    9.16  };
    9.17  
    9.18 -type hook = string * info -> theory -> theory;
    9.19 +structure TypecopyInterpretator = TheoryInterpretatorFun(struct type T = string; val eq = op = end);
    9.20  
    9.21  structure TypecopyData = TheoryDataFun
    9.22  (
    9.23 -  type T = info Symtab.table * (serial * hook) list;
    9.24 -  val empty = (Symtab.empty, []);
    9.25 +  type T = info Symtab.table;
    9.26 +  val empty = Symtab.empty;
    9.27    val copy = I;
    9.28    val extend = I;
    9.29 -  fun merge _ ((tab1, hooks1), (tab2, hooks2) : T) =
    9.30 -    (Symtab.merge (K true) (tab1, tab2), AList.merge (op =) (K true) (hooks1, hooks2));
    9.31 +  fun merge _ = Symtab.merge (K true);
    9.32  );
    9.33  
    9.34  fun print_typecopies thy =
    9.35    let
    9.36 -    val (tab, _) = TypecopyData.get thy;
    9.37 +    val tab = TypecopyData.get thy;
    9.38      fun mk (tyco, { vs, constr, typ, proj = (proj, _), ... } : info) =
    9.39        (Pretty.block o Pretty.breaks) [
    9.40          Sign.pretty_typ thy (Type (tyco, map TFree vs)),
    9.41 @@ -68,17 +67,16 @@
    9.42          (Pretty.str "type copies:" :: map mk (Symtab.dest tab))
    9.43      end;
    9.44  
    9.45 -val get_typecopies = Symtab.keys o fst o TypecopyData.get;
    9.46 -val get_typecopy_info = Symtab.lookup o fst o TypecopyData.get;
    9.47 +val get_typecopies = Symtab.keys o TypecopyData.get;
    9.48 +val get_typecopy_info = Symtab.lookup o TypecopyData.get;
    9.49  
    9.50  
    9.51 -(* hook management *)
    9.52 +(* interpretator management *)
    9.53  
    9.54 -fun add_hook hook =
    9.55 -  (TypecopyData.map o apsnd o cons) (serial (), hook);
    9.56 +type interpretator = string * info -> theory -> theory;
    9.57  
    9.58 -fun invoke_hooks tyco_info thy =
    9.59 -  fold_rev (fn (_, f) => f tyco_info) ((snd o TypecopyData.get) thy) thy;
    9.60 +fun add_interpretator interp = TypecopyInterpretator.add_interpretator
    9.61 +  (fold (fn tyco => fn thy => interp (tyco, (the o get_typecopy_info thy) tyco) thy));
    9.62  
    9.63  
    9.64  (* add a type copy *)
    9.65 @@ -109,8 +107,8 @@
    9.66            };
    9.67          in
    9.68            thy
    9.69 -          |> (TypecopyData.map o apfst o Symtab.update_new) (tyco, info)
    9.70 -          |> invoke_hooks (tyco, info)
    9.71 +          |> (TypecopyData.map o Symtab.update_new) (tyco, info)
    9.72 +          |> TypecopyInterpretator.add_those [tyco]
    9.73            |> pair (tyco, info)
    9.74          end
    9.75    in
    9.76 @@ -139,10 +137,10 @@
    9.77    in (vs, [(constr, [typ])]) end;
    9.78  
    9.79  
    9.80 -(* hook for projection function code *)
    9.81 +(* interpretator for projection function code *)
    9.82  
    9.83  fun add_project (_ , {proj_def, ...} : info) = Code.add_default_func proj_def;
    9.84  
    9.85 -val setup = add_hook add_project;
    9.86 +val setup = TypecopyInterpretator.init #> add_interpretator add_project;
    9.87  
    9.88  end;
    10.1 --- a/src/HOL/ex/ExecutableContent.thy	Tue Sep 18 07:36:38 2007 +0200
    10.2 +++ b/src/HOL/ex/ExecutableContent.thy	Tue Sep 18 07:46:00 2007 +0200
    10.3 @@ -7,7 +7,7 @@
    10.4  theory ExecutableContent
    10.5  imports
    10.6    Main
    10.7 -  Eval
    10.8 +  (*Eval*)
    10.9    "~~/src/HOL/ex/Records"
   10.10    AssocList
   10.11    Binomial
    11.1 --- a/src/Pure/theory.ML	Tue Sep 18 07:36:38 2007 +0200
    11.2 +++ b/src/Pure/theory.ML	Tue Sep 18 07:46:00 2007 +0200
    11.3 @@ -51,10 +51,108 @@
    11.4    val add_oracle: bstring * (theory * Object.T -> term) -> theory -> theory
    11.5  end
    11.6  
    11.7 -structure Theory: THEORY =
    11.8 +signature THEORY_INTERPRETATOR =
    11.9 +sig
   11.10 +  type T
   11.11 +  type interpretator = T list -> theory -> theory
   11.12 +  val add_those: T list -> theory -> theory
   11.13 +  val all_those: theory -> T list
   11.14 +  val add_interpretator: interpretator -> theory -> theory
   11.15 +  val init: theory -> theory
   11.16 +end;
   11.17 +
   11.18 +signature THEORY_INTERPRETATOR_KEY =
   11.19 +sig
   11.20 +  type T
   11.21 +  val eq: T * T -> bool
   11.22 +end;
   11.23 +
   11.24 +structure Theory =
   11.25  struct
   11.26  
   11.27  
   11.28 +(** datatype thy **)
   11.29 +
   11.30 +datatype thy = Thy of
   11.31 + {axioms: term NameSpace.table,
   11.32 +  defs: Defs.T,
   11.33 +  oracles: ((theory * Object.T -> term) * stamp) NameSpace.table,
   11.34 +  consolidate: theory -> theory};
   11.35 +
   11.36 +fun make_thy (axioms, defs, oracles, consolidate) =
   11.37 +  Thy {axioms = axioms, defs = defs, oracles = oracles, consolidate = consolidate};
   11.38 +
   11.39 +fun err_dup_axm dup = error ("Duplicate axiom: " ^ quote dup);
   11.40 +fun err_dup_ora dup = error ("Duplicate oracle: " ^ quote dup);
   11.41 +
   11.42 +structure ThyData = TheoryDataFun
   11.43 +(
   11.44 +  type T = thy;
   11.45 +  val empty = make_thy (NameSpace.empty_table, Defs.empty, NameSpace.empty_table, I);
   11.46 +  val copy = I;
   11.47 +
   11.48 +  fun extend (Thy {axioms, defs, oracles, consolidate}) =
   11.49 +    make_thy (NameSpace.empty_table, defs, oracles, consolidate);
   11.50 +
   11.51 +  fun merge pp (thy1, thy2) =
   11.52 +    let
   11.53 +      val Thy {axioms = _, defs = defs1, oracles = oracles1,
   11.54 +        consolidate = consolidate1} = thy1;
   11.55 +      val Thy {axioms = _, defs = defs2, oracles = oracles2,
   11.56 +        consolidate = consolidate2} = thy2;
   11.57 +
   11.58 +      val axioms = NameSpace.empty_table;
   11.59 +      val defs = Defs.merge pp (defs1, defs2);
   11.60 +      val oracles = NameSpace.merge_tables (eq_snd (op =)) (oracles1, oracles2)
   11.61 +        handle Symtab.DUP dup => err_dup_ora dup;
   11.62 +      val consolidate = consolidate1 #> consolidate2;
   11.63 +    in make_thy (axioms, defs, oracles, consolidate) end;
   11.64 +);
   11.65 +
   11.66 +fun rep_theory thy = ThyData.get thy |> (fn Thy {axioms, defs, oracles, ...} =>
   11.67 +  {axioms = axioms, defs = defs, oracles = oracles});
   11.68 +
   11.69 +fun map_thy f = ThyData.map (fn (Thy {axioms, defs, oracles, consolidate}) =>
   11.70 +  make_thy (f (axioms, defs, oracles, consolidate)));
   11.71 +
   11.72 +fun map_axioms f = map_thy
   11.73 +  (fn (axioms, defs, oracles, consolidate) => (f axioms, defs, oracles, consolidate));
   11.74 +fun map_defs f = map_thy
   11.75 +  (fn (axioms, defs, oracles, consolidate) => (axioms, f defs, oracles, consolidate));
   11.76 +fun map_oracles f = map_thy
   11.77 +  (fn (axioms, defs, oracles, consolidate) => (axioms, defs, f oracles, consolidate));
   11.78 +
   11.79 +
   11.80 +(* basic operations *)
   11.81 +
   11.82 +val axiom_space = #1 o #axioms o rep_theory;
   11.83 +val axiom_table = #2 o #axioms o rep_theory;
   11.84 +
   11.85 +val oracle_space = #1 o #oracles o rep_theory;
   11.86 +val oracle_table = #2 o #oracles o rep_theory;
   11.87 +
   11.88 +val axioms_of = Symtab.dest o #2 o #axioms o rep_theory;
   11.89 +
   11.90 +val defs_of = #defs o rep_theory;
   11.91 +
   11.92 +fun requires thy name what =
   11.93 +  if Context.exists_name name thy then ()
   11.94 +  else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);
   11.95 +
   11.96 +
   11.97 +(* interpretators *)
   11.98 +
   11.99 +fun add_consolidate f = map_thy
  11.100 +  (fn (axioms, defs, oracles, consolidate) => (axioms, defs, oracles, consolidate #> f));
  11.101 +
  11.102 +fun consolidate thy =
  11.103 +  let
  11.104 +    val Thy {consolidate, ...} = ThyData.get thy;
  11.105 +  in
  11.106 +    thy |> consolidate
  11.107 +  end;
  11.108 +
  11.109 +
  11.110  (** type theory **)
  11.111  
  11.112  (* context operations *)
  11.113 @@ -62,6 +160,10 @@
  11.114  val eq_thy = Context.eq_thy;
  11.115  val subthy = Context.subthy;
  11.116  
  11.117 +fun assert_super thy1 thy2 =
  11.118 +  if subthy (thy1, thy2) then thy2
  11.119 +  else raise THEORY ("Not a super theory", [thy1, thy2]);
  11.120 +
  11.121  val parents_of = Context.parents_of;
  11.122  val ancestors_of = Context.ancestors_of;
  11.123  
  11.124 @@ -73,7 +175,7 @@
  11.125  fun merge_list [] = raise THEORY ("Empty merge of theories", [])
  11.126    | merge_list (thy :: thys) = Library.foldl merge (thy, thys);
  11.127  
  11.128 -val begin_theory = Sign.local_path oo Context.begin_thy Sign.pp;
  11.129 +val begin_theory = Sign.local_path o consolidate oo Context.begin_thy Sign.pp;
  11.130  val end_theory = Context.finish_thy;
  11.131  val checkpoint = Context.checkpoint_thy;
  11.132  val copy = Context.copy_thy;
  11.133 @@ -86,73 +188,10 @@
  11.134  
  11.135  
  11.136  
  11.137 -(** datatype thy **)
  11.138 -
  11.139 -datatype thy = Thy of
  11.140 - {axioms: term NameSpace.table,
  11.141 -  defs: Defs.T,
  11.142 -  oracles: ((theory * Object.T -> term) * stamp) NameSpace.table};
  11.143 -
  11.144 -fun make_thy (axioms, defs, oracles) =
  11.145 -  Thy {axioms = axioms, defs = defs, oracles = oracles};
  11.146 -
  11.147 -fun err_dup_axm dup = error ("Duplicate axiom: " ^ quote dup);
  11.148 -fun err_dup_ora dup = error ("Duplicate oracle: " ^ quote dup);
  11.149 -
  11.150 -structure ThyData = TheoryDataFun
  11.151 -(
  11.152 -  type T = thy;
  11.153 -  val empty = make_thy (NameSpace.empty_table, Defs.empty, NameSpace.empty_table);
  11.154 -  val copy = I;
  11.155 -
  11.156 -  fun extend (Thy {axioms, defs, oracles}) = make_thy (NameSpace.empty_table, defs, oracles);
  11.157 -
  11.158 -  fun merge pp (thy1, thy2) =
  11.159 -    let
  11.160 -      val Thy {axioms = _, defs = defs1, oracles = oracles1} = thy1;
  11.161 -      val Thy {axioms = _, defs = defs2, oracles = oracles2} = thy2;
  11.162 +(** axioms **)
  11.163  
  11.164 -      val axioms = NameSpace.empty_table;
  11.165 -      val defs = Defs.merge pp (defs1, defs2);
  11.166 -      val oracles = NameSpace.merge_tables (eq_snd (op =)) (oracles1, oracles2)
  11.167 -        handle Symtab.DUP dup => err_dup_ora dup;
  11.168 -    in make_thy (axioms, defs, oracles) end;
  11.169 -);
  11.170 -
  11.171 -fun rep_theory thy = ThyData.get thy |> (fn Thy args => args);
  11.172 -
  11.173 -fun map_thy f = ThyData.map (fn (Thy {axioms, defs, oracles}) =>
  11.174 -  make_thy (f (axioms, defs, oracles)));
  11.175 -
  11.176 -fun map_axioms f = map_thy (fn (axioms, defs, oracles) => (f axioms, defs, oracles));
  11.177 -fun map_defs f = map_thy (fn (axioms, defs, oracles) => (axioms, f defs, oracles));
  11.178 -fun map_oracles f = map_thy (fn (axioms, defs, oracles) => (axioms, defs, f oracles));
  11.179 -
  11.180 -
  11.181 -(* basic operations *)
  11.182 -
  11.183 -val axiom_space = #1 o #axioms o rep_theory;
  11.184 -val axiom_table = #2 o #axioms o rep_theory;
  11.185 -
  11.186 -val oracle_space = #1 o #oracles o rep_theory;
  11.187 -val oracle_table = #2 o #oracles o rep_theory;
  11.188 -
  11.189 -val axioms_of = Symtab.dest o #2 o #axioms o rep_theory;
  11.190  fun all_axioms_of thy = maps axioms_of (thy :: ancestors_of thy);
  11.191  
  11.192 -val defs_of = #defs o rep_theory;
  11.193 -
  11.194 -fun requires thy name what =
  11.195 -  if Context.exists_name name thy then ()
  11.196 -  else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);
  11.197 -
  11.198 -fun assert_super thy1 thy2 =
  11.199 -  if subthy (thy1, thy2) then thy2
  11.200 -  else raise THEORY ("Not a super theory", [thy1, thy2]);
  11.201 -
  11.202 -
  11.203 -
  11.204 -(** add axioms **)
  11.205  
  11.206  (* prepare axioms *)
  11.207  
  11.208 @@ -311,5 +350,66 @@
  11.209  
  11.210  end;
  11.211  
  11.212 +functor TheoryInterpretatorFun(Key: THEORY_INTERPRETATOR_KEY) : THEORY_INTERPRETATOR =
  11.213 +struct
  11.214 +
  11.215 +open Key;
  11.216 +
  11.217 +type interpretator = T list -> theory -> theory;
  11.218 +
  11.219 +fun apply ips x = fold_rev (fn (_, f) => f x) ips;
  11.220 +
  11.221 +structure InterpretatorData = TheoryDataFun (
  11.222 +  type T = ((serial * interpretator) list * T list) * (theory -> theory);
  11.223 +  val empty = (([], []), I);
  11.224 +  val extend = I;
  11.225 +  val copy = I;
  11.226 +  fun merge pp (((interpretators1, done1), upd1), ((interpretators2, done2), upd2)) =
  11.227 +    let
  11.228 +      fun diff (interpretators1 : (serial * interpretator) list, done1)
  11.229 +        (interpretators2, done2) = let
  11.230 +          val interpretators = subtract (eq_fst (op =)) interpretators1 interpretators2;
  11.231 +          val undone = subtract eq done2 done1;
  11.232 +        in apply interpretators undone end;
  11.233 +      val interpretators = AList.merge (op =) (K true) (interpretators1, interpretators2);
  11.234 +      val done = Library.merge eq (done1, done2);
  11.235 +      val upd_new = diff (interpretators2, done2) (interpretators1, done1)
  11.236 +        #> diff (interpretators1, done1) (interpretators2, done2);
  11.237 +      val upd = upd1 #> upd2 #> upd_new;
  11.238 +    in ((interpretators, done), upd) end;
  11.239 +);
  11.240 +
  11.241 +fun consolidate thy =
  11.242 +  let
  11.243 +    val (_, upd) = InterpretatorData.get thy;
  11.244 +  in
  11.245 +    thy |> upd |> (InterpretatorData.map o apsnd) (K I)
  11.246 +  end;
  11.247 +
  11.248 +val init = Theory.add_consolidate consolidate;
  11.249 +
  11.250 +fun add_those xs thy =
  11.251 +  let
  11.252 +    val ((interpretators, _), _) = InterpretatorData.get thy;
  11.253 +  in
  11.254 +    thy
  11.255 +    |> apply interpretators xs
  11.256 +    |> (InterpretatorData.map o apfst o apsnd) (append xs)
  11.257 +  end;
  11.258 +
  11.259 +val all_those = snd o fst o InterpretatorData.get;
  11.260 +
  11.261 +fun add_interpretator interpretator thy =
  11.262 +  let
  11.263 +    val ((interpretators, xs), _) = InterpretatorData.get thy;
  11.264 +  in
  11.265 +    thy
  11.266 +    |> interpretator (rev xs)
  11.267 +    |> (InterpretatorData.map o apfst o apfst) (cons (serial (), interpretator))
  11.268 +  end;
  11.269 +
  11.270 +end;
  11.271 +
  11.272 +structure Theory: THEORY = Theory;
  11.273  structure BasicTheory: BASIC_THEORY = Theory;
  11.274  open BasicTheory;