src/Pure/Isar/locale.ML
changeset 32801 6f97a67e8da8
parent 32800 57fcca4e7c0e
child 32804 ca430e6aee1c
     1.1 --- a/src/Pure/Isar/locale.ML	Wed Aug 19 19:35:46 2009 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Sat Sep 19 18:43:11 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 -> theory -> theory
     1.8 +  val amend_registration: morphism * bool -> string * 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 @@ -325,29 +327,93 @@
    1.13  
    1.14  structure Registrations = TheoryDataFun
    1.15  (
    1.16 -  type T = ((string * (morphism * morphism)) * stamp) list;
    1.17 -    (* FIXME mixins need to be stamped *)
    1.18 +  type T = ((string * (morphism * morphism)) * stamp) list *
    1.19      (* registrations, in reverse order of declaration *)
    1.20 -  val empty = [];
    1.21 +    (stamp * ((morphism * bool) * stamp) list) list;
    1.22 +    (* alist of mixin lists, per list mixins in reverse order of declaration *)
    1.23 +  val empty = ([], []);
    1.24    val extend = I;
    1.25    val copy = I;
    1.26 -  fun merge _ data : T = Library.merge (eq_snd op =) data;
    1.27 +  fun merge _ ((r1, m1), (r2, m2)) : T =
    1.28 +    (Library.merge (eq_snd op =) (r1, r2),
    1.29 +      AList.join (op =) (K (Library.merge (eq_snd op =))) (m1, m2));
    1.30      (* FIXME consolidate with dependencies, consider one data slot only *)
    1.31  );
    1.32  
    1.33 -fun reg_morph ((name, (base, export)), _) = (name, base $> export);
    1.34 +
    1.35 +(* Primitive operations *)
    1.36 +
    1.37 +fun compose_mixins mixins =
    1.38 +  fold_rev Morphism.compose (map (fst o fst) mixins) Morphism.identity;
    1.39 +
    1.40 +fun reg_morph mixins ((name, (base, export)), stamp) =
    1.41 +  let val mix = the_default [] (AList.lookup (op =) mixins stamp) |> compose_mixins;
    1.42 +  in (name, base $> mix $> export) end;
    1.43  
    1.44  fun these_registrations thy name = Registrations.get thy
    1.45 -  |> filter (curry (op =) name o fst o fst)
    1.46 -  |> map reg_morph;
    1.47 +  |>> filter (curry (op =) name o fst o fst)
    1.48 +  |-> (fn regs => fn mixins => map (reg_morph mixins) regs);
    1.49  
    1.50  fun all_registrations thy = Registrations.get thy
    1.51 -  |> map reg_morph;
    1.52 +  |-> (fn regs => fn mixins => map (reg_morph mixins) regs);
    1.53 +
    1.54 +fun collect_mixins thy (name, base_morph) = Registrations.get thy
    1.55 +  |>> filter (fn ((name', (morph', _)), _) => ident_eq thy
    1.56 +     ((name, instance_of thy name base_morph), (name', instance_of thy name' morph')))
    1.57 +  |-> (fn regs => fn mixins =>
    1.58 +     fold_rev (fn (_, stamp) => the_default [] (AList.lookup (op =) mixins stamp)
    1.59 +       |> curry (merge (eq_snd op =))) regs []);
    1.60 +
    1.61 +
    1.62 +(* Add and extend registrations *)
    1.63 +
    1.64 +(* Note that a registration that would be subsumed by an existing one will not be
    1.65 +   generated, and it will not be possible to amend it. *)
    1.66 +
    1.67 +fun add_registration (name, base_morph) export thy =
    1.68 +  let
    1.69 +    val base = instance_of thy name base_morph;
    1.70 +  in
    1.71 +    if member (ident_eq thy) (get_idents (Context.Theory thy)) (name, base)
    1.72 +    then thy
    1.73 +    else
    1.74 +      let
    1.75 +        val mixins = roundup thy (fn dep => fn mixins =>
    1.76 +          merge (eq_snd op =) (mixins, collect_mixins thy dep)) (name, base_morph) ([], [])
    1.77 +          |> snd |> filter (snd o fst)  (* only inheritable mixins *);
    1.78 +        val stamp = stamp ();
    1.79 +      in
    1.80 +        thy
    1.81 +        (* add registration and its mixins *)
    1.82 +        |> Registrations.map (apfst (cons ((name, (base_morph, export)), stamp))
    1.83 +          #> apsnd (cons (stamp, mixins)))
    1.84 +        (* activate import hierarchy as far as not already active *)
    1.85 +        |> Context.theory_map (activate_facts (name, base_morph
    1.86 +          $> compose_mixins mixins $> export))
    1.87 +      end
    1.88 +  end;
    1.89 +
    1.90 +fun amend_registration mixin (name, base_morph) thy =
    1.91 +  let
    1.92 +    val regs = Registrations.get thy |> fst;
    1.93 +    val base = instance_of thy name base_morph;
    1.94 +    fun match ((name', (morph', _)), _) =
    1.95 +      name = name' andalso eq_list (op aconv) (base, instance_of thy name' morph');
    1.96 +  in
    1.97 +    case find_first match (rev regs) of
    1.98 +        NONE => error ("No registration of locale " ^
    1.99 +          quote (extern thy name) ^ " and parameter instantiation " ^
   1.100 +          space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
   1.101 +          " available")
   1.102 +      | SOME (_, stamp') => Registrations.map 
   1.103 +          (apsnd (AList.map_default (op =) (stamp', []) (cons (mixin, stamp ())))) thy
   1.104 +    (* FIXME deal with inheritance: propagate to existing children *)
   1.105 +  end;
   1.106  
   1.107  fun amend_registration_legacy morph (name, base_morph) thy =
   1.108    (* legacy, never modify base morphism *)
   1.109    let
   1.110 -    val regs = map #1 (Registrations.get thy);
   1.111 +    val regs = Registrations.get thy |> fst |> map fst;
   1.112      val base = instance_of thy name base_morph;
   1.113      fun match (name', (morph', _)) =
   1.114        name = name' andalso eq_list (op aconv) (base, instance_of thy name' morph');
   1.115 @@ -358,7 +424,7 @@
   1.116          space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^ " available")
   1.117        else ();
   1.118    in
   1.119 -    Registrations.map (nth_map (length regs - 1 - i)
   1.120 +    Registrations.map ((apfst o nth_map (length regs - 1 - i))
   1.121        (fn ((name, (base, export)), stamp) => ((name, (base $> morph, export)), stamp))) thy
   1.122    end;
   1.123  
   1.124 @@ -369,7 +435,7 @@
   1.125    in
   1.126      (get_idents (Context.Theory thy), thy)
   1.127      |> roundup thy (fn (dep', morph') =>
   1.128 -        Registrations.map (cons ((dep', (morph', export)), stamp ()))) (dep, morph)
   1.129 +        Registrations.map (apfst (cons ((dep', (morph', export)), stamp ())))) (dep, morph)
   1.130      |> snd
   1.131      |> Context.theory_map (activate_facts (dep, morph $> export))
   1.132    end;
   1.133 @@ -382,6 +448,7 @@
   1.134    |> (change_locale loc o apsnd) (cons ((dep, morph $> export), stamp ()))
   1.135    |> (fn thy => fold_rev (Context.theory_map o activate_facts)
   1.136        (all_registrations thy) thy);
   1.137 +  (* FIXME deal with inheritance: propagate mixins to new children *)
   1.138  
   1.139  
   1.140  (*** Storing results ***)