src/Pure/Isar/locale.ML
changeset 37105 e464f84f3680
parent 37104 3877a6c45d57
child 37133 1d048c6940c8
     1.1 --- a/src/Pure/Isar/locale.ML	Mon May 24 10:48:32 2010 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Mon May 24 10:48:32 2010 +0200
     1.3 @@ -175,8 +175,15 @@
     1.4  
     1.5  (** Identifiers: activated locales in theory or proof context **)
     1.6  
     1.7 -fun ident_eq ((n: string, ts), (m, ss)) = (m = n) andalso eq_list (op aconv) (ts, ss);
     1.8 +(* subsumption *)
     1.9  fun ident_le thy ((n: string, ts), (m, ss)) = (m = n) andalso Pattern.matchess thy (ss, ts);
    1.10 +  (* smaller term is more general *)
    1.11 +
    1.12 +(* total order *)
    1.13 +fun ident_ord ((n: string, ts), (m, ss)) =
    1.14 +  case fast_string_ord (m, n) of
    1.15 +      EQUAL => list_ord Term_Ord.fast_term_ord (ts, ss)
    1.16 +    | ord => ord;
    1.17  
    1.18  local
    1.19  
    1.20 @@ -328,20 +335,22 @@
    1.21  
    1.22  (*** Registrations: interpretations in theories ***)
    1.23  
    1.24 +structure Idtab = Table(type key = string * term list val ord = ident_ord);
    1.25 +
    1.26  structure Registrations = Theory_Data
    1.27  (
    1.28 -  type T = (((string * term list) * (morphism * morphism)) * serial) list *
    1.29 -    (* registrations, in reverse order of declaration;
    1.30 +  type T = ((morphism * morphism) * serial) Idtab.table *
    1.31 +    (* registrations, indexed by locale name and instance;
    1.32         serial points to mixin list *)
    1.33 -    (serial * ((morphism * bool) * serial) list) list;
    1.34 -    (* alist of mixin lists, per list mixins in reverse order of declaration;
    1.35 +    (((morphism * bool) * serial) list) Inttab.table;
    1.36 +    (* table of mixin lists, per list mixins in reverse order of declaration;
    1.37         lists indexed by registration serial,
    1.38         entries for empty lists may be omitted *)
    1.39 -  val empty = ([], []);
    1.40 +  val empty = (Idtab.empty, Inttab.empty);
    1.41    val extend = I;
    1.42    fun merge ((r1, m1), (r2, m2)) : T =
    1.43 -    (Library.merge (eq_snd op =) (r1, r2),
    1.44 -      AList.join (op =) (K (Library.merge (eq_snd op =))) (m1, m2));
    1.45 +    (Idtab.join (K (fst)) (r1, r2), (* pick left registration, FIXME? *)
    1.46 +      Inttab.join (K (Library.merge (eq_snd op =))) (m1, m2));
    1.47      (* FIXME consolidate with dependencies, consider one data slot only *)
    1.48  );
    1.49  
    1.50 @@ -349,20 +358,20 @@
    1.51  (* Primitive operations *)
    1.52  
    1.53  fun add_reg thy export (name, morph) =
    1.54 -  Registrations.map (apfst (cons (((name, instance_of thy name (morph $> export)), (morph, export)), serial ())));
    1.55 +  Registrations.map (apfst (Idtab.insert (K false)
    1.56 +    ((name, instance_of thy name (morph $> export)), ((morph, export), serial ()))));
    1.57  
    1.58  fun add_mixin serial' mixin =
    1.59    (* registration to be amended identified by its serial id *)
    1.60 -  Registrations.map (apsnd (AList.map_default (op =) (serial', []) (cons (mixin, serial ()))));
    1.61 +  Registrations.map (apsnd (Inttab.map_default (serial', []) (cons (mixin, serial ()))));
    1.62  
    1.63  fun get_mixins thy (name, morph) =
    1.64    let
    1.65      val (regs, mixins) = Registrations.get thy;
    1.66    in
    1.67 -    case find_first (fn (((name', inst'), (morph', export')), _) => ident_eq
    1.68 -      ((name', inst'), (name, instance_of thy name morph))) (rev regs) of
    1.69 +    case Idtab.lookup regs (name, instance_of thy name morph) of
    1.70        NONE => []
    1.71 -    | SOME (_, serial) => the_default [] (AList.lookup (op =) mixins serial)
    1.72 +    | SOME (_, serial) => the_default [] (Inttab.lookup mixins serial)
    1.73    end;
    1.74  
    1.75  fun collect_mixins thy (name, morph) =
    1.76 @@ -379,14 +388,16 @@
    1.77    in (name, base $> mix $> export) end;
    1.78  
    1.79  fun these_registrations thy name = Registrations.get thy
    1.80 -  |>> filter (curry (op =) name o fst o fst o fst)
    1.81 +  |>> Idtab.dest
    1.82 +  |>> filter (curry (op =) name o fst o fst)
    1.83    (* with inherited mixins *)
    1.84 -  |-> (fn regs => fn _ => map (fn (((name, _), (base, export)) ,_) =>
    1.85 +  |-> (fn regs => fn _ => map (fn ((name, _), ((base, export) ,_)) =>
    1.86      (name, base $> (collect_mixins thy (name, base $> export) |> compose_mixins) $> export)) regs);
    1.87  
    1.88  fun all_registrations thy = Registrations.get thy (* FIXME clone *)
    1.89 +  |>> Idtab.dest
    1.90    (* with inherited mixins *)
    1.91 -  |-> (fn regs => fn _ => map (fn (((name, _), (base, export)) ,_) =>
    1.92 +  |-> (fn regs => fn _ => map (fn ((name, _), ((base, export) ,_)) =>
    1.93      (name, base $> (collect_mixins thy (name, base $> export) |> compose_mixins) $> export)) regs);
    1.94  
    1.95  fun activate_notes' activ_elem transfer thy export (name, morph) input =
    1.96 @@ -446,9 +457,8 @@
    1.97    let
    1.98      val regs = Registrations.get thy |> fst;
    1.99      val base = instance_of thy name (morph $> export);
   1.100 -    fun match (((name', inst'), _), _) = ident_eq ((name, base), (name', inst'));
   1.101    in
   1.102 -    case find_first match (rev regs) of
   1.103 +    case Idtab.lookup regs (name, base) of
   1.104          NONE => error ("No interpretation of locale " ^
   1.105            quote (extern thy name) ^ " and\nparameter instantiation " ^
   1.106            space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^