src/Pure/Isar/locale.ML
author haftmann
Mon Nov 29 11:38:59 2010 +0100 (2010-11-29 ago)
changeset 40803 3f66ea311d44
parent 40782 aa533c5e3f48
child 41270 dea60d052923
permissions -rw-r--r--
tuned
     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 -> theory -> theory
    75 
    76   (* Diagnostic *)
    77   val all_locales: theory -> string list
    78   val print_locales: theory -> unit
    79   val print_locale: theory -> bool -> xstring -> unit
    80   val print_registrations: Proof.context -> string -> unit
    81   val locale_deps: theory ->
    82     {params: ((string * typ) * mixfix) list, axioms: term list, registrations: term list list} Graph.T
    83       * term list list Symtab.table Symtab.table
    84 end;
    85 
    86 structure Locale: LOCALE =
    87 struct
    88 
    89 datatype ctxt = datatype Element.ctxt;
    90 
    91 
    92 (*** Locales ***)
    93 
    94 datatype locale = Loc of {
    95   (** static part **)
    96   parameters: (string * sort) list * ((string * typ) * mixfix) list,
    97     (* type and term parameters *)
    98   spec: term option * term list,
    99     (* assumptions (as a single predicate expression) and defines *)
   100   intros: thm option * thm option,
   101   axioms: thm list,
   102   (** dynamic part **)
   103   syntax_decls: (declaration * serial) list,
   104     (* syntax declarations *)
   105   notes: ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * serial) list,
   106     (* theorem declarations *)
   107   dependencies: ((string * (morphism * morphism)) * serial) list
   108     (* locale dependencies (sublocale relation) *)
   109 };
   110 
   111 fun mk_locale ((parameters, spec, intros, axioms), ((syntax_decls, notes), dependencies)) =
   112   Loc {parameters = parameters, intros = intros, axioms = axioms, spec = spec,
   113     syntax_decls = syntax_decls, notes = notes, dependencies = dependencies};
   114 
   115 fun map_locale f (Loc {parameters, spec, intros, axioms, syntax_decls, notes, dependencies}) =
   116   mk_locale (f ((parameters, spec, intros, axioms), ((syntax_decls, notes), dependencies)));
   117 
   118 fun merge_locale
   119  (Loc {parameters, spec, intros, axioms, syntax_decls, notes, dependencies},
   120   Loc {syntax_decls = syntax_decls', notes = notes', dependencies = dependencies', ...}) =
   121     mk_locale
   122       ((parameters, spec, intros, axioms),
   123         ((merge (eq_snd op =) (syntax_decls, syntax_decls'),
   124           merge (eq_snd op =) (notes, notes')),
   125             merge (eq_snd op =) (dependencies, dependencies')));
   126 
   127 structure Locales = Theory_Data
   128 (
   129   type T = locale Name_Space.table;
   130   val empty : T = Name_Space.empty_table "locale";
   131   val extend = I;
   132   val merge = Name_Space.join_tables (K merge_locale);
   133 );
   134 
   135 val intern = Name_Space.intern o #1 o Locales.get;
   136 val extern = Name_Space.extern o #1 o Locales.get;
   137 
   138 val get_locale = Symtab.lookup o #2 o Locales.get;
   139 val defined = Symtab.defined o #2 o Locales.get;
   140 
   141 fun the_locale thy name =
   142   (case get_locale thy name of
   143     SOME (Loc loc) => loc
   144   | NONE => error ("Unknown locale " ^ quote name));
   145 
   146 fun register_locale binding parameters spec intros axioms syntax_decls notes dependencies thy =
   147   thy |> Locales.map (Name_Space.define true (Sign.naming_of thy)
   148     (binding,
   149       mk_locale ((parameters, spec, intros, axioms),
   150         ((map (fn decl => (decl, serial ())) syntax_decls, map (fn n => (n, serial ())) notes),
   151           map (fn d => (d |> apsnd (rpair Morphism.identity), serial ())) dependencies))) #> snd);
   152           (* FIXME *)
   153 
   154 fun change_locale name =
   155   Locales.map o apsnd o Symtab.map_entry name o map_locale o apsnd;
   156 
   157 
   158 (** Primitive operations **)
   159 
   160 fun params_of thy = snd o #parameters o the_locale thy;
   161 
   162 fun intros_of thy = #intros o the_locale thy;
   163 
   164 fun axioms_of thy = #axioms o the_locale thy;
   165 
   166 fun instance_of thy name morph = params_of thy name |>
   167   map (Morphism.term morph o Free o #1);
   168 
   169 fun specification_of thy = #spec o the_locale thy;
   170 
   171 fun dependencies_of thy name = the_locale thy name |>
   172   #dependencies |> map fst;
   173 
   174 (* Print instance and qualifiers *)
   175 
   176 fun pretty_reg thy (name, morph) =
   177   let
   178     val name' = extern thy name;
   179     val ctxt = ProofContext.init_global thy;
   180     fun prt_qual (qual, mand) = Pretty.str (qual ^ (if mand then "!" else "?"));
   181     fun prt_quals qs = Pretty.separate "." (map prt_qual qs) |> Pretty.block;
   182     val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
   183     fun prt_term' t =
   184       if Config.get ctxt show_types
   185       then Pretty.block [prt_term t, Pretty.brk 1, Pretty.str "::",
   186         Pretty.brk 1, (Pretty.quote o Syntax.pretty_typ ctxt) (type_of t)]
   187       else prt_term t;
   188     fun prt_inst ts =
   189       Pretty.block (Pretty.breaks (Pretty.str name' :: map prt_term' ts));
   190 
   191     val qs = Binding.name "x" |> Morphism.binding morph |> Binding.prefix_of;
   192     val ts = instance_of thy name morph;
   193   in
   194     (case qs of
   195       [] => prt_inst ts
   196     | qs => Pretty.block [prt_quals qs, Pretty.brk 1, Pretty.str ":", Pretty.brk 1, prt_inst ts])
   197   end;
   198 
   199 
   200 (*** Identifiers: activated locales in theory or proof context ***)
   201 
   202 (* subsumption *)
   203 fun ident_le thy ((n: string, ts), (m, ss)) = (m = n) andalso Pattern.matchess thy (ss, ts);
   204   (* smaller term is more general *)
   205 
   206 (* total order *)
   207 fun ident_ord ((n: string, ts), (m, ss)) =
   208   (case fast_string_ord (m, n) of
   209     EQUAL => list_ord Term_Ord.fast_term_ord (ts, ss)
   210   | ord => ord);
   211 
   212 local
   213 
   214 datatype 'a delayed = Ready of 'a | ToDo of 'a delayed * 'a delayed;
   215 
   216 structure Identifiers = Generic_Data
   217 (
   218   type T = (string * term list) list delayed;
   219   val empty = Ready [];
   220   val extend = I;
   221   val merge = ToDo;
   222 );
   223 
   224 fun finish thy (ToDo (i1, i2)) = merge (ident_le thy) (finish thy i1, finish thy i2)
   225   | finish _ (Ready ids) = ids;
   226 
   227 val _ = Context.>> (Context.map_theory (Theory.at_begin (fn thy =>
   228   (case Identifiers.get (Context.Theory thy) of
   229     Ready _ => NONE
   230   | ids => SOME (Context.theory_map (Identifiers.put (Ready (finish thy ids))) thy)))));
   231 
   232 in
   233 
   234 val get_idents = (fn Ready ids => ids) o Identifiers.get;
   235 val put_idents = Identifiers.put o Ready;
   236 
   237 end;
   238 
   239 
   240 (** Resolve locale dependencies in a depth-first fashion **)
   241 
   242 local
   243 
   244 val roundup_bound = 120;
   245 
   246 fun add thy depth export (name, morph) (deps, marked) =
   247   if depth > roundup_bound
   248   then error "Roundup bound exceeded (sublocale relation probably not terminating)."
   249   else
   250     let
   251       val dependencies = dependencies_of thy name;
   252       val instance = instance_of thy name (morph $> export);
   253     in
   254       if member (ident_le thy) marked (name, instance)
   255       then (deps, marked)
   256       else
   257         let
   258           val dependencies' =
   259             map (fn (name, (morph', export')) => (name, morph' $> export' $> morph)) dependencies;
   260           val marked' = (name, instance) :: marked;
   261           val (deps', marked'') = fold_rev (add thy (depth + 1) export) dependencies' ([], marked');
   262         in
   263           ((name, morph) :: deps' @ deps, marked'')
   264         end
   265     end;
   266 
   267 in
   268 
   269 (* Note that while identifiers always have the external (exported) view, activate_dep
   270   is presented with the internal view. *)
   271 
   272 fun roundup thy activate_dep export (name, morph) (marked, input) =
   273   let
   274     (* Find all dependencies incuding new ones (which are dependencies enriching
   275       existing registrations). *)
   276     val (dependencies, marked') = add thy 0 export (name, morph) ([], []);
   277     (* Filter out fragments from marked; these won't be activated. *)
   278     val dependencies' = filter_out (fn (name, morph) =>
   279       member (ident_le thy) marked (name, instance_of thy name (morph $> export))) dependencies;
   280   in
   281     (merge (ident_le thy) (marked, marked'), input |> fold_rev activate_dep dependencies')
   282   end;
   283 
   284 end;
   285 
   286 
   287 (*** Registrations: interpretations in theories or proof contexts ***)
   288 
   289 structure Idtab = Table(type key = string * term list val ord = ident_ord);
   290 
   291 structure Registrations = Generic_Data
   292 (
   293   type T = ((morphism * morphism) * serial) Idtab.table *
   294     (* registrations, indexed by locale name and instance;
   295        serial points to mixin list *)
   296     (((morphism * bool) * serial) list) Inttab.table;
   297     (* table of mixin lists, per list mixins in reverse order of declaration;
   298        lists indexed by registration serial,
   299        entries for empty lists may be omitted *)
   300   val empty = (Idtab.empty, Inttab.empty);
   301   val extend = I;
   302   fun merge ((reg1, mix1), (reg2, mix2)) : T =
   303     (Idtab.join (fn id => fn (r1 as (_, s1), r2 as (_, s2)) =>
   304         if s1 = s2 then raise Idtab.SAME else raise Idtab.DUP id) (reg1, reg2),
   305       Inttab.join (K (Library.merge (eq_snd op =))) (mix1, mix2))
   306     handle Idtab.DUP id =>
   307       (* distinct interpretations with same base: merge their mixins *)
   308       let
   309         val (_, s1) = Idtab.lookup reg1 id |> the;
   310         val (morph2, s2) = Idtab.lookup reg2 id |> the;
   311         val reg2' = Idtab.update (id, (morph2, s1)) reg2;
   312         val mix2' =
   313           (case Inttab.lookup mix2 s2 of
   314             NONE => mix2
   315           | SOME mxs => Inttab.delete s2 mix2 |> Inttab.update_new (s1, mxs));
   316         val _ = warning "Removed duplicate interpretation after retrieving its mixins.";
   317         (* FIXME print interpretations,
   318            which is not straightforward without theory context *)
   319       in merge ((reg1, mix1), (reg2', mix2')) end;
   320     (* FIXME consolidate with dependencies, consider one data slot only *)
   321 );
   322 
   323 
   324 (* Primitive operations *)
   325 
   326 fun add_reg thy export (name, morph) =
   327   Registrations.map (apfst (Idtab.insert (K false)
   328     ((name, instance_of thy name (morph $> export)), ((morph, export), serial ()))));
   329 
   330 fun add_mixin serial' mixin =
   331   (* registration to be amended identified by its serial id *)
   332   Registrations.map (apsnd (Inttab.map_default (serial', []) (cons (mixin, serial ()))));
   333 
   334 fun get_mixins context (name, morph) =
   335   let
   336     val thy = Context.theory_of context;
   337     val (regs, mixins) = Registrations.get context;
   338   in
   339     (case Idtab.lookup regs (name, instance_of thy name morph) of
   340       NONE => []
   341     | SOME (_, serial) => the_default [] (Inttab.lookup mixins serial))
   342   end;
   343 
   344 fun compose_mixins mixins =
   345   fold_rev Morphism.compose (map (fst o fst) mixins) Morphism.identity;
   346 
   347 fun collect_mixins context (name, morph) =
   348   let
   349     val thy = Context.theory_of context;
   350   in
   351     roundup thy (fn dep => fn mixins => merge (eq_snd op =) (mixins, get_mixins context dep))
   352       Morphism.identity (name, morph) ([(name, instance_of thy name morph)], [])
   353     |> snd |> filter (snd o fst)  (* only inheritable mixins *)
   354     |> (fn x => merge (eq_snd op =) (x, get_mixins context (name, morph)))
   355     |> compose_mixins
   356   end;
   357 
   358 fun get_registrations context select = Registrations.get context
   359   |>> Idtab.dest |>> select
   360   (* with inherited mixins *)
   361   |-> (fn regs => fn _ => map (fn ((name, _), ((base, export) ,_)) =>
   362     (name, base $> (collect_mixins context (name, base $> export)) $> export)) regs);
   363 
   364 fun registrations_of context name =
   365   get_registrations context (filter (curry (op =) name o fst o fst));
   366 
   367 fun all_registrations context = get_registrations context I;
   368 
   369 
   370 (*** Activate context elements of locale ***)
   371 
   372 (* Declarations, facts and entire locale content *)
   373 
   374 fun activate_syntax_decls (name, morph) context =
   375   let
   376     val thy = Context.theory_of context;
   377     val {syntax_decls, ...} = the_locale thy name;
   378   in
   379     context
   380     |> fold_rev (fn (decl, _) => decl morph) syntax_decls
   381   end;
   382 
   383 fun activate_notes activ_elem transfer context export' (name, morph) input =
   384   let
   385     val thy = Context.theory_of context;
   386     val {notes, ...} = the_locale thy name;
   387     fun activate ((kind, facts), _) input =
   388       let
   389         val mixin =
   390           (case export' of
   391             NONE => Morphism.identity
   392           | SOME export => collect_mixins context (name, morph $> export) $> export);
   393         val facts' = facts
   394           |> Element.facts_map (Element.morph_ctxt (transfer input $> morph $> mixin));
   395       in activ_elem (Notes (kind, facts')) input end;
   396   in
   397     fold_rev activate notes input
   398   end;
   399 
   400 fun activate_all name thy activ_elem transfer (marked, input) =
   401   let
   402     val {parameters = (_, params), spec = (asm, defs), ...} = the_locale thy name;
   403     val input' = input |>
   404       (not (null params) ?
   405         activ_elem (Fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params))) |>
   406       (* FIXME type parameters *)
   407       (case asm of SOME A => activ_elem (Assumes [(Attrib.empty_binding, [(A, [])])]) | _ => I) |>
   408       (not (null defs) ?
   409         activ_elem (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs)));
   410     val activate = activate_notes activ_elem transfer (Context.Theory thy) NONE;
   411   in
   412     roundup thy activate Morphism.identity (name, Morphism.identity) (marked, input')
   413   end;
   414 
   415 
   416 (** Public activation functions **)
   417 
   418 fun activate_declarations dep = Context.proof_map (fn context =>
   419   let
   420     val thy = Context.theory_of context;
   421   in
   422     roundup thy activate_syntax_decls Morphism.identity dep (get_idents context, context)
   423     |-> put_idents
   424   end);
   425 
   426 fun activate_facts export dep context =
   427   let
   428     val thy = Context.theory_of context;
   429     val activate = activate_notes Element.init (Element.transfer_morphism o Context.theory_of) context export;
   430   in
   431     roundup thy activate (case export of NONE => Morphism.identity | SOME export => export)
   432       dep (get_idents context, context)
   433     |-> put_idents
   434   end;
   435 
   436 fun init name thy =
   437   activate_all name thy Element.init (Element.transfer_morphism o Context.theory_of)
   438     ([], Context.Proof (ProofContext.init_global thy)) |-> put_idents |> Context.proof_of;
   439 
   440 
   441 (*** Add and extend registrations ***)
   442 
   443 fun amend_registration (name, morph) mixin export context =
   444   let
   445     val thy = Context.theory_of context;
   446     val regs = Registrations.get context |> fst;
   447     val base = instance_of thy name (morph $> export);
   448   in
   449     (case Idtab.lookup regs (name, base) of
   450       NONE =>
   451         error ("No interpretation of locale " ^
   452           quote (extern thy name) ^ " and\nparameter instantiation " ^
   453           space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
   454           " available")
   455     | SOME (_, serial') => add_mixin serial' mixin context)
   456   end;
   457 
   458 (* Note that a registration that would be subsumed by an existing one will not be
   459    generated, and it will not be possible to amend it. *)
   460 
   461 fun add_registration (name, base_morph) mixin export context =
   462   let
   463     val thy = Context.theory_of context;
   464     val mix = (case mixin of NONE => Morphism.identity | SOME (mix, _) => mix);
   465     val morph = base_morph $> mix;
   466     val inst = instance_of thy name morph;
   467   in
   468     if member (ident_le thy) (get_idents context) (name, inst)
   469     then context
   470     else
   471       (get_idents context, context)
   472       (* add new registrations with inherited mixins *)
   473       |> roundup thy (add_reg thy export) export (name, morph)
   474       |> snd
   475       (* add mixin *)
   476       |>
   477         (case mixin of
   478           NONE => I
   479         | SOME mixin => amend_registration (name, morph) mixin export)
   480       (* activate import hierarchy as far as not already active *)
   481       |> activate_facts (SOME export) (name, morph)
   482   end;
   483 
   484 
   485 (*** Dependencies ***)
   486 
   487 fun add_dependency loc (name, morph) export thy =
   488   let
   489     val thy' = (change_locale loc o apsnd) (cons ((name, (morph, export)), serial ())) thy;
   490     val context' = Context.Theory thy';
   491     val (_, regs) = fold_rev (roundup thy' cons export)
   492       (registrations_of context' loc) (get_idents (context'), []);
   493   in
   494     thy'
   495     |> fold_rev (fn dep => Context.theory_map (add_registration dep NONE export)) regs
   496   end;
   497 
   498 
   499 (*** Storing results ***)
   500 
   501 (* Theorems *)
   502 
   503 fun add_thmss loc kind args ctxt =
   504   let
   505     val (Notes args', ctxt') = Element.activate_i (Notes (kind, args)) ctxt;
   506     val ctxt'' = ctxt' |> ProofContext.background_theory
   507      ((change_locale loc o apfst o apsnd) (cons (args', serial ()))
   508         #>
   509       (* Registrations *)
   510       (fn thy => fold_rev (fn (_, morph) =>
   511             let
   512               val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |>
   513                 Attrib.map_facts (Attrib.attribute_i thy)
   514             in Global_Theory.note_thmss kind args'' #> snd end)
   515         (registrations_of (Context.Theory thy) loc) thy))
   516   in ctxt'' end;
   517 
   518 
   519 (* Declarations *)
   520 
   521 fun add_declaration loc decl =
   522   add_thmss loc ""
   523     [((Binding.conceal Binding.empty,
   524         [Attrib.internal (fn phi => Thm.declaration_attribute (K (decl phi)))]),
   525       [([Drule.dummy_thm], [])])];
   526 
   527 fun add_syntax_declaration loc decl =
   528   ProofContext.background_theory ((change_locale loc o apfst o apfst) (cons (decl, serial ())))
   529   #> add_declaration loc decl;
   530 
   531 
   532 (*** Reasoning about locales ***)
   533 
   534 (* Storage for witnesses, intro and unfold rules *)
   535 
   536 structure Thms = Generic_Data
   537 (
   538   type T = thm list * thm list * thm list;
   539   val empty = ([], [], []);
   540   val extend = I;
   541   fun merge ((witnesses1, intros1, unfolds1), (witnesses2, intros2, unfolds2)) =
   542    (Thm.merge_thms (witnesses1, witnesses2),
   543     Thm.merge_thms (intros1, intros2),
   544     Thm.merge_thms (unfolds1, unfolds2));
   545 );
   546 
   547 val get_witnesses = #1 o Thms.get o Context.Proof;
   548 val get_intros = #2 o Thms.get o Context.Proof;
   549 val get_unfolds = #3 o Thms.get o Context.Proof;
   550 
   551 val witness_add =
   552   Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (Thm.add_thm th x, y, z)));
   553 val intro_add =
   554   Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (x, Thm.add_thm th y, z)));
   555 val unfold_add =
   556   Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (x, y, Thm.add_thm th z)));
   557 
   558 
   559 (* Tactics *)
   560 
   561 fun gen_intro_locales_tac intros_tac eager ctxt =
   562   intros_tac
   563     (get_witnesses ctxt @ get_intros ctxt @ (if eager then get_unfolds ctxt else []));
   564 
   565 val intro_locales_tac = gen_intro_locales_tac Method.intros_tac;
   566 val try_intro_locales_tac= gen_intro_locales_tac Method.try_intros_tac;
   567 
   568 val _ = Context.>> (Context.map_theory
   569  (Method.setup (Binding.name "intro_locales") (Scan.succeed (METHOD o try_intro_locales_tac false))
   570     "back-chain introduction rules of locales without unfolding predicates" #>
   571   Method.setup (Binding.name "unfold_locales") (Scan.succeed (METHOD o try_intro_locales_tac true))
   572     "back-chain all introduction rules of locales"));
   573 
   574 
   575 (*** diagnostic commands and interfaces ***)
   576 
   577 val all_locales = Symtab.keys o snd o Locales.get;
   578 
   579 fun print_locales thy =
   580   Pretty.strs ("locales:" :: map #1 (Name_Space.extern_table (Locales.get thy)))
   581   |> Pretty.writeln;
   582 
   583 fun print_locale thy show_facts raw_name =
   584   let
   585     val name = intern thy raw_name;
   586     val ctxt = init name thy;
   587     fun cons_elem (elem as Notes _) = show_facts ? cons elem
   588       | cons_elem elem = cons elem;
   589     val elems =
   590       activate_all name thy cons_elem (K (Element.transfer_morphism thy)) ([], [])
   591       |> snd |> rev;
   592   in
   593     Pretty.big_list "locale elements:" (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)
   594     |> Pretty.writeln
   595   end;
   596 
   597 fun print_registrations ctxt raw_name =
   598   let
   599     val thy = ProofContext.theory_of ctxt;
   600   in
   601     (case registrations_of (Context.Proof ctxt) (* FIXME *) (intern thy raw_name) of
   602       [] => Pretty.str ("no interpretations")
   603     | regs => Pretty.big_list "interpretations:" (map (pretty_reg thy) (rev regs)))
   604   end |> Pretty.writeln;
   605 
   606 fun locale_deps thy =
   607   let
   608     val names = all_locales thy
   609     fun add_locale_node name =
   610       let
   611         val params = params_of thy name;
   612         val axioms =
   613           these (Option.map (Logic.strip_imp_prems o Thm.prop_of) (fst (intros_of thy name)));
   614         val registrations =
   615           map (instance_of thy name o snd) (registrations_of (Context.Theory thy) name);
   616       in
   617         Graph.new_node (name, {params = params, axioms = axioms, registrations = registrations})
   618       end;
   619     fun add_locale_deps name =
   620       let
   621         val dependencies =
   622           (map o apsnd) (instance_of thy name o op $>) (dependencies_of thy name);
   623       in
   624         fold (fn (super, ts) => fn (gr, deps) => (gr |> Graph.add_edge (super, name),
   625           deps |> Symtab.map_default (super, Symtab.empty) (Symtab.cons_list (name, ts))))
   626             dependencies
   627       end;
   628   in
   629     Graph.empty
   630     |> fold add_locale_node names
   631     |> rpair Symtab.empty
   632     |> fold add_locale_deps names
   633   end;
   634 
   635 end;