clarified signature: explicit type Locale.registration;
authorwenzelm
Thu Aug 30 13:38:52 2018 +0200 (13 months ago)
changeset 688516c9825c1e26b
parent 68850 6d2735ca0271
child 68852 becaeaa334ae
clarified signature: explicit type Locale.registration;
src/Pure/Isar/class.ML
src/Pure/Isar/class_declaration.ML
src/Pure/Isar/generic_target.ML
src/Pure/Isar/interpretation.ML
src/Pure/Isar/local_theory.ML
src/Pure/Isar/locale.ML
     1.1 --- a/src/Pure/Isar/class.ML	Thu Aug 30 12:36:26 2018 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Thu Aug 30 13:38:52 2018 +0200
     1.3 @@ -229,9 +229,13 @@
     1.4  
     1.5  fun activate_defs class thms thy =
     1.6    (case Element.eq_morphism thy thms of
     1.7 -    SOME eq_morph => fold (fn cls => fn thy =>
     1.8 -      Context.theory_map (Locale.amend_registration (cls, base_morphism thy cls)
     1.9 -        (eq_morph, true) (export_morphism thy cls)) thy) (heritage thy [class]) thy
    1.10 +    SOME eq_morph =>
    1.11 +      fold (fn cls => fn thy =>
    1.12 +        Context.theory_map
    1.13 +          (Locale.amend_registration
    1.14 +            {dep = (cls, base_morphism thy cls),
    1.15 +              mixin = SOME (eq_morph, true),
    1.16 +              export = export_morphism thy cls}) thy) (heritage thy [class]) thy
    1.17    | NONE => thy);
    1.18  
    1.19  fun register_operation class (c, t) input_only thy =
    1.20 @@ -484,10 +488,13 @@
    1.21      val diff_sort = Sign.complete_sort thy [sup]
    1.22        |> subtract (op =) (Sign.complete_sort thy [sub])
    1.23        |> filter (is_class thy);
    1.24 -    fun add_dependency some_wit = case some_dep_morph of
    1.25 -        SOME dep_morph => Generic_Target.locale_dependency sub
    1.26 -          (sup, dep_morph $> Element.satisfy_morphism (the_list some_witn)) NONE export
    1.27 -      | NONE => I;
    1.28 +    fun add_dependency some_wit (* FIXME unused!? *) =
    1.29 +      (case some_dep_morph of
    1.30 +        SOME dep_morph =>
    1.31 +          Generic_Target.locale_dependency sub
    1.32 +            {dep = (sup, dep_morph $> Element.satisfy_morphism (the_list some_witn)),
    1.33 +              mixin = NONE, export = export}
    1.34 +      | NONE => I);
    1.35    in
    1.36      lthy
    1.37      |> Local_Theory.raw_theory
     2.1 --- a/src/Pure/Isar/class_declaration.ML	Thu Aug 30 12:36:26 2018 +0200
     2.2 +++ b/src/Pure/Isar/class_declaration.ML	Thu Aug 30 13:38:52 2018 +0200
     2.3 @@ -328,8 +328,10 @@
     2.4      |-> (fn (param_map, params, assm_axiom) =>
     2.5         `(fn thy => calculate thy class sups base_sort param_map assm_axiom)
     2.6      #-> (fn (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) =>
     2.7 -       Context.theory_map (Locale.add_registration (class, base_morph)
     2.8 -         (Option.map (rpair true) eq_morph) export_morph)
     2.9 +       Context.theory_map (Locale.add_registration
    2.10 +         {dep = (class, base_morph),
    2.11 +           mixin = Option.map (rpair true) eq_morph,
    2.12 +           export = export_morph})
    2.13      #> Class.register class sups params base_sort base_morph export_morph some_axiom some_assm_intro of_class
    2.14      #> Global_Theory.store_thm (prefix (Binding.qualified_name (class ^ ".of_class.intro")), of_class)))
    2.15      |> snd
     3.1 --- a/src/Pure/Isar/generic_target.ML	Thu Aug 30 12:36:26 2018 +0200
     3.2 +++ b/src/Pure/Isar/generic_target.ML	Thu Aug 30 13:38:52 2018 +0200
     3.3 @@ -52,8 +52,7 @@
     3.4    val theory_abbrev: Syntax.mode -> (binding * mixfix) * term ->
     3.5      local_theory -> (term * term) * local_theory
     3.6    val theory_declaration: declaration -> local_theory -> local_theory
     3.7 -  val theory_registration: string * morphism -> (morphism * bool) option -> morphism ->
     3.8 -    local_theory -> local_theory
     3.9 +  val theory_registration: Locale.registration -> local_theory -> local_theory
    3.10  
    3.11    (*locale target primitives*)
    3.12    val locale_target_notes: string -> string -> Attrib.fact list -> Attrib.fact list ->
    3.13 @@ -71,8 +70,7 @@
    3.14      local_theory -> local_theory
    3.15    val locale_const: string -> Syntax.mode -> (binding * mixfix) * term ->
    3.16      local_theory -> local_theory
    3.17 -  val locale_dependency: string -> string * morphism -> (morphism * bool) option -> morphism ->
    3.18 -    local_theory -> local_theory
    3.19 +  val locale_dependency: string -> Locale.registration -> local_theory -> local_theory
    3.20  
    3.21    (*initialisation*)
    3.22    val init: {background_naming: Name_Space.naming, setup: theory -> Proof.context,
    3.23 @@ -372,7 +370,7 @@
    3.24    background_declaration decl #> standard_declaration (K true) decl;
    3.25  
    3.26  val theory_registration =
    3.27 -  Local_Theory.raw_theory o Context.theory_map ooo Locale.add_registration;
    3.28 +  Local_Theory.raw_theory o Context.theory_map o Locale.add_registration;
    3.29  
    3.30  
    3.31  
    3.32 @@ -406,9 +404,9 @@
    3.33    locale_target_const locale (K true) prmode ((b, mx), rhs)
    3.34    #> standard_const (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, mx), rhs);
    3.35  
    3.36 -fun locale_dependency locale dep_morph mixin export =
    3.37 -  (Local_Theory.raw_theory ooo Locale.add_dependency locale) dep_morph mixin export
    3.38 -  #> Locale.activate_fragment_nonbrittle dep_morph mixin export;
    3.39 +fun locale_dependency locale registration =
    3.40 +  Local_Theory.raw_theory (Locale.add_dependency locale registration)
    3.41 +  #> Locale.activate_fragment_nonbrittle registration;
    3.42  
    3.43  
    3.44  (** locale abbreviations **)
     4.1 --- a/src/Pure/Isar/interpretation.ML	Thu Aug 30 12:36:26 2018 +0200
     4.2 +++ b/src/Pure/Isar/interpretation.ML	Thu Aug 30 13:38:52 2018 +0200
     4.3 @@ -119,9 +119,12 @@
     4.4            $> Morphism.binding_morphism "position" (Binding.set_pos pos)
     4.5          in (dep, morph') end) deps witss;
     4.6      fun register (dep_morph, eqns) ctxt =
     4.7 -      add_registration dep_morph
     4.8 -        (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) (eqns @ eqns')))
     4.9 -        export ctxt;
    4.10 +      ctxt |> add_registration
    4.11 +        {dep = dep_morph,
    4.12 +          mixin =
    4.13 +            Option.map (rpair true)
    4.14 +              (Element.eq_morphism (Proof_Context.theory_of ctxt) (eqns @ eqns')),
    4.15 +          export = export};
    4.16    in ctxt'' |> fold register (dep_morphs ~~ eqnss') end;
    4.17  
    4.18  in
    4.19 @@ -150,9 +153,9 @@
    4.20      (fn witss => fn eqns => Proof.map_context (after_qed witss eqns) #> Proof.reset_facts)
    4.21      "interpret" propss eqns goal_ctxt state;
    4.22  
    4.23 -fun add_registration reg mixin export ctxt = ctxt
    4.24 +fun add_registration registration ctxt = ctxt
    4.25    |> Proof_Context.set_stmt false
    4.26 -  |> Context.proof_map (Locale.add_registration reg mixin export)
    4.27 +  |> Context.proof_map (Locale.add_registration registration)
    4.28    |> Proof_Context.restore_stmt ctxt;
    4.29  
    4.30  fun gen_interpret prep_interpretation expression state =
     5.1 --- a/src/Pure/Isar/local_theory.ML	Thu Aug 30 12:36:26 2018 +0200
     5.2 +++ b/src/Pure/Isar/local_theory.ML	Thu Aug 30 13:38:52 2018 +0200
     5.3 @@ -14,6 +14,11 @@
     5.4    type fact = binding * thms;
     5.5  end;
     5.6  
     5.7 +structure Locale =
     5.8 +struct
     5.9 +  type registration = {dep: string * morphism, mixin: (morphism * bool) option, export: morphism};
    5.10 +end;
    5.11 +
    5.12  signature LOCAL_THEORY =
    5.13  sig
    5.14    type operations
    5.15 @@ -54,10 +59,8 @@
    5.16    val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
    5.17      (term * term) * local_theory
    5.18    val declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory
    5.19 -  val theory_registration: string * morphism -> (morphism * bool) option -> morphism ->
    5.20 -    local_theory -> local_theory
    5.21 -  val locale_dependency: string * morphism -> (morphism * bool) option -> morphism ->
    5.22 -    local_theory -> local_theory
    5.23 +  val theory_registration: Locale.registration -> local_theory -> local_theory
    5.24 +  val locale_dependency: Locale.registration -> local_theory -> local_theory
    5.25    val pretty: local_theory -> Pretty.T list
    5.26    val add_thms_dynamic: binding * (Context.generic -> thm list) -> local_theory -> local_theory
    5.27    val set_defsort: sort -> local_theory -> local_theory
    5.28 @@ -91,10 +94,8 @@
    5.29    abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
    5.30      (term * term) * local_theory,
    5.31    declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory,
    5.32 -  theory_registration: string * morphism -> (morphism * bool) option -> morphism ->
    5.33 -     local_theory -> local_theory,
    5.34 -  locale_dependency: string * morphism -> (morphism * bool) option -> morphism ->
    5.35 -     local_theory -> local_theory,
    5.36 +  theory_registration: Locale.registration -> local_theory -> local_theory,
    5.37 +  locale_dependency: Locale.registration -> local_theory -> local_theory,
    5.38    pretty: local_theory -> Pretty.T list};
    5.39  
    5.40  type lthy =
    5.41 @@ -276,10 +277,10 @@
    5.42  val define_internal = operation2 #define true;
    5.43  val notes_kind = operation2 #notes;
    5.44  val declaration = operation2 #declaration;
    5.45 -fun theory_registration dep_morph mixin export =
    5.46 -  assert_bottom #> operation (fn ops => #theory_registration ops dep_morph mixin export);
    5.47 -fun locale_dependency dep_morph mixin export =
    5.48 -  assert_bottom #> operation (fn ops => #locale_dependency ops dep_morph mixin export);
    5.49 +fun theory_registration registration =
    5.50 +  assert_bottom #> operation (fn ops => #theory_registration ops registration);
    5.51 +fun locale_dependency registration =
    5.52 +  assert_bottom #> operation (fn ops => #locale_dependency ops registration);
    5.53  
    5.54  
    5.55  (* theorems *)
     6.1 --- a/src/Pure/Isar/locale.ML	Thu Aug 30 12:36:26 2018 +0200
     6.2 +++ b/src/Pure/Isar/locale.ML	Thu Aug 30 13:38:52 2018 +0200
     6.3 @@ -73,17 +73,13 @@
     6.4    val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
     6.5  
     6.6    (* Registrations and dependencies *)
     6.7 -  val add_registration: string * morphism -> (morphism * bool) option ->
     6.8 -    morphism -> Context.generic -> Context.generic
     6.9 -  val activate_fragment: string * morphism -> (morphism * bool) option -> morphism ->
    6.10 -    local_theory -> local_theory
    6.11 -  val activate_fragment_nonbrittle: string * morphism -> (morphism * bool) option -> morphism ->
    6.12 -    local_theory -> local_theory
    6.13 -  val amend_registration: string * morphism -> morphism * bool ->
    6.14 -    morphism -> Context.generic -> Context.generic
    6.15 +  type registration = {dep: string * morphism, mixin: (morphism * bool) option, export: morphism}
    6.16 +  val amend_registration: registration -> Context.generic -> Context.generic
    6.17 +  val add_registration: registration -> Context.generic -> Context.generic
    6.18 +  val activate_fragment: registration -> local_theory -> local_theory
    6.19 +  val activate_fragment_nonbrittle: registration -> local_theory -> local_theory
    6.20    val registrations_of: Context.generic -> string -> (string * morphism) list
    6.21 -  val add_dependency: string -> string * morphism -> (morphism * bool) option ->
    6.22 -    morphism -> theory -> theory
    6.23 +  val add_dependency: string -> registration -> theory -> theory
    6.24  
    6.25    (* Diagnostic *)
    6.26    val hyp_spec_of: theory -> string -> Element.context_i list
    6.27 @@ -516,29 +512,32 @@
    6.28  
    6.29  (*** Add and extend registrations ***)
    6.30  
    6.31 -fun amend_registration (name, morph) mixin export context =
    6.32 -  let
    6.33 -    val thy = Context.theory_of context;
    6.34 -    val ctxt = Context.proof_of context;
    6.35 +type registration = Locale.registration;
    6.36 +
    6.37 +fun amend_registration {mixin = NONE, ...} context = context
    6.38 +  | amend_registration {dep = (name, morph), mixin = SOME mixin, export} context =
    6.39 +      let
    6.40 +        val thy = Context.theory_of context;
    6.41 +        val ctxt = Context.proof_of context;
    6.42  
    6.43 -    val regs = Registrations.get context |> fst;
    6.44 -    val base = instance_of thy name (morph $> export);
    6.45 -    val serial' =
    6.46 -      (case Idtab.lookup regs (name, base) of
    6.47 -        NONE =>
    6.48 -          error ("No interpretation of locale " ^ quote (markup_name ctxt name) ^
    6.49 -            " with\nparameter instantiation " ^
    6.50 -            space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
    6.51 -            " available")
    6.52 -      | SOME (_, serial') => serial');
    6.53 -  in
    6.54 -    add_mixin serial' mixin context
    6.55 -  end;
    6.56 +        val regs = Registrations.get context |> fst;
    6.57 +        val base = instance_of thy name (morph $> export);
    6.58 +        val serial' =
    6.59 +          (case Idtab.lookup regs (name, base) of
    6.60 +            NONE =>
    6.61 +              error ("No interpretation of locale " ^ quote (markup_name ctxt name) ^
    6.62 +                " with\nparameter instantiation " ^
    6.63 +                space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
    6.64 +                " available")
    6.65 +          | SOME (_, serial') => serial');
    6.66 +      in
    6.67 +        add_mixin serial' mixin context
    6.68 +      end;
    6.69  
    6.70  (* Note that a registration that would be subsumed by an existing one will not be
    6.71     generated, and it will not be possible to amend it. *)
    6.72  
    6.73 -fun add_registration (name, base_morph) mixin export context =
    6.74 +fun add_registration {dep = (name, base_morph), mixin, export} context =
    6.75    let
    6.76      val thy = Context.theory_of context;
    6.77      val mix = (case mixin of NONE => Morphism.identity | SOME (mix, _) => mix);
    6.78 @@ -554,7 +553,7 @@
    6.79        |> roundup thy (add_reg thy export) export (name, morph)
    6.80        |> snd
    6.81        (* add mixin *)
    6.82 -      |> (case mixin of NONE => I | SOME mixin => amend_registration (name, morph) mixin export)
    6.83 +      |> amend_registration {dep = (name, morph), mixin = mixin, export = export}
    6.84        (* activate import hierarchy as far as not already active *)
    6.85        |> activate_facts (SOME export) (name, morph)
    6.86    end;
    6.87 @@ -562,14 +561,14 @@
    6.88  
    6.89  (* locale fragments within local theory *)
    6.90  
    6.91 -fun activate_fragment_nonbrittle dep_morph mixin export lthy =
    6.92 +fun activate_fragment_nonbrittle registration lthy =
    6.93    let val n = Local_Theory.level lthy in
    6.94      lthy |> Local_Theory.map_contexts (fn level =>
    6.95 -      level = n - 1 ? Context.proof_map (add_registration dep_morph mixin export))
    6.96 +      level = n - 1 ? Context.proof_map (add_registration registration))
    6.97    end;
    6.98  
    6.99 -fun activate_fragment dep_morph mixin export =
   6.100 -  Local_Theory.mark_brittle #> activate_fragment_nonbrittle dep_morph mixin export;
   6.101 +fun activate_fragment registration =
   6.102 +  Local_Theory.mark_brittle #> activate_fragment_nonbrittle registration;
   6.103  
   6.104  
   6.105  
   6.106 @@ -590,7 +589,7 @@
   6.107    end;
   6.108  *)
   6.109  
   6.110 -fun add_dependency loc (name, morph) mixin export thy =
   6.111 +fun add_dependency loc {dep = (name, morph), mixin, export} thy =
   6.112    let
   6.113      val serial' = serial ();
   6.114      val thy' = thy |>
   6.115 @@ -601,10 +600,8 @@
   6.116      val (_, regs) =
   6.117        fold_rev (roundup thy' cons export)
   6.118          (registrations_of context' loc) (Idents.get context', []);
   6.119 -  in
   6.120 -    thy'
   6.121 -    |> fold_rev (fn dep => Context.theory_map (add_registration dep NONE export)) regs
   6.122 -  end;
   6.123 +    fun add_dep dep = add_registration {dep = dep, mixin = NONE, export = export};
   6.124 +  in thy' |> fold_rev (Context.theory_map o add_dep) regs end;
   6.125  
   6.126  
   6.127  (*** Storing results ***)