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