src/Pure/Isar/locale.ML
author wenzelm
Thu Mar 19 13:28:55 2009 +0100 (2009-03-19)
changeset 30585 6b2ba4666336
parent 30515 bca05b17b618
child 30725 c23a5b3cd1b9
permissions -rw-r--r--
use Name.of_binding for basic logical entities without name space (fixes, case names etc.);
     1 (*  Title:      Pure/Isar/locale.ML
     2     Author:     Clemens Ballarin, TU Muenchen
     3 
     4 Locales -- Isar proof contexts as meta-level predicates, with local
     5 syntax and implicit structures.
     6 
     7 Draws basic ideas from Florian Kammueller's original version of
     8 locales, but uses the richer infrastructure of Isar instead of the raw
     9 meta-logic.  Furthermore, structured import of contexts (with merge
    10 and rename operations) are provided, as well as type-inference of the
    11 signature parts, and predicate definitions of the specification text.
    12 
    13 Interpretation enables the reuse of theorems of locales in other
    14 contexts, namely those defined by theories, structured proofs and
    15 locales themselves.
    16 
    17 See also:
    18 
    19 [1] Clemens Ballarin. Locales and Locale Expressions in Isabelle/Isar.
    20     In Stefano Berardi et al., Types for Proofs and Programs: International
    21     Workshop, TYPES 2003, Torino, Italy, LNCS 3085, pages 34-50, 2004.
    22 [2] Clemens Ballarin. Interpretation of Locales in Isabelle: Managing
    23     Dependencies between Locales. Technical Report TUM-I0607, Technische
    24     Universitaet Muenchen, 2006.
    25 [3] Clemens Ballarin. Interpretation of Locales in Isabelle: Theories and
    26     Proof Contexts. In J.M. Borwein and W.M. Farmer, MKM 2006, LNAI 4108,
    27     pages 31-43, 2006.
    28 *)
    29 
    30 signature LOCALE =
    31 sig
    32   (* Locale specification *)
    33   val register_locale: binding ->
    34     (string * sort) list * (binding * typ option * mixfix) list ->
    35     term option * term list ->
    36     thm option * thm option -> thm list ->
    37     (declaration * stamp) list * (declaration * stamp) list ->
    38     ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * stamp) list ->
    39     ((string * morphism) * stamp) list -> theory -> theory
    40   val intern: theory -> xstring -> string
    41   val extern: theory -> string -> xstring
    42   val defined: theory -> string -> bool
    43   val params_of: theory -> string -> (binding * typ option * 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   val declarations_of: theory -> string -> declaration list * declaration list
    49   val dependencies_of: theory -> string -> (string * morphism) list
    50 
    51   (* Storing results *)
    52   val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
    53     Proof.context -> Proof.context
    54   val add_type_syntax: string -> declaration -> Proof.context -> Proof.context
    55   val add_term_syntax: string -> declaration -> Proof.context -> Proof.context
    56   val add_declaration: string -> declaration -> Proof.context -> Proof.context
    57   val add_dependency: string -> string * morphism -> theory -> theory
    58 
    59   (* Activation *)
    60   val activate_declarations: theory -> string * morphism ->
    61     Proof.context -> Proof.context
    62   val activate_global_facts: string * morphism -> theory -> theory
    63   val activate_local_facts: string * morphism -> Proof.context -> Proof.context
    64   val init: string -> theory -> Proof.context
    65 
    66   (* Reasoning about locales *)
    67   val witness_attrib: attribute
    68   val intro_attrib: attribute
    69   val unfold_attrib: attribute
    70   val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
    71 
    72   (* Registrations *)
    73   val add_registration: string * (morphism * morphism) ->
    74     theory -> theory
    75   val amend_registration: morphism -> string * morphism ->
    76     theory -> theory
    77   val get_registrations: theory -> (string * morphism) list
    78 
    79   (* Diagnostic *)
    80   val print_locales: theory -> unit
    81   val print_locale: theory -> bool -> xstring -> unit
    82 end;
    83 
    84 
    85 (*** Theorem list extensible via attribute --- to control intro_locales_tac ***)
    86 
    87 (* FIXME: consider moving named_thms.ML up in the build hierarchy and using that *)
    88 functor ThmsFun() =
    89 struct
    90 
    91 structure Data = GenericDataFun
    92 (
    93   type T = thm list;
    94   val empty = [];
    95   val extend = I;
    96   fun merge _ = Thm.merge_thms;
    97 );
    98 
    99 val get = Data.get o Context.Proof;
   100 val add = Thm.declaration_attribute (Data.map o Thm.add_thm);
   101 
   102 end;
   103 
   104 
   105 structure Locale: LOCALE =
   106 struct
   107 
   108 datatype ctxt = datatype Element.ctxt;
   109 
   110 
   111 (*** Theory data ***)
   112 
   113 datatype locale = Loc of {
   114   (** static part **)
   115   parameters: (string * sort) list * (binding * typ option * mixfix) list,
   116     (* type and term parameters *)
   117   spec: term option * term list,
   118     (* assumptions (as a single predicate expression) and defines *)
   119   intros: thm option * thm option,
   120   axioms: thm list,
   121   (** dynamic part **)
   122   decls: (declaration * stamp) list * (declaration * stamp) list,
   123     (* type and term syntax declarations *)
   124   notes: ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * stamp) list,
   125     (* theorem declarations *)
   126   dependencies: ((string * morphism) * stamp) list
   127     (* locale dependencies (sublocale relation) *)
   128 };
   129 
   130 fun mk_locale ((parameters, spec, intros, axioms), ((decls, notes), dependencies)) =
   131   Loc {parameters = parameters, intros = intros, axioms = axioms, spec = spec,
   132     decls = decls, notes = notes, dependencies = dependencies};
   133 fun map_locale f (Loc {parameters, spec, intros, axioms, decls, notes, dependencies}) =
   134   mk_locale (f ((parameters, spec, intros, axioms), ((decls, notes), dependencies)));
   135 fun merge_locale (Loc {parameters, spec, intros, axioms, decls = (decls1, decls2),
   136   notes, dependencies}, Loc {decls = (decls1', decls2'), notes = notes',
   137     dependencies = dependencies', ...}) = mk_locale
   138       ((parameters, spec, intros, axioms),
   139         (((merge (eq_snd op =) (decls1, decls1'), merge (eq_snd op =) (decls2, decls2')),
   140           merge (eq_snd op =) (notes, notes')),
   141             merge (eq_snd op =) (dependencies, dependencies')));
   142 
   143 structure LocalesData = TheoryDataFun
   144 (
   145   type T = locale NameSpace.table;
   146   val empty = NameSpace.empty_table;
   147   val copy = I;
   148   val extend = I;
   149   fun merge _ = NameSpace.join_tables (K merge_locale);
   150 );
   151 
   152 val intern = NameSpace.intern o #1 o LocalesData.get;
   153 val extern = NameSpace.extern o #1 o LocalesData.get;
   154 
   155 fun get_locale thy = Symtab.lookup (#2 (LocalesData.get thy));
   156 
   157 fun defined thy = is_some o get_locale thy;
   158 
   159 fun the_locale thy name = case get_locale thy name
   160  of SOME (Loc loc) => loc
   161   | NONE => error ("Unknown locale " ^ quote name);
   162 
   163 fun register_locale binding parameters spec intros axioms decls notes dependencies thy =
   164   thy |> LocalesData.map (NameSpace.define (Sign.naming_of thy) (binding,
   165     mk_locale ((parameters, spec, intros, axioms), ((decls, notes), dependencies))) #> snd);
   166 
   167 fun change_locale name =
   168   LocalesData.map o apsnd o Symtab.map_entry name o map_locale o apsnd;
   169 
   170 fun print_locales thy =
   171   Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (LocalesData.get thy)))
   172   |> Pretty.writeln;
   173 
   174 
   175 (*** Primitive operations ***)
   176 
   177 fun params_of thy = snd o #parameters o the_locale thy;
   178 
   179 fun intros_of thy = #intros o the_locale thy;
   180 
   181 fun axioms_of thy = #axioms o the_locale thy;
   182 
   183 fun instance_of thy name morph = params_of thy name |>
   184   map ((fn (b, T, _) => Free (Name.of_binding b, the T)) #> Morphism.term morph);
   185 
   186 fun specification_of thy = #spec o the_locale thy;
   187 
   188 fun declarations_of thy name = the_locale thy name |>
   189   #decls |> apfst (map fst) |> apsnd (map fst);
   190 
   191 fun dependencies_of thy name = the_locale thy name |>
   192   #dependencies |> map fst;
   193 
   194 
   195 (*** Activate context elements of locale ***)
   196 
   197 (** Identifiers: activated locales in theory or proof context **)
   198 
   199 type identifiers = (string * term list) list;
   200 
   201 val empty = ([] : identifiers);
   202 
   203 fun ident_eq thy ((n: string, ts), (m, ss)) = (m = n) andalso Pattern.matchess thy (ss, ts);
   204 
   205 local
   206 
   207 datatype 'a delayed = Ready of 'a | ToDo of ('a delayed * 'a delayed);
   208 
   209 structure IdentifiersData = GenericDataFun
   210 (
   211   type T = identifiers delayed;
   212   val empty = Ready empty;
   213   val extend = I;
   214   fun merge _ = ToDo;
   215 );
   216 
   217 in
   218 
   219 fun finish thy (ToDo (i1, i2)) = merge (ident_eq thy) (finish thy i1, finish thy i2)
   220   | finish _ (Ready ids) = ids;
   221 
   222 val _ = Context.>> (Context.map_theory (Theory.at_begin (fn thy =>
   223   (case IdentifiersData.get (Context.Theory thy) of
   224     Ready _ => NONE |
   225     ids => SOME (Context.theory_map (IdentifiersData.put (Ready (finish thy ids))) thy))
   226   )));
   227 
   228 fun get_global_idents thy =
   229   let val (Ready ids) = (IdentifiersData.get o Context.Theory) thy in ids end;
   230 val put_global_idents = Context.theory_map o IdentifiersData.put o Ready;
   231 
   232 fun get_local_idents ctxt =
   233   let val (Ready ids) = (IdentifiersData.get o Context.Proof) ctxt in ids end;
   234 val put_local_idents = Context.proof_map o IdentifiersData.put o Ready;
   235 
   236 end;
   237 
   238 
   239 (** Resolve locale dependencies in a depth-first fashion **)
   240 
   241 local
   242 
   243 val roundup_bound = 120;
   244 
   245 fun add thy depth (name, morph) (deps, marked) =
   246   if depth > roundup_bound
   247   then error "Roundup bound exceeded (sublocale relation probably not terminating)."
   248   else
   249     let
   250       val {parameters = (_, params), dependencies, ...} = the_locale thy name;
   251       val instance = instance_of thy name morph;
   252     in
   253       if member (ident_eq thy) marked (name, instance)
   254       then (deps, marked)
   255       else
   256         let
   257           val dependencies' =
   258             map (fn ((name, morph'), _) => (name, morph' $>  morph)) dependencies;
   259           val marked' = (name, instance) :: marked;
   260           val (deps', marked'') = fold_rev (add thy (depth + 1)) dependencies' ([], marked');
   261         in
   262           ((name, morph) :: deps' @ deps, marked'')
   263         end
   264     end;
   265 
   266 in
   267 
   268 fun roundup thy activate_dep (name, morph) (marked, input) =
   269   let
   270     (* Find all dependencies incuding new ones (which are dependencies enriching
   271       existing registrations). *)
   272     val (dependencies, marked') = add thy 0 (name, morph) ([], empty);
   273     (* Filter out exisiting fragments. *)
   274     val dependencies' = filter_out (fn (name, morph) =>
   275       member (ident_eq thy) marked (name, instance_of thy name morph)) dependencies;
   276   in
   277     (merge (ident_eq thy) (marked, marked'), input |> fold_rev (activate_dep thy) dependencies')
   278   end;
   279 
   280 end;
   281 
   282 
   283 (* Declarations, facts and entire locale content *)
   284 
   285 fun activate_decls thy (name, morph) ctxt =
   286   let
   287     val {decls = (typ_decls, term_decls), ...} = the_locale thy name;
   288   in
   289     ctxt |> fold_rev (fn (decl, _) => Context.proof_map (decl morph)) typ_decls |>
   290       fold_rev (fn (decl, _) => Context.proof_map (decl morph)) term_decls
   291   end;
   292 
   293 fun activate_notes activ_elem transfer thy (name, morph) input =
   294   let
   295     val {notes, ...} = the_locale thy name;
   296     fun activate ((kind, facts), _) input =
   297       let
   298         val facts' = facts |> Element.facts_map (Element.morph_ctxt (transfer input $> morph))
   299       in activ_elem (Notes (kind, facts')) input end;
   300   in
   301     fold_rev activate notes input
   302   end;
   303 
   304 fun activate_all name thy activ_elem transfer (marked, input) =
   305   let
   306     val {parameters = (_, params), spec = (asm, defs), ...} =
   307       the_locale thy name;
   308   in
   309     input |>
   310       (if not (null params) then activ_elem (Fixes params) else I) |>
   311       (* FIXME type parameters *)
   312       (if is_some asm then activ_elem (Assumes [(Attrib.empty_binding, [(the asm, [])])]) else I) |>
   313       (if not (null defs)
   314         then activ_elem (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs))
   315         else I) |>
   316       pair marked |> roundup thy (activate_notes activ_elem transfer) (name, Morphism.identity)
   317   end;
   318 
   319 
   320 (** Public activation functions **)
   321 
   322 local
   323 
   324 fun init_global_elem (Notes (kind, facts)) thy =
   325   let
   326     val facts' = Attrib.map_facts (Attrib.attribute_i thy) facts
   327   in PureThy.note_thmss kind facts' thy |> snd end
   328 
   329 fun init_local_elem (Fixes fixes) ctxt = ctxt |>
   330       ProofContext.add_fixes_i fixes |> snd
   331   | init_local_elem (Assumes assms) ctxt =
   332       let
   333         val assms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) assms
   334       in
   335         ctxt |> fold Variable.auto_fixes (maps (map fst o snd) assms') |>
   336           ProofContext.add_assms_i Assumption.assume_export assms' |> snd
   337      end
   338   | init_local_elem (Defines defs) ctxt =
   339       let
   340         val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs
   341       in
   342         ctxt |> fold Variable.auto_fixes (map (fst o snd) defs') |>
   343           ProofContext.add_assms_i LocalDefs.def_export (map (fn (attn, t) => (attn, [t])) defs') |>
   344           snd
   345       end
   346   | init_local_elem (Notes (kind, facts)) ctxt =
   347       let
   348         val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts
   349       in ProofContext.note_thmss_i kind facts' ctxt |> snd end
   350 
   351 fun cons_elem false (Notes notes) elems = elems
   352   | cons_elem _ elem elems = elem :: elems
   353 
   354 in
   355 
   356 fun activate_declarations thy dep ctxt =
   357   roundup thy activate_decls dep (get_local_idents ctxt, ctxt) |-> put_local_idents;
   358 
   359 fun activate_global_facts dep thy =
   360   roundup thy (activate_notes init_global_elem Element.transfer_morphism)
   361     dep (get_global_idents thy, thy) |-> put_global_idents;
   362 
   363 fun activate_local_facts dep ctxt =
   364   roundup (ProofContext.theory_of ctxt)
   365   (activate_notes init_local_elem (Element.transfer_morphism o ProofContext.theory_of)) dep
   366     (get_local_idents ctxt, ctxt) |-> put_local_idents;
   367 
   368 fun init name thy =
   369   activate_all name thy init_local_elem (Element.transfer_morphism o ProofContext.theory_of)
   370     (empty, ProofContext.init thy) |-> put_local_idents;
   371 
   372 fun print_locale thy show_facts name =
   373   let
   374     val name' = intern thy name;
   375     val ctxt = init name' thy
   376   in
   377     Pretty.big_list "locale elements:"
   378       (activate_all name' thy (cons_elem show_facts) (K (Element.transfer_morphism thy))
   379         (empty, []) |> snd |> rev |>
   380         map (Element.pretty_ctxt ctxt) |> map Pretty.chunks) |> Pretty.writeln
   381   end
   382 
   383 end;
   384 
   385 
   386 (*** Registrations: interpretations in theories ***)
   387 
   388 structure RegistrationsData = TheoryDataFun
   389 (
   390   type T = ((string * (morphism * morphism)) * stamp) list;
   391     (* FIXME mixins need to be stamped *)
   392     (* registrations, in reverse order of declaration *)
   393   val empty = [];
   394   val extend = I;
   395   val copy = I;
   396   fun merge _ data : T = Library.merge (eq_snd op =) data;
   397     (* FIXME consolidate with dependencies, consider one data slot only *)
   398 );
   399 
   400 val get_registrations =
   401   RegistrationsData.get #> map fst #> map (apsnd op $>);
   402 
   403 fun add_registration (name, (base_morph, export)) thy =
   404   roundup thy (fn _ => fn (name', morph') =>
   405     (RegistrationsData.map o cons) ((name', (morph', export)), stamp ()))
   406     (name, base_morph) (get_global_idents thy, thy) |> snd
   407     (* FIXME |-> put_global_idents ?*);
   408 
   409 fun amend_registration morph (name, base_morph) thy =
   410   let
   411     val regs = (RegistrationsData.get #> map fst) thy;
   412     val base = instance_of thy name base_morph;
   413     fun match (name', (morph', _)) =
   414       name = name' andalso eq_list (op aconv) (base, instance_of thy name' morph');
   415     val i = find_index match (rev regs);
   416     val _ = if i = ~1 then error ("No registration of locale " ^
   417         quote (extern thy name) ^ " and parameter instantiation " ^
   418         space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^ " available.")
   419       else ();
   420   in
   421     RegistrationsData.map (nth_map (length regs - 1 - i)
   422       (fn ((name, (base, export)), stamp) => ((name, (base $> morph, export)), stamp))) thy
   423   end;
   424 
   425 
   426 
   427 (*** Storing results ***)
   428 
   429 (* Theorems *)
   430 
   431 fun add_thmss loc kind args ctxt =
   432   let
   433     val ([Notes args'], ctxt') = Element.activate_i [Notes (kind, args)] ctxt;
   434     val ctxt'' = ctxt' |> ProofContext.theory (
   435       (change_locale loc o apfst o apsnd) (cons (args', stamp ()))
   436         #>
   437       (* Registrations *)
   438       (fn thy => fold_rev (fn (name, morph) =>
   439             let
   440               val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |>
   441                 Attrib.map_facts (Attrib.attribute_i thy)
   442             in PureThy.note_thmss kind args'' #> snd end)
   443         (get_registrations thy |> filter (fn (name, _) => name = loc)) thy))
   444   in ctxt'' end;
   445 
   446 
   447 (* Declarations *)
   448 
   449 local
   450 
   451 fun decl_attrib decl phi = Thm.declaration_attribute (K (decl phi));
   452 
   453 fun add_decls add loc decl =
   454   ProofContext.theory ((change_locale loc o apfst o apfst) (add (decl, stamp ()))) #>
   455   add_thmss loc Thm.internalK
   456     [((Binding.empty, [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
   457 
   458 in
   459 
   460 val add_type_syntax = add_decls (apfst o cons);
   461 val add_term_syntax = add_decls (apsnd o cons);
   462 val add_declaration = add_decls (K I);
   463 
   464 end;
   465 
   466 (* Dependencies *)
   467 
   468 fun add_dependency loc dep = (change_locale loc o apsnd) (cons (dep, stamp ()));
   469 
   470 
   471 (*** Reasoning about locales ***)
   472 
   473 (** Storage for witnesses, intro and unfold rules **)
   474 
   475 structure Witnesses = ThmsFun();
   476 structure Intros = ThmsFun();
   477 structure Unfolds = ThmsFun();
   478 
   479 val witness_attrib = Witnesses.add;
   480 val intro_attrib = Intros.add;
   481 val unfold_attrib = Unfolds.add;
   482 
   483 (** Tactic **)
   484 
   485 fun intro_locales_tac eager ctxt facts st =
   486   Method.intros_tac
   487     (Witnesses.get ctxt @ Intros.get ctxt @ (if eager then Unfolds.get ctxt else [])) facts st;
   488 
   489 val _ = Context.>> (Context.map_theory
   490  (Method.setup (Binding.name "intro_locales") (Scan.succeed (METHOD o intro_locales_tac false))
   491     "back-chain introduction rules of locales without unfolding predicates" #>
   492   Method.setup (Binding.name "unfold_locales") (Scan.succeed (METHOD o intro_locales_tac true))
   493     "back-chain all introduction rules of locales"));
   494 
   495 end;
   496