src/Pure/Isar/locale.ML
author ballarin
Sat, 31 Jul 2010 21:14:20 +0200
changeset 38107 3a46cebd7983
parent 37973 2b4ff2518ebf
child 38109 06fd1914b902
permissions -rw-r--r--
Make registrations generic data.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
     1
(*  Title:      Pure/Isar/locale.ML
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
     2
    Author:     Clemens Ballarin, TU Muenchen
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
     3
30725
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
     4
Locales -- managed Isar proof contexts, based on Pure predicates.
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
     5
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
     6
Draws basic ideas from Florian Kammueller's original version of
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
     7
locales, but uses the richer infrastructure of Isar instead of the raw
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
     8
meta-logic.  Furthermore, structured import of contexts (with merge
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
     9
and rename operations) are provided, as well as type-inference of the
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    10
signature parts, and predicate definitions of the specification text.
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    11
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    12
Interpretation enables the reuse of theorems of locales in other
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    13
contexts, namely those defined by theories, structured proofs and
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    14
locales themselves.
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    15
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    16
See also:
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    17
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    18
[1] Clemens Ballarin. Locales and Locale Expressions in Isabelle/Isar.
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    19
    In Stefano Berardi et al., Types for Proofs and Programs: International
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    20
    Workshop, TYPES 2003, Torino, Italy, LNCS 3085, pages 34-50, 2004.
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    21
[2] Clemens Ballarin. Interpretation of Locales in Isabelle: Managing
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    22
    Dependencies between Locales. Technical Report TUM-I0607, Technische
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    23
    Universitaet Muenchen, 2006.
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    24
[3] Clemens Ballarin. Interpretation of Locales in Isabelle: Theories and
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    25
    Proof Contexts. In J.M. Borwein and W.M. Farmer, MKM 2006, LNAI 4108,
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    26
    pages 31-43, 2006.
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    27
*)
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    28
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    29
signature LOCALE =
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    30
sig
29576
669b560fc2b9 wrecked old locale package and related modules
haftmann
parents: 29544
diff changeset
    31
  (* Locale specification *)
30344
10a67c5ddddb more uniform handling of binding in targets and derived elements;
wenzelm
parents: 30223
diff changeset
    32
  val register_locale: binding ->
30755
7ef503d216c2 simplified internal locale parameters: maintain proper name and type, instead of binding and constraint;
wenzelm
parents: 30754
diff changeset
    33
    (string * sort) list * ((string * typ) * mixfix) list ->
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    34
    term option * term list ->
29441
28d7d7572b81 explicit bookkeeping of intro rules and axiom
haftmann
parents: 29392
diff changeset
    35
    thm option * thm option -> thm list ->
35798
fd1bb29f8170 replaced type_syntax/term_syntax by uniform syntax_declaration;
wenzelm
parents: 33643
diff changeset
    36
    declaration list ->
30725
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
    37
    (string * (Attrib.binding * (thm list * Attrib.src list) list) list) list ->
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
    38
    (string * morphism) list -> theory -> theory
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    39
  val intern: theory -> xstring -> string
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    40
  val extern: theory -> string -> xstring
29392
aa3a30b625d1 tuned signature; internal code reorganisation
haftmann
parents: 29363
diff changeset
    41
  val defined: theory -> string -> bool
30755
7ef503d216c2 simplified internal locale parameters: maintain proper name and type, instead of binding and constraint;
wenzelm
parents: 30754
diff changeset
    42
  val params_of: theory -> string -> ((string * typ) * mixfix) list
29441
28d7d7572b81 explicit bookkeeping of intro rules and axiom
haftmann
parents: 29392
diff changeset
    43
  val intros_of: theory -> string -> thm option * thm option
28d7d7572b81 explicit bookkeeping of intro rules and axiom
haftmann
parents: 29392
diff changeset
    44
  val axioms_of: theory -> string -> thm list
29544
bc50244cd1d7 exported depedencies; tuned signature
haftmann
parents: 29502
diff changeset
    45
  val instance_of: theory -> string -> morphism -> term list
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    46
  val specification_of: theory -> string -> term option * term list
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    47
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    48
  (* Storing results *)
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    49
  val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    50
    Proof.context -> Proof.context
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    51
  val add_declaration: string -> declaration -> Proof.context -> Proof.context
35798
fd1bb29f8170 replaced type_syntax/term_syntax by uniform syntax_declaration;
wenzelm
parents: 33643
diff changeset
    52
  val add_syntax_declaration: string -> declaration -> Proof.context -> Proof.context
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    53
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    54
  (* Activation *)
30764
3e3e7aa0cc7a simplified Locale.activate operations, using generic context;
wenzelm
parents: 30763
diff changeset
    55
  val activate_declarations: string * morphism -> Proof.context -> Proof.context
3e3e7aa0cc7a simplified Locale.activate operations, using generic context;
wenzelm
parents: 30763
diff changeset
    56
  val activate_facts: string * morphism -> Context.generic -> Context.generic
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    57
  val init: string -> theory -> Proof.context
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    58
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    59
  (* Reasoning about locales *)
30725
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
    60
  val get_witnesses: Proof.context -> thm list
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
    61
  val get_intros: Proof.context -> thm list
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
    62
  val get_unfolds: Proof.context -> thm list
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
    63
  val witness_add: attribute
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
    64
  val intro_add: attribute
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
    65
  val unfold_add: attribute
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    66
  val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    67
31988
801aabf9f376 tuned locale interface
haftmann
parents: 30777
diff changeset
    68
  (* Registrations and dependencies *)
32845
d2d0b9b1a69d Avoid administrative overhead for identity mixins.
ballarin
parents: 32804
diff changeset
    69
  val add_registration: string * morphism -> (morphism * bool) option ->
38107
3a46cebd7983 Make registrations generic data.
ballarin
parents: 37973
diff changeset
    70
    morphism -> Context.generic -> Context.generic
32845
d2d0b9b1a69d Avoid administrative overhead for identity mixins.
ballarin
parents: 32804
diff changeset
    71
  val amend_registration: string * morphism -> morphism * bool ->
38107
3a46cebd7983 Make registrations generic data.
ballarin
parents: 37973
diff changeset
    72
    morphism -> Context.generic -> Context.generic
3a46cebd7983 Make registrations generic data.
ballarin
parents: 37973
diff changeset
    73
  val registrations_of_locale: Context.generic -> string -> (string * morphism) list
32074
76d6ba08a05f simplification of locale interfaces
haftmann
parents: 31988
diff changeset
    74
  val add_dependency: string -> string * morphism -> morphism -> theory -> theory
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    75
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    76
  (* Diagnostic *)
37471
907e13072675 separate section for diagnostic commands
haftmann
parents: 37133
diff changeset
    77
  val all_locales: theory -> string list
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    78
  val print_locales: theory -> unit
30344
10a67c5ddddb more uniform handling of binding in targets and derived elements;
wenzelm
parents: 30223
diff changeset
    79
  val print_locale: theory -> bool -> xstring -> unit
32804
ca430e6aee1c Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents: 32803 32801
diff changeset
    80
  val print_registrations: theory -> string -> unit
37897
c5ad6fec3470 abstract visualization of locale ingredients; all_locales yields proper locale identifiers
haftmann
parents: 37491
diff changeset
    81
  val locale_deps: theory ->
c5ad6fec3470 abstract visualization of locale ingredients; all_locales yields proper locale identifiers
haftmann
parents: 37491
diff changeset
    82
    { params: ((string * typ) * mixfix) list, axioms: term list, registrations: term list list } Graph.T
c5ad6fec3470 abstract visualization of locale ingredients; all_locales yields proper locale identifiers
haftmann
parents: 37491
diff changeset
    83
      * term list list Symtab.table Symtab.table
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    84
end;
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    85
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    86
structure Locale: LOCALE =
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    87
struct
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    88
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    89
datatype ctxt = datatype Element.ctxt;
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    90
29392
aa3a30b625d1 tuned signature; internal code reorganisation
haftmann
parents: 29363
diff changeset
    91
aa3a30b625d1 tuned signature; internal code reorganisation
haftmann
parents: 29363
diff changeset
    92
(*** Theory data ***)
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    93
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    94
datatype locale = Loc of {
29392
aa3a30b625d1 tuned signature; internal code reorganisation
haftmann
parents: 29363
diff changeset
    95
  (** static part **)
30755
7ef503d216c2 simplified internal locale parameters: maintain proper name and type, instead of binding and constraint;
wenzelm
parents: 30754
diff changeset
    96
  parameters: (string * sort) list * ((string * typ) * mixfix) list,
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    97
    (* type and term parameters *)
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    98
  spec: term option * term list,
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
    99
    (* assumptions (as a single predicate expression) and defines *)
29441
28d7d7572b81 explicit bookkeeping of intro rules and axiom
haftmann
parents: 29392
diff changeset
   100
  intros: thm option * thm option,
28d7d7572b81 explicit bookkeeping of intro rules and axiom
haftmann
parents: 29392
diff changeset
   101
  axioms: thm list,
29392
aa3a30b625d1 tuned signature; internal code reorganisation
haftmann
parents: 29363
diff changeset
   102
  (** dynamic part **)
36096
abc6a2ea4b88 Merged resolving conflicts NEWS and locale.ML.
ballarin
parents: 36095 35798
diff changeset
   103
  syntax_decls: (declaration * serial) list,
35798
fd1bb29f8170 replaced type_syntax/term_syntax by uniform syntax_declaration;
wenzelm
parents: 33643
diff changeset
   104
    (* syntax declarations *)
36096
abc6a2ea4b88 Merged resolving conflicts NEWS and locale.ML.
ballarin
parents: 36095 35798
diff changeset
   105
  notes: ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * serial) list,
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   106
    (* theorem declarations *)
36651
97c3bbe63389 Explicitly manage export in dependencies.
ballarin
parents: 36240
diff changeset
   107
  dependencies: ((string * (morphism * morphism)) * serial) list
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   108
    (* locale dependencies (sublocale relation) *)
29392
aa3a30b625d1 tuned signature; internal code reorganisation
haftmann
parents: 29363
diff changeset
   109
};
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   110
35798
fd1bb29f8170 replaced type_syntax/term_syntax by uniform syntax_declaration;
wenzelm
parents: 33643
diff changeset
   111
fun mk_locale ((parameters, spec, intros, axioms), ((syntax_decls, notes), dependencies)) =
29441
28d7d7572b81 explicit bookkeeping of intro rules and axiom
haftmann
parents: 29392
diff changeset
   112
  Loc {parameters = parameters, intros = intros, axioms = axioms, spec = spec,
35798
fd1bb29f8170 replaced type_syntax/term_syntax by uniform syntax_declaration;
wenzelm
parents: 33643
diff changeset
   113
    syntax_decls = syntax_decls, notes = notes, dependencies = dependencies};
fd1bb29f8170 replaced type_syntax/term_syntax by uniform syntax_declaration;
wenzelm
parents: 33643
diff changeset
   114
fd1bb29f8170 replaced type_syntax/term_syntax by uniform syntax_declaration;
wenzelm
parents: 33643
diff changeset
   115
fun map_locale f (Loc {parameters, spec, intros, axioms, syntax_decls, notes, dependencies}) =
fd1bb29f8170 replaced type_syntax/term_syntax by uniform syntax_declaration;
wenzelm
parents: 33643
diff changeset
   116
  mk_locale (f ((parameters, spec, intros, axioms), ((syntax_decls, notes), dependencies)));
30754
c896167de3d5 minor tuning;
wenzelm
parents: 30725
diff changeset
   117
35798
fd1bb29f8170 replaced type_syntax/term_syntax by uniform syntax_declaration;
wenzelm
parents: 33643
diff changeset
   118
fun merge_locale
fd1bb29f8170 replaced type_syntax/term_syntax by uniform syntax_declaration;
wenzelm
parents: 33643
diff changeset
   119
 (Loc {parameters, spec, intros, axioms, syntax_decls, notes, dependencies},
fd1bb29f8170 replaced type_syntax/term_syntax by uniform syntax_declaration;
wenzelm
parents: 33643
diff changeset
   120
  Loc {syntax_decls = syntax_decls', notes = notes', dependencies = dependencies', ...}) =
fd1bb29f8170 replaced type_syntax/term_syntax by uniform syntax_declaration;
wenzelm
parents: 33643
diff changeset
   121
    mk_locale
29441
28d7d7572b81 explicit bookkeeping of intro rules and axiom
haftmann
parents: 29392
diff changeset
   122
      ((parameters, spec, intros, axioms),
35798
fd1bb29f8170 replaced type_syntax/term_syntax by uniform syntax_declaration;
wenzelm
parents: 33643
diff changeset
   123
        ((merge (eq_snd op =) (syntax_decls, syntax_decls'),
29441
28d7d7572b81 explicit bookkeeping of intro rules and axiom
haftmann
parents: 29392
diff changeset
   124
          merge (eq_snd op =) (notes, notes')),
28d7d7572b81 explicit bookkeeping of intro rules and axiom
haftmann
parents: 29392
diff changeset
   125
            merge (eq_snd op =) (dependencies, dependencies')));
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   126
33522
737589bb9bb8 adapted Theory_Data;
wenzelm
parents: 33519
diff changeset
   127
structure Locales = Theory_Data
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   128
(
33095
bbd52d2f8696 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
wenzelm
parents: 33092
diff changeset
   129
  type T = locale Name_Space.table;
33159
369da293bbd4 make SML/NJ happy;
wenzelm
parents: 33096
diff changeset
   130
  val empty : T = Name_Space.empty_table "locale";
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   131
  val extend = I;
33522
737589bb9bb8 adapted Theory_Data;
wenzelm
parents: 33519
diff changeset
   132
  val merge = Name_Space.join_tables (K merge_locale);
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   133
);
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   134
33095
bbd52d2f8696 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
wenzelm
parents: 33092
diff changeset
   135
val intern = Name_Space.intern o #1 o Locales.get;
bbd52d2f8696 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
wenzelm
parents: 33092
diff changeset
   136
val extern = Name_Space.extern o #1 o Locales.get;
29392
aa3a30b625d1 tuned signature; internal code reorganisation
haftmann
parents: 29363
diff changeset
   137
30725
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
   138
val get_locale = Symtab.lookup o #2 o Locales.get;
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
   139
val defined = Symtab.defined o #2 o Locales.get;
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   140
30725
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
   141
fun the_locale thy name =
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
   142
  (case get_locale thy name of
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
   143
    SOME (Loc loc) => loc
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
   144
  | NONE => error ("Unknown locale " ^ quote name));
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   145
35798
fd1bb29f8170 replaced type_syntax/term_syntax by uniform syntax_declaration;
wenzelm
parents: 33643
diff changeset
   146
fun register_locale binding parameters spec intros axioms syntax_decls notes dependencies thy =
33095
bbd52d2f8696 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
wenzelm
parents: 33092
diff changeset
   147
  thy |> Locales.map (Name_Space.define true (Sign.naming_of thy)
30725
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
   148
    (binding,
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
   149
      mk_locale ((parameters, spec, intros, axioms),
36096
abc6a2ea4b88 Merged resolving conflicts NEWS and locale.ML.
ballarin
parents: 36095 35798
diff changeset
   150
        ((map (fn decl => (decl, serial ())) syntax_decls, map (fn n => (n, serial ())) notes),
36651
97c3bbe63389 Explicitly manage export in dependencies.
ballarin
parents: 36240
diff changeset
   151
          map (fn d => (d |> apsnd (rpair Morphism.identity), serial ())) dependencies))) #> snd);
97c3bbe63389 Explicitly manage export in dependencies.
ballarin
parents: 36240
diff changeset
   152
          (* FIXME *)
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   153
29392
aa3a30b625d1 tuned signature; internal code reorganisation
haftmann
parents: 29363
diff changeset
   154
fun change_locale name =
30725
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
   155
  Locales.map o apsnd o Symtab.map_entry name o map_locale o apsnd;
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   156
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   157
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   158
(*** Primitive operations ***)
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   159
29392
aa3a30b625d1 tuned signature; internal code reorganisation
haftmann
parents: 29363
diff changeset
   160
fun params_of thy = snd o #parameters o the_locale thy;
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   161
29441
28d7d7572b81 explicit bookkeeping of intro rules and axiom
haftmann
parents: 29392
diff changeset
   162
fun intros_of thy = #intros o the_locale thy;
28d7d7572b81 explicit bookkeeping of intro rules and axiom
haftmann
parents: 29392
diff changeset
   163
28d7d7572b81 explicit bookkeeping of intro rules and axiom
haftmann
parents: 29392
diff changeset
   164
fun axioms_of thy = #axioms o the_locale thy;
28d7d7572b81 explicit bookkeeping of intro rules and axiom
haftmann
parents: 29392
diff changeset
   165
29392
aa3a30b625d1 tuned signature; internal code reorganisation
haftmann
parents: 29363
diff changeset
   166
fun instance_of thy name morph = params_of thy name |>
30755
7ef503d216c2 simplified internal locale parameters: maintain proper name and type, instead of binding and constraint;
wenzelm
parents: 30754
diff changeset
   167
  map (Morphism.term morph o Free o #1);
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   168
29392
aa3a30b625d1 tuned signature; internal code reorganisation
haftmann
parents: 29363
diff changeset
   169
fun specification_of thy = #spec o the_locale thy;
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   170
29544
bc50244cd1d7 exported depedencies; tuned signature
haftmann
parents: 29502
diff changeset
   171
fun dependencies_of thy name = the_locale thy name |>
bc50244cd1d7 exported depedencies; tuned signature
haftmann
parents: 29502
diff changeset
   172
  #dependencies |> map fst;
bc50244cd1d7 exported depedencies; tuned signature
haftmann
parents: 29502
diff changeset
   173
37133
1d048c6940c8 Merge mixins of distinct interpretations with same base.
ballarin
parents: 37105
diff changeset
   174
(* Print instance and qualifiers *)
1d048c6940c8 Merge mixins of distinct interpretations with same base.
ballarin
parents: 37105
diff changeset
   175
1d048c6940c8 Merge mixins of distinct interpretations with same base.
ballarin
parents: 37105
diff changeset
   176
fun pretty_reg thy (name, morph) =
1d048c6940c8 Merge mixins of distinct interpretations with same base.
ballarin
parents: 37105
diff changeset
   177
  let
1d048c6940c8 Merge mixins of distinct interpretations with same base.
ballarin
parents: 37105
diff changeset
   178
    val name' = extern thy name;
1d048c6940c8 Merge mixins of distinct interpretations with same base.
ballarin
parents: 37105
diff changeset
   179
    val ctxt = ProofContext.init_global thy;
1d048c6940c8 Merge mixins of distinct interpretations with same base.
ballarin
parents: 37105
diff changeset
   180
    fun prt_qual (qual, mand) = Pretty.str (qual ^ (if mand then "!" else "?"));
1d048c6940c8 Merge mixins of distinct interpretations with same base.
ballarin
parents: 37105
diff changeset
   181
    fun prt_quals qs = Pretty.separate "." (map prt_qual qs) |> Pretty.block;
1d048c6940c8 Merge mixins of distinct interpretations with same base.
ballarin
parents: 37105
diff changeset
   182
    val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
1d048c6940c8 Merge mixins of distinct interpretations with same base.
ballarin
parents: 37105
diff changeset
   183
    fun prt_term' t = if !show_types
1d048c6940c8 Merge mixins of distinct interpretations with same base.
ballarin
parents: 37105
diff changeset
   184
      then Pretty.block [prt_term t, Pretty.brk 1, Pretty.str "::",
1d048c6940c8 Merge mixins of distinct interpretations with same base.
ballarin
parents: 37105
diff changeset
   185
        Pretty.brk 1, (Pretty.quote o Syntax.pretty_typ ctxt) (type_of t)]
1d048c6940c8 Merge mixins of distinct interpretations with same base.
ballarin
parents: 37105
diff changeset
   186
      else prt_term t;
1d048c6940c8 Merge mixins of distinct interpretations with same base.
ballarin
parents: 37105
diff changeset
   187
    fun prt_inst ts =
1d048c6940c8 Merge mixins of distinct interpretations with same base.
ballarin
parents: 37105
diff changeset
   188
      Pretty.block (Pretty.breaks (Pretty.str name' :: map prt_term' ts));
1d048c6940c8 Merge mixins of distinct interpretations with same base.
ballarin
parents: 37105
diff changeset
   189
1d048c6940c8 Merge mixins of distinct interpretations with same base.
ballarin
parents: 37105
diff changeset
   190
    val qs = Binding.name "x" |> Morphism.binding morph |> Binding.prefix_of;
1d048c6940c8 Merge mixins of distinct interpretations with same base.
ballarin
parents: 37105
diff changeset
   191
    val ts = instance_of thy name morph;
1d048c6940c8 Merge mixins of distinct interpretations with same base.
ballarin
parents: 37105
diff changeset
   192
  in
1d048c6940c8 Merge mixins of distinct interpretations with same base.
ballarin
parents: 37105
diff changeset
   193
    case qs of
1d048c6940c8 Merge mixins of distinct interpretations with same base.
ballarin
parents: 37105
diff changeset
   194
       [] => prt_inst ts
1d048c6940c8 Merge mixins of distinct interpretations with same base.
ballarin
parents: 37105
diff changeset
   195
     | qs => Pretty.block [prt_quals qs, Pretty.brk 1, Pretty.str ":",
1d048c6940c8 Merge mixins of distinct interpretations with same base.
ballarin
parents: 37105
diff changeset
   196
         Pretty.brk 1, prt_inst ts]
1d048c6940c8 Merge mixins of distinct interpretations with same base.
ballarin
parents: 37105
diff changeset
   197
  end;
1d048c6940c8 Merge mixins of distinct interpretations with same base.
ballarin
parents: 37105
diff changeset
   198
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   199
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   200
(*** Activate context elements of locale ***)
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   201
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   202
(** Identifiers: activated locales in theory or proof context **)
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   203
37105
e464f84f3680 Store registrations in efficient data structure.
ballarin
parents: 37104
diff changeset
   204
(* subsumption *)
37103
6ea25bb157e1 Consistently use equality for registration lookup.
ballarin
parents: 37102
diff changeset
   205
fun ident_le thy ((n: string, ts), (m, ss)) = (m = n) andalso Pattern.matchess thy (ss, ts);
37105
e464f84f3680 Store registrations in efficient data structure.
ballarin
parents: 37104
diff changeset
   206
  (* smaller term is more general *)
e464f84f3680 Store registrations in efficient data structure.
ballarin
parents: 37104
diff changeset
   207
e464f84f3680 Store registrations in efficient data structure.
ballarin
parents: 37104
diff changeset
   208
(* total order *)
e464f84f3680 Store registrations in efficient data structure.
ballarin
parents: 37104
diff changeset
   209
fun ident_ord ((n: string, ts), (m, ss)) =
e464f84f3680 Store registrations in efficient data structure.
ballarin
parents: 37104
diff changeset
   210
  case fast_string_ord (m, n) of
e464f84f3680 Store registrations in efficient data structure.
ballarin
parents: 37104
diff changeset
   211
      EQUAL => list_ord Term_Ord.fast_term_ord (ts, ss)
e464f84f3680 Store registrations in efficient data structure.
ballarin
parents: 37104
diff changeset
   212
    | ord => ord;
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   213
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   214
local
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   215
30754
c896167de3d5 minor tuning;
wenzelm
parents: 30725
diff changeset
   216
datatype 'a delayed = Ready of 'a | ToDo of 'a delayed * 'a delayed;
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   217
33519
e31a85f92ce9 adapted Generic_Data, Proof_Data;
wenzelm
parents: 33278
diff changeset
   218
structure Identifiers = Generic_Data
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   219
(
30754
c896167de3d5 minor tuning;
wenzelm
parents: 30725
diff changeset
   220
  type T = (string * term list) list delayed;
c896167de3d5 minor tuning;
wenzelm
parents: 30725
diff changeset
   221
  val empty = Ready [];
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   222
  val extend = I;
33519
e31a85f92ce9 adapted Generic_Data, Proof_Data;
wenzelm
parents: 33278
diff changeset
   223
  val merge = ToDo;
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   224
);
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   225
37103
6ea25bb157e1 Consistently use equality for registration lookup.
ballarin
parents: 37102
diff changeset
   226
fun finish thy (ToDo (i1, i2)) = merge (ident_le thy) (finish thy i1, finish thy i2)
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   227
  | finish _ (Ready ids) = ids;
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   228
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   229
val _ = Context.>> (Context.map_theory (Theory.at_begin (fn thy =>
30725
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
   230
  (case Identifiers.get (Context.Theory thy) of
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
   231
    Ready _ => NONE
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
   232
  | ids => SOME (Context.theory_map (Identifiers.put (Ready (finish thy ids))) thy)))));
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   233
30764
3e3e7aa0cc7a simplified Locale.activate operations, using generic context;
wenzelm
parents: 30763
diff changeset
   234
in
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   235
30764
3e3e7aa0cc7a simplified Locale.activate operations, using generic context;
wenzelm
parents: 30763
diff changeset
   236
val get_idents = (fn Ready ids => ids) o Identifiers.get;
3e3e7aa0cc7a simplified Locale.activate operations, using generic context;
wenzelm
parents: 30763
diff changeset
   237
val put_idents = Identifiers.put o Ready;
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   238
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   239
end;
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   240
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   241
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   242
(** Resolve locale dependencies in a depth-first fashion **)
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   243
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   244
local
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   245
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   246
val roundup_bound = 120;
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   247
32803
fc02b4b9eccc Archive registrations by external view.
ballarin
parents: 32800
diff changeset
   248
fun add thy depth export (name, morph) (deps, marked) =
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   249
  if depth > roundup_bound
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   250
  then error "Roundup bound exceeded (sublocale relation probably not terminating)."
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   251
  else
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   252
    let
30754
c896167de3d5 minor tuning;
wenzelm
parents: 30725
diff changeset
   253
      val dependencies = dependencies_of thy name;
32803
fc02b4b9eccc Archive registrations by external view.
ballarin
parents: 32800
diff changeset
   254
      val instance = instance_of thy name (morph $> export);
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   255
    in
37103
6ea25bb157e1 Consistently use equality for registration lookup.
ballarin
parents: 37102
diff changeset
   256
      if member (ident_le thy) marked (name, instance)
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   257
      then (deps, marked)
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   258
      else
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   259
        let
36651
97c3bbe63389 Explicitly manage export in dependencies.
ballarin
parents: 36240
diff changeset
   260
          val dependencies' = map (fn (name, (morph', export')) => (name, morph' $> export' $> morph)) dependencies;
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   261
          val marked' = (name, instance) :: marked;
32803
fc02b4b9eccc Archive registrations by external view.
ballarin
parents: 32800
diff changeset
   262
          val (deps', marked'') = fold_rev (add thy (depth + 1) export) dependencies' ([], marked');
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   263
        in
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   264
          ((name, morph) :: deps' @ deps, marked'')
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   265
        end
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   266
    end;
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   267
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   268
in
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   269
33541
e716c6ad381b Removed obsolete code.
ballarin
parents: 33522
diff changeset
   270
(* Note that while identifiers always have the external (exported) view, activate_dep
32803
fc02b4b9eccc Archive registrations by external view.
ballarin
parents: 32800
diff changeset
   271
  is presented with the internal view. *)
fc02b4b9eccc Archive registrations by external view.
ballarin
parents: 32800
diff changeset
   272
fc02b4b9eccc Archive registrations by external view.
ballarin
parents: 32800
diff changeset
   273
fun roundup thy activate_dep export (name, morph) (marked, input) =
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   274
  let
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   275
    (* Find all dependencies incuding new ones (which are dependencies enriching
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   276
      existing registrations). *)
32803
fc02b4b9eccc Archive registrations by external view.
ballarin
parents: 32800
diff changeset
   277
    val (dependencies, marked') = add thy 0 export (name, morph) ([], []);
32800
57fcca4e7c0e Improved comments and api names.
ballarin
parents: 32113
diff changeset
   278
    (* Filter out fragments from marked; these won't be activated. *)
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   279
    val dependencies' = filter_out (fn (name, morph) =>
37103
6ea25bb157e1 Consistently use equality for registration lookup.
ballarin
parents: 37102
diff changeset
   280
      member (ident_le thy) marked (name, instance_of thy name (morph $> export))) dependencies;
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   281
  in
37103
6ea25bb157e1 Consistently use equality for registration lookup.
ballarin
parents: 37102
diff changeset
   282
    (merge (ident_le thy) (marked, marked'), input |> fold_rev activate_dep dependencies')
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   283
  end;
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   284
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   285
end;
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   286
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   287
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   288
(* Declarations, facts and entire locale content *)
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   289
35798
fd1bb29f8170 replaced type_syntax/term_syntax by uniform syntax_declaration;
wenzelm
parents: 33643
diff changeset
   290
fun activate_syntax_decls (name, morph) context =
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   291
  let
30764
3e3e7aa0cc7a simplified Locale.activate operations, using generic context;
wenzelm
parents: 30763
diff changeset
   292
    val thy = Context.theory_of context;
35798
fd1bb29f8170 replaced type_syntax/term_syntax by uniform syntax_declaration;
wenzelm
parents: 33643
diff changeset
   293
    val {syntax_decls, ...} = the_locale thy name;
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   294
  in
30764
3e3e7aa0cc7a simplified Locale.activate operations, using generic context;
wenzelm
parents: 30763
diff changeset
   295
    context
35798
fd1bb29f8170 replaced type_syntax/term_syntax by uniform syntax_declaration;
wenzelm
parents: 33643
diff changeset
   296
    |> fold_rev (fn (decl, _) => decl morph) syntax_decls
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   297
  end;
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   298
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   299
fun activate_notes activ_elem transfer thy (name, morph) input =
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   300
  let
29392
aa3a30b625d1 tuned signature; internal code reorganisation
haftmann
parents: 29363
diff changeset
   301
    val {notes, ...} = the_locale thy name;
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   302
    fun activate ((kind, facts), _) input =
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   303
      let
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   304
        val facts' = facts |> Element.facts_map (Element.morph_ctxt (transfer input $> morph))
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   305
      in activ_elem (Notes (kind, facts')) input end;
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   306
  in
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   307
    fold_rev activate notes input
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   308
  end;
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   309
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   310
fun activate_all name thy activ_elem transfer (marked, input) =
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   311
  let
30764
3e3e7aa0cc7a simplified Locale.activate operations, using generic context;
wenzelm
parents: 30763
diff changeset
   312
    val {parameters = (_, params), spec = (asm, defs), ...} = the_locale thy name;
3e3e7aa0cc7a simplified Locale.activate operations, using generic context;
wenzelm
parents: 30763
diff changeset
   313
    val input' = input |>
30755
7ef503d216c2 simplified internal locale parameters: maintain proper name and type, instead of binding and constraint;
wenzelm
parents: 30754
diff changeset
   314
      (not (null params) ?
7ef503d216c2 simplified internal locale parameters: maintain proper name and type, instead of binding and constraint;
wenzelm
parents: 30754
diff changeset
   315
        activ_elem (Fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params))) |>
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   316
      (* FIXME type parameters *)
30764
3e3e7aa0cc7a simplified Locale.activate operations, using generic context;
wenzelm
parents: 30763
diff changeset
   317
      (case asm of SOME A => activ_elem (Assumes [(Attrib.empty_binding, [(A, [])])]) | _ => I) |>
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   318
      (if not (null defs)
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   319
        then activ_elem (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs))
30764
3e3e7aa0cc7a simplified Locale.activate operations, using generic context;
wenzelm
parents: 30763
diff changeset
   320
        else I);
30773
6cc9964436c3 simplified roundup activation interface;
wenzelm
parents: 30764
diff changeset
   321
    val activate = activate_notes activ_elem transfer thy;
30764
3e3e7aa0cc7a simplified Locale.activate operations, using generic context;
wenzelm
parents: 30763
diff changeset
   322
  in
32803
fc02b4b9eccc Archive registrations by external view.
ballarin
parents: 32800
diff changeset
   323
    roundup thy activate Morphism.identity (name, Morphism.identity) (marked, input')
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   324
  end;
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   325
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   326
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   327
(** Public activation functions **)
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   328
30775
71f777103225 added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
wenzelm
parents: 30773
diff changeset
   329
fun activate_declarations dep = Context.proof_map (fn context =>
30764
3e3e7aa0cc7a simplified Locale.activate operations, using generic context;
wenzelm
parents: 30763
diff changeset
   330
  let
3e3e7aa0cc7a simplified Locale.activate operations, using generic context;
wenzelm
parents: 30763
diff changeset
   331
    val thy = Context.theory_of context;
35798
fd1bb29f8170 replaced type_syntax/term_syntax by uniform syntax_declaration;
wenzelm
parents: 33643
diff changeset
   332
  in
fd1bb29f8170 replaced type_syntax/term_syntax by uniform syntax_declaration;
wenzelm
parents: 33643
diff changeset
   333
    roundup thy activate_syntax_decls Morphism.identity dep (get_idents context, context)
fd1bb29f8170 replaced type_syntax/term_syntax by uniform syntax_declaration;
wenzelm
parents: 33643
diff changeset
   334
    |-> put_idents
fd1bb29f8170 replaced type_syntax/term_syntax by uniform syntax_declaration;
wenzelm
parents: 33643
diff changeset
   335
  end);
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   336
30764
3e3e7aa0cc7a simplified Locale.activate operations, using generic context;
wenzelm
parents: 30763
diff changeset
   337
fun activate_facts dep context =
3e3e7aa0cc7a simplified Locale.activate operations, using generic context;
wenzelm
parents: 30763
diff changeset
   338
  let
3e3e7aa0cc7a simplified Locale.activate operations, using generic context;
wenzelm
parents: 30763
diff changeset
   339
    val thy = Context.theory_of context;
30775
71f777103225 added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
wenzelm
parents: 30773
diff changeset
   340
    val activate = activate_notes Element.init (Element.transfer_morphism o Context.theory_of) thy;
32803
fc02b4b9eccc Archive registrations by external view.
ballarin
parents: 32800
diff changeset
   341
  in roundup thy activate Morphism.identity dep (get_idents context, context) |-> put_idents end;
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   342
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   343
fun init name thy =
30775
71f777103225 added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
wenzelm
parents: 30773
diff changeset
   344
  activate_all name thy Element.init (Element.transfer_morphism o Context.theory_of)
36610
bafd82950e24 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
wenzelm
parents: 36240
diff changeset
   345
    ([], Context.Proof (ProofContext.init_global thy)) |-> put_idents |> Context.proof_of;
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   346
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   347
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   348
(*** Registrations: interpretations in theories ***)
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   349
37105
e464f84f3680 Store registrations in efficient data structure.
ballarin
parents: 37104
diff changeset
   350
structure Idtab = Table(type key = string * term list val ord = ident_ord);
e464f84f3680 Store registrations in efficient data structure.
ballarin
parents: 37104
diff changeset
   351
38107
3a46cebd7983 Make registrations generic data.
ballarin
parents: 37973
diff changeset
   352
structure Registrations = Generic_Data
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   353
(
37105
e464f84f3680 Store registrations in efficient data structure.
ballarin
parents: 37104
diff changeset
   354
  type T = ((morphism * morphism) * serial) Idtab.table *
e464f84f3680 Store registrations in efficient data structure.
ballarin
parents: 37104
diff changeset
   355
    (* registrations, indexed by locale name and instance;
36090
87e950efb359 Clarified invariant; tuned.
ballarin
parents: 36088
diff changeset
   356
       serial points to mixin list *)
37105
e464f84f3680 Store registrations in efficient data structure.
ballarin
parents: 37104
diff changeset
   357
    (((morphism * bool) * serial) list) Inttab.table;
e464f84f3680 Store registrations in efficient data structure.
ballarin
parents: 37104
diff changeset
   358
    (* table of mixin lists, per list mixins in reverse order of declaration;
36090
87e950efb359 Clarified invariant; tuned.
ballarin
parents: 36088
diff changeset
   359
       lists indexed by registration serial,
87e950efb359 Clarified invariant; tuned.
ballarin
parents: 36088
diff changeset
   360
       entries for empty lists may be omitted *)
37105
e464f84f3680 Store registrations in efficient data structure.
ballarin
parents: 37104
diff changeset
   361
  val empty = (Idtab.empty, Inttab.empty);
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   362
  val extend = I;
37133
1d048c6940c8 Merge mixins of distinct interpretations with same base.
ballarin
parents: 37105
diff changeset
   363
  fun merge ((reg1, mix1), (reg2, mix2)) : T =
1d048c6940c8 Merge mixins of distinct interpretations with same base.
ballarin
parents: 37105
diff changeset
   364
    (Idtab.join (fn id => fn (r1 as (_, s1), r2 as (_, s2)) =>
1d048c6940c8 Merge mixins of distinct interpretations with same base.
ballarin
parents: 37105
diff changeset
   365
        if s1 = s2 then raise Idtab.SAME else raise Idtab.DUP id) (reg1, reg2),
1d048c6940c8 Merge mixins of distinct interpretations with same base.
ballarin
parents: 37105
diff changeset
   366
      Inttab.join (K (Library.merge (eq_snd op =))) (mix1, mix2))
1d048c6940c8 Merge mixins of distinct interpretations with same base.
ballarin
parents: 37105
diff changeset
   367
    handle Idtab.DUP id =>
1d048c6940c8 Merge mixins of distinct interpretations with same base.
ballarin
parents: 37105
diff changeset
   368
      (* distinct interpretations with same base: merge their mixins *)
1d048c6940c8 Merge mixins of distinct interpretations with same base.
ballarin
parents: 37105
diff changeset
   369
      let
1d048c6940c8 Merge mixins of distinct interpretations with same base.
ballarin
parents: 37105
diff changeset
   370
        val (_, s1) = Idtab.lookup reg1 id |> the;
1d048c6940c8 Merge mixins of distinct interpretations with same base.
ballarin
parents: 37105
diff changeset
   371
        val (morph2, s2) = Idtab.lookup reg2 id |> the;
1d048c6940c8 Merge mixins of distinct interpretations with same base.
ballarin
parents: 37105
diff changeset
   372
        val reg2' = Idtab.update (id, (morph2, s1)) reg2;
1d048c6940c8 Merge mixins of distinct interpretations with same base.
ballarin
parents: 37105
diff changeset
   373
        val mix2' = case Inttab.lookup mix2 s2 of
1d048c6940c8 Merge mixins of distinct interpretations with same base.
ballarin
parents: 37105
diff changeset
   374
              NONE => mix2 |
1d048c6940c8 Merge mixins of distinct interpretations with same base.
ballarin
parents: 37105
diff changeset
   375
              SOME mxs => Inttab.delete s2 mix2 |> Inttab.update_new (s1, mxs);
1d048c6940c8 Merge mixins of distinct interpretations with same base.
ballarin
parents: 37105
diff changeset
   376
        val _ = warning "Removed duplicate interpretation after retrieving its mixins.";
1d048c6940c8 Merge mixins of distinct interpretations with same base.
ballarin
parents: 37105
diff changeset
   377
        (* FIXME print interpretations,
1d048c6940c8 Merge mixins of distinct interpretations with same base.
ballarin
parents: 37105
diff changeset
   378
           which is not straightforward without theory context *)
1d048c6940c8 Merge mixins of distinct interpretations with same base.
ballarin
parents: 37105
diff changeset
   379
      in merge ((reg1, mix1), (reg2', mix2')) end;
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   380
    (* FIXME consolidate with dependencies, consider one data slot only *)
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   381
);
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   382
32801
6f97a67e8da8 Explicit management of registration mixins.
ballarin
parents: 32800
diff changeset
   383
6f97a67e8da8 Explicit management of registration mixins.
ballarin
parents: 32800
diff changeset
   384
(* Primitive operations *)
6f97a67e8da8 Explicit management of registration mixins.
ballarin
parents: 32800
diff changeset
   385
37104
3877a6c45d57 Avoid recomputation of registration instance for lookup.
ballarin
parents: 37103
diff changeset
   386
fun add_reg thy export (name, morph) =
37105
e464f84f3680 Store registrations in efficient data structure.
ballarin
parents: 37104
diff changeset
   387
  Registrations.map (apfst (Idtab.insert (K false)
e464f84f3680 Store registrations in efficient data structure.
ballarin
parents: 37104
diff changeset
   388
    ((name, instance_of thy name (morph $> export)), ((morph, export), serial ()))));
31988
801aabf9f376 tuned locale interface
haftmann
parents: 30777
diff changeset
   389
36095
059c3568fdc8 Proper inheritance of mixins for activated facts and locale dependencies.
ballarin
parents: 36094
diff changeset
   390
fun add_mixin serial' mixin =
059c3568fdc8 Proper inheritance of mixins for activated facts and locale dependencies.
ballarin
parents: 36094
diff changeset
   391
  (* registration to be amended identified by its serial id *)
37105
e464f84f3680 Store registrations in efficient data structure.
ballarin
parents: 37104
diff changeset
   392
  Registrations.map (apsnd (Inttab.map_default (serial', []) (cons (mixin, serial ()))));
32801
6f97a67e8da8 Explicit management of registration mixins.
ballarin
parents: 32800
diff changeset
   393
38107
3a46cebd7983 Make registrations generic data.
ballarin
parents: 37973
diff changeset
   394
fun get_mixins context (name, morph) =
32804
ca430e6aee1c Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents: 32803 32801
diff changeset
   395
  let
38107
3a46cebd7983 Make registrations generic data.
ballarin
parents: 37973
diff changeset
   396
    val thy = Context.theory_of context;
3a46cebd7983 Make registrations generic data.
ballarin
parents: 37973
diff changeset
   397
    val (regs, mixins) = Registrations.get context;
32804
ca430e6aee1c Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents: 32803 32801
diff changeset
   398
  in
37105
e464f84f3680 Store registrations in efficient data structure.
ballarin
parents: 37104
diff changeset
   399
    case Idtab.lookup regs (name, instance_of thy name morph) of
32804
ca430e6aee1c Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents: 32803 32801
diff changeset
   400
      NONE => []
37105
e464f84f3680 Store registrations in efficient data structure.
ballarin
parents: 37104
diff changeset
   401
    | SOME (_, serial) => the_default [] (Inttab.lookup mixins serial)
32804
ca430e6aee1c Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents: 32803 32801
diff changeset
   402
  end;
ca430e6aee1c Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents: 32803 32801
diff changeset
   403
36091
055934ed89b0 A rough implementation of full mixin inheritance; additional unit tests.
ballarin
parents: 36090
diff changeset
   404
fun compose_mixins mixins =
055934ed89b0 A rough implementation of full mixin inheritance; additional unit tests.
ballarin
parents: 36090
diff changeset
   405
  fold_rev Morphism.compose (map (fst o fst) mixins) Morphism.identity;
055934ed89b0 A rough implementation of full mixin inheritance; additional unit tests.
ballarin
parents: 36090
diff changeset
   406
38107
3a46cebd7983 Make registrations generic data.
ballarin
parents: 37973
diff changeset
   407
fun collect_mixins context (name, morph) =
3a46cebd7983 Make registrations generic data.
ballarin
parents: 37973
diff changeset
   408
  let
3a46cebd7983 Make registrations generic data.
ballarin
parents: 37973
diff changeset
   409
    val thy = Context.theory_of context;
3a46cebd7983 Make registrations generic data.
ballarin
parents: 37973
diff changeset
   410
  in
3a46cebd7983 Make registrations generic data.
ballarin
parents: 37973
diff changeset
   411
    roundup thy (fn dep => fn mixins => merge (eq_snd op =) (mixins, get_mixins context dep))
3a46cebd7983 Make registrations generic data.
ballarin
parents: 37973
diff changeset
   412
      Morphism.identity (name, morph) ([(name, instance_of thy name morph)], [])
3a46cebd7983 Make registrations generic data.
ballarin
parents: 37973
diff changeset
   413
    |> snd |> filter (snd o fst)  (* only inheritable mixins *)
3a46cebd7983 Make registrations generic data.
ballarin
parents: 37973
diff changeset
   414
    |> (fn x => merge (eq_snd op =) (x, get_mixins context (name, morph)))
3a46cebd7983 Make registrations generic data.
ballarin
parents: 37973
diff changeset
   415
    |> compose_mixins
3a46cebd7983 Make registrations generic data.
ballarin
parents: 37973
diff changeset
   416
  end;
36091
055934ed89b0 A rough implementation of full mixin inheritance; additional unit tests.
ballarin
parents: 36090
diff changeset
   417
38107
3a46cebd7983 Make registrations generic data.
ballarin
parents: 37973
diff changeset
   418
fun get_registrations context select = Registrations.get context
37491
b5989aa32358 Proper treatment of non-inherited mixins.
ballarin
parents: 37471
diff changeset
   419
  |>> Idtab.dest |>> select
36095
059c3568fdc8 Proper inheritance of mixins for activated facts and locale dependencies.
ballarin
parents: 36094
diff changeset
   420
  (* with inherited mixins *)
37105
e464f84f3680 Store registrations in efficient data structure.
ballarin
parents: 37104
diff changeset
   421
  |-> (fn regs => fn _ => map (fn ((name, _), ((base, export) ,_)) =>
38107
3a46cebd7983 Make registrations generic data.
ballarin
parents: 37973
diff changeset
   422
    (name, base $> (collect_mixins context (name, base $> export)) $> export)) regs);
36091
055934ed89b0 A rough implementation of full mixin inheritance; additional unit tests.
ballarin
parents: 36090
diff changeset
   423
38107
3a46cebd7983 Make registrations generic data.
ballarin
parents: 37973
diff changeset
   424
fun registrations_of_locale context name =
3a46cebd7983 Make registrations generic data.
ballarin
parents: 37973
diff changeset
   425
  get_registrations context (filter (curry (op =) name o fst o fst));
37491
b5989aa32358 Proper treatment of non-inherited mixins.
ballarin
parents: 37471
diff changeset
   426
38107
3a46cebd7983 Make registrations generic data.
ballarin
parents: 37973
diff changeset
   427
fun all_registrations context = get_registrations context I;
37973
2b4ff2518ebf get_registrations interface
haftmann
parents: 37897
diff changeset
   428
38107
3a46cebd7983 Make registrations generic data.
ballarin
parents: 37973
diff changeset
   429
fun activate_notes' activ_elem transfer context export (name, morph) input =
32804
ca430e6aee1c Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents: 32803 32801
diff changeset
   430
  let
38107
3a46cebd7983 Make registrations generic data.
ballarin
parents: 37973
diff changeset
   431
    val thy = Context.theory_of context;
32804
ca430e6aee1c Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents: 32803 32801
diff changeset
   432
    val {notes, ...} = the_locale thy name;
ca430e6aee1c Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents: 32803 32801
diff changeset
   433
    fun activate ((kind, facts), _) input =
ca430e6aee1c Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents: 32803 32801
diff changeset
   434
      let
38107
3a46cebd7983 Make registrations generic data.
ballarin
parents: 37973
diff changeset
   435
        val mixin = collect_mixins context (name, morph $> export);
32804
ca430e6aee1c Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents: 32803 32801
diff changeset
   436
        val facts' = facts |> Element.facts_map (Element.morph_ctxt (transfer input $> morph $> mixin $> export))
ca430e6aee1c Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents: 32803 32801
diff changeset
   437
      in activ_elem (Notes (kind, facts')) input end;
ca430e6aee1c Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents: 32803 32801
diff changeset
   438
  in
ca430e6aee1c Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents: 32803 32801
diff changeset
   439
    fold_rev activate notes input
ca430e6aee1c Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents: 32803 32801
diff changeset
   440
  end;
ca430e6aee1c Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents: 32803 32801
diff changeset
   441
ca430e6aee1c Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents: 32803 32801
diff changeset
   442
fun activate_facts' export dep context =
ca430e6aee1c Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents: 32803 32801
diff changeset
   443
  let
ca430e6aee1c Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents: 32803 32801
diff changeset
   444
    val thy = Context.theory_of context;
38107
3a46cebd7983 Make registrations generic data.
ballarin
parents: 37973
diff changeset
   445
    val activate = activate_notes' Element.init (Element.transfer_morphism o Context.theory_of) context export;
32804
ca430e6aee1c Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents: 32803 32801
diff changeset
   446
  in roundup thy activate export dep (get_idents context, context) |-> put_idents end;
ca430e6aee1c Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents: 32803 32801
diff changeset
   447
ca430e6aee1c Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents: 32803 32801
diff changeset
   448
32801
6f97a67e8da8 Explicit management of registration mixins.
ballarin
parents: 32800
diff changeset
   449
(* Add and extend registrations *)
6f97a67e8da8 Explicit management of registration mixins.
ballarin
parents: 32800
diff changeset
   450
38107
3a46cebd7983 Make registrations generic data.
ballarin
parents: 37973
diff changeset
   451
fun amend_registration (name, morph) mixin export context =
32804
ca430e6aee1c Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents: 32803 32801
diff changeset
   452
  let
38107
3a46cebd7983 Make registrations generic data.
ballarin
parents: 37973
diff changeset
   453
    val thy = Context.theory_of context;
3a46cebd7983 Make registrations generic data.
ballarin
parents: 37973
diff changeset
   454
    val regs = Registrations.get context |> fst;
32804
ca430e6aee1c Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents: 32803 32801
diff changeset
   455
    val base = instance_of thy name (morph $> export);
ca430e6aee1c Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents: 32803 32801
diff changeset
   456
  in
37105
e464f84f3680 Store registrations in efficient data structure.
ballarin
parents: 37104
diff changeset
   457
    case Idtab.lookup regs (name, base) of
32804
ca430e6aee1c Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents: 32803 32801
diff changeset
   458
        NONE => error ("No interpretation of locale " ^
ca430e6aee1c Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents: 32803 32801
diff changeset
   459
          quote (extern thy name) ^ " and\nparameter instantiation " ^
ca430e6aee1c Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents: 32803 32801
diff changeset
   460
          space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
ca430e6aee1c Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents: 32803 32801
diff changeset
   461
          " available")
38107
3a46cebd7983 Make registrations generic data.
ballarin
parents: 37973
diff changeset
   462
      | SOME (_, serial') => add_mixin serial' mixin context
32804
ca430e6aee1c Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents: 32803 32801
diff changeset
   463
  end;
ca430e6aee1c Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents: 32803 32801
diff changeset
   464
32801
6f97a67e8da8 Explicit management of registration mixins.
ballarin
parents: 32800
diff changeset
   465
(* Note that a registration that would be subsumed by an existing one will not be
6f97a67e8da8 Explicit management of registration mixins.
ballarin
parents: 32800
diff changeset
   466
   generated, and it will not be possible to amend it. *)
6f97a67e8da8 Explicit management of registration mixins.
ballarin
parents: 32800
diff changeset
   467
38107
3a46cebd7983 Make registrations generic data.
ballarin
parents: 37973
diff changeset
   468
fun add_registration (name, base_morph) mixin export context =
32801
6f97a67e8da8 Explicit management of registration mixins.
ballarin
parents: 32800
diff changeset
   469
  let
38107
3a46cebd7983 Make registrations generic data.
ballarin
parents: 37973
diff changeset
   470
    val thy = Context.theory_of context;
37101
7099a9ed3be2 Reapply mixin patch: base for performance improvements.
ballarin
parents: 36919
diff changeset
   471
    val mix = case mixin of NONE => Morphism.identity
7099a9ed3be2 Reapply mixin patch: base for performance improvements.
ballarin
parents: 36919
diff changeset
   472
          | SOME (mix, _) => mix;
37102
785348a83a2b Cleaner implementation of sublocale command.
ballarin
parents: 37101
diff changeset
   473
    val morph = base_morph $> mix;
785348a83a2b Cleaner implementation of sublocale command.
ballarin
parents: 37101
diff changeset
   474
    val inst = instance_of thy name morph;
32801
6f97a67e8da8 Explicit management of registration mixins.
ballarin
parents: 32800
diff changeset
   475
  in
38107
3a46cebd7983 Make registrations generic data.
ballarin
parents: 37973
diff changeset
   476
    if member (ident_le thy) (get_idents context) (name, inst)
3a46cebd7983 Make registrations generic data.
ballarin
parents: 37973
diff changeset
   477
    then context
32801
6f97a67e8da8 Explicit management of registration mixins.
ballarin
parents: 32800
diff changeset
   478
    else
38107
3a46cebd7983 Make registrations generic data.
ballarin
parents: 37973
diff changeset
   479
      (get_idents context, context)
36095
059c3568fdc8 Proper inheritance of mixins for activated facts and locale dependencies.
ballarin
parents: 36094
diff changeset
   480
      (* add new registrations with inherited mixins *)
37104
3877a6c45d57 Avoid recomputation of registration instance for lookup.
ballarin
parents: 37103
diff changeset
   481
      |> roundup thy (add_reg thy export) export (name, morph)
36095
059c3568fdc8 Proper inheritance of mixins for activated facts and locale dependencies.
ballarin
parents: 36094
diff changeset
   482
      |> snd
059c3568fdc8 Proper inheritance of mixins for activated facts and locale dependencies.
ballarin
parents: 36094
diff changeset
   483
      (* add mixin *)
059c3568fdc8 Proper inheritance of mixins for activated facts and locale dependencies.
ballarin
parents: 36094
diff changeset
   484
      |> (case mixin of NONE => I
37102
785348a83a2b Cleaner implementation of sublocale command.
ballarin
parents: 37101
diff changeset
   485
           | SOME mixin => amend_registration (name, morph) mixin export)
36095
059c3568fdc8 Proper inheritance of mixins for activated facts and locale dependencies.
ballarin
parents: 36094
diff changeset
   486
      (* activate import hierarchy as far as not already active *)
38107
3a46cebd7983 Make registrations generic data.
ballarin
parents: 37973
diff changeset
   487
      |> activate_facts' export (name, morph)
32801
6f97a67e8da8 Explicit management of registration mixins.
ballarin
parents: 32800
diff changeset
   488
  end;
6f97a67e8da8 Explicit management of registration mixins.
ballarin
parents: 32800
diff changeset
   489
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   490
31988
801aabf9f376 tuned locale interface
haftmann
parents: 30777
diff changeset
   491
(*** Dependencies ***)
801aabf9f376 tuned locale interface
haftmann
parents: 30777
diff changeset
   492
37102
785348a83a2b Cleaner implementation of sublocale command.
ballarin
parents: 37101
diff changeset
   493
fun add_dependency loc (name, morph) export thy =
785348a83a2b Cleaner implementation of sublocale command.
ballarin
parents: 37101
diff changeset
   494
  let
785348a83a2b Cleaner implementation of sublocale command.
ballarin
parents: 37101
diff changeset
   495
    val thy' = (change_locale loc o apsnd) (cons ((name, (morph, export)), serial ())) thy;
38107
3a46cebd7983 Make registrations generic data.
ballarin
parents: 37973
diff changeset
   496
    val context' = Context.Theory thy';
37102
785348a83a2b Cleaner implementation of sublocale command.
ballarin
parents: 37101
diff changeset
   497
    val (_, regs) = fold_rev (roundup thy' cons export)
38107
3a46cebd7983 Make registrations generic data.
ballarin
parents: 37973
diff changeset
   498
      (all_registrations context') (get_idents (context'), []);
37102
785348a83a2b Cleaner implementation of sublocale command.
ballarin
parents: 37101
diff changeset
   499
  in
785348a83a2b Cleaner implementation of sublocale command.
ballarin
parents: 37101
diff changeset
   500
    thy'
38107
3a46cebd7983 Make registrations generic data.
ballarin
parents: 37973
diff changeset
   501
    |> fold_rev (fn dep => Context.theory_map (add_registration dep NONE export)) regs
37102
785348a83a2b Cleaner implementation of sublocale command.
ballarin
parents: 37101
diff changeset
   502
  end;
31988
801aabf9f376 tuned locale interface
haftmann
parents: 30777
diff changeset
   503
801aabf9f376 tuned locale interface
haftmann
parents: 30777
diff changeset
   504
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   505
(*** Storing results ***)
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   506
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   507
(* Theorems *)
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   508
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   509
fun add_thmss loc kind args ctxt =
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   510
  let
30777
9960ff945c52 simplified Element.activate(_i): singleton version;
wenzelm
parents: 30775
diff changeset
   511
    val (Notes args', ctxt') = Element.activate_i (Notes (kind, args)) ctxt;
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   512
    val ctxt'' = ctxt' |> ProofContext.theory (
36088
a4369989bc45 Use serial to be more debug friendly.
ballarin
parents: 33643
diff changeset
   513
      (change_locale loc o apfst o apsnd) (cons (args', serial ()))
29392
aa3a30b625d1 tuned signature; internal code reorganisation
haftmann
parents: 29363
diff changeset
   514
        #>
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   515
      (* Registrations *)
31988
801aabf9f376 tuned locale interface
haftmann
parents: 30777
diff changeset
   516
      (fn thy => fold_rev (fn (_, morph) =>
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   517
            let
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   518
              val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |>
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   519
                Attrib.map_facts (Attrib.attribute_i thy)
30438
c2d49315b93b eliminated qualified_names naming policy: qualified names are only permitted via explicit Binding.qualify/qualified_name etc. (NB: user-level outer syntax should never do this);
wenzelm
parents: 30344
diff changeset
   520
            in PureThy.note_thmss kind args'' #> snd end)
38107
3a46cebd7983 Make registrations generic data.
ballarin
parents: 37973
diff changeset
   521
        (registrations_of_locale (Context.Theory thy) loc) thy))
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   522
  in ctxt'' end;
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   523
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   524
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   525
(* Declarations *)
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   526
35798
fd1bb29f8170 replaced type_syntax/term_syntax by uniform syntax_declaration;
wenzelm
parents: 33643
diff changeset
   527
fun add_declaration loc decl =
33643
b275f26a638b eliminated obsolete "internal" kind -- collapsed to unspecific "";
wenzelm
parents: 33541
diff changeset
   528
  add_thmss loc ""
35798
fd1bb29f8170 replaced type_syntax/term_syntax by uniform syntax_declaration;
wenzelm
parents: 33643
diff changeset
   529
    [((Binding.conceal Binding.empty,
fd1bb29f8170 replaced type_syntax/term_syntax by uniform syntax_declaration;
wenzelm
parents: 33643
diff changeset
   530
        [Attrib.internal (fn phi => Thm.declaration_attribute (K (decl phi)))]),
33278
ba9f52f56356 conceal internal bindings;
wenzelm
parents: 33159
diff changeset
   531
      [([Drule.dummy_thm], [])])];
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   532
35798
fd1bb29f8170 replaced type_syntax/term_syntax by uniform syntax_declaration;
wenzelm
parents: 33643
diff changeset
   533
fun add_syntax_declaration loc decl =
36096
abc6a2ea4b88 Merged resolving conflicts NEWS and locale.ML.
ballarin
parents: 36095 35798
diff changeset
   534
  ProofContext.theory ((change_locale loc o apfst o apfst) (cons (decl, serial ())))
35798
fd1bb29f8170 replaced type_syntax/term_syntax by uniform syntax_declaration;
wenzelm
parents: 33643
diff changeset
   535
  #> add_declaration loc decl;
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   536
30725
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
   537
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   538
(*** Reasoning about locales ***)
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   539
30725
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
   540
(* Storage for witnesses, intro and unfold rules *)
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   541
33519
e31a85f92ce9 adapted Generic_Data, Proof_Data;
wenzelm
parents: 33278
diff changeset
   542
structure Thms = Generic_Data
30725
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
   543
(
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
   544
  type T = thm list * thm list * thm list;
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
   545
  val empty = ([], [], []);
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
   546
  val extend = I;
33519
e31a85f92ce9 adapted Generic_Data, Proof_Data;
wenzelm
parents: 33278
diff changeset
   547
  fun merge ((witnesses1, intros1, unfolds1), (witnesses2, intros2, unfolds2)) =
30725
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
   548
   (Thm.merge_thms (witnesses1, witnesses2),
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
   549
    Thm.merge_thms (intros1, intros2),
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
   550
    Thm.merge_thms (unfolds1, unfolds2));
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
   551
);
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   552
30725
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
   553
val get_witnesses = #1 o Thms.get o Context.Proof;
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
   554
val get_intros = #2 o Thms.get o Context.Proof;
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
   555
val get_unfolds = #3 o Thms.get o Context.Proof;
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   556
30725
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
   557
val witness_add =
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
   558
  Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (Thm.add_thm th x, y, z)));
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
   559
val intro_add =
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
   560
  Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (x, Thm.add_thm th y, z)));
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
   561
val unfold_add =
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
   562
  Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (x, y, Thm.add_thm th z)));
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   563
30725
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
   564
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
   565
(* Tactic *)
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
   566
36093
0880493627ca Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.
ballarin
parents: 36091
diff changeset
   567
fun gen_intro_locales_tac intros_tac eager ctxt =
0880493627ca Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.
ballarin
parents: 36091
diff changeset
   568
  intros_tac
30725
c23a5b3cd1b9 register_locale: produce stamps at the spot where elements are registered;
wenzelm
parents: 30585
diff changeset
   569
    (get_witnesses ctxt @ get_intros ctxt @ (if eager then get_unfolds ctxt else []));
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   570
36093
0880493627ca Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.
ballarin
parents: 36091
diff changeset
   571
val intro_locales_tac = gen_intro_locales_tac Method.intros_tac;
0880493627ca Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.
ballarin
parents: 36091
diff changeset
   572
val try_intro_locales_tac= gen_intro_locales_tac Method.try_intros_tac;
0880493627ca Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.
ballarin
parents: 36091
diff changeset
   573
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   574
val _ = Context.>> (Context.map_theory
36093
0880493627ca Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.
ballarin
parents: 36091
diff changeset
   575
 (Method.setup (Binding.name "intro_locales") (Scan.succeed (METHOD o try_intro_locales_tac false))
30515
bca05b17b618 simplified method setup;
wenzelm
parents: 30510
diff changeset
   576
    "back-chain introduction rules of locales without unfolding predicates" #>
36093
0880493627ca Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.
ballarin
parents: 36091
diff changeset
   577
  Method.setup (Binding.name "unfold_locales") (Scan.succeed (METHOD o try_intro_locales_tac true))
30515
bca05b17b618 simplified method setup;
wenzelm
parents: 30510
diff changeset
   578
    "back-chain all introduction rules of locales"));
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   579
37471
907e13072675 separate section for diagnostic commands
haftmann
parents: 37133
diff changeset
   580
907e13072675 separate section for diagnostic commands
haftmann
parents: 37133
diff changeset
   581
(*** diagnostic commands and interfaces ***)
907e13072675 separate section for diagnostic commands
haftmann
parents: 37133
diff changeset
   582
37897
c5ad6fec3470 abstract visualization of locale ingredients; all_locales yields proper locale identifiers
haftmann
parents: 37491
diff changeset
   583
val all_locales = Symtab.keys o snd o Locales.get;
37471
907e13072675 separate section for diagnostic commands
haftmann
parents: 37133
diff changeset
   584
907e13072675 separate section for diagnostic commands
haftmann
parents: 37133
diff changeset
   585
fun print_locales thy =
37897
c5ad6fec3470 abstract visualization of locale ingredients; all_locales yields proper locale identifiers
haftmann
parents: 37491
diff changeset
   586
  Pretty.strs ("locales:" :: map #1 (Name_Space.extern_table (Locales.get thy)))
37471
907e13072675 separate section for diagnostic commands
haftmann
parents: 37133
diff changeset
   587
  |> Pretty.writeln;
907e13072675 separate section for diagnostic commands
haftmann
parents: 37133
diff changeset
   588
907e13072675 separate section for diagnostic commands
haftmann
parents: 37133
diff changeset
   589
fun print_locale thy show_facts raw_name =
907e13072675 separate section for diagnostic commands
haftmann
parents: 37133
diff changeset
   590
  let
907e13072675 separate section for diagnostic commands
haftmann
parents: 37133
diff changeset
   591
    val name = intern thy raw_name;
907e13072675 separate section for diagnostic commands
haftmann
parents: 37133
diff changeset
   592
    val ctxt = init name thy;
907e13072675 separate section for diagnostic commands
haftmann
parents: 37133
diff changeset
   593
    fun cons_elem (elem as Notes _) = show_facts ? cons elem
907e13072675 separate section for diagnostic commands
haftmann
parents: 37133
diff changeset
   594
      | cons_elem elem = cons elem;
907e13072675 separate section for diagnostic commands
haftmann
parents: 37133
diff changeset
   595
    val elems =
907e13072675 separate section for diagnostic commands
haftmann
parents: 37133
diff changeset
   596
      activate_all name thy cons_elem (K (Element.transfer_morphism thy)) ([], [])
907e13072675 separate section for diagnostic commands
haftmann
parents: 37133
diff changeset
   597
      |> snd |> rev;
907e13072675 separate section for diagnostic commands
haftmann
parents: 37133
diff changeset
   598
  in
907e13072675 separate section for diagnostic commands
haftmann
parents: 37133
diff changeset
   599
    Pretty.big_list "locale elements:" (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)
907e13072675 separate section for diagnostic commands
haftmann
parents: 37133
diff changeset
   600
    |> Pretty.writeln
907e13072675 separate section for diagnostic commands
haftmann
parents: 37133
diff changeset
   601
  end;
907e13072675 separate section for diagnostic commands
haftmann
parents: 37133
diff changeset
   602
907e13072675 separate section for diagnostic commands
haftmann
parents: 37133
diff changeset
   603
fun print_registrations thy raw_name =
38107
3a46cebd7983 Make registrations generic data.
ballarin
parents: 37973
diff changeset
   604
  (case registrations_of_locale (Context.Theory thy) (intern thy raw_name) of
37471
907e13072675 separate section for diagnostic commands
haftmann
parents: 37133
diff changeset
   605
      [] => Pretty.str ("no interpretations")
907e13072675 separate section for diagnostic commands
haftmann
parents: 37133
diff changeset
   606
    | regs => Pretty.big_list "interpretations:" (map (pretty_reg thy) (rev regs)))
907e13072675 separate section for diagnostic commands
haftmann
parents: 37133
diff changeset
   607
  |> Pretty.writeln;
907e13072675 separate section for diagnostic commands
haftmann
parents: 37133
diff changeset
   608
37897
c5ad6fec3470 abstract visualization of locale ingredients; all_locales yields proper locale identifiers
haftmann
parents: 37491
diff changeset
   609
fun locale_deps thy =
c5ad6fec3470 abstract visualization of locale ingredients; all_locales yields proper locale identifiers
haftmann
parents: 37491
diff changeset
   610
  let
c5ad6fec3470 abstract visualization of locale ingredients; all_locales yields proper locale identifiers
haftmann
parents: 37491
diff changeset
   611
    val names = all_locales thy
c5ad6fec3470 abstract visualization of locale ingredients; all_locales yields proper locale identifiers
haftmann
parents: 37491
diff changeset
   612
    fun add_locale_node name =
c5ad6fec3470 abstract visualization of locale ingredients; all_locales yields proper locale identifiers
haftmann
parents: 37491
diff changeset
   613
      let
c5ad6fec3470 abstract visualization of locale ingredients; all_locales yields proper locale identifiers
haftmann
parents: 37491
diff changeset
   614
        val params = params_of thy name;
c5ad6fec3470 abstract visualization of locale ingredients; all_locales yields proper locale identifiers
haftmann
parents: 37491
diff changeset
   615
        val axioms = (these o Option.map (Logic.strip_imp_prems o Thm.prop_of) o fst o intros_of thy) name;
c5ad6fec3470 abstract visualization of locale ingredients; all_locales yields proper locale identifiers
haftmann
parents: 37491
diff changeset
   616
        val registrations = map (instance_of thy name o snd)
38107
3a46cebd7983 Make registrations generic data.
ballarin
parents: 37973
diff changeset
   617
          (registrations_of_locale (Context.Theory thy) name);
37897
c5ad6fec3470 abstract visualization of locale ingredients; all_locales yields proper locale identifiers
haftmann
parents: 37491
diff changeset
   618
      in 
c5ad6fec3470 abstract visualization of locale ingredients; all_locales yields proper locale identifiers
haftmann
parents: 37491
diff changeset
   619
        Graph.new_node (name, { params = params, axioms = axioms, registrations = registrations })
c5ad6fec3470 abstract visualization of locale ingredients; all_locales yields proper locale identifiers
haftmann
parents: 37491
diff changeset
   620
      end;
c5ad6fec3470 abstract visualization of locale ingredients; all_locales yields proper locale identifiers
haftmann
parents: 37491
diff changeset
   621
    fun add_locale_deps name =
c5ad6fec3470 abstract visualization of locale ingredients; all_locales yields proper locale identifiers
haftmann
parents: 37491
diff changeset
   622
      let
c5ad6fec3470 abstract visualization of locale ingredients; all_locales yields proper locale identifiers
haftmann
parents: 37491
diff changeset
   623
        val dependencies = (map o apsnd) (instance_of thy name o op $>)
c5ad6fec3470 abstract visualization of locale ingredients; all_locales yields proper locale identifiers
haftmann
parents: 37491
diff changeset
   624
          (dependencies_of thy name);
c5ad6fec3470 abstract visualization of locale ingredients; all_locales yields proper locale identifiers
haftmann
parents: 37491
diff changeset
   625
      in
c5ad6fec3470 abstract visualization of locale ingredients; all_locales yields proper locale identifiers
haftmann
parents: 37491
diff changeset
   626
        fold (fn (super, ts) => fn (gr, deps) => (gr |> Graph.add_edge (super, name),
c5ad6fec3470 abstract visualization of locale ingredients; all_locales yields proper locale identifiers
haftmann
parents: 37491
diff changeset
   627
          deps |> Symtab.map_default (super, Symtab.empty) (Symtab.cons_list (name, ts))))
c5ad6fec3470 abstract visualization of locale ingredients; all_locales yields proper locale identifiers
haftmann
parents: 37491
diff changeset
   628
            dependencies
c5ad6fec3470 abstract visualization of locale ingredients; all_locales yields proper locale identifiers
haftmann
parents: 37491
diff changeset
   629
      end;
c5ad6fec3470 abstract visualization of locale ingredients; all_locales yields proper locale identifiers
haftmann
parents: 37491
diff changeset
   630
  in
c5ad6fec3470 abstract visualization of locale ingredients; all_locales yields proper locale identifiers
haftmann
parents: 37491
diff changeset
   631
    Graph.empty
c5ad6fec3470 abstract visualization of locale ingredients; all_locales yields proper locale identifiers
haftmann
parents: 37491
diff changeset
   632
    |> fold add_locale_node names
c5ad6fec3470 abstract visualization of locale ingredients; all_locales yields proper locale identifiers
haftmann
parents: 37491
diff changeset
   633
    |> rpair Symtab.empty
c5ad6fec3470 abstract visualization of locale ingredients; all_locales yields proper locale identifiers
haftmann
parents: 37491
diff changeset
   634
    |> fold add_locale_deps names
c5ad6fec3470 abstract visualization of locale ingredients; all_locales yields proper locale identifiers
haftmann
parents: 37491
diff changeset
   635
  end;
c5ad6fec3470 abstract visualization of locale ingredients; all_locales yields proper locale identifiers
haftmann
parents: 37491
diff changeset
   636
29361
764d51ab0198 locale -> old_locale, new_locale -> locale
haftmann
parents:
diff changeset
   637
end;