src/Pure/Isar/locale.ML
author wenzelm
Fri Apr 08 16:34:14 2011 +0200 (2011-04-08)
changeset 42290 b1f544c84040
parent 41435 12585dfb86fe
child 42358 b47d41d9f4b5
permissions -rw-r--r--
discontinued special treatment of structure Lexicon;
     1 (*  Title:      Pure/Isar/locale.ML
     2     Author:     Clemens Ballarin, TU Muenchen
     3 
     4 Locales -- managed Isar proof contexts, based on Pure predicates.
     5 
     6 Draws basic ideas from Florian Kammueller's original version of
     7 locales, but uses the richer infrastructure of Isar instead of the raw
     8 meta-logic.  Furthermore, structured import of contexts (with merge
     9 and rename operations) are provided, as well as type-inference of the
    10 signature parts, and predicate definitions of the specification text.
    11 
    12 Interpretation enables the reuse of theorems of locales in other
    13 contexts, namely those defined by theories, structured proofs and
    14 locales themselves.
    15 
    16 See also:
    17 
    18 [1] Clemens Ballarin. Locales and Locale Expressions in Isabelle/Isar.
    19     In Stefano Berardi et al., Types for Proofs and Programs: International
    20     Workshop, TYPES 2003, Torino, Italy, LNCS 3085, pages 34-50, 2004.
    21 [2] Clemens Ballarin. Interpretation of Locales in Isabelle: Managing
    22     Dependencies between Locales. Technical Report TUM-I0607, Technische
    23     Universitaet Muenchen, 2006.
    24 [3] Clemens Ballarin. Interpretation of Locales in Isabelle: Theories and
    25     Proof Contexts. In J.M. Borwein and W.M. Farmer, MKM 2006, LNAI 4108,
    26     pages 31-43, 2006.
    27 *)
    28 
    29 signature LOCALE =
    30 sig
    31   (* Locale specification *)
    32   val register_locale: binding ->
    33     (string * sort) list * ((string * typ) * mixfix) list ->
    34     term option * term list ->
    35     thm option * thm option -> thm list ->
    36     declaration list ->
    37     (string * (Attrib.binding * (thm list * Attrib.src list) list) list) list ->
    38     (string * morphism) list -> theory -> theory
    39   val intern: theory -> xstring -> string
    40   val extern: theory -> string -> xstring
    41   val defined: theory -> string -> bool
    42   val params_of: theory -> string -> ((string * typ) * mixfix) list
    43   val intros_of: theory -> string -> thm option * thm option
    44   val axioms_of: theory -> string -> thm list
    45   val instance_of: theory -> string -> morphism -> term list
    46   val specification_of: theory -> string -> term option * term list
    47 
    48   (* Storing results *)
    49   val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
    50     Proof.context -> Proof.context
    51   val add_declaration: string -> declaration -> Proof.context -> Proof.context
    52   val add_syntax_declaration: string -> declaration -> Proof.context -> Proof.context
    53 
    54   (* Activation *)
    55   val activate_declarations: string * morphism -> Proof.context -> Proof.context
    56   val activate_facts: morphism option -> string * morphism -> Context.generic -> Context.generic
    57   val init: string -> theory -> Proof.context
    58 
    59   (* Reasoning about locales *)
    60   val get_witnesses: Proof.context -> thm list
    61   val get_intros: Proof.context -> thm list
    62   val get_unfolds: Proof.context -> thm list
    63   val witness_add: attribute
    64   val intro_add: attribute
    65   val unfold_add: attribute
    66   val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
    67 
    68   (* Registrations and dependencies *)
    69   val add_registration: string * morphism -> (morphism * bool) option ->
    70     morphism -> Context.generic -> Context.generic
    71   val amend_registration: string * morphism -> morphism * bool ->
    72     morphism -> Context.generic -> Context.generic
    73   val registrations_of: Context.generic -> string -> (string * morphism) list
    74   val add_dependency: string -> string * morphism -> (morphism * bool) option ->
    75     morphism -> theory -> theory
    76 
    77   (* Diagnostic *)
    78   val all_locales: theory -> string list
    79   val print_locales: theory -> unit
    80   val print_locale: theory -> bool -> xstring -> unit
    81   val print_registrations: Proof.context -> string -> unit
    82   val print_dependencies: Proof.context -> bool -> morphism -> (string * morphism) list -> unit
    83   val locale_deps: theory ->
    84     {params: ((string * typ) * mixfix) list, axioms: term list, registrations: term list list} Graph.T
    85       * term list list Symtab.table Symtab.table
    86 end;
    87 
    88 structure Locale: LOCALE =
    89 struct
    90 
    91 datatype ctxt = datatype Element.ctxt;
    92 
    93 
    94 (*** Locales ***)
    95 
    96 type mixins = (((morphism * bool) * serial) list) Inttab.table;
    97   (* table of mixin lists, per list mixins in reverse order of declaration;
    98      lists indexed by registration/dependency serial,
    99      entries for empty lists may be omitted *)
   100 
   101 fun lookup_mixins serial' mixins = the_default [] (Inttab.lookup mixins serial');
   102 
   103 fun merge_mixins (mix1, mix2) = Inttab.join (K (Library.merge (eq_snd op =))) (mix1, mix2);
   104 
   105 fun insert_mixin serial' mixin =
   106   Inttab.map_default (serial', []) (cons (mixin, serial ()));
   107 
   108 fun rename_mixin (old, new) mix =
   109   case Inttab.lookup mix old of
   110     NONE => mix |
   111     SOME mxs => Inttab.delete old mix |> Inttab.update_new (new, mxs);
   112 
   113 fun compose_mixins mixins =
   114   fold_rev Morphism.compose (map (fst o fst) mixins) Morphism.identity;
   115 
   116 datatype locale = Loc of {
   117   (** static part **)
   118   parameters: (string * sort) list * ((string * typ) * mixfix) list,
   119     (* type and term parameters *)
   120   spec: term option * term list,
   121     (* assumptions (as a single predicate expression) and defines *)
   122   intros: thm option * thm option,
   123   axioms: thm list,
   124   (** dynamic part **)
   125   syntax_decls: (declaration * serial) list,
   126     (* syntax declarations *)
   127   notes: ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * serial) list,
   128     (* theorem declarations *)
   129   dependencies: ((string * (morphism * morphism)) * serial) list
   130     (* locale dependencies (sublocale relation) in reverse order *),
   131   mixins: mixins
   132     (* mixin part of dependencies *)
   133 };
   134 
   135 fun mk_locale ((parameters, spec, intros, axioms),
   136     ((syntax_decls, notes), (dependencies, mixins))) =
   137   Loc {parameters = parameters, intros = intros, axioms = axioms, spec = spec,
   138     syntax_decls = syntax_decls, notes = notes, dependencies = dependencies, mixins = mixins};
   139 
   140 fun map_locale f (Loc {parameters, spec, intros, axioms,
   141     syntax_decls, notes, dependencies, mixins}) =
   142   mk_locale (f ((parameters, spec, intros, axioms),
   143     ((syntax_decls, notes), (dependencies, mixins))));
   144 
   145 fun merge_locale
   146  (Loc {parameters, spec, intros, axioms, syntax_decls, notes, dependencies, mixins},
   147   Loc {syntax_decls = syntax_decls', notes = notes',
   148       dependencies = dependencies', mixins = mixins', ...}) =
   149     mk_locale
   150       ((parameters, spec, intros, axioms),
   151         ((merge (eq_snd op =) (syntax_decls, syntax_decls'),
   152           merge (eq_snd op =) (notes, notes')),
   153             (merge (eq_snd op =) (dependencies, dependencies'),
   154               (merge_mixins (mixins, mixins')))));
   155 
   156 structure Locales = Theory_Data
   157 (
   158   type T = locale Name_Space.table;
   159   val empty : T = Name_Space.empty_table "locale";
   160   val extend = I;
   161   val merge = Name_Space.join_tables (K merge_locale);
   162 );
   163 
   164 val intern = Name_Space.intern o #1 o Locales.get;
   165 val extern = Name_Space.extern o #1 o Locales.get;
   166 
   167 val get_locale = Symtab.lookup o #2 o Locales.get;
   168 val defined = Symtab.defined o #2 o Locales.get;
   169 
   170 fun the_locale thy name =
   171   (case get_locale thy name of
   172     SOME (Loc loc) => loc
   173   | NONE => error ("Unknown locale " ^ quote name));
   174 
   175 fun register_locale binding parameters spec intros axioms syntax_decls notes dependencies thy =
   176   thy |> Locales.map (Name_Space.define true (Sign.naming_of thy)
   177     (binding,
   178       mk_locale ((parameters, spec, intros, axioms),
   179         ((map (fn decl => (decl, serial ())) syntax_decls, map (fn n => (n, serial ())) notes),
   180           (map (fn d => (d |> apsnd (rpair Morphism.identity), serial ())) dependencies,
   181             Inttab.empty)))) #> snd);
   182           (* FIXME Morphism.identity *)
   183 
   184 fun change_locale name =
   185   Locales.map o apsnd o Symtab.map_entry name o map_locale o apsnd;
   186 
   187 
   188 (** Primitive operations **)
   189 
   190 fun params_of thy = snd o #parameters o the_locale thy;
   191 
   192 fun intros_of thy = #intros o the_locale thy;
   193 
   194 fun axioms_of thy = #axioms o the_locale thy;
   195 
   196 fun instance_of thy name morph = params_of thy name |>
   197   map (Morphism.term morph o Free o #1);
   198 
   199 fun specification_of thy = #spec o the_locale thy;
   200 
   201 fun dependencies_of thy name = the_locale thy name |>
   202   #dependencies;
   203 
   204 fun mixins_of thy name serial = the_locale thy name |>
   205   #mixins |> lookup_mixins serial;
   206 
   207 (* unused *)
   208 fun identity_on thy name morph =
   209   let val mk_instance = instance_of thy name
   210   in
   211     forall2 (curry Term.aconv_untyped) (mk_instance Morphism.identity) (mk_instance morph)
   212   end;
   213 
   214 (* Print instance and qualifiers *)
   215 
   216 fun pretty_reg ctxt (name, morph) =
   217   let
   218     val thy = ProofContext.theory_of ctxt;
   219     val name' = extern thy name;
   220     fun prt_qual (qual, mand) = Pretty.str (qual ^ (if mand then "!" else "?"));
   221     fun prt_quals qs = Pretty.separate "." (map prt_qual qs) |> Pretty.block;
   222     val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
   223     fun prt_term' t =
   224       if Config.get ctxt show_types
   225       then Pretty.block [prt_term t, Pretty.brk 1, Pretty.str "::",
   226         Pretty.brk 1, (Pretty.quote o Syntax.pretty_typ ctxt) (type_of t)]
   227       else prt_term t;
   228     fun prt_inst ts =
   229       Pretty.block (Pretty.breaks (Pretty.str name' :: map prt_term' ts));
   230 
   231     val qs = Binding.name "x" |> Morphism.binding morph |> Binding.prefix_of;
   232     val ts = instance_of thy name morph;
   233   in
   234     (case qs of
   235       [] => prt_inst ts
   236     | qs => Pretty.block [prt_quals qs, Pretty.brk 1, Pretty.str ":", Pretty.brk 1, prt_inst ts])
   237   end;
   238 
   239 
   240 (*** Identifiers: activated locales in theory or proof context ***)
   241 
   242 (* subsumption *)
   243 fun ident_le thy ((n: string, ts), (m, ss)) = (m = n) andalso Pattern.matchess thy (ss, ts);
   244   (* smaller term is more general *)
   245 
   246 (* total order *)
   247 fun ident_ord ((n: string, ts), (m, ss)) =
   248   (case fast_string_ord (m, n) of
   249     EQUAL => list_ord Term_Ord.fast_term_ord (ts, ss)
   250   | ord => ord);
   251 
   252 local
   253 
   254 datatype 'a delayed = Ready of 'a | ToDo of 'a delayed * 'a delayed;
   255 
   256 structure Identifiers = Generic_Data
   257 (
   258   type T = (string * term list) list delayed;
   259   val empty = Ready [];
   260   val extend = I;
   261   val merge = ToDo;
   262 );
   263 
   264 fun finish thy (ToDo (i1, i2)) = merge (ident_le thy) (finish thy i1, finish thy i2)
   265   | finish _ (Ready ids) = ids;
   266 
   267 val _ = Context.>> (Context.map_theory (Theory.at_begin (fn thy =>
   268   (case Identifiers.get (Context.Theory thy) of
   269     Ready _ => NONE
   270   | ids => SOME (Context.theory_map (Identifiers.put (Ready (finish thy ids))) thy)))));
   271 
   272 in
   273 
   274 val get_idents = (fn Ready ids => ids) o Identifiers.get;
   275 val put_idents = Identifiers.put o Ready;
   276 
   277 end;
   278 
   279 
   280 (** Resolve locale dependencies in a depth-first fashion **)
   281 
   282 local
   283 
   284 val roundup_bound = 120;
   285 
   286 fun add thy depth stem export (name, morph, mixins) (deps, marked) =
   287   if depth > roundup_bound
   288   then error "Roundup bound exceeded (sublocale relation probably not terminating)."
   289   else
   290     let
   291       val instance = instance_of thy name (morph $> stem $> export);
   292     in
   293       if member (ident_le thy) marked (name, instance)
   294       then (deps, marked)
   295       else
   296         let
   297           val full_morph = morph $> compose_mixins mixins $> stem;
   298           (* no inheritance of mixins, regardless of requests by clients *)
   299           val dependencies = dependencies_of thy name |>
   300             map (fn ((name', (morph', export')), serial') =>
   301               (name', morph' $> export', mixins_of thy name serial'));
   302           val marked' = (name, instance) :: marked;
   303           val (deps', marked'') =
   304             fold_rev (add thy (depth + 1) full_morph export) dependencies
   305               ([], marked');
   306         in
   307           ((name, full_morph) :: deps' @ deps, marked'')
   308         end
   309     end;
   310 
   311 in
   312 
   313 (* Note that while identifiers always have the external (exported) view, activate_dep
   314   is presented with the internal view. *)
   315 
   316 fun roundup thy activate_dep export (name, morph) (marked, input) =
   317   let
   318     (* Find all dependencies including new ones (which are dependencies enriching
   319       existing registrations). *)
   320     val (dependencies, marked') =
   321       add thy 0 Morphism.identity export (name, morph, []) ([], []);
   322     (* Filter out fragments from marked; these won't be activated. *)
   323     val dependencies' = filter_out (fn (name, morph) =>
   324       member (ident_le thy) marked (name, instance_of thy name (morph $> export))) dependencies;
   325   in
   326     (merge (ident_le thy) (marked, marked'), input |> fold_rev activate_dep dependencies')
   327   end;
   328 
   329 end;
   330 
   331 
   332 (*** Registrations: interpretations in theories or proof contexts ***)
   333 
   334 structure Idtab = Table(type key = string * term list val ord = ident_ord);
   335 
   336 structure Registrations = Generic_Data
   337 (
   338   type T = ((morphism * morphism) * serial) Idtab.table * mixins;
   339     (* registrations, indexed by locale name and instance;
   340        unique registration serial points to mixin list *)
   341   val empty = (Idtab.empty, Inttab.empty);
   342   val extend = I;
   343   fun merge ((reg1, mix1), (reg2, mix2)) : T =
   344     (Idtab.join (fn id => fn (r1 as (_, s1), r2 as (_, s2)) =>
   345         if s1 = s2 then raise Idtab.SAME else raise Idtab.DUP id) (reg1, reg2),
   346       merge_mixins (mix1, mix2))
   347     handle Idtab.DUP id =>
   348       (* distinct interpretations with same base: merge their mixins *)
   349       let
   350         val (_, s1) = Idtab.lookup reg1 id |> the;
   351         val (morph2, s2) = Idtab.lookup reg2 id |> the;
   352         val reg2' = Idtab.update (id, (morph2, s1)) reg2;
   353         val _ = warning "Removed duplicate interpretation after retrieving its mixins.";
   354         (* FIXME print interpretations,
   355            which is not straightforward without theory context *)
   356       in merge ((reg1, mix1), (reg2', rename_mixin (s2, s1) mix2)) end;
   357     (* FIXME consolidate with dependencies, consider one data slot only *)
   358 );
   359 
   360 
   361 (* Primitive operations *)
   362 
   363 fun add_reg thy export (name, morph) =
   364   Registrations.map (apfst (Idtab.insert (K false)
   365     ((name, instance_of thy name (morph $> export)), ((morph, export), serial ()))));
   366 
   367 fun add_mixin serial' mixin =
   368   (* registration to be amended identified by its serial id *)
   369   Registrations.map (apsnd (insert_mixin serial' mixin));
   370 
   371 fun get_mixins context (name, morph) =
   372   let
   373     val thy = Context.theory_of context;
   374     val (regs, mixins) = Registrations.get context;
   375   in
   376     (case Idtab.lookup regs (name, instance_of thy name morph) of
   377       NONE => []
   378     | SOME (_, serial) => lookup_mixins serial mixins)
   379   end;
   380 
   381 fun collect_mixins context (name, morph) =
   382   let
   383     val thy = Context.theory_of context;
   384   in
   385     roundup thy (fn dep => fn mixins => merge (eq_snd op =) (mixins, get_mixins context dep))
   386       Morphism.identity (name, morph) ([(name, instance_of thy name morph)], [])
   387     |> snd |> filter (snd o fst)  (* only inheritable mixins *)
   388     |> (fn x => merge (eq_snd op =) (x, get_mixins context (name, morph)))
   389     |> compose_mixins
   390   end;
   391 
   392 fun get_registrations context select = Registrations.get context
   393   |>> Idtab.dest |>> select
   394   (* with inherited mixins *)
   395   |-> (fn regs => fn _ => map (fn ((name, _), ((base, export) ,_)) =>
   396     (name, base $> (collect_mixins context (name, base $> export)) $> export)) regs);
   397 
   398 fun registrations_of context name =
   399   get_registrations context (filter (curry (op =) name o fst o fst));
   400 
   401 fun all_registrations context = get_registrations context I;
   402 
   403 
   404 (*** Activate context elements of locale ***)
   405 
   406 (* Declarations, facts and entire locale content *)
   407 
   408 fun activate_syntax_decls (name, morph) context =
   409   let
   410     val thy = Context.theory_of context;
   411     val {syntax_decls, ...} = the_locale thy name;
   412   in
   413     context
   414     |> fold_rev (fn (decl, _) => decl morph) syntax_decls
   415   end;
   416 
   417 fun activate_notes activ_elem transfer context export' (name, morph) input =
   418   let
   419     val thy = Context.theory_of context;
   420     val {notes, ...} = the_locale thy name;
   421     fun activate ((kind, facts), _) input =
   422       let
   423         val mixin =
   424           (case export' of
   425             NONE => Morphism.identity
   426           | SOME export => collect_mixins context (name, morph $> export) $> export);
   427         val facts' = facts
   428           |> Element.facts_map (Element.morph_ctxt (transfer input $> morph $> mixin));
   429       in activ_elem (Notes (kind, facts')) input end;
   430   in
   431     fold_rev activate notes input
   432   end;
   433 
   434 fun activate_all name thy activ_elem transfer (marked, input) =
   435   let
   436     val {parameters = (_, params), spec = (asm, defs), ...} = the_locale thy name;
   437     val input' = input |>
   438       (not (null params) ?
   439         activ_elem (Fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params))) |>
   440       (* FIXME type parameters *)
   441       (case asm of SOME A => activ_elem (Assumes [(Attrib.empty_binding, [(A, [])])]) | _ => I) |>
   442       (not (null defs) ?
   443         activ_elem (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs)));
   444     val activate = activate_notes activ_elem transfer (Context.Theory thy) NONE;
   445   in
   446     roundup thy activate Morphism.identity (name, Morphism.identity) (marked, input')
   447   end;
   448 
   449 
   450 (** Public activation functions **)
   451 
   452 fun activate_declarations dep = Context.proof_map (fn context =>
   453   let
   454     val thy = Context.theory_of context;
   455   in
   456     roundup thy activate_syntax_decls Morphism.identity dep (get_idents context, context)
   457     |-> put_idents
   458   end);
   459 
   460 fun activate_facts export dep context =
   461   let
   462     val thy = Context.theory_of context;
   463     val activate = activate_notes Element.init (Element.transfer_morphism o Context.theory_of) context export;
   464   in
   465     roundup thy activate (case export of NONE => Morphism.identity | SOME export => export)
   466       dep (get_idents context, context)
   467     |-> put_idents
   468   end;
   469 
   470 fun init name thy =
   471   activate_all name thy Element.init (Element.transfer_morphism o Context.theory_of)
   472     ([], Context.Proof (ProofContext.init_global thy)) |-> put_idents |> Context.proof_of;
   473 
   474 
   475 (*** Add and extend registrations ***)
   476 
   477 fun amend_registration (name, morph) mixin export context =
   478   let
   479     val thy = Context.theory_of context;
   480     val regs = Registrations.get context |> fst;
   481     val base = instance_of thy name (morph $> export);
   482   in
   483     (case Idtab.lookup regs (name, base) of
   484       NONE =>
   485         error ("No interpretation of locale " ^
   486           quote (extern thy name) ^ " with\nparameter instantiation " ^
   487           space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
   488           " available")
   489     | SOME (_, serial') => add_mixin serial' mixin context)
   490   end;
   491 
   492 (* Note that a registration that would be subsumed by an existing one will not be
   493    generated, and it will not be possible to amend it. *)
   494 
   495 fun add_registration (name, base_morph) mixin export context =
   496   let
   497     val thy = Context.theory_of context;
   498     val mix = (case mixin of NONE => Morphism.identity | SOME (mix, _) => mix);
   499     val morph = base_morph $> mix;
   500     val inst = instance_of thy name morph;
   501   in
   502     if member (ident_le thy) (get_idents context) (name, inst)
   503     then context  (* FIXME amend mixins? *)
   504     else
   505       (get_idents context, context)
   506       (* add new registrations with inherited mixins *)
   507       |> roundup thy (add_reg thy export) export (name, morph)
   508       |> snd
   509       (* add mixin *)
   510       |>
   511         (case mixin of
   512           NONE => I
   513         | SOME mixin => amend_registration (name, morph) mixin export)
   514       (* activate import hierarchy as far as not already active *)
   515       |> activate_facts (SOME export) (name, morph)
   516   end;
   517 
   518 
   519 (*** Dependencies ***)
   520 
   521 (*
   522 fun amend_dependency loc (name, morph) mixin export thy =
   523   let
   524     val deps = dependencies_of thy loc;
   525   in
   526     case AList.lookup (fn ((name, morph), ((name', (morph', _)), _)) =>
   527       ident_ord ((name, instance_of thy name morph), (name', instance_of thy name' morph')) = EQUAL) deps (name, morph) of
   528         NONE => error ("Locale " ^
   529           quote (extern thy name) ^ " with\parameter instantiation " ^
   530           space_implode " " (map (quote o Syntax.string_of_term_global thy) morph) ^
   531           " not a sublocale of " ^ quote (extern thy loc))
   532       | SOME (_, serial') => change_locale ...
   533   end;
   534 *)
   535 
   536 fun add_dependency loc (name, morph) mixin export thy =
   537   let
   538     val serial' = serial ();
   539     val thy' = thy |>
   540       (change_locale loc o apsnd)
   541         (apfst (cons ((name, (morph, export)), serial')) #>
   542           apsnd (case mixin of NONE => I | SOME mixin => insert_mixin serial' mixin));
   543     val context' = Context.Theory thy';
   544     val (_, regs) = fold_rev (roundup thy' cons export)
   545       (registrations_of context' loc) (get_idents (context'), []);
   546   in
   547     thy'
   548     |> fold_rev (fn dep => Context.theory_map (add_registration dep NONE export)) regs
   549   end;
   550 
   551 
   552 (*** Storing results ***)
   553 
   554 (* Theorems *)
   555 
   556 fun add_thmss loc kind args ctxt =
   557   let
   558     val (Notes args', ctxt') = Element.activate_i (Notes (kind, args)) ctxt;
   559     val ctxt'' = ctxt' |> ProofContext.background_theory
   560      ((change_locale loc o apfst o apsnd) (cons (args', serial ()))
   561         #>
   562       (* Registrations *)
   563       (fn thy => fold_rev (fn (_, morph) =>
   564             let
   565               val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |>
   566                 Attrib.map_facts (Attrib.attribute_i thy)
   567             in Global_Theory.note_thmss kind args'' #> snd end)
   568         (registrations_of (Context.Theory thy) loc) thy))
   569   in ctxt'' end;
   570 
   571 
   572 (* Declarations *)
   573 
   574 fun add_declaration loc decl =
   575   add_thmss loc ""
   576     [((Binding.conceal Binding.empty,
   577         [Attrib.internal (fn phi => Thm.declaration_attribute (K (decl phi)))]),
   578       [([Drule.dummy_thm], [])])];
   579 
   580 fun add_syntax_declaration loc decl =
   581   ProofContext.background_theory ((change_locale loc o apfst o apfst) (cons (decl, serial ())))
   582   #> add_declaration loc decl;
   583 
   584 
   585 (*** Reasoning about locales ***)
   586 
   587 (* Storage for witnesses, intro and unfold rules *)
   588 
   589 structure Thms = Generic_Data
   590 (
   591   type T = thm list * thm list * thm list;
   592   val empty = ([], [], []);
   593   val extend = I;
   594   fun merge ((witnesses1, intros1, unfolds1), (witnesses2, intros2, unfolds2)) =
   595    (Thm.merge_thms (witnesses1, witnesses2),
   596     Thm.merge_thms (intros1, intros2),
   597     Thm.merge_thms (unfolds1, unfolds2));
   598 );
   599 
   600 val get_witnesses = #1 o Thms.get o Context.Proof;
   601 val get_intros = #2 o Thms.get o Context.Proof;
   602 val get_unfolds = #3 o Thms.get o Context.Proof;
   603 
   604 val witness_add =
   605   Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (Thm.add_thm th x, y, z)));
   606 val intro_add =
   607   Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (x, Thm.add_thm th y, z)));
   608 val unfold_add =
   609   Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (x, y, Thm.add_thm th z)));
   610 
   611 
   612 (* Tactics *)
   613 
   614 fun gen_intro_locales_tac intros_tac eager ctxt =
   615   intros_tac
   616     (get_witnesses ctxt @ get_intros ctxt @ (if eager then get_unfolds ctxt else []));
   617 
   618 val intro_locales_tac = gen_intro_locales_tac Method.intros_tac;
   619 val try_intro_locales_tac= gen_intro_locales_tac Method.try_intros_tac;
   620 
   621 val _ = Context.>> (Context.map_theory
   622  (Method.setup (Binding.name "intro_locales") (Scan.succeed (METHOD o try_intro_locales_tac false))
   623     "back-chain introduction rules of locales without unfolding predicates" #>
   624   Method.setup (Binding.name "unfold_locales") (Scan.succeed (METHOD o try_intro_locales_tac true))
   625     "back-chain all introduction rules of locales"));
   626 
   627 
   628 (*** diagnostic commands and interfaces ***)
   629 
   630 val all_locales = Symtab.keys o snd o Locales.get;
   631 
   632 fun print_locales thy =
   633   Pretty.strs ("locales:" :: map #1 (Name_Space.extern_table (Locales.get thy)))
   634   |> Pretty.writeln;
   635 
   636 fun print_locale thy show_facts raw_name =
   637   let
   638     val name = intern thy raw_name;
   639     val ctxt = init name thy;
   640     fun cons_elem (elem as Notes _) = show_facts ? cons elem
   641       | cons_elem elem = cons elem;
   642     val elems =
   643       activate_all name thy cons_elem (K (Element.transfer_morphism thy)) ([], [])
   644       |> snd |> rev;
   645   in
   646     Pretty.big_list "locale elements:" (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)
   647     |> Pretty.writeln
   648   end;
   649 
   650 fun print_registrations ctxt raw_name =
   651   let
   652     val thy = ProofContext.theory_of ctxt;
   653     val name = intern thy raw_name;
   654     val _ = the_locale thy name;  (* error if locale unknown *)
   655   in
   656     (case registrations_of (Context.Proof ctxt) (* FIXME *) name of
   657       [] => Pretty.str ("no interpretations")
   658     | regs => Pretty.big_list "interpretations:" (map (pretty_reg ctxt) (rev regs)))
   659   end |> Pretty.writeln;
   660 
   661 fun print_dependencies ctxt clean export insts =
   662   let
   663     val thy = ProofContext.theory_of ctxt;
   664     val idents = if clean then [] else get_idents (Context.Proof ctxt);
   665   in
   666     (case fold (roundup thy cons export) insts (idents, []) |> snd of
   667       [] => Pretty.str ("no dependencies")
   668     | deps => Pretty.big_list "dependencies:" (map (pretty_reg ctxt) (rev deps)))
   669   end |> Pretty.writeln;
   670 
   671 fun locale_deps thy =
   672   let
   673     val names = all_locales thy
   674     fun add_locale_node name =
   675       let
   676         val params = params_of thy name;
   677         val axioms =
   678           these (Option.map (Logic.strip_imp_prems o Thm.prop_of) (fst (intros_of thy name)));
   679         val registrations =
   680           map (instance_of thy name o snd) (registrations_of (Context.Theory thy) name);
   681       in
   682         Graph.new_node (name, {params = params, axioms = axioms, registrations = registrations})
   683       end;
   684     fun add_locale_deps name =
   685       let
   686         val dependencies =
   687           (map o apsnd) (instance_of thy name o op $>) (dependencies_of thy name |> map fst);
   688       in
   689         fold (fn (super, ts) => fn (gr, deps) => (gr |> Graph.add_edge (super, name),
   690           deps |> Symtab.map_default (super, Symtab.empty) (Symtab.cons_list (name, ts))))
   691             dependencies
   692       end;
   693   in
   694     Graph.empty
   695     |> fold add_locale_node names
   696     |> rpair Symtab.empty
   697     |> fold add_locale_deps names
   698   end;
   699 
   700 end;