# HG changeset patch
# User wenzelm
# Date 1535629132 -7200
# Node ID 6c9825c1e26b144ebed2029536b9057719f22372
# Parent  6d2735ca02713f59c7b3eb2a81205c4ec37f3431
clarified signature: explicit type Locale.registration;

diff -r 6d2735ca0271 -r 6c9825c1e26b src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Thu Aug 30 12:36:26 2018 +0200
+++ b/src/Pure/Isar/class.ML	Thu Aug 30 13:38:52 2018 +0200
@@ -229,9 +229,13 @@
 
 fun activate_defs class thms thy =
   (case Element.eq_morphism thy thms of
-    SOME eq_morph => fold (fn cls => fn thy =>
-      Context.theory_map (Locale.amend_registration (cls, base_morphism thy cls)
-        (eq_morph, true) (export_morphism thy cls)) thy) (heritage thy [class]) thy
+    SOME eq_morph =>
+      fold (fn cls => fn thy =>
+        Context.theory_map
+          (Locale.amend_registration
+            {dep = (cls, base_morphism thy cls),
+              mixin = SOME (eq_morph, true),
+              export = export_morphism thy cls}) thy) (heritage thy [class]) thy
   | NONE => thy);
 
 fun register_operation class (c, t) input_only thy =
@@ -484,10 +488,13 @@
     val diff_sort = Sign.complete_sort thy [sup]
       |> subtract (op =) (Sign.complete_sort thy [sub])
       |> filter (is_class thy);
-    fun add_dependency some_wit = case some_dep_morph of
-        SOME dep_morph => Generic_Target.locale_dependency sub
-          (sup, dep_morph $> Element.satisfy_morphism (the_list some_witn)) NONE export
-      | NONE => I;
+    fun add_dependency some_wit (* FIXME unused!? *) =
+      (case some_dep_morph of
+        SOME dep_morph =>
+          Generic_Target.locale_dependency sub
+            {dep = (sup, dep_morph $> Element.satisfy_morphism (the_list some_witn)),
+              mixin = NONE, export = export}
+      | NONE => I);
   in
     lthy
     |> Local_Theory.raw_theory
diff -r 6d2735ca0271 -r 6c9825c1e26b src/Pure/Isar/class_declaration.ML
--- a/src/Pure/Isar/class_declaration.ML	Thu Aug 30 12:36:26 2018 +0200
+++ b/src/Pure/Isar/class_declaration.ML	Thu Aug 30 13:38:52 2018 +0200
@@ -328,8 +328,10 @@
     |-> (fn (param_map, params, assm_axiom) =>
        `(fn thy => calculate thy class sups base_sort param_map assm_axiom)
     #-> (fn (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) =>
-       Context.theory_map (Locale.add_registration (class, base_morph)
-         (Option.map (rpair true) eq_morph) export_morph)
+       Context.theory_map (Locale.add_registration
+         {dep = (class, base_morph),
+           mixin = Option.map (rpair true) eq_morph,
+           export = export_morph})
     #> Class.register class sups params base_sort base_morph export_morph some_axiom some_assm_intro of_class
     #> Global_Theory.store_thm (prefix (Binding.qualified_name (class ^ ".of_class.intro")), of_class)))
     |> snd
diff -r 6d2735ca0271 -r 6c9825c1e26b src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Thu Aug 30 12:36:26 2018 +0200
+++ b/src/Pure/Isar/generic_target.ML	Thu Aug 30 13:38:52 2018 +0200
@@ -52,8 +52,7 @@
   val theory_abbrev: Syntax.mode -> (binding * mixfix) * term ->
     local_theory -> (term * term) * local_theory
   val theory_declaration: declaration -> local_theory -> local_theory
-  val theory_registration: string * morphism -> (morphism * bool) option -> morphism ->
-    local_theory -> local_theory
+  val theory_registration: Locale.registration -> local_theory -> local_theory
 
   (*locale target primitives*)
   val locale_target_notes: string -> string -> Attrib.fact list -> Attrib.fact list ->
@@ -71,8 +70,7 @@
     local_theory -> local_theory
   val locale_const: string -> Syntax.mode -> (binding * mixfix) * term ->
     local_theory -> local_theory
-  val locale_dependency: string -> string * morphism -> (morphism * bool) option -> morphism ->
-    local_theory -> local_theory
+  val locale_dependency: string -> Locale.registration -> local_theory -> local_theory
 
   (*initialisation*)
   val init: {background_naming: Name_Space.naming, setup: theory -> Proof.context,
@@ -372,7 +370,7 @@
   background_declaration decl #> standard_declaration (K true) decl;
 
 val theory_registration =
-  Local_Theory.raw_theory o Context.theory_map ooo Locale.add_registration;
+  Local_Theory.raw_theory o Context.theory_map o Locale.add_registration;
 
 
 
@@ -406,9 +404,9 @@
   locale_target_const locale (K true) prmode ((b, mx), rhs)
   #> standard_const (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, mx), rhs);
 
-fun locale_dependency locale dep_morph mixin export =
-  (Local_Theory.raw_theory ooo Locale.add_dependency locale) dep_morph mixin export
-  #> Locale.activate_fragment_nonbrittle dep_morph mixin export;
+fun locale_dependency locale registration =
+  Local_Theory.raw_theory (Locale.add_dependency locale registration)
+  #> Locale.activate_fragment_nonbrittle registration;
 
 
 (** locale abbreviations **)
diff -r 6d2735ca0271 -r 6c9825c1e26b src/Pure/Isar/interpretation.ML
--- a/src/Pure/Isar/interpretation.ML	Thu Aug 30 12:36:26 2018 +0200
+++ b/src/Pure/Isar/interpretation.ML	Thu Aug 30 13:38:52 2018 +0200
@@ -119,9 +119,12 @@
           $> Morphism.binding_morphism "position" (Binding.set_pos pos)
         in (dep, morph') end) deps witss;
     fun register (dep_morph, eqns) ctxt =
-      add_registration dep_morph
-        (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) (eqns @ eqns')))
-        export ctxt;
+      ctxt |> add_registration
+        {dep = dep_morph,
+          mixin =
+            Option.map (rpair true)
+              (Element.eq_morphism (Proof_Context.theory_of ctxt) (eqns @ eqns')),
+          export = export};
   in ctxt'' |> fold register (dep_morphs ~~ eqnss') end;
 
 in
@@ -150,9 +153,9 @@
     (fn witss => fn eqns => Proof.map_context (after_qed witss eqns) #> Proof.reset_facts)
     "interpret" propss eqns goal_ctxt state;
 
-fun add_registration reg mixin export ctxt = ctxt
+fun add_registration registration ctxt = ctxt
   |> Proof_Context.set_stmt false
-  |> Context.proof_map (Locale.add_registration reg mixin export)
+  |> Context.proof_map (Locale.add_registration registration)
   |> Proof_Context.restore_stmt ctxt;
 
 fun gen_interpret prep_interpretation expression state =
diff -r 6d2735ca0271 -r 6c9825c1e26b src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Thu Aug 30 12:36:26 2018 +0200
+++ b/src/Pure/Isar/local_theory.ML	Thu Aug 30 13:38:52 2018 +0200
@@ -14,6 +14,11 @@
   type fact = binding * thms;
 end;
 
+structure Locale =
+struct
+  type registration = {dep: string * morphism, mixin: (morphism * bool) option, export: morphism};
+end;
+
 signature LOCAL_THEORY =
 sig
   type operations
@@ -54,10 +59,8 @@
   val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
     (term * term) * local_theory
   val declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory
-  val theory_registration: string * morphism -> (morphism * bool) option -> morphism ->
-    local_theory -> local_theory
-  val locale_dependency: string * morphism -> (morphism * bool) option -> morphism ->
-    local_theory -> local_theory
+  val theory_registration: Locale.registration -> local_theory -> local_theory
+  val locale_dependency: Locale.registration -> local_theory -> local_theory
   val pretty: local_theory -> Pretty.T list
   val add_thms_dynamic: binding * (Context.generic -> thm list) -> local_theory -> local_theory
   val set_defsort: sort -> local_theory -> local_theory
@@ -91,10 +94,8 @@
   abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
     (term * term) * local_theory,
   declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory,
-  theory_registration: string * morphism -> (morphism * bool) option -> morphism ->
-     local_theory -> local_theory,
-  locale_dependency: string * morphism -> (morphism * bool) option -> morphism ->
-     local_theory -> local_theory,
+  theory_registration: Locale.registration -> local_theory -> local_theory,
+  locale_dependency: Locale.registration -> local_theory -> local_theory,
   pretty: local_theory -> Pretty.T list};
 
 type lthy =
@@ -276,10 +277,10 @@
 val define_internal = operation2 #define true;
 val notes_kind = operation2 #notes;
 val declaration = operation2 #declaration;
-fun theory_registration dep_morph mixin export =
-  assert_bottom #> operation (fn ops => #theory_registration ops dep_morph mixin export);
-fun locale_dependency dep_morph mixin export =
-  assert_bottom #> operation (fn ops => #locale_dependency ops dep_morph mixin export);
+fun theory_registration registration =
+  assert_bottom #> operation (fn ops => #theory_registration ops registration);
+fun locale_dependency registration =
+  assert_bottom #> operation (fn ops => #locale_dependency ops registration);
 
 
 (* theorems *)
diff -r 6d2735ca0271 -r 6c9825c1e26b src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Aug 30 12:36:26 2018 +0200
+++ b/src/Pure/Isar/locale.ML	Thu Aug 30 13:38:52 2018 +0200
@@ -73,17 +73,13 @@
   val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
 
   (* Registrations and dependencies *)
-  val add_registration: string * morphism -> (morphism * bool) option ->
-    morphism -> Context.generic -> Context.generic
-  val activate_fragment: string * morphism -> (morphism * bool) option -> morphism ->
-    local_theory -> local_theory
-  val activate_fragment_nonbrittle: string * morphism -> (morphism * bool) option -> morphism ->
-    local_theory -> local_theory
-  val amend_registration: string * morphism -> morphism * bool ->
-    morphism -> Context.generic -> Context.generic
+  type registration = {dep: string * morphism, mixin: (morphism * bool) option, export: morphism}
+  val amend_registration: registration -> Context.generic -> Context.generic
+  val add_registration: registration -> Context.generic -> Context.generic
+  val activate_fragment: registration -> local_theory -> local_theory
+  val activate_fragment_nonbrittle: registration -> local_theory -> local_theory
   val registrations_of: Context.generic -> string -> (string * morphism) list
-  val add_dependency: string -> string * morphism -> (morphism * bool) option ->
-    morphism -> theory -> theory
+  val add_dependency: string -> registration -> theory -> theory
 
   (* Diagnostic *)
   val hyp_spec_of: theory -> string -> Element.context_i list
@@ -516,29 +512,32 @@
 
 (*** Add and extend registrations ***)
 
-fun amend_registration (name, morph) mixin export context =
-  let
-    val thy = Context.theory_of context;
-    val ctxt = Context.proof_of context;
+type registration = Locale.registration;
+
+fun amend_registration {mixin = NONE, ...} context = context
+  | amend_registration {dep = (name, morph), mixin = SOME mixin, export} context =
+      let
+        val thy = Context.theory_of context;
+        val ctxt = Context.proof_of context;
 
-    val regs = Registrations.get context |> fst;
-    val base = instance_of thy name (morph $> export);
-    val serial' =
-      (case Idtab.lookup regs (name, base) of
-        NONE =>
-          error ("No interpretation of locale " ^ quote (markup_name ctxt name) ^
-            " with\nparameter instantiation " ^
-            space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
-            " available")
-      | SOME (_, serial') => serial');
-  in
-    add_mixin serial' mixin context
-  end;
+        val regs = Registrations.get context |> fst;
+        val base = instance_of thy name (morph $> export);
+        val serial' =
+          (case Idtab.lookup regs (name, base) of
+            NONE =>
+              error ("No interpretation of locale " ^ quote (markup_name ctxt name) ^
+                " with\nparameter instantiation " ^
+                space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
+                " available")
+          | SOME (_, serial') => serial');
+      in
+        add_mixin serial' mixin context
+      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 context =
+fun add_registration {dep = (name, base_morph), mixin, export} context =
   let
     val thy = Context.theory_of context;
     val mix = (case mixin of NONE => Morphism.identity | SOME (mix, _) => mix);
@@ -554,7 +553,7 @@
       |> roundup thy (add_reg thy export) export (name, morph)
       |> snd
       (* add mixin *)
-      |> (case mixin of NONE => I | SOME mixin => amend_registration (name, morph) mixin export)
+      |> amend_registration {dep = (name, morph), mixin = mixin, export = export}
       (* activate import hierarchy as far as not already active *)
       |> activate_facts (SOME export) (name, morph)
   end;
@@ -562,14 +561,14 @@
 
 (* locale fragments within local theory *)
 
-fun activate_fragment_nonbrittle dep_morph mixin export lthy =
+fun activate_fragment_nonbrittle registration lthy =
   let val n = Local_Theory.level lthy in
     lthy |> Local_Theory.map_contexts (fn level =>
-      level = n - 1 ? Context.proof_map (add_registration dep_morph mixin export))
+      level = n - 1 ? Context.proof_map (add_registration registration))
   end;
 
-fun activate_fragment dep_morph mixin export =
-  Local_Theory.mark_brittle #> activate_fragment_nonbrittle dep_morph mixin export;
+fun activate_fragment registration =
+  Local_Theory.mark_brittle #> activate_fragment_nonbrittle registration;
 
 
 
@@ -590,7 +589,7 @@
   end;
 *)
 
-fun add_dependency loc (name, morph) mixin export thy =
+fun add_dependency loc {dep = (name, morph), mixin, export} thy =
   let
     val serial' = serial ();
     val thy' = thy |>
@@ -601,10 +600,8 @@
     val (_, regs) =
       fold_rev (roundup thy' cons export)
         (registrations_of context' loc) (Idents.get context', []);
-  in
-    thy'
-    |> fold_rev (fn dep => Context.theory_map (add_registration dep NONE export)) regs
-  end;
+    fun add_dep dep = add_registration {dep = dep, mixin = NONE, export = export};
+  in thy' |> fold_rev (Context.theory_map o add_dep) regs end;
 
 
 (*** Storing results ***)