src/Pure/Isar/locale.ML
author wenzelm
Sun Mar 29 16:13:24 2009 +0200 (2009-03-29)
changeset 30773 6cc9964436c3
parent 30764 3e3e7aa0cc7a
child 30775 71f777103225
permissions -rw-r--r--
simplified roundup activation interface;
     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: string * morphism -> Proof.context -> Proof.context
    60   val activate_facts: string * morphism -> Context.generic -> Context.generic
    61   val init: string -> theory -> Proof.context
    62 
    63   (* Reasoning about locales *)
    64   val get_witnesses: Proof.context -> thm list
    65   val get_intros: Proof.context -> thm list
    66   val get_unfolds: Proof.context -> thm list
    67   val witness_add: attribute
    68   val intro_add: attribute
    69   val unfold_add: attribute
    70   val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
    71 
    72   (* Registrations *)
    73   val add_registration: string * (morphism * morphism) -> theory -> theory
    74   val amend_registration: morphism -> string * morphism -> theory -> theory
    75   val get_registrations: theory -> (string * morphism) list
    76 
    77   (* Diagnostic *)
    78   val print_locales: theory -> unit
    79   val print_locale: theory -> bool -> xstring -> unit
    80 end;
    81 
    82 structure Locale: LOCALE =
    83 struct
    84 
    85 datatype ctxt = datatype Element.ctxt;
    86 
    87 
    88 (*** Theory data ***)
    89 
    90 datatype locale = Loc of {
    91   (** static part **)
    92   parameters: (string * sort) list * ((string * typ) * mixfix) list,
    93     (* type and term parameters *)
    94   spec: term option * term list,
    95     (* assumptions (as a single predicate expression) and defines *)
    96   intros: thm option * thm option,
    97   axioms: thm list,
    98   (** dynamic part **)
    99   decls: (declaration * stamp) list * (declaration * stamp) list,
   100     (* type and term syntax declarations *)
   101   notes: ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * stamp) list,
   102     (* theorem declarations *)
   103   dependencies: ((string * morphism) * stamp) list
   104     (* locale dependencies (sublocale relation) *)
   105 };
   106 
   107 fun mk_locale ((parameters, spec, intros, axioms), ((decls, notes), dependencies)) =
   108   Loc {parameters = parameters, intros = intros, axioms = axioms, spec = spec,
   109     decls = decls, notes = notes, dependencies = dependencies};
   110 
   111 fun map_locale f (Loc {parameters, spec, intros, axioms, decls, notes, dependencies}) =
   112   mk_locale (f ((parameters, spec, intros, axioms), ((decls, notes), dependencies)));
   113 
   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 (Morphism.term morph o Free o #1);
   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 fun ident_eq thy ((n: string, ts), (m, ss)) = (m = n) andalso Pattern.matchess thy (ss, ts);
   182 
   183 local
   184 
   185 datatype 'a delayed = Ready of 'a | ToDo of 'a delayed * 'a delayed;
   186 
   187 structure Identifiers = GenericDataFun
   188 (
   189   type T = (string * term list) list delayed;
   190   val empty = Ready [];
   191   val extend = I;
   192   fun merge _ = ToDo;
   193 );
   194 
   195 fun finish thy (ToDo (i1, i2)) = merge (ident_eq thy) (finish thy i1, finish thy i2)
   196   | finish _ (Ready ids) = ids;
   197 
   198 val _ = Context.>> (Context.map_theory (Theory.at_begin (fn thy =>
   199   (case Identifiers.get (Context.Theory thy) of
   200     Ready _ => NONE
   201   | ids => SOME (Context.theory_map (Identifiers.put (Ready (finish thy ids))) thy)))));
   202 
   203 in
   204 
   205 val get_idents = (fn Ready ids => ids) o Identifiers.get;
   206 val put_idents = Identifiers.put o Ready;
   207 
   208 end;
   209 
   210 
   211 (** Resolve locale dependencies in a depth-first fashion **)
   212 
   213 local
   214 
   215 val roundup_bound = 120;
   216 
   217 fun add thy depth (name, morph) (deps, marked) =
   218   if depth > roundup_bound
   219   then error "Roundup bound exceeded (sublocale relation probably not terminating)."
   220   else
   221     let
   222       val dependencies = dependencies_of thy name;
   223       val instance = instance_of thy name morph;
   224     in
   225       if member (ident_eq thy) marked (name, instance)
   226       then (deps, marked)
   227       else
   228         let
   229           val dependencies' = map (fn (name, morph') => (name, morph' $> morph)) dependencies;
   230           val marked' = (name, instance) :: marked;
   231           val (deps', marked'') = fold_rev (add thy (depth + 1)) dependencies' ([], marked');
   232         in
   233           ((name, morph) :: deps' @ deps, marked'')
   234         end
   235     end;
   236 
   237 in
   238 
   239 fun roundup thy activate_dep (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 (name, morph) ([], []);
   244     (* Filter out exisiting fragments. *)
   245     val dependencies' = filter_out (fn (name, morph) =>
   246       member (ident_eq thy) marked (name, instance_of thy name morph)) 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_decls (name, morph) context =
   257   let
   258     val thy = Context.theory_of context;
   259     val {decls = (typ_decls, term_decls), ...} = the_locale thy name;
   260   in
   261     context
   262     |> fold_rev (fn (decl, _) => decl morph) typ_decls
   263     |> fold_rev (fn (decl, _) => decl morph) term_decls
   264   end;
   265 
   266 fun activate_notes activ_elem transfer thy (name, morph) input =
   267   let
   268     val {notes, ...} = the_locale thy name;
   269     fun activate ((kind, facts), _) input =
   270       let
   271         val facts' = facts |> Element.facts_map (Element.morph_ctxt (transfer input $> morph))
   272       in activ_elem (Notes (kind, facts')) input end;
   273   in
   274     fold_rev activate notes input
   275   end;
   276 
   277 fun activate_all name thy activ_elem transfer (marked, input) =
   278   let
   279     val {parameters = (_, params), spec = (asm, defs), ...} = the_locale thy name;
   280     val input' = input |>
   281       (not (null params) ?
   282         activ_elem (Fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params))) |>
   283       (* FIXME type parameters *)
   284       (case asm of SOME A => activ_elem (Assumes [(Attrib.empty_binding, [(A, [])])]) | _ => I) |>
   285       (if not (null defs)
   286         then activ_elem (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs))
   287         else I);
   288     val activate = activate_notes activ_elem transfer thy;
   289   in
   290     roundup thy activate (name, Morphism.identity) (marked, input')
   291   end;
   292 
   293 
   294 (** Public activation functions **)
   295 
   296 local
   297 
   298 fun init_elem (Fixes fixes) (Context.Proof ctxt) =
   299       Context.Proof (ProofContext.add_fixes fixes ctxt |> snd)
   300   | init_elem (Assumes assms) (Context.Proof ctxt) =
   301       let
   302         val assms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) assms;
   303         val ctxt' = ctxt
   304           |> fold Variable.auto_fixes (maps (map fst o snd) assms')
   305           |> ProofContext.add_assms_i Assumption.assume_export assms' |> snd;
   306       in Context.Proof ctxt' end
   307   | init_elem (Defines defs) (Context.Proof ctxt) =
   308       let
   309         val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
   310         val ctxt' = ctxt
   311           |> fold Variable.auto_fixes (map (fst o snd) defs')
   312           |> ProofContext.add_assms_i LocalDefs.def_export (map (fn (attn, t) => (attn, [t])) defs')
   313           |> snd;
   314       in Context.Proof ctxt' end
   315   | init_elem (Notes (kind, facts)) (Context.Proof ctxt) =
   316       let
   317         val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts
   318       in Context.Proof (ProofContext.note_thmss kind facts' ctxt |> snd) end
   319   | init_elem (Notes (kind, facts)) (Context.Theory thy) =
   320       let
   321         val facts' = Attrib.map_facts (Attrib.attribute_i thy) facts
   322       in Context.Theory (PureThy.note_thmss kind facts' thy |> snd) end
   323   | init_elem _ (Context.Theory _) = raise Fail "Bad context element in global theory";
   324 
   325 in
   326 
   327 fun activate_declarations dep ctxt =
   328   let
   329     val context = Context.Proof ctxt;
   330     val thy = Context.theory_of context;
   331     val context' = roundup thy activate_decls dep (get_idents context, context) |-> put_idents;
   332   in Context.the_proof context' end;
   333 
   334 fun activate_facts dep context =
   335   let
   336     val thy = Context.theory_of context;
   337     val activate = activate_notes init_elem (Element.transfer_morphism o Context.theory_of) thy;
   338   in roundup thy activate dep (get_idents context, context) |-> put_idents end;
   339 
   340 fun init name thy =
   341   activate_all name thy init_elem (Element.transfer_morphism o Context.theory_of)
   342     ([], Context.Proof (ProofContext.init thy)) |-> put_idents |> Context.proof_of;
   343 
   344 fun print_locale thy show_facts raw_name =
   345   let
   346     val name = intern thy raw_name;
   347     val ctxt = init name thy;
   348     fun cons_elem (elem as Notes _) = show_facts ? cons elem
   349       | cons_elem elem = cons elem;
   350     val elems =
   351       activate_all name thy cons_elem (K (Element.transfer_morphism thy)) ([], [])
   352       |> snd |> rev;
   353   in
   354     Pretty.big_list "locale elements:" (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)
   355     |> Pretty.writeln
   356   end;
   357 
   358 end;
   359 
   360 
   361 (*** Registrations: interpretations in theories ***)
   362 
   363 structure Registrations = TheoryDataFun
   364 (
   365   type T = ((string * (morphism * morphism)) * stamp) list;
   366     (* FIXME mixins need to be stamped *)
   367     (* registrations, in reverse order of declaration *)
   368   val empty = [];
   369   val extend = I;
   370   val copy = I;
   371   fun merge _ data : T = Library.merge (eq_snd op =) data;
   372     (* FIXME consolidate with dependencies, consider one data slot only *)
   373 );
   374 
   375 val get_registrations =
   376   Registrations.get #> map (#1 #> apsnd op $>);
   377 
   378 fun add_registration (name, (base_morph, export)) thy =
   379   roundup thy (fn (name', morph') => Registrations.map (cons ((name', (morph', export)), stamp ())))
   380     (name, base_morph) (get_idents (Context.Theory thy), thy) |> snd;
   381     (* FIXME |-> put_global_idents ?*)
   382 
   383 fun amend_registration morph (name, base_morph) thy =
   384   let
   385     val regs = map #1 (Registrations.get thy);
   386     val base = instance_of thy name base_morph;
   387     fun match (name', (morph', _)) =
   388       name = name' andalso eq_list (op aconv) (base, instance_of thy name' morph');
   389     val i = find_index match (rev regs);
   390     val _ =
   391       if i = ~1 then error ("No registration of locale " ^
   392         quote (extern thy name) ^ " and parameter instantiation " ^
   393         space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^ " available")
   394       else ();
   395   in
   396     Registrations.map (nth_map (length regs - 1 - i)
   397       (fn ((name, (base, export)), stamp) => ((name, (base $> morph, export)), stamp))) thy
   398   end;
   399 
   400 
   401 
   402 (*** Storing results ***)
   403 
   404 (* Theorems *)
   405 
   406 fun add_thmss loc kind args ctxt =
   407   let
   408     val ([Notes args'], ctxt') = Element.activate_i [Notes (kind, args)] ctxt;
   409     val ctxt'' = ctxt' |> ProofContext.theory (
   410       (change_locale loc o apfst o apsnd) (cons (args', stamp ()))
   411         #>
   412       (* Registrations *)
   413       (fn thy => fold_rev (fn (name, morph) =>
   414             let
   415               val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |>
   416                 Attrib.map_facts (Attrib.attribute_i thy)
   417             in PureThy.note_thmss kind args'' #> snd end)
   418         (get_registrations thy |> filter (fn (name, _) => name = loc)) thy))
   419   in ctxt'' end;
   420 
   421 
   422 (* Declarations *)
   423 
   424 local
   425 
   426 fun decl_attrib decl phi = Thm.declaration_attribute (K (decl phi));
   427 
   428 fun add_decls add loc decl =
   429   ProofContext.theory ((change_locale loc o apfst o apfst) (add (decl, stamp ()))) #>
   430   add_thmss loc Thm.internalK
   431     [((Binding.empty, [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
   432 
   433 in
   434 
   435 val add_type_syntax = add_decls (apfst o cons);
   436 val add_term_syntax = add_decls (apsnd o cons);
   437 val add_declaration = add_decls (K I);
   438 
   439 end;
   440 
   441 
   442 (* Dependencies *)
   443 
   444 fun add_dependency loc dep = (change_locale loc o apsnd) (cons (dep, stamp ()));
   445 
   446 
   447 (*** Reasoning about locales ***)
   448 
   449 (* Storage for witnesses, intro and unfold rules *)
   450 
   451 structure Thms = GenericDataFun
   452 (
   453   type T = thm list * thm list * thm list;
   454   val empty = ([], [], []);
   455   val extend = I;
   456   fun merge _ ((witnesses1, intros1, unfolds1), (witnesses2, intros2, unfolds2)) =
   457    (Thm.merge_thms (witnesses1, witnesses2),
   458     Thm.merge_thms (intros1, intros2),
   459     Thm.merge_thms (unfolds1, unfolds2));
   460 );
   461 
   462 val get_witnesses = #1 o Thms.get o Context.Proof;
   463 val get_intros = #2 o Thms.get o Context.Proof;
   464 val get_unfolds = #3 o Thms.get o Context.Proof;
   465 
   466 val witness_add =
   467   Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (Thm.add_thm th x, y, z)));
   468 val intro_add =
   469   Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (x, Thm.add_thm th y, z)));
   470 val unfold_add =
   471   Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (x, y, Thm.add_thm th z)));
   472 
   473 
   474 (* Tactic *)
   475 
   476 fun intro_locales_tac eager ctxt =
   477   Method.intros_tac
   478     (get_witnesses ctxt @ get_intros ctxt @ (if eager then get_unfolds ctxt else []));
   479 
   480 val _ = Context.>> (Context.map_theory
   481  (Method.setup (Binding.name "intro_locales") (Scan.succeed (METHOD o intro_locales_tac false))
   482     "back-chain introduction rules of locales without unfolding predicates" #>
   483   Method.setup (Binding.name "unfold_locales") (Scan.succeed (METHOD o intro_locales_tac true))
   484     "back-chain all introduction rules of locales"));
   485 
   486 end;
   487