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