Propagation of mixins for interpretation; reactivated diagnostic command print_interps.

--- a/doc-src/Locales/Locales/Examples3.thy	Sun Sep 27 11:50:27 2009 +0200
+++ b/doc-src/Locales/Locales/Examples3.thy	Tue Sep 29 22:15:54 2009 +0200
@@ -14,7 +14,7 @@
   interpretation.  The third revision of the example illustrates this.  *}
 
 interpretation %visible nat: partial_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
-  where nat_less_eq: "partial_order.less op \<le> (x::nat) y = (x < y)"
+  where "partial_order.less op \<le> (x::nat) y = (x < y)"
 proof -
   show "partial_order (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)"
     by unfold_locales auto
@@ -44,11 +44,10 @@
   elaborate interpretation proof.  *}
 
 interpretation %visible nat: lattice "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
-  where "partial_order.less op \<le> (x::nat) y = (x < y)"
-    and nat_meet_eq: "lattice.meet op \<le> (x::nat) y = min x y"
-    and nat_join_eq: "lattice.join op \<le> (x::nat) y = max x y"
+  where "lattice.meet op \<le> (x::nat) y = min x y"
+    and "lattice.join op \<le> (x::nat) y = max x y"
 proof -
-  show lattice: "lattice (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)"
+  show "lattice (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)"
     txt {* We have already shown that this is a partial order, *}
     apply unfold_locales
     txt {* hence only the lattice axioms remain to be shown: @{subgoals
@@ -57,13 +56,9 @@
     txt {* the goals become @{subgoals [display]} which can be solved
       by Presburger arithmetic. *}
     by arith+
-  txt {* For the first of the equations, we refer to the theorem
-  shown in the previous interpretation. *}
-  show "partial_order.less op \<le> (x::nat) y = (x < y)"
-    by (rule nat_less_eq)
-  txt {* In order to show the remaining equations, we put ourselves in a
+  txt {* In order to show the equations, we put ourselves in a
     situation where the lattice theorems can be used in a convenient way. *}
-  from lattice interpret nat: lattice "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool" .
+  then interpret nat: lattice "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool" .
   show "lattice.meet op \<le> (x::nat) y = min x y"
     by (bestsimp simp: nat.meet_def nat.is_inf_def)
   show "lattice.join op \<le> (x::nat) y = max x y"
@@ -73,25 +68,7 @@
 text {* Next follows that @{text \<le>} is a total order. *}
 
 interpretation %visible nat: total_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
-  where "partial_order.less op \<le> (x::nat) y = (x < y)"
-    and "lattice.meet op \<le> (x::nat) y = min x y"
-    and "lattice.join op \<le> (x::nat) y = max x y"
-proof -
-  show "total_order (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)"
-    by unfold_locales arith
-qed (rule nat_less_eq nat_meet_eq nat_join_eq)+
-
-text {* Since the locale hierarchy reflects that total
-  orders are distributive lattices, an explicit interpretation of
-  distributive lattices for the order relation on natural numbers is
-  only necessary for mapping the definitions to the right operators on
-  @{typ nat}. *}
-
-interpretation %visible nat: distrib_lattice "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
-  where "partial_order.less op \<le> (x::nat) y = (x < y)"
-    and "lattice.meet op \<le> (x::nat) y = min x y"
-    and "lattice.join op \<le> (x::nat) y = max x y"
-  by unfold_locales [1] (rule nat_less_eq nat_meet_eq nat_join_eq)+
+  by unfold_locales arith
 
 text {* Theorems that are available in the theory at this point are shown in
   Table~\ref{tab:nat-lattice}.
@@ -115,6 +92,29 @@
 \caption{Interpreted theorems for @{text \<le>} on the natural numbers.}
 \label{tab:nat-lattice}
 \end{table}
+
+  Note that since the locale hierarchy reflects that total orders are
+  distributive lattices, an explicit interpretation of distributive
+  lattices for the order relation on natural numbers is not neccessary.
+
+  Why not push this idea further and just give the last interpretation
+  as a single interpretation instead of the sequence of three?  The
+  reasons for this are twofold:
+\begin{itemize}
+\item
+  Often it is easier to work in an incremental fashion, because later
+  interpretations require theorems provided by earlier
+  interpretations.
+\item
+  Assume that a definition is made in some locale $l_1$, and that $l_2$
+  imports $l_1$.  Let an equation for the definition be
+  proved in an interpretation of $l_2$.  The equation will be unfolded
+  in interpretations of theorems added to $l_2$ or below in the import
+  hierarchy, but not for theorems added above $l_2$.
+  Hence, an equation interpreting a definition should always be given in
+  an interpretation of the locale where the definition is made, not in
+  an interpretation of a locale further down the hierarchy.
+\end{itemize}
   *}
 
 
@@ -125,8 +125,7 @@
   incrementally. *}
 
 interpretation nat_dvd: partial_order "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
-  where nat_dvd_less_eq:
-    "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
+  where "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
 proof -
   show "partial_order (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool)"
     by unfold_locales (auto simp: dvd_def)
@@ -142,8 +141,7 @@
   x \<noteq> y"}.  *}
 
 interpretation nat_dvd: lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
-  where "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
-    and nat_dvd_meet_eq: "lattice.meet (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = gcd"
+  where nat_dvd_meet_eq: "lattice.meet (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = gcd"
     and nat_dvd_join_eq: "lattice.join (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = lcm"
 proof -
   show "lattice (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool)"
@@ -155,8 +153,6 @@
     apply (auto intro: lcm_least_nat)
     done
   then interpret nat_dvd: lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool" .
-  show "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
-    by (rule nat_dvd_less_eq)
   show "lattice.meet (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = gcd"
     apply (auto simp add: expand_fun_eq)
     apply (unfold nat_dvd.meet_def)
@@ -198,18 +194,11 @@
 
 interpretation %visible nat_dvd:
   distrib_lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
-  where "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
-    and "lattice.meet (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = gcd"
-    and "lattice.join (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = lcm"
-proof -
-  show "distrib_lattice (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool)"
-    apply unfold_locales
-    txt {* @{subgoals [display]} *}
-    apply (unfold nat_dvd_meet_eq nat_dvd_join_eq)
-    txt {* @{subgoals [display]} *}
-    apply (rule gcd_lcm_distr)
-    done
-qed (rule nat_dvd_less_eq nat_dvd_meet_eq nat_dvd_join_eq)+
+  apply unfold_locales
+  txt {* @{subgoals [display]} *}
+  apply (unfold nat_dvd_meet_eq nat_dvd_join_eq)
+  txt {* @{subgoals [display]} *}
+  apply (rule gcd_lcm_distr) done
 
 
 text {* Theorems that are available in the theory after these

--- a/etc/isar-keywords-ZF.el	Sun Sep 27 11:50:27 2009 +0200
+++ b/etc/isar-keywords-ZF.el	Tue Sep 29 22:15:54 2009 +0200
@@ -139,6 +139,7 @@
     "print_drafts"
     "print_facts"
     "print_induct_rules"
+    "print_interps"
     "print_locale"
     "print_locales"
     "print_methods"
@@ -304,6 +305,7 @@
     "print_drafts"
     "print_facts"
     "print_induct_rules"
+    "print_interps"
     "print_locale"
     "print_locales"
     "print_methods"

--- a/etc/isar-keywords.el	Sun Sep 27 11:50:27 2009 +0200
+++ b/etc/isar-keywords.el	Tue Sep 29 22:15:54 2009 +0200
@@ -176,6 +176,7 @@
     "print_drafts"
     "print_facts"
     "print_induct_rules"
+    "print_interps"
     "print_locale"
     "print_locales"
     "print_methods"
@@ -379,6 +380,7 @@
     "print_drafts"
     "print_facts"
     "print_induct_rules"
+    "print_interps"
     "print_locale"
     "print_locales"
     "print_methods"

--- a/src/Pure/Isar/expression.ML	Sun Sep 27 11:50:27 2009 +0200
+++ b/src/Pure/Isar/expression.ML	Tue Sep 29 22:15:54 2009 +0200
@@ -818,8 +818,9 @@
 
     fun after_qed witss eqns = ProofContext.theory (note_eqns eqns
       #-> (fn eqns => fold (fn ((dep, morph), wits) =>
-        Locale.add_registration_eqs (dep, morph $> Element.satisfy_morphism
-          (map (Element.morph_witness export') wits)) eqns export) (deps ~~ witss)));
+        fn thy => Locale.add_registration (dep, morph $> Element.satisfy_morphism
+            (map (Element.morph_witness export') wits))
+          (Element.eq_morphism thy eqns, true) export thy) (deps ~~ witss)));
 
   in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
 

--- a/src/Pure/Isar/isar_cmd.ML	Sun Sep 27 11:50:27 2009 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Sep 29 22:15:54 2009 +0200
@@ -53,6 +53,7 @@
   val print_theorems: Toplevel.transition -> Toplevel.transition
   val print_locales: Toplevel.transition -> Toplevel.transition
   val print_locale: bool * xstring -> Toplevel.transition -> Toplevel.transition
+  val print_registrations: string -> Toplevel.transition -> Toplevel.transition
   val print_attributes: Toplevel.transition -> Toplevel.transition
   val print_simpset: Toplevel.transition -> Toplevel.transition
   val print_rules: Toplevel.transition -> Toplevel.transition
@@ -357,6 +358,10 @@
   Toplevel.keep (fn state =>
     Locale.print_locale (Toplevel.theory_of state) show_facts name);
 
+fun print_registrations name = Toplevel.unknown_context o
+  Toplevel.keep (fn state =>
+    Locale.print_registrations (Toplevel.theory_of state) name);
+
 val print_attributes = Toplevel.unknown_theory o
   Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of);
 

--- a/src/Pure/Isar/isar_syn.ML	Sun Sep 27 11:50:27 2009 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Sep 29 22:15:54 2009 +0200
@@ -800,10 +800,15 @@
       o Toplevel.keep (Class.print_classes o Toplevel.theory_of)));
 
 val _ =
-  OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag
+  OuterSyntax.improper_command "print_locale" "print locale of this theory" K.diag
     (opt_bang -- P.xname >> (Toplevel.no_timing oo IsarCmd.print_locale));
 
 val _ =
+  OuterSyntax.improper_command "print_interps"
+    "print interpretations of locale for this theory" K.diag
+    (P.xname >> (Toplevel.no_timing oo IsarCmd.print_registrations));
+
+val _ =
   OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag
     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes));
 

--- a/src/Pure/Isar/locale.ML	Sun Sep 27 11:50:27 2009 +0200
+++ b/src/Pure/Isar/locale.ML	Tue Sep 29 22:15:54 2009 +0200
@@ -68,6 +68,8 @@
   val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
 
   (* Registrations and dependencies *)
+  val add_registration: string * morphism -> morphism * bool -> morphism -> theory -> theory
+  val amend_registration: string * morphism -> morphism * bool -> morphism -> theory -> theory
   val add_registration_eqs: string * morphism -> thm list -> morphism -> theory -> theory
   val amend_registration_legacy: morphism -> string * morphism -> theory -> theory
   val add_dependency: string -> string * morphism -> morphism -> theory -> theory
@@ -75,6 +77,7 @@
   (* Diagnostic *)
   val print_locales: theory -> unit
   val print_locale: theory -> bool -> xstring -> unit
+  val print_registrations: theory -> string -> unit
 end;
 
 structure Locale: LOCALE =
@@ -177,6 +180,7 @@
 (** Identifiers: activated locales in theory or proof context **)
 
 fun ident_eq thy ((n: string, ts), (m, ss)) = (m = n) andalso Pattern.matchess thy (ss, ts);
+(* FIXME: this is ident_le, smaller term is more general *)
 
 local
 
@@ -234,7 +238,7 @@
 
 in
 
-(* Note that while identifiers always have the exported view, activate_dep is
+(* Note that while identifiers always have the external (exported) view, activate_dep is
   is presented with the internal view. *)
 
 fun roundup thy activate_dep export (name, morph) (marked, input) =
@@ -328,29 +332,158 @@
 
 structure Registrations = TheoryDataFun
 (
-  type T = ((string * (morphism * morphism)) * stamp) list;
-    (* FIXME mixins need to be stamped *)
+  type T = ((string * (morphism * morphism)) * stamp) list *
     (* registrations, in reverse order of declaration *)
-  val empty = [];
+    (stamp * ((morphism * bool) * stamp) list) list;
+    (* alist of mixin lists, per list mixins in reverse order of declaration *)
+  val empty = ([], []);
   val extend = I;
   val copy = I;
-  fun merge _ data : T = Library.merge (eq_snd op =) data;
+  fun merge _ ((r1, m1), (r2, m2)) : T =
+    (Library.merge (eq_snd op =) (r1, r2),
+      AList.join (op =) (K (Library.merge (eq_snd op =))) (m1, m2));
     (* FIXME consolidate with dependencies, consider one data slot only *)
 );
 
-fun reg_morph ((name, (base, export)), _) = (name, base $> export);
+
+(* Primitive operations *)
+
+fun compose_mixins mixins =
+  fold_rev Morphism.compose (map (fst o fst) mixins) Morphism.identity;
+
+fun reg_morph mixins ((name, (base, export)), stamp) =
+  let val mix = the_default [] (AList.lookup (op =) mixins stamp) |> compose_mixins;
+  in (name, base $> mix $> export) end;
 
 fun these_registrations thy name = Registrations.get thy
-  |> filter (curry (op =) name o fst o fst)
-  |> map reg_morph;
+  |>> filter (curry (op =) name o fst o fst)
+  |-> (fn regs => fn mixins => map (reg_morph mixins) regs);
 
 fun all_registrations thy = Registrations.get thy
-  |> map reg_morph;
+  |-> (fn regs => fn mixins => map (reg_morph mixins) regs);
+
+fun get_mixins thy (name, morph) =
+  let
+    val (regs, mixins) = Registrations.get thy;
+  in
+    case find_first (fn ((name', (morph', export')), _) => ident_eq thy
+      ((name', instance_of thy name' (morph' $> export')), (name, instance_of thy name morph))) (rev regs) of
+      NONE => []
+    | SOME (_, stamp) => the_default [] (AList.lookup (op =) mixins stamp)
+  end;
+
+fun collect_mixins thy (name, morph) =
+  roundup thy (fn dep => fn mixins =>
+    merge (eq_snd op =) (mixins, get_mixins thy dep)) Morphism.identity (name, morph) ([], [])
+  |> snd |> filter (snd o fst);  (* only inheritable mixins *)
+
+fun activate_notes' activ_elem transfer thy export (name, morph) input =
+  let
+    val {notes, ...} = the_locale thy name;
+    fun activate ((kind, facts), _) input =
+      let
+        val mixin = collect_mixins thy (name, morph $> export) |> compose_mixins;
+        val facts' = facts |> Element.facts_map (Element.morph_ctxt (transfer input $> morph $> mixin $> export))
+      in activ_elem (Notes (kind, facts')) input end;
+  in
+    fold_rev activate notes input
+  end;
+
+fun activate_facts' export dep context =
+  let
+    val thy = Context.theory_of context;
+    val activate = activate_notes' Element.init (Element.transfer_morphism o Context.theory_of) thy export;
+  in roundup thy activate export dep (get_idents context, context) |-> put_idents end;
+
+
+(* Diagnostic *)
+
+fun print_registrations thy raw_name =
+  let
+    val name = intern thy raw_name;
+    val name' = extern thy name;
+    val ctxt = ProofContext.init thy;
+    fun prt_qual (qual, mand) = Pretty.str (qual ^ (if mand then "!" else "?"));
+    fun prt_quals qs = Pretty.separate "." (map prt_qual qs) |> Pretty.block;
+    val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
+    fun prt_term' t = if !show_types
+      then Pretty.block [prt_term t, Pretty.brk 1, Pretty.str "::",
+        Pretty.brk 1, (Pretty.quote o Syntax.pretty_typ ctxt) (type_of t)]
+      else prt_term t;
+    fun prt_inst ts =
+      Pretty.block (Pretty.breaks (Pretty.str name' :: map prt_term' ts));
+    fun prt_reg (name, morph) =
+      let
+        val qs = Binding.name "x" |> Morphism.binding morph |> Binding.prefix_of;
+        val ts = instance_of thy name morph;
+      in
+        case qs of
+           [] => prt_inst ts
+         | qs => Pretty.block [prt_quals qs, Pretty.brk 1, Pretty.str ":",
+             Pretty.brk 1, prt_inst ts]
+      end;
+  in
+    (case these_registrations thy name of
+        [] => Pretty.str ("no interpretations")
+      | regs => Pretty.big_list "interpretations:" (map prt_reg regs))
+    |> Pretty.writeln
+  end;
+
+
+(* Add and extend registrations *)
+
+fun amend_registration (name, morph) mixin export thy =
+  let
+    val regs = Registrations.get thy |> fst;
+    val base = instance_of thy name (morph $> export);
+    fun match ((name', (morph', export')), _) =
+      name = name' andalso eq_list (op aconv) (base, instance_of thy name' (morph' $> export'));
+  in
+    case find_first match (rev regs) of
+        NONE => error ("No interpretation of locale " ^
+          quote (extern thy name) ^ " and\nparameter instantiation " ^
+          space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
+          " available")
+      | SOME (_, stamp') => Registrations.map 
+          (apsnd (AList.map_default (op =) (stamp', []) (cons (mixin, stamp ())))) thy
+    (* FIXME deal with inheritance: propagate to existing children *)
+  end;
+
+(* Note that a registration that would be subsumed by an existing one will not be
+   generated, and it will not be possible to amend it. *)
+
+fun add_registration (name, base_morph) mixin export thy =
+  let
+    val base = instance_of thy name base_morph;
+  in
+    if member (ident_eq thy) (get_idents (Context.Theory thy)) (name, base)
+    then thy
+    else
+      let
+        fun add_reg (dep', morph') =
+          let
+            val mixins = collect_mixins thy (dep', morph' $> export);
+            val stamp = stamp ();
+          in
+            Registrations.map (apfst (cons ((dep', (morph', export)), stamp))
+              #> apsnd (cons (stamp, mixins)))
+          end
+      in
+        (get_idents (Context.Theory thy), thy)
+        (* add new registrations with inherited mixins *)
+        |> roundup thy add_reg export (name, base_morph)
+        |> snd
+        (* add mixin *)
+        |> amend_registration (name, base_morph) mixin export
+        (* activate import hierarchy as far as not already active *)
+        |> Context.theory_map (activate_facts' export (name, base_morph))
+      end
+  end;
 
 fun amend_registration_legacy morph (name, base_morph) thy =
   (* legacy, never modify base morphism *)
   let
-    val regs = map #1 (Registrations.get thy);
+    val regs = Registrations.get thy |> fst |> map fst;
     val base = instance_of thy name base_morph;
     fun match (name', (morph', _)) =
       name = name' andalso eq_list (op aconv) (base, instance_of thy name' morph');
@@ -361,7 +494,7 @@
         space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^ " available")
       else ();
   in
-    Registrations.map (nth_map (length regs - 1 - i)
+    Registrations.map ((apfst o nth_map (length regs - 1 - i))
       (fn ((name, (base, export)), stamp) => ((name, (base $> morph, export)), stamp))) thy
   end;
 
@@ -372,7 +505,7 @@
   in
     (get_idents (Context.Theory thy), thy)
     |> roundup thy (fn (dep', morph') =>
-        Registrations.map (cons ((dep', (morph', export)), stamp ()))) export (dep, morph)
+        Registrations.map (apfst (cons ((dep', (morph', export)), stamp ())))) export (dep, morph)
     |> snd
     |> Context.theory_map (activate_facts (dep, morph $> export))
   end;
@@ -383,8 +516,9 @@
 fun add_dependency loc (dep, morph) export thy =
   thy
   |> (change_locale loc o apsnd) (cons ((dep, morph $> export), stamp ()))
-  |> (fn thy => fold_rev (Context.theory_map o activate_facts)
+  |> (fn thy => fold_rev (Context.theory_map o activate_facts' export)
       (all_registrations thy) thy);
+  (* FIXME deal with inheritance: propagate mixins to new children *)
 
 
 (*** Storing results ***)