Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
authorballarin
Tue Sep 29 22:15:54 2009 +0200 (2009-09-29)
changeset 32804ca430e6aee1c
parent 32803 fc02b4b9eccc
parent 32801 6f97a67e8da8
child 32805 9b535493ac8d
Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
doc-src/Locales/Locales/Examples3.thy
etc/isar-keywords-ZF.el
etc/isar-keywords.el
src/Pure/Isar/expression.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/locale.ML
     1.1 --- a/doc-src/Locales/Locales/Examples3.thy	Sun Sep 27 11:50:27 2009 +0200
     1.2 +++ b/doc-src/Locales/Locales/Examples3.thy	Tue Sep 29 22:15:54 2009 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4    interpretation.  The third revision of the example illustrates this.  *}
     1.5  
     1.6  interpretation %visible nat: partial_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
     1.7 -  where nat_less_eq: "partial_order.less op \<le> (x::nat) y = (x < y)"
     1.8 +  where "partial_order.less op \<le> (x::nat) y = (x < y)"
     1.9  proof -
    1.10    show "partial_order (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)"
    1.11      by unfold_locales auto
    1.12 @@ -44,11 +44,10 @@
    1.13    elaborate interpretation proof.  *}
    1.14  
    1.15  interpretation %visible nat: lattice "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
    1.16 -  where "partial_order.less op \<le> (x::nat) y = (x < y)"
    1.17 -    and nat_meet_eq: "lattice.meet op \<le> (x::nat) y = min x y"
    1.18 -    and nat_join_eq: "lattice.join op \<le> (x::nat) y = max x y"
    1.19 +  where "lattice.meet op \<le> (x::nat) y = min x y"
    1.20 +    and "lattice.join op \<le> (x::nat) y = max x y"
    1.21  proof -
    1.22 -  show lattice: "lattice (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)"
    1.23 +  show "lattice (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)"
    1.24      txt {* We have already shown that this is a partial order, *}
    1.25      apply unfold_locales
    1.26      txt {* hence only the lattice axioms remain to be shown: @{subgoals
    1.27 @@ -57,13 +56,9 @@
    1.28      txt {* the goals become @{subgoals [display]} which can be solved
    1.29        by Presburger arithmetic. *}
    1.30      by arith+
    1.31 -  txt {* For the first of the equations, we refer to the theorem
    1.32 -  shown in the previous interpretation. *}
    1.33 -  show "partial_order.less op \<le> (x::nat) y = (x < y)"
    1.34 -    by (rule nat_less_eq)
    1.35 -  txt {* In order to show the remaining equations, we put ourselves in a
    1.36 +  txt {* In order to show the equations, we put ourselves in a
    1.37      situation where the lattice theorems can be used in a convenient way. *}
    1.38 -  from lattice interpret nat: lattice "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool" .
    1.39 +  then interpret nat: lattice "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool" .
    1.40    show "lattice.meet op \<le> (x::nat) y = min x y"
    1.41      by (bestsimp simp: nat.meet_def nat.is_inf_def)
    1.42    show "lattice.join op \<le> (x::nat) y = max x y"
    1.43 @@ -73,25 +68,7 @@
    1.44  text {* Next follows that @{text \<le>} is a total order. *}
    1.45  
    1.46  interpretation %visible nat: total_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
    1.47 -  where "partial_order.less op \<le> (x::nat) y = (x < y)"
    1.48 -    and "lattice.meet op \<le> (x::nat) y = min x y"
    1.49 -    and "lattice.join op \<le> (x::nat) y = max x y"
    1.50 -proof -
    1.51 -  show "total_order (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)"
    1.52 -    by unfold_locales arith
    1.53 -qed (rule nat_less_eq nat_meet_eq nat_join_eq)+
    1.54 -
    1.55 -text {* Since the locale hierarchy reflects that total
    1.56 -  orders are distributive lattices, an explicit interpretation of
    1.57 -  distributive lattices for the order relation on natural numbers is
    1.58 -  only necessary for mapping the definitions to the right operators on
    1.59 -  @{typ nat}. *}
    1.60 -
    1.61 -interpretation %visible nat: distrib_lattice "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
    1.62 -  where "partial_order.less op \<le> (x::nat) y = (x < y)"
    1.63 -    and "lattice.meet op \<le> (x::nat) y = min x y"
    1.64 -    and "lattice.join op \<le> (x::nat) y = max x y"
    1.65 -  by unfold_locales [1] (rule nat_less_eq nat_meet_eq nat_join_eq)+
    1.66 +  by unfold_locales arith
    1.67  
    1.68  text {* Theorems that are available in the theory at this point are shown in
    1.69    Table~\ref{tab:nat-lattice}.
    1.70 @@ -115,6 +92,29 @@
    1.71  \caption{Interpreted theorems for @{text \<le>} on the natural numbers.}
    1.72  \label{tab:nat-lattice}
    1.73  \end{table}
    1.74 +
    1.75 +  Note that since the locale hierarchy reflects that total orders are
    1.76 +  distributive lattices, an explicit interpretation of distributive
    1.77 +  lattices for the order relation on natural numbers is not neccessary.
    1.78 +
    1.79 +  Why not push this idea further and just give the last interpretation
    1.80 +  as a single interpretation instead of the sequence of three?  The
    1.81 +  reasons for this are twofold:
    1.82 +\begin{itemize}
    1.83 +\item
    1.84 +  Often it is easier to work in an incremental fashion, because later
    1.85 +  interpretations require theorems provided by earlier
    1.86 +  interpretations.
    1.87 +\item
    1.88 +  Assume that a definition is made in some locale $l_1$, and that $l_2$
    1.89 +  imports $l_1$.  Let an equation for the definition be
    1.90 +  proved in an interpretation of $l_2$.  The equation will be unfolded
    1.91 +  in interpretations of theorems added to $l_2$ or below in the import
    1.92 +  hierarchy, but not for theorems added above $l_2$.
    1.93 +  Hence, an equation interpreting a definition should always be given in
    1.94 +  an interpretation of the locale where the definition is made, not in
    1.95 +  an interpretation of a locale further down the hierarchy.
    1.96 +\end{itemize}
    1.97    *}
    1.98  
    1.99  
   1.100 @@ -125,8 +125,7 @@
   1.101    incrementally. *}
   1.102  
   1.103  interpretation nat_dvd: partial_order "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
   1.104 -  where nat_dvd_less_eq:
   1.105 -    "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
   1.106 +  where "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
   1.107  proof -
   1.108    show "partial_order (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool)"
   1.109      by unfold_locales (auto simp: dvd_def)
   1.110 @@ -142,8 +141,7 @@
   1.111    x \<noteq> y"}.  *}
   1.112  
   1.113  interpretation nat_dvd: lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
   1.114 -  where "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
   1.115 -    and nat_dvd_meet_eq: "lattice.meet (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = gcd"
   1.116 +  where nat_dvd_meet_eq: "lattice.meet (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = gcd"
   1.117      and nat_dvd_join_eq: "lattice.join (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = lcm"
   1.118  proof -
   1.119    show "lattice (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool)"
   1.120 @@ -155,8 +153,6 @@
   1.121      apply (auto intro: lcm_least_nat)
   1.122      done
   1.123    then interpret nat_dvd: lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool" .
   1.124 -  show "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
   1.125 -    by (rule nat_dvd_less_eq)
   1.126    show "lattice.meet (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = gcd"
   1.127      apply (auto simp add: expand_fun_eq)
   1.128      apply (unfold nat_dvd.meet_def)
   1.129 @@ -198,18 +194,11 @@
   1.130  
   1.131  interpretation %visible nat_dvd:
   1.132    distrib_lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
   1.133 -  where "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
   1.134 -    and "lattice.meet (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = gcd"
   1.135 -    and "lattice.join (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = lcm"
   1.136 -proof -
   1.137 -  show "distrib_lattice (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool)"
   1.138 -    apply unfold_locales
   1.139 -    txt {* @{subgoals [display]} *}
   1.140 -    apply (unfold nat_dvd_meet_eq nat_dvd_join_eq)
   1.141 -    txt {* @{subgoals [display]} *}
   1.142 -    apply (rule gcd_lcm_distr)
   1.143 -    done
   1.144 -qed (rule nat_dvd_less_eq nat_dvd_meet_eq nat_dvd_join_eq)+
   1.145 +  apply unfold_locales
   1.146 +  txt {* @{subgoals [display]} *}
   1.147 +  apply (unfold nat_dvd_meet_eq nat_dvd_join_eq)
   1.148 +  txt {* @{subgoals [display]} *}
   1.149 +  apply (rule gcd_lcm_distr) done
   1.150  
   1.151  
   1.152  text {* Theorems that are available in the theory after these
     2.1 --- a/etc/isar-keywords-ZF.el	Sun Sep 27 11:50:27 2009 +0200
     2.2 +++ b/etc/isar-keywords-ZF.el	Tue Sep 29 22:15:54 2009 +0200
     2.3 @@ -139,6 +139,7 @@
     2.4      "print_drafts"
     2.5      "print_facts"
     2.6      "print_induct_rules"
     2.7 +    "print_interps"
     2.8      "print_locale"
     2.9      "print_locales"
    2.10      "print_methods"
    2.11 @@ -304,6 +305,7 @@
    2.12      "print_drafts"
    2.13      "print_facts"
    2.14      "print_induct_rules"
    2.15 +    "print_interps"
    2.16      "print_locale"
    2.17      "print_locales"
    2.18      "print_methods"
     3.1 --- a/etc/isar-keywords.el	Sun Sep 27 11:50:27 2009 +0200
     3.2 +++ b/etc/isar-keywords.el	Tue Sep 29 22:15:54 2009 +0200
     3.3 @@ -176,6 +176,7 @@
     3.4      "print_drafts"
     3.5      "print_facts"
     3.6      "print_induct_rules"
     3.7 +    "print_interps"
     3.8      "print_locale"
     3.9      "print_locales"
    3.10      "print_methods"
    3.11 @@ -379,6 +380,7 @@
    3.12      "print_drafts"
    3.13      "print_facts"
    3.14      "print_induct_rules"
    3.15 +    "print_interps"
    3.16      "print_locale"
    3.17      "print_locales"
    3.18      "print_methods"
     4.1 --- a/src/Pure/Isar/expression.ML	Sun Sep 27 11:50:27 2009 +0200
     4.2 +++ b/src/Pure/Isar/expression.ML	Tue Sep 29 22:15:54 2009 +0200
     4.3 @@ -818,8 +818,9 @@
     4.4  
     4.5      fun after_qed witss eqns = ProofContext.theory (note_eqns eqns
     4.6        #-> (fn eqns => fold (fn ((dep, morph), wits) =>
     4.7 -        Locale.add_registration_eqs (dep, morph $> Element.satisfy_morphism
     4.8 -          (map (Element.morph_witness export') wits)) eqns export) (deps ~~ witss)));
     4.9 +        fn thy => Locale.add_registration (dep, morph $> Element.satisfy_morphism
    4.10 +            (map (Element.morph_witness export') wits))
    4.11 +          (Element.eq_morphism thy eqns, true) export thy) (deps ~~ witss)));
    4.12  
    4.13    in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
    4.14  
     5.1 --- a/src/Pure/Isar/isar_cmd.ML	Sun Sep 27 11:50:27 2009 +0200
     5.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Sep 29 22:15:54 2009 +0200
     5.3 @@ -53,6 +53,7 @@
     5.4    val print_theorems: Toplevel.transition -> Toplevel.transition
     5.5    val print_locales: Toplevel.transition -> Toplevel.transition
     5.6    val print_locale: bool * xstring -> Toplevel.transition -> Toplevel.transition
     5.7 +  val print_registrations: string -> Toplevel.transition -> Toplevel.transition
     5.8    val print_attributes: Toplevel.transition -> Toplevel.transition
     5.9    val print_simpset: Toplevel.transition -> Toplevel.transition
    5.10    val print_rules: Toplevel.transition -> Toplevel.transition
    5.11 @@ -357,6 +358,10 @@
    5.12    Toplevel.keep (fn state =>
    5.13      Locale.print_locale (Toplevel.theory_of state) show_facts name);
    5.14  
    5.15 +fun print_registrations name = Toplevel.unknown_context o
    5.16 +  Toplevel.keep (fn state =>
    5.17 +    Locale.print_registrations (Toplevel.theory_of state) name);
    5.18 +
    5.19  val print_attributes = Toplevel.unknown_theory o
    5.20    Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of);
    5.21  
     6.1 --- a/src/Pure/Isar/isar_syn.ML	Sun Sep 27 11:50:27 2009 +0200
     6.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Sep 29 22:15:54 2009 +0200
     6.3 @@ -800,10 +800,15 @@
     6.4        o Toplevel.keep (Class.print_classes o Toplevel.theory_of)));
     6.5  
     6.6  val _ =
     6.7 -  OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag
     6.8 +  OuterSyntax.improper_command "print_locale" "print locale of this theory" K.diag
     6.9      (opt_bang -- P.xname >> (Toplevel.no_timing oo IsarCmd.print_locale));
    6.10  
    6.11  val _ =
    6.12 +  OuterSyntax.improper_command "print_interps"
    6.13 +    "print interpretations of locale for this theory" K.diag
    6.14 +    (P.xname >> (Toplevel.no_timing oo IsarCmd.print_registrations));
    6.15 +
    6.16 +val _ =
    6.17    OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag
    6.18      (Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes));
    6.19  
     7.1 --- a/src/Pure/Isar/locale.ML	Sun Sep 27 11:50:27 2009 +0200
     7.2 +++ b/src/Pure/Isar/locale.ML	Tue Sep 29 22:15:54 2009 +0200
     7.3 @@ -68,6 +68,8 @@
     7.4    val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
     7.5  
     7.6    (* Registrations and dependencies *)
     7.7 +  val add_registration: string * morphism -> morphism * bool -> morphism -> theory -> theory
     7.8 +  val amend_registration: string * morphism -> morphism * bool -> morphism -> theory -> theory
     7.9    val add_registration_eqs: string * morphism -> thm list -> morphism -> theory -> theory
    7.10    val amend_registration_legacy: morphism -> string * morphism -> theory -> theory
    7.11    val add_dependency: string -> string * morphism -> morphism -> theory -> theory
    7.12 @@ -75,6 +77,7 @@
    7.13    (* Diagnostic *)
    7.14    val print_locales: theory -> unit
    7.15    val print_locale: theory -> bool -> xstring -> unit
    7.16 +  val print_registrations: theory -> string -> unit
    7.17  end;
    7.18  
    7.19  structure Locale: LOCALE =
    7.20 @@ -177,6 +180,7 @@
    7.21  (** Identifiers: activated locales in theory or proof context **)
    7.22  
    7.23  fun ident_eq thy ((n: string, ts), (m, ss)) = (m = n) andalso Pattern.matchess thy (ss, ts);
    7.24 +(* FIXME: this is ident_le, smaller term is more general *)
    7.25  
    7.26  local
    7.27  
    7.28 @@ -234,7 +238,7 @@
    7.29  
    7.30  in
    7.31  
    7.32 -(* Note that while identifiers always have the exported view, activate_dep is
    7.33 +(* Note that while identifiers always have the external (exported) view, activate_dep is
    7.34    is presented with the internal view. *)
    7.35  
    7.36  fun roundup thy activate_dep export (name, morph) (marked, input) =
    7.37 @@ -328,29 +332,158 @@
    7.38  
    7.39  structure Registrations = TheoryDataFun
    7.40  (
    7.41 -  type T = ((string * (morphism * morphism)) * stamp) list;
    7.42 -    (* FIXME mixins need to be stamped *)
    7.43 +  type T = ((string * (morphism * morphism)) * stamp) list *
    7.44      (* registrations, in reverse order of declaration *)
    7.45 -  val empty = [];
    7.46 +    (stamp * ((morphism * bool) * stamp) list) list;
    7.47 +    (* alist of mixin lists, per list mixins in reverse order of declaration *)
    7.48 +  val empty = ([], []);
    7.49    val extend = I;
    7.50    val copy = I;
    7.51 -  fun merge _ data : T = Library.merge (eq_snd op =) data;
    7.52 +  fun merge _ ((r1, m1), (r2, m2)) : T =
    7.53 +    (Library.merge (eq_snd op =) (r1, r2),
    7.54 +      AList.join (op =) (K (Library.merge (eq_snd op =))) (m1, m2));
    7.55      (* FIXME consolidate with dependencies, consider one data slot only *)
    7.56  );
    7.57  
    7.58 -fun reg_morph ((name, (base, export)), _) = (name, base $> export);
    7.59 +
    7.60 +(* Primitive operations *)
    7.61 +
    7.62 +fun compose_mixins mixins =
    7.63 +  fold_rev Morphism.compose (map (fst o fst) mixins) Morphism.identity;
    7.64 +
    7.65 +fun reg_morph mixins ((name, (base, export)), stamp) =
    7.66 +  let val mix = the_default [] (AList.lookup (op =) mixins stamp) |> compose_mixins;
    7.67 +  in (name, base $> mix $> export) end;
    7.68  
    7.69  fun these_registrations thy name = Registrations.get thy
    7.70 -  |> filter (curry (op =) name o fst o fst)
    7.71 -  |> map reg_morph;
    7.72 +  |>> filter (curry (op =) name o fst o fst)
    7.73 +  |-> (fn regs => fn mixins => map (reg_morph mixins) regs);
    7.74  
    7.75  fun all_registrations thy = Registrations.get thy
    7.76 -  |> map reg_morph;
    7.77 +  |-> (fn regs => fn mixins => map (reg_morph mixins) regs);
    7.78 +
    7.79 +fun get_mixins thy (name, morph) =
    7.80 +  let
    7.81 +    val (regs, mixins) = Registrations.get thy;
    7.82 +  in
    7.83 +    case find_first (fn ((name', (morph', export')), _) => ident_eq thy
    7.84 +      ((name', instance_of thy name' (morph' $> export')), (name, instance_of thy name morph))) (rev regs) of
    7.85 +      NONE => []
    7.86 +    | SOME (_, stamp) => the_default [] (AList.lookup (op =) mixins stamp)
    7.87 +  end;
    7.88 +
    7.89 +fun collect_mixins thy (name, morph) =
    7.90 +  roundup thy (fn dep => fn mixins =>
    7.91 +    merge (eq_snd op =) (mixins, get_mixins thy dep)) Morphism.identity (name, morph) ([], [])
    7.92 +  |> snd |> filter (snd o fst);  (* only inheritable mixins *)
    7.93 +
    7.94 +fun activate_notes' activ_elem transfer thy export (name, morph) input =
    7.95 +  let
    7.96 +    val {notes, ...} = the_locale thy name;
    7.97 +    fun activate ((kind, facts), _) input =
    7.98 +      let
    7.99 +        val mixin = collect_mixins thy (name, morph $> export) |> compose_mixins;
   7.100 +        val facts' = facts |> Element.facts_map (Element.morph_ctxt (transfer input $> morph $> mixin $> export))
   7.101 +      in activ_elem (Notes (kind, facts')) input end;
   7.102 +  in
   7.103 +    fold_rev activate notes input
   7.104 +  end;
   7.105 +
   7.106 +fun activate_facts' export dep context =
   7.107 +  let
   7.108 +    val thy = Context.theory_of context;
   7.109 +    val activate = activate_notes' Element.init (Element.transfer_morphism o Context.theory_of) thy export;
   7.110 +  in roundup thy activate export dep (get_idents context, context) |-> put_idents end;
   7.111 +
   7.112 +
   7.113 +(* Diagnostic *)
   7.114 +
   7.115 +fun print_registrations thy raw_name =
   7.116 +  let
   7.117 +    val name = intern thy raw_name;
   7.118 +    val name' = extern thy name;
   7.119 +    val ctxt = ProofContext.init thy;
   7.120 +    fun prt_qual (qual, mand) = Pretty.str (qual ^ (if mand then "!" else "?"));
   7.121 +    fun prt_quals qs = Pretty.separate "." (map prt_qual qs) |> Pretty.block;
   7.122 +    val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
   7.123 +    fun prt_term' t = if !show_types
   7.124 +      then Pretty.block [prt_term t, Pretty.brk 1, Pretty.str "::",
   7.125 +        Pretty.brk 1, (Pretty.quote o Syntax.pretty_typ ctxt) (type_of t)]
   7.126 +      else prt_term t;
   7.127 +    fun prt_inst ts =
   7.128 +      Pretty.block (Pretty.breaks (Pretty.str name' :: map prt_term' ts));
   7.129 +    fun prt_reg (name, morph) =
   7.130 +      let
   7.131 +        val qs = Binding.name "x" |> Morphism.binding morph |> Binding.prefix_of;
   7.132 +        val ts = instance_of thy name morph;
   7.133 +      in
   7.134 +        case qs of
   7.135 +           [] => prt_inst ts
   7.136 +         | qs => Pretty.block [prt_quals qs, Pretty.brk 1, Pretty.str ":",
   7.137 +             Pretty.brk 1, prt_inst ts]
   7.138 +      end;
   7.139 +  in
   7.140 +    (case these_registrations thy name of
   7.141 +        [] => Pretty.str ("no interpretations")
   7.142 +      | regs => Pretty.big_list "interpretations:" (map prt_reg regs))
   7.143 +    |> Pretty.writeln
   7.144 +  end;
   7.145 +
   7.146 +
   7.147 +(* Add and extend registrations *)
   7.148 +
   7.149 +fun amend_registration (name, morph) mixin export thy =
   7.150 +  let
   7.151 +    val regs = Registrations.get thy |> fst;
   7.152 +    val base = instance_of thy name (morph $> export);
   7.153 +    fun match ((name', (morph', export')), _) =
   7.154 +      name = name' andalso eq_list (op aconv) (base, instance_of thy name' (morph' $> export'));
   7.155 +  in
   7.156 +    case find_first match (rev regs) of
   7.157 +        NONE => error ("No interpretation of locale " ^
   7.158 +          quote (extern thy name) ^ " and\nparameter instantiation " ^
   7.159 +          space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
   7.160 +          " available")
   7.161 +      | SOME (_, stamp') => Registrations.map 
   7.162 +          (apsnd (AList.map_default (op =) (stamp', []) (cons (mixin, stamp ())))) thy
   7.163 +    (* FIXME deal with inheritance: propagate to existing children *)
   7.164 +  end;
   7.165 +
   7.166 +(* Note that a registration that would be subsumed by an existing one will not be
   7.167 +   generated, and it will not be possible to amend it. *)
   7.168 +
   7.169 +fun add_registration (name, base_morph) mixin export thy =
   7.170 +  let
   7.171 +    val base = instance_of thy name base_morph;
   7.172 +  in
   7.173 +    if member (ident_eq thy) (get_idents (Context.Theory thy)) (name, base)
   7.174 +    then thy
   7.175 +    else
   7.176 +      let
   7.177 +        fun add_reg (dep', morph') =
   7.178 +          let
   7.179 +            val mixins = collect_mixins thy (dep', morph' $> export);
   7.180 +            val stamp = stamp ();
   7.181 +          in
   7.182 +            Registrations.map (apfst (cons ((dep', (morph', export)), stamp))
   7.183 +              #> apsnd (cons (stamp, mixins)))
   7.184 +          end
   7.185 +      in
   7.186 +        (get_idents (Context.Theory thy), thy)
   7.187 +        (* add new registrations with inherited mixins *)
   7.188 +        |> roundup thy add_reg export (name, base_morph)
   7.189 +        |> snd
   7.190 +        (* add mixin *)
   7.191 +        |> amend_registration (name, base_morph) mixin export
   7.192 +        (* activate import hierarchy as far as not already active *)
   7.193 +        |> Context.theory_map (activate_facts' export (name, base_morph))
   7.194 +      end
   7.195 +  end;
   7.196  
   7.197  fun amend_registration_legacy morph (name, base_morph) thy =
   7.198    (* legacy, never modify base morphism *)
   7.199    let
   7.200 -    val regs = map #1 (Registrations.get thy);
   7.201 +    val regs = Registrations.get thy |> fst |> map fst;
   7.202      val base = instance_of thy name base_morph;
   7.203      fun match (name', (morph', _)) =
   7.204        name = name' andalso eq_list (op aconv) (base, instance_of thy name' morph');
   7.205 @@ -361,7 +494,7 @@
   7.206          space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^ " available")
   7.207        else ();
   7.208    in
   7.209 -    Registrations.map (nth_map (length regs - 1 - i)
   7.210 +    Registrations.map ((apfst o nth_map (length regs - 1 - i))
   7.211        (fn ((name, (base, export)), stamp) => ((name, (base $> morph, export)), stamp))) thy
   7.212    end;
   7.213  
   7.214 @@ -372,7 +505,7 @@
   7.215    in
   7.216      (get_idents (Context.Theory thy), thy)
   7.217      |> roundup thy (fn (dep', morph') =>
   7.218 -        Registrations.map (cons ((dep', (morph', export)), stamp ()))) export (dep, morph)
   7.219 +        Registrations.map (apfst (cons ((dep', (morph', export)), stamp ())))) export (dep, morph)
   7.220      |> snd
   7.221      |> Context.theory_map (activate_facts (dep, morph $> export))
   7.222    end;
   7.223 @@ -383,8 +516,9 @@
   7.224  fun add_dependency loc (dep, morph) export thy =
   7.225    thy
   7.226    |> (change_locale loc o apsnd) (cons ((dep, morph $> export), stamp ()))
   7.227 -  |> (fn thy => fold_rev (Context.theory_map o activate_facts)
   7.228 +  |> (fn thy => fold_rev (Context.theory_map o activate_facts' export)
   7.229        (all_registrations thy) thy);
   7.230 +  (* FIXME deal with inheritance: propagate mixins to new children *)
   7.231  
   7.232  
   7.233  (*** Storing results ***)