author ballarin Tue Sep 29 22:15:54 2009 +0200 (2009-09-29) changeset 32804 ca430e6aee1c 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 file | annotate | diff | revisions etc/isar-keywords-ZF.el file | annotate | diff | revisions etc/isar-keywords.el file | annotate | diff | revisions src/Pure/Isar/expression.ML file | annotate | diff | revisions src/Pure/Isar/isar_cmd.ML file | annotate | diff | revisions src/Pure/Isar/isar_syn.ML file | annotate | diff | revisions src/Pure/Isar/locale.ML file | annotate | diff | revisions
     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 ***)