# HG changeset patch
# User ballarin
# Date 1292694196 -3600
# Node ID b806a767808309bb566f683beabab5c7092295fe
# Parent  6da953d30f48ea5618b954c9ea2d968a977a3ab2
Add mixins to locale dependencies.

diff -r 6da953d30f48 -r b806a7678083 src/FOL/ex/Locale_Test/Locale_Test1.thy
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Sat Dec 18 18:43:14 2010 +0100
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Sat Dec 18 18:43:16 2010 +0100
@@ -697,7 +697,69 @@
 locale mixin_thy_merge = le: reflexive le + le': reflexive le' for le le'
 
 
-subsection {* Interpretation in proofs *}
+subsection {* Mixins in sublocale *}
+
+text {* Simulate a specification of left groups where unit and inverse are defined
+  rather than specified.  This is possible, but not in FOL, due to the lack of a
+  selection operator. *}
+
+axiomatization glob_one and glob_inv
+  where glob_lone: "prod(glob_one(prod), x) = x"
+    and glob_linv: "prod(glob_inv(prod, x), x) = glob_one(prod)"
+
+locale dgrp = semi
+begin
+
+definition one where "one = glob_one(prod)"
+
+lemma lone: "one ** x = x"
+  unfolding one_def by (rule glob_lone)
+
+definition inv where "inv(x) = glob_inv(prod, x)"
+
+lemma linv: "inv(x) ** x = one"
+  unfolding one_def inv_def by (rule glob_linv)
+
+end
+
+sublocale lgrp < "def": dgrp
+  where one_equation: "dgrp.one(prod) = one" and inv_equation: "dgrp.inv(prod, x) = inv(x)"
+proof -
+  show "dgrp(prod)" by unfold_locales
+  from this interpret d: dgrp .
+  -- Unit
+  have "dgrp.one(prod) = glob_one(prod)" by (rule d.one_def)
+  also have "... = glob_one(prod) ** one" by (simp add: rone)
+  also have "... = one" by (simp add: glob_lone)
+  finally show "dgrp.one(prod) = one" .
+  -- Inverse
+  then have "dgrp.inv(prod, x) ** x = inv(x) ** x" by (simp add: glob_linv d.linv linv)
+  then show "dgrp.inv(prod, x) = inv(x)" by (simp add: rcancel)
+qed
+
+print_locale! lgrp
+
+context lgrp begin
+
+text {* Equations stored in target *}
+
+lemma "dgrp.one(prod) = one" by (rule one_equation)
+lemma "dgrp.inv(prod, x) = inv(x)" by (rule inv_equation)
+
+text {* Mixins applied *}
+
+lemma "one = glob_one(prod)" by (rule one_def)
+lemma "inv(x) = glob_inv(prod, x)" by (rule inv_def)
+
+end
+
+text {* Interpreted versions *}
+
+lemma "0 = glob_one (op +)" by (rule int.def.one_def)
+lemma "- x = glob_inv(op +, x)" by (rule int.def.inv_def)
+
+
+section {* Interpretation in proofs *}
 
 lemma True
 proof
diff -r 6da953d30f48 -r b806a7678083 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sat Dec 18 18:43:14 2010 +0100
+++ b/src/Pure/Isar/locale.ML	Sat Dec 18 18:43:16 2010 +0100
@@ -92,6 +92,26 @@
 
 (*** Locales ***)
 
+type mixins = (((morphism * bool) * serial) list) Inttab.table;
+  (* table of mixin lists, per list mixins in reverse order of declaration;
+     lists indexed by registration/dependency serial,
+     entries for empty lists may be omitted *)
+
+fun lookup_mixins serial' mixins = the_default [] (Inttab.lookup mixins serial');
+
+fun merge_mixins (mix1, mix2) = Inttab.join (K (Library.merge (eq_snd op =))) (mix1, mix2);
+
+fun insert_mixin serial' mixin =
+  Inttab.map_default (serial', []) (cons (mixin, serial ()));
+
+fun rename_mixin (old, new) mix =
+  case Inttab.lookup mix old of
+    NONE => mix |
+    SOME mxs => Inttab.delete old mix |> Inttab.update_new (new, mxs);
+
+fun compose_mixins mixins =
+  fold_rev Morphism.compose (map (fst o fst) mixins) Morphism.identity;
+
 datatype locale = Loc of {
   (** static part **)
   parameters: (string * sort) list * ((string * typ) * mixfix) list,
@@ -106,24 +126,31 @@
   notes: ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * serial) list,
     (* theorem declarations *)
   dependencies: ((string * (morphism * morphism)) * serial) list
-    (* locale dependencies (sublocale relation) *)
+    (* locale dependencies (sublocale relation) in reverse order *),
+  mixins: mixins
+    (* mixin part of dependencies *)
 };
 
-fun mk_locale ((parameters, spec, intros, axioms), ((syntax_decls, notes), dependencies)) =
+fun mk_locale ((parameters, spec, intros, axioms),
+    ((syntax_decls, notes), (dependencies, mixins))) =
   Loc {parameters = parameters, intros = intros, axioms = axioms, spec = spec,
-    syntax_decls = syntax_decls, notes = notes, dependencies = dependencies};
+    syntax_decls = syntax_decls, notes = notes, dependencies = dependencies, mixins = mixins};
 
-fun map_locale f (Loc {parameters, spec, intros, axioms, syntax_decls, notes, dependencies}) =
-  mk_locale (f ((parameters, spec, intros, axioms), ((syntax_decls, notes), dependencies)));
+fun map_locale f (Loc {parameters, spec, intros, axioms,
+    syntax_decls, notes, dependencies, mixins}) =
+  mk_locale (f ((parameters, spec, intros, axioms),
+    ((syntax_decls, notes), (dependencies, mixins))));
 
 fun merge_locale
- (Loc {parameters, spec, intros, axioms, syntax_decls, notes, dependencies},
-  Loc {syntax_decls = syntax_decls', notes = notes', dependencies = dependencies', ...}) =
+ (Loc {parameters, spec, intros, axioms, syntax_decls, notes, dependencies, mixins},
+  Loc {syntax_decls = syntax_decls', notes = notes',
+      dependencies = dependencies', mixins = mixins', ...}) =
     mk_locale
       ((parameters, spec, intros, axioms),
         ((merge (eq_snd op =) (syntax_decls, syntax_decls'),
           merge (eq_snd op =) (notes, notes')),
-            merge (eq_snd op =) (dependencies, dependencies')));
+            (merge (eq_snd op =) (dependencies, dependencies'),
+              (merge_mixins (mixins, mixins')))));
 
 structure Locales = Theory_Data
 (
@@ -149,8 +176,9 @@
     (binding,
       mk_locale ((parameters, spec, intros, axioms),
         ((map (fn decl => (decl, serial ())) syntax_decls, map (fn n => (n, serial ())) notes),
-          map (fn d => (d |> apsnd (rpair Morphism.identity), serial ())) dependencies))) #> snd);
-          (* FIXME *)
+          (map (fn d => (d |> apsnd (rpair Morphism.identity), serial ())) dependencies,
+            Inttab.empty)))) #> snd);
+          (* FIXME Morphism.identity *)
 
 fun change_locale name =
   Locales.map o apsnd o Symtab.map_entry name o map_locale o apsnd;
@@ -170,7 +198,17 @@
 fun specification_of thy = #spec o the_locale thy;
 
 fun dependencies_of thy name = the_locale thy name |>
-  #dependencies |> map fst;
+  #dependencies;
+
+fun mixins_of thy name serial = the_locale thy name |>
+  #mixins |> lookup_mixins serial;
+
+(* unused *)
+fun identity_on thy name morph =
+  let val mk_instance = instance_of thy name
+  in
+    forall2 (curry Term.aconv_untyped) (mk_instance Morphism.identity) (mk_instance morph)
+  end;
 
 (* Print instance and qualifiers *)
 
@@ -244,24 +282,28 @@
 
 val roundup_bound = 120;
 
-fun add thy depth export (name, morph) (deps, marked) =
+fun add thy depth stem export (name, morph, mixins) (deps, marked) =
   if depth > roundup_bound
   then error "Roundup bound exceeded (sublocale relation probably not terminating)."
   else
     let
-      val dependencies = dependencies_of thy name;
-      val instance = instance_of thy name (morph $> export);
+      val instance = instance_of thy name (morph $> stem $> export);
     in
       if member (ident_le thy) marked (name, instance)
       then (deps, marked)
       else
         let
-          val dependencies' =
-            map (fn (name, (morph', export')) => (name, morph' $> export' $> morph)) dependencies;
+          val full_morph = morph $> compose_mixins mixins $> stem;
+          (* no inheritance of mixins, regardless of requests by clients *)
+          val dependencies = dependencies_of thy name |>
+            map (fn ((name', (morph', export')), serial') =>
+              (name', morph' $> export', mixins_of thy name serial'));
           val marked' = (name, instance) :: marked;
-          val (deps', marked'') = fold_rev (add thy (depth + 1) export) dependencies' ([], marked');
+          val (deps', marked'') =
+            fold_rev (add thy (depth + 1) full_morph export) dependencies
+              ([], marked');
         in
-          ((name, morph) :: deps' @ deps, marked'')
+          ((name, full_morph) :: deps' @ deps, marked'')
         end
     end;
 
@@ -272,9 +314,10 @@
 
 fun roundup thy activate_dep export (name, morph) (marked, input) =
   let
-    (* Find all dependencies incuding new ones (which are dependencies enriching
+    (* Find all dependencies including new ones (which are dependencies enriching
       existing registrations). *)
-    val (dependencies, marked') = add thy 0 export (name, morph) ([], []);
+    val (dependencies, marked') =
+      add thy 0 Morphism.identity export (name, morph, []) ([], []);
     (* Filter out fragments from marked; these won't be activated. *)
     val dependencies' = filter_out (fn (name, morph) =>
       member (ident_le thy) marked (name, instance_of thy name (morph $> export))) dependencies;
@@ -291,33 +334,25 @@
 
 structure Registrations = Generic_Data
 (
-  type T = ((morphism * morphism) * serial) Idtab.table *
+  type T = ((morphism * morphism) * serial) Idtab.table * mixins;
     (* registrations, indexed by locale name and instance;
-       unique serial, points to mixin list *)
-    (((morphism * bool) * serial) list) Inttab.table;
-    (* table of mixin lists, per list mixins in reverse order of declaration;
-       lists indexed by registration serial,
-       entries for empty lists may be omitted *)
+       unique registration serial points to mixin list *)
   val empty = (Idtab.empty, Inttab.empty);
   val extend = I;
   fun merge ((reg1, mix1), (reg2, mix2)) : T =
     (Idtab.join (fn id => fn (r1 as (_, s1), r2 as (_, s2)) =>
         if s1 = s2 then raise Idtab.SAME else raise Idtab.DUP id) (reg1, reg2),
-      Inttab.join (K (Library.merge (eq_snd op =))) (mix1, mix2))
+      merge_mixins (mix1, mix2))
     handle Idtab.DUP id =>
       (* distinct interpretations with same base: merge their mixins *)
       let
         val (_, s1) = Idtab.lookup reg1 id |> the;
         val (morph2, s2) = Idtab.lookup reg2 id |> the;
         val reg2' = Idtab.update (id, (morph2, s1)) reg2;
-        val mix2' =
-          (case Inttab.lookup mix2 s2 of
-            NONE => mix2
-          | SOME mxs => Inttab.delete s2 mix2 |> Inttab.update_new (s1, mxs));
         val _ = warning "Removed duplicate interpretation after retrieving its mixins.";
         (* FIXME print interpretations,
            which is not straightforward without theory context *)
-      in merge ((reg1, mix1), (reg2', mix2')) end;
+      in merge ((reg1, mix1), (reg2', rename_mixin (s2, s1) mix2)) end;
     (* FIXME consolidate with dependencies, consider one data slot only *)
 );
 
@@ -330,7 +365,7 @@
 
 fun add_mixin serial' mixin =
   (* registration to be amended identified by its serial id *)
-  Registrations.map (apsnd (Inttab.map_default (serial', []) (cons (mixin, serial ()))));
+  Registrations.map (apsnd (insert_mixin serial' mixin));
 
 fun get_mixins context (name, morph) =
   let
@@ -339,12 +374,9 @@
   in
     (case Idtab.lookup regs (name, instance_of thy name morph) of
       NONE => []
-    | SOME (_, serial) => the_default [] (Inttab.lookup mixins serial))
+    | SOME (_, serial) => lookup_mixins serial mixins)
   end;
 
-fun compose_mixins mixins =
-  fold_rev Morphism.compose (map (fst o fst) mixins) Morphism.identity;
-
 fun collect_mixins context (name, morph) =
   let
     val thy = Context.theory_of context;
@@ -450,7 +482,7 @@
     (case Idtab.lookup regs (name, base) of
       NONE =>
         error ("No interpretation of locale " ^
-          quote (extern thy name) ^ " and\nparameter instantiation " ^
+          quote (extern thy name) ^ " with\nparameter instantiation " ^
           space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
           " available")
     | SOME (_, serial') => add_mixin serial' mixin context)
@@ -467,7 +499,7 @@
     val inst = instance_of thy name morph;
   in
     if member (ident_le thy) (get_idents context) (name, inst)
-    then context
+    then context  (* FIXME amend mixins? *)
     else
       (get_idents context, context)
       (* add new registrations with inherited mixins *)
@@ -485,9 +517,28 @@
 
 (*** Dependencies ***)
 
+(*
+fun amend_dependency loc (name, morph) mixin export thy =
+  let
+    val deps = dependencies_of thy loc;
+  in
+    case AList.lookup (fn ((name, morph), ((name', (morph', _)), _)) =>
+      ident_ord ((name, instance_of thy name morph), (name', instance_of thy name' morph')) = EQUAL) deps (name, morph) of
+        NONE => error ("Locale " ^
+          quote (extern thy name) ^ " with\parameter instantiation " ^
+          space_implode " " (map (quote o Syntax.string_of_term_global thy) morph) ^
+          " not a sublocale of " ^ quote (extern thy loc))
+      | SOME (_, serial') => change_locale ...
+  end;
+*)
+
 fun add_dependency loc (name, morph) mixin export thy =
   let
-    val thy' = (change_locale loc o apsnd) (cons ((name, (morph, export)), serial ())) thy;
+    val serial' = serial ();
+    val thy' = thy |>
+      (change_locale loc o apsnd)
+        (apfst (cons ((name, (morph, export)), serial')) #>
+          apsnd (case mixin of NONE => I | SOME mixin => insert_mixin serial' mixin));
     val context' = Context.Theory thy';
     val (_, regs) = fold_rev (roundup thy' cons export)
       (registrations_of context' loc) (get_idents (context'), []);
@@ -620,7 +671,7 @@
     fun add_locale_deps name =
       let
         val dependencies =
-          (map o apsnd) (instance_of thy name o op $>) (dependencies_of thy name);
+          (map o apsnd) (instance_of thy name o op $>) (dependencies_of thy name |> map fst);
       in
         fold (fn (super, ts) => fn (gr, deps) => (gr |> Graph.add_edge (super, name),
           deps |> Symtab.map_default (super, Symtab.empty) (Symtab.cons_list (name, ts))))