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