src/Pure/Isar/locale.ML
author wenzelm
Sun Mar 01 23:36:12 2009 +0100 (2009-03-01)
changeset 30190 479806475f3c
parent 29576 669b560fc2b9
child 30223 24d975352879
permissions -rw-r--r--
use long names for old-style fold combinators;
     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: bstring ->
    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 -> bstring -> 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 fun global_note_qualified kind facts thy = (*FIXME*)
   111   thy
   112   |> Sign.qualified_names
   113   |> PureThy.note_thmss kind facts
   114   ||> Sign.restore_naming thy;
   115 
   116 fun local_note_qualified kind facts ctxt = (*FIXME*)
   117   ctxt
   118   |> ProofContext.qualified_names
   119   |> ProofContext.note_thmss_i kind facts
   120   ||> ProofContext.restore_naming ctxt;
   121 
   122 
   123 
   124 (*** Theory data ***)
   125 
   126 datatype locale = Loc of {
   127   (** static part **)
   128   parameters: (string * sort) list * (binding * typ option * mixfix) list,
   129     (* type and term parameters *)
   130   spec: term option * term list,
   131     (* assumptions (as a single predicate expression) and defines *)
   132   intros: thm option * thm option,
   133   axioms: thm list,
   134   (** dynamic part **)
   135   decls: (declaration * stamp) list * (declaration * stamp) list,
   136     (* type and term syntax declarations *)
   137   notes: ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * stamp) list,
   138     (* theorem declarations *)
   139   dependencies: ((string * morphism) * stamp) list
   140     (* locale dependencies (sublocale relation) *)
   141 };
   142 
   143 fun mk_locale ((parameters, spec, intros, axioms), ((decls, notes), dependencies)) =
   144   Loc {parameters = parameters, intros = intros, axioms = axioms, spec = spec,
   145     decls = decls, notes = notes, dependencies = dependencies};
   146 fun map_locale f (Loc {parameters, spec, intros, axioms, decls, notes, dependencies}) =
   147   mk_locale (f ((parameters, spec, intros, axioms), ((decls, notes), dependencies)));
   148 fun merge_locale (Loc {parameters, spec, intros, axioms, decls = (decls1, decls2),
   149   notes, dependencies}, Loc {decls = (decls1', decls2'), notes = notes',
   150     dependencies = dependencies', ...}) = mk_locale
   151       ((parameters, spec, intros, axioms),
   152         (((merge (eq_snd op =) (decls1, decls1'), merge (eq_snd op =) (decls2, decls2')),
   153           merge (eq_snd op =) (notes, notes')),
   154             merge (eq_snd op =) (dependencies, dependencies')));
   155 
   156 structure LocalesData = TheoryDataFun
   157 (
   158   type T = locale NameSpace.table;
   159   val empty = NameSpace.empty_table;
   160   val copy = I;
   161   val extend = I;
   162   fun merge _ = NameSpace.join_tables (K merge_locale);
   163 );
   164 
   165 val intern = NameSpace.intern o #1 o LocalesData.get;
   166 val extern = NameSpace.extern o #1 o LocalesData.get;
   167 
   168 fun get_locale thy = Symtab.lookup (#2 (LocalesData.get thy));
   169 
   170 fun defined thy = is_some o get_locale thy;
   171 
   172 fun the_locale thy name = case get_locale thy name
   173  of SOME (Loc loc) => loc
   174   | NONE => error ("Unknown locale " ^ quote name);
   175 
   176 fun register_locale bname parameters spec intros axioms decls notes dependencies thy =
   177   thy |> LocalesData.map (NameSpace.bind (Sign.naming_of thy) (Binding.name bname,
   178     mk_locale ((parameters, spec, intros, axioms), ((decls, notes), dependencies))) #> snd);
   179 
   180 fun change_locale name =
   181   LocalesData.map o apsnd o Symtab.map_entry name o map_locale o apsnd;
   182 
   183 fun print_locales thy =
   184   Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (LocalesData.get thy)))
   185   |> Pretty.writeln;
   186 
   187 
   188 (*** Primitive operations ***)
   189 
   190 fun params_of thy = snd o #parameters o the_locale thy;
   191 
   192 fun intros_of thy = #intros o the_locale thy;
   193 
   194 fun axioms_of thy = #axioms o the_locale thy;
   195 
   196 fun instance_of thy name morph = params_of thy name |>
   197   map ((fn (b, T, _) => Free (Binding.base_name b, the T)) #> Morphism.term morph);
   198 
   199 fun specification_of thy = #spec o the_locale thy;
   200 
   201 fun declarations_of thy name = the_locale thy name |>
   202   #decls |> apfst (map fst) |> apsnd (map fst);
   203 
   204 fun dependencies_of thy name = the_locale thy name |>
   205   #dependencies |> map fst;
   206 
   207 
   208 (*** Activate context elements of locale ***)
   209 
   210 (** Identifiers: activated locales in theory or proof context **)
   211 
   212 type identifiers = (string * term list) list;
   213 
   214 val empty = ([] : identifiers);
   215 
   216 fun ident_eq thy ((n: string, ts), (m, ss)) = (m = n) andalso Pattern.matchess thy (ss, ts);
   217 
   218 local
   219 
   220 datatype 'a delayed = Ready of 'a | ToDo of ('a delayed * 'a delayed);
   221 
   222 structure IdentifiersData = GenericDataFun
   223 (
   224   type T = identifiers delayed;
   225   val empty = Ready empty;
   226   val extend = I;
   227   fun merge _ = ToDo;
   228 );
   229 
   230 in
   231 
   232 fun finish thy (ToDo (i1, i2)) = merge (ident_eq thy) (finish thy i1, finish thy i2)
   233   | finish _ (Ready ids) = ids;
   234 
   235 val _ = Context.>> (Context.map_theory (Theory.at_begin (fn thy =>
   236   (case IdentifiersData.get (Context.Theory thy) of
   237     Ready _ => NONE |
   238     ids => SOME (Context.theory_map (IdentifiersData.put (Ready (finish thy ids))) thy))
   239   )));
   240 
   241 fun get_global_idents thy =
   242   let val (Ready ids) = (IdentifiersData.get o Context.Theory) thy in ids end;
   243 val put_global_idents = Context.theory_map o IdentifiersData.put o Ready;
   244 
   245 fun get_local_idents ctxt =
   246   let val (Ready ids) = (IdentifiersData.get o Context.Proof) ctxt in ids end;
   247 val put_local_idents = Context.proof_map o IdentifiersData.put o Ready;
   248 
   249 end;
   250 
   251 
   252 (** Resolve locale dependencies in a depth-first fashion **)
   253 
   254 local
   255 
   256 val roundup_bound = 120;
   257 
   258 fun add thy depth (name, morph) (deps, marked) =
   259   if depth > roundup_bound
   260   then error "Roundup bound exceeded (sublocale relation probably not terminating)."
   261   else
   262     let
   263       val {parameters = (_, params), dependencies, ...} = the_locale thy name;
   264       val instance = instance_of thy name morph;
   265     in
   266       if member (ident_eq thy) marked (name, instance)
   267       then (deps, marked)
   268       else
   269         let
   270           val dependencies' =
   271             map (fn ((name, morph'), _) => (name, morph' $>  morph)) dependencies;
   272           val marked' = (name, instance) :: marked;
   273           val (deps', marked'') = fold_rev (add thy (depth + 1)) dependencies' ([], marked');
   274         in
   275           ((name, morph) :: deps' @ deps, marked'')
   276         end
   277     end;
   278 
   279 in
   280 
   281 fun roundup thy activate_dep (name, morph) (marked, input) =
   282   let
   283     (* Find all dependencies incuding new ones (which are dependencies enriching
   284       existing registrations). *)
   285     val (dependencies, marked') = add thy 0 (name, morph) ([], empty);
   286     (* Filter out exisiting fragments. *)
   287     val dependencies' = filter_out (fn (name, morph) =>
   288       member (ident_eq thy) marked (name, instance_of thy name morph)) dependencies;
   289   in
   290     (merge (ident_eq thy) (marked, marked'), input |> fold_rev (activate_dep thy) dependencies')
   291   end;
   292 
   293 end;
   294 
   295 
   296 (* Declarations, facts and entire locale content *)
   297 
   298 fun activate_decls thy (name, morph) ctxt =
   299   let
   300     val {decls = (typ_decls, term_decls), ...} = the_locale thy name;
   301   in
   302     ctxt |> fold_rev (fn (decl, _) => Context.proof_map (decl morph)) typ_decls |>
   303       fold_rev (fn (decl, _) => Context.proof_map (decl morph)) term_decls
   304   end;
   305 
   306 fun activate_notes activ_elem transfer thy (name, morph) input =
   307   let
   308     val {notes, ...} = the_locale thy name;
   309     fun activate ((kind, facts), _) input =
   310       let
   311         val facts' = facts |> Element.facts_map (Element.morph_ctxt (transfer input $> morph))
   312       in activ_elem (Notes (kind, facts')) input end;
   313   in
   314     fold_rev activate notes input
   315   end;
   316 
   317 fun activate_all name thy activ_elem transfer (marked, input) =
   318   let
   319     val {parameters = (_, params), spec = (asm, defs), ...} =
   320       the_locale thy name;
   321   in
   322     input |>
   323       (if not (null params) then activ_elem (Fixes params) else I) |>
   324       (* FIXME type parameters *)
   325       (if is_some asm then activ_elem (Assumes [(Attrib.empty_binding, [(the asm, [])])]) else I) |>
   326       (if not (null defs)
   327         then activ_elem (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs))
   328         else I) |>
   329       pair marked |> roundup thy (activate_notes activ_elem transfer) (name, Morphism.identity)
   330   end;
   331 
   332 
   333 (** Public activation functions **)
   334 
   335 local
   336 
   337 fun init_global_elem (Notes (kind, facts)) thy =
   338   let
   339     val facts' = Attrib.map_facts (Attrib.attribute_i thy) facts
   340   in global_note_qualified kind facts' thy |> snd end
   341 
   342 fun init_local_elem (Fixes fixes) ctxt = ctxt |>
   343       ProofContext.add_fixes_i fixes |> snd
   344   | init_local_elem (Assumes assms) ctxt =
   345       let
   346         val assms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) assms
   347       in
   348         ctxt |> fold Variable.auto_fixes (maps (map fst o snd) assms') |>
   349           ProofContext.add_assms_i Assumption.assume_export assms' |> snd
   350      end
   351   | init_local_elem (Defines defs) ctxt =
   352       let
   353         val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs
   354       in
   355         ctxt |> fold Variable.auto_fixes (map (fst o snd) defs') |>
   356           ProofContext.add_assms_i LocalDefs.def_export (map (fn (attn, t) => (attn, [t])) defs') |>
   357           snd
   358       end
   359   | init_local_elem (Notes (kind, facts)) ctxt =
   360       let
   361         val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts
   362       in local_note_qualified kind facts' ctxt |> snd end
   363 
   364 fun cons_elem false (Notes notes) elems = elems
   365   | cons_elem _ elem elems = elem :: elems
   366 
   367 in
   368 
   369 fun activate_declarations thy dep ctxt =
   370   roundup thy activate_decls dep (get_local_idents ctxt, ctxt) |-> put_local_idents;
   371 
   372 fun activate_global_facts dep thy =
   373   roundup thy (activate_notes init_global_elem Element.transfer_morphism)
   374     dep (get_global_idents thy, thy) |-> put_global_idents;
   375 
   376 fun activate_local_facts dep ctxt =
   377   roundup (ProofContext.theory_of ctxt)
   378   (activate_notes init_local_elem (Element.transfer_morphism o ProofContext.theory_of)) dep
   379     (get_local_idents ctxt, ctxt) |-> put_local_idents;
   380 
   381 fun init name thy =
   382   activate_all name thy init_local_elem (Element.transfer_morphism o ProofContext.theory_of)
   383     (empty, ProofContext.init thy) |-> put_local_idents;
   384 
   385 fun print_locale thy show_facts name =
   386   let
   387     val name' = intern thy name;
   388     val ctxt = init name' thy
   389   in
   390     Pretty.big_list "locale elements:"
   391       (activate_all name' thy (cons_elem show_facts) (K (Element.transfer_morphism thy))
   392         (empty, []) |> snd |> rev |>
   393         map (Element.pretty_ctxt ctxt) |> map Pretty.chunks) |> Pretty.writeln
   394   end
   395 
   396 end;
   397 
   398 
   399 (*** Registrations: interpretations in theories ***)
   400 
   401 structure RegistrationsData = TheoryDataFun
   402 (
   403   type T = ((string * (morphism * morphism)) * stamp) list;
   404     (* FIXME mixins need to be stamped *)
   405     (* registrations, in reverse order of declaration *)
   406   val empty = [];
   407   val extend = I;
   408   val copy = I;
   409   fun merge _ data : T = Library.merge (eq_snd op =) data;
   410     (* FIXME consolidate with dependencies, consider one data slot only *)
   411 );
   412 
   413 val get_registrations =
   414   RegistrationsData.get #> map fst #> map (apsnd op $>);
   415 
   416 fun add_registration (name, (base_morph, export)) thy =
   417   roundup thy (fn _ => fn (name', morph') =>
   418     (RegistrationsData.map o cons) ((name', (morph', export)), stamp ()))
   419     (name, base_morph) (get_global_idents thy, thy) |> snd
   420     (* FIXME |-> put_global_idents ?*);
   421 
   422 fun amend_registration morph (name, base_morph) thy =
   423   let
   424     val regs = (RegistrationsData.get #> map fst) thy;
   425     val base = instance_of thy name base_morph;
   426     fun match (name', (morph', _)) =
   427       name = name' andalso eq_list (op aconv) (base, instance_of thy name' morph');
   428     val i = find_index match (rev regs);
   429     val _ = if i = ~1 then error ("No registration of locale " ^
   430         quote (extern thy name) ^ " and parameter instantiation " ^
   431         space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^ " available.")
   432       else ();
   433   in
   434     RegistrationsData.map (nth_map (length regs - 1 - i)
   435       (fn ((name, (base, export)), stamp) => ((name, (base $> morph, export)), stamp))) thy
   436   end;
   437 
   438 
   439 
   440 (*** Storing results ***)
   441 
   442 (* Theorems *)
   443 
   444 fun add_thmss loc kind args ctxt =
   445   let
   446     val ([Notes args'], ctxt') = Element.activate_i [Notes (kind, args)] ctxt;
   447     val ctxt'' = ctxt' |> ProofContext.theory (
   448       (change_locale loc o apfst o apsnd) (cons (args', stamp ()))
   449         #>
   450       (* Registrations *)
   451       (fn thy => fold_rev (fn (name, morph) =>
   452             let
   453               val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |>
   454                 Attrib.map_facts (Attrib.attribute_i thy)
   455             in global_note_qualified kind args'' #> snd end)
   456         (get_registrations thy |> filter (fn (name, _) => name = loc)) thy))
   457   in ctxt'' end;
   458 
   459 
   460 (* Declarations *)
   461 
   462 local
   463 
   464 fun decl_attrib decl phi = Thm.declaration_attribute (K (decl phi));
   465 
   466 fun add_decls add loc decl =
   467   ProofContext.theory ((change_locale loc o apfst o apfst) (add (decl, stamp ())))
   468     #>
   469   add_thmss loc Thm.internalK
   470     [((Binding.empty, [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
   471 
   472 in
   473 
   474 val add_type_syntax = add_decls (apfst o cons);
   475 val add_term_syntax = add_decls (apsnd o cons);
   476 val add_declaration = add_decls (K I);
   477 
   478 end;
   479 
   480 (* Dependencies *)
   481 
   482 fun add_dependency loc dep = (change_locale loc o apsnd) (cons (dep, stamp ()));
   483 
   484 
   485 (*** Reasoning about locales ***)
   486 
   487 (** Storage for witnesses, intro and unfold rules **)
   488 
   489 structure Witnesses = ThmsFun();
   490 structure Intros = ThmsFun();
   491 structure Unfolds = ThmsFun();
   492 
   493 val witness_attrib = Witnesses.add;
   494 val intro_attrib = Intros.add;
   495 val unfold_attrib = Unfolds.add;
   496 
   497 (** Tactic **)
   498 
   499 fun intro_locales_tac eager ctxt facts st =
   500   Method.intros_tac
   501     (Witnesses.get ctxt @ Intros.get ctxt @ (if eager then Unfolds.get ctxt else [])) facts st;
   502 
   503 val _ = Context.>> (Context.map_theory
   504   (Method.add_methods
   505     [("intro_locales",
   506       Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac false ctxt)),
   507       "back-chain introduction rules of locales without unfolding predicates"),
   508      ("unfold_locales",
   509       Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac true ctxt)),
   510       "back-chain all introduction rules of locales")]));
   511 
   512 end;
   513