src/Pure/Isar/locale.ML
changeset 32804 ca430e6aee1c
parent 32803 fc02b4b9eccc
parent 32801 6f97a67e8da8
child 32845 d2d0b9b1a69d
     1.1 --- a/src/Pure/Isar/locale.ML	Sun Sep 27 11:50:27 2009 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Tue Sep 29 22:15:54 2009 +0200
     1.3 @@ -68,6 +68,8 @@
     1.4    val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
     1.5  
     1.6    (* Registrations and dependencies *)
     1.7 +  val add_registration: string * morphism -> morphism * bool -> morphism -> theory -> theory
     1.8 +  val amend_registration: string * morphism -> morphism * bool -> morphism -> theory -> theory
     1.9    val add_registration_eqs: string * morphism -> thm list -> morphism -> theory -> theory
    1.10    val amend_registration_legacy: morphism -> string * morphism -> theory -> theory
    1.11    val add_dependency: string -> string * morphism -> morphism -> theory -> theory
    1.12 @@ -75,6 +77,7 @@
    1.13    (* Diagnostic *)
    1.14    val print_locales: theory -> unit
    1.15    val print_locale: theory -> bool -> xstring -> unit
    1.16 +  val print_registrations: theory -> string -> unit
    1.17  end;
    1.18  
    1.19  structure Locale: LOCALE =
    1.20 @@ -177,6 +180,7 @@
    1.21  (** Identifiers: activated locales in theory or proof context **)
    1.22  
    1.23  fun ident_eq thy ((n: string, ts), (m, ss)) = (m = n) andalso Pattern.matchess thy (ss, ts);
    1.24 +(* FIXME: this is ident_le, smaller term is more general *)
    1.25  
    1.26  local
    1.27  
    1.28 @@ -234,7 +238,7 @@
    1.29  
    1.30  in
    1.31  
    1.32 -(* Note that while identifiers always have the exported view, activate_dep is
    1.33 +(* Note that while identifiers always have the external (exported) view, activate_dep is
    1.34    is presented with the internal view. *)
    1.35  
    1.36  fun roundup thy activate_dep export (name, morph) (marked, input) =
    1.37 @@ -328,29 +332,158 @@
    1.38  
    1.39  structure Registrations = TheoryDataFun
    1.40  (
    1.41 -  type T = ((string * (morphism * morphism)) * stamp) list;
    1.42 -    (* FIXME mixins need to be stamped *)
    1.43 +  type T = ((string * (morphism * morphism)) * stamp) list *
    1.44      (* registrations, in reverse order of declaration *)
    1.45 -  val empty = [];
    1.46 +    (stamp * ((morphism * bool) * stamp) list) list;
    1.47 +    (* alist of mixin lists, per list mixins in reverse order of declaration *)
    1.48 +  val empty = ([], []);
    1.49    val extend = I;
    1.50    val copy = I;
    1.51 -  fun merge _ data : T = Library.merge (eq_snd op =) data;
    1.52 +  fun merge _ ((r1, m1), (r2, m2)) : T =
    1.53 +    (Library.merge (eq_snd op =) (r1, r2),
    1.54 +      AList.join (op =) (K (Library.merge (eq_snd op =))) (m1, m2));
    1.55      (* FIXME consolidate with dependencies, consider one data slot only *)
    1.56  );
    1.57  
    1.58 -fun reg_morph ((name, (base, export)), _) = (name, base $> export);
    1.59 +
    1.60 +(* Primitive operations *)
    1.61 +
    1.62 +fun compose_mixins mixins =
    1.63 +  fold_rev Morphism.compose (map (fst o fst) mixins) Morphism.identity;
    1.64 +
    1.65 +fun reg_morph mixins ((name, (base, export)), stamp) =
    1.66 +  let val mix = the_default [] (AList.lookup (op =) mixins stamp) |> compose_mixins;
    1.67 +  in (name, base $> mix $> export) end;
    1.68  
    1.69  fun these_registrations thy name = Registrations.get thy
    1.70 -  |> filter (curry (op =) name o fst o fst)
    1.71 -  |> map reg_morph;
    1.72 +  |>> filter (curry (op =) name o fst o fst)
    1.73 +  |-> (fn regs => fn mixins => map (reg_morph mixins) regs);
    1.74  
    1.75  fun all_registrations thy = Registrations.get thy
    1.76 -  |> map reg_morph;
    1.77 +  |-> (fn regs => fn mixins => map (reg_morph mixins) regs);
    1.78 +
    1.79 +fun get_mixins thy (name, morph) =
    1.80 +  let
    1.81 +    val (regs, mixins) = Registrations.get thy;
    1.82 +  in
    1.83 +    case find_first (fn ((name', (morph', export')), _) => ident_eq thy
    1.84 +      ((name', instance_of thy name' (morph' $> export')), (name, instance_of thy name morph))) (rev regs) of
    1.85 +      NONE => []
    1.86 +    | SOME (_, stamp) => the_default [] (AList.lookup (op =) mixins stamp)
    1.87 +  end;
    1.88 +
    1.89 +fun collect_mixins thy (name, morph) =
    1.90 +  roundup thy (fn dep => fn mixins =>
    1.91 +    merge (eq_snd op =) (mixins, get_mixins thy dep)) Morphism.identity (name, morph) ([], [])
    1.92 +  |> snd |> filter (snd o fst);  (* only inheritable mixins *)
    1.93 +
    1.94 +fun activate_notes' activ_elem transfer thy export (name, morph) input =
    1.95 +  let
    1.96 +    val {notes, ...} = the_locale thy name;
    1.97 +    fun activate ((kind, facts), _) input =
    1.98 +      let
    1.99 +        val mixin = collect_mixins thy (name, morph $> export) |> compose_mixins;
   1.100 +        val facts' = facts |> Element.facts_map (Element.morph_ctxt (transfer input $> morph $> mixin $> export))
   1.101 +      in activ_elem (Notes (kind, facts')) input end;
   1.102 +  in
   1.103 +    fold_rev activate notes input
   1.104 +  end;
   1.105 +
   1.106 +fun activate_facts' export dep context =
   1.107 +  let
   1.108 +    val thy = Context.theory_of context;
   1.109 +    val activate = activate_notes' Element.init (Element.transfer_morphism o Context.theory_of) thy export;
   1.110 +  in roundup thy activate export dep (get_idents context, context) |-> put_idents end;
   1.111 +
   1.112 +
   1.113 +(* Diagnostic *)
   1.114 +
   1.115 +fun print_registrations thy raw_name =
   1.116 +  let
   1.117 +    val name = intern thy raw_name;
   1.118 +    val name' = extern thy name;
   1.119 +    val ctxt = ProofContext.init thy;
   1.120 +    fun prt_qual (qual, mand) = Pretty.str (qual ^ (if mand then "!" else "?"));
   1.121 +    fun prt_quals qs = Pretty.separate "." (map prt_qual qs) |> Pretty.block;
   1.122 +    val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
   1.123 +    fun prt_term' t = if !show_types
   1.124 +      then Pretty.block [prt_term t, Pretty.brk 1, Pretty.str "::",
   1.125 +        Pretty.brk 1, (Pretty.quote o Syntax.pretty_typ ctxt) (type_of t)]
   1.126 +      else prt_term t;
   1.127 +    fun prt_inst ts =
   1.128 +      Pretty.block (Pretty.breaks (Pretty.str name' :: map prt_term' ts));
   1.129 +    fun prt_reg (name, morph) =
   1.130 +      let
   1.131 +        val qs = Binding.name "x" |> Morphism.binding morph |> Binding.prefix_of;
   1.132 +        val ts = instance_of thy name morph;
   1.133 +      in
   1.134 +        case qs of
   1.135 +           [] => prt_inst ts
   1.136 +         | qs => Pretty.block [prt_quals qs, Pretty.brk 1, Pretty.str ":",
   1.137 +             Pretty.brk 1, prt_inst ts]
   1.138 +      end;
   1.139 +  in
   1.140 +    (case these_registrations thy name of
   1.141 +        [] => Pretty.str ("no interpretations")
   1.142 +      | regs => Pretty.big_list "interpretations:" (map prt_reg regs))
   1.143 +    |> Pretty.writeln
   1.144 +  end;
   1.145 +
   1.146 +
   1.147 +(* Add and extend registrations *)
   1.148 +
   1.149 +fun amend_registration (name, morph) mixin export thy =
   1.150 +  let
   1.151 +    val regs = Registrations.get thy |> fst;
   1.152 +    val base = instance_of thy name (morph $> export);
   1.153 +    fun match ((name', (morph', export')), _) =
   1.154 +      name = name' andalso eq_list (op aconv) (base, instance_of thy name' (morph' $> export'));
   1.155 +  in
   1.156 +    case find_first match (rev regs) of
   1.157 +        NONE => error ("No interpretation of locale " ^
   1.158 +          quote (extern thy name) ^ " and\nparameter instantiation " ^
   1.159 +          space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
   1.160 +          " available")
   1.161 +      | SOME (_, stamp') => Registrations.map 
   1.162 +          (apsnd (AList.map_default (op =) (stamp', []) (cons (mixin, stamp ())))) thy
   1.163 +    (* FIXME deal with inheritance: propagate to existing children *)
   1.164 +  end;
   1.165 +
   1.166 +(* Note that a registration that would be subsumed by an existing one will not be
   1.167 +   generated, and it will not be possible to amend it. *)
   1.168 +
   1.169 +fun add_registration (name, base_morph) mixin export thy =
   1.170 +  let
   1.171 +    val base = instance_of thy name base_morph;
   1.172 +  in
   1.173 +    if member (ident_eq thy) (get_idents (Context.Theory thy)) (name, base)
   1.174 +    then thy
   1.175 +    else
   1.176 +      let
   1.177 +        fun add_reg (dep', morph') =
   1.178 +          let
   1.179 +            val mixins = collect_mixins thy (dep', morph' $> export);
   1.180 +            val stamp = stamp ();
   1.181 +          in
   1.182 +            Registrations.map (apfst (cons ((dep', (morph', export)), stamp))
   1.183 +              #> apsnd (cons (stamp, mixins)))
   1.184 +          end
   1.185 +      in
   1.186 +        (get_idents (Context.Theory thy), thy)
   1.187 +        (* add new registrations with inherited mixins *)
   1.188 +        |> roundup thy add_reg export (name, base_morph)
   1.189 +        |> snd
   1.190 +        (* add mixin *)
   1.191 +        |> amend_registration (name, base_morph) mixin export
   1.192 +        (* activate import hierarchy as far as not already active *)
   1.193 +        |> Context.theory_map (activate_facts' export (name, base_morph))
   1.194 +      end
   1.195 +  end;
   1.196  
   1.197  fun amend_registration_legacy morph (name, base_morph) thy =
   1.198    (* legacy, never modify base morphism *)
   1.199    let
   1.200 -    val regs = map #1 (Registrations.get thy);
   1.201 +    val regs = Registrations.get thy |> fst |> map fst;
   1.202      val base = instance_of thy name base_morph;
   1.203      fun match (name', (morph', _)) =
   1.204        name = name' andalso eq_list (op aconv) (base, instance_of thy name' morph');
   1.205 @@ -361,7 +494,7 @@
   1.206          space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^ " available")
   1.207        else ();
   1.208    in
   1.209 -    Registrations.map (nth_map (length regs - 1 - i)
   1.210 +    Registrations.map ((apfst o nth_map (length regs - 1 - i))
   1.211        (fn ((name, (base, export)), stamp) => ((name, (base $> morph, export)), stamp))) thy
   1.212    end;
   1.213  
   1.214 @@ -372,7 +505,7 @@
   1.215    in
   1.216      (get_idents (Context.Theory thy), thy)
   1.217      |> roundup thy (fn (dep', morph') =>
   1.218 -        Registrations.map (cons ((dep', (morph', export)), stamp ()))) export (dep, morph)
   1.219 +        Registrations.map (apfst (cons ((dep', (morph', export)), stamp ())))) export (dep, morph)
   1.220      |> snd
   1.221      |> Context.theory_map (activate_facts (dep, morph $> export))
   1.222    end;
   1.223 @@ -383,8 +516,9 @@
   1.224  fun add_dependency loc (dep, morph) export thy =
   1.225    thy
   1.226    |> (change_locale loc o apsnd) (cons ((dep, morph $> export), stamp ()))
   1.227 -  |> (fn thy => fold_rev (Context.theory_map o activate_facts)
   1.228 +  |> (fn thy => fold_rev (Context.theory_map o activate_facts' export)
   1.229        (all_registrations thy) thy);
   1.230 +  (* FIXME deal with inheritance: propagate mixins to new children *)
   1.231  
   1.232  
   1.233  (*** Storing results ***)