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