src/Pure/Isar/locale.ML
author wenzelm
Sun Mar 29 17:47:50 2009 +0200 (2009-03-29)
changeset 30775 71f777103225
parent 30773 6cc9964436c3
child 30777 9960ff945c52
permissions -rw-r--r--
added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
tuned;
     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 fun activate_declarations dep = Context.proof_map (fn context =>
   297   let
   298     val thy = Context.theory_of context;
   299     val context' = roundup thy activate_decls dep (get_idents context, context) |-> put_idents;
   300   in context' end);
   301 
   302 fun activate_facts dep context =
   303   let
   304     val thy = Context.theory_of context;
   305     val activate = activate_notes Element.init (Element.transfer_morphism o Context.theory_of) thy;
   306   in roundup thy activate dep (get_idents context, context) |-> put_idents end;
   307 
   308 fun init name thy =
   309   activate_all name thy Element.init (Element.transfer_morphism o Context.theory_of)
   310     ([], Context.Proof (ProofContext.init thy)) |-> put_idents |> Context.proof_of;
   311 
   312 fun print_locale thy show_facts raw_name =
   313   let
   314     val name = intern thy raw_name;
   315     val ctxt = init name thy;
   316     fun cons_elem (elem as Notes _) = show_facts ? cons elem
   317       | cons_elem elem = cons elem;
   318     val elems =
   319       activate_all name thy cons_elem (K (Element.transfer_morphism thy)) ([], [])
   320       |> snd |> rev;
   321   in
   322     Pretty.big_list "locale elements:" (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)
   323     |> Pretty.writeln
   324   end;
   325 
   326 
   327 (*** Registrations: interpretations in theories ***)
   328 
   329 structure Registrations = TheoryDataFun
   330 (
   331   type T = ((string * (morphism * morphism)) * stamp) list;
   332     (* FIXME mixins need to be stamped *)
   333     (* registrations, in reverse order of declaration *)
   334   val empty = [];
   335   val extend = I;
   336   val copy = I;
   337   fun merge _ data : T = Library.merge (eq_snd op =) data;
   338     (* FIXME consolidate with dependencies, consider one data slot only *)
   339 );
   340 
   341 val get_registrations =
   342   Registrations.get #> map (#1 #> apsnd op $>);
   343 
   344 fun add_registration (name, (base_morph, export)) thy =
   345   roundup thy (fn (name', morph') => Registrations.map (cons ((name', (morph', export)), stamp ())))
   346     (name, base_morph) (get_idents (Context.Theory thy), thy) |> snd;
   347     (* FIXME |-> put_global_idents ?*)
   348 
   349 fun amend_registration morph (name, base_morph) thy =
   350   let
   351     val regs = map #1 (Registrations.get thy);
   352     val base = instance_of thy name base_morph;
   353     fun match (name', (morph', _)) =
   354       name = name' andalso eq_list (op aconv) (base, instance_of thy name' morph');
   355     val i = find_index match (rev regs);
   356     val _ =
   357       if i = ~1 then error ("No registration of locale " ^
   358         quote (extern thy name) ^ " and parameter instantiation " ^
   359         space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^ " available")
   360       else ();
   361   in
   362     Registrations.map (nth_map (length regs - 1 - i)
   363       (fn ((name, (base, export)), stamp) => ((name, (base $> morph, export)), stamp))) thy
   364   end;
   365 
   366 
   367 (*** Storing results ***)
   368 
   369 (* Theorems *)
   370 
   371 fun add_thmss loc kind args ctxt =
   372   let
   373     val ([Notes args'], ctxt') = Element.activate_i [Notes (kind, args)] ctxt;
   374     val ctxt'' = ctxt' |> ProofContext.theory (
   375       (change_locale loc o apfst o apsnd) (cons (args', stamp ()))
   376         #>
   377       (* Registrations *)
   378       (fn thy => fold_rev (fn (name, morph) =>
   379             let
   380               val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |>
   381                 Attrib.map_facts (Attrib.attribute_i thy)
   382             in PureThy.note_thmss kind args'' #> snd end)
   383         (get_registrations thy |> filter (fn (name, _) => name = loc)) thy))
   384   in ctxt'' end;
   385 
   386 
   387 (* Declarations *)
   388 
   389 local
   390 
   391 fun decl_attrib decl phi = Thm.declaration_attribute (K (decl phi));
   392 
   393 fun add_decls add loc decl =
   394   ProofContext.theory ((change_locale loc o apfst o apfst) (add (decl, stamp ()))) #>
   395   add_thmss loc Thm.internalK
   396     [((Binding.empty, [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
   397 
   398 in
   399 
   400 val add_type_syntax = add_decls (apfst o cons);
   401 val add_term_syntax = add_decls (apsnd o cons);
   402 val add_declaration = add_decls (K I);
   403 
   404 end;
   405 
   406 
   407 (* Dependencies *)
   408 
   409 fun add_dependency loc dep = (change_locale loc o apsnd) (cons (dep, stamp ()));
   410 
   411 
   412 (*** Reasoning about locales ***)
   413 
   414 (* Storage for witnesses, intro and unfold rules *)
   415 
   416 structure Thms = GenericDataFun
   417 (
   418   type T = thm list * thm list * thm list;
   419   val empty = ([], [], []);
   420   val extend = I;
   421   fun merge _ ((witnesses1, intros1, unfolds1), (witnesses2, intros2, unfolds2)) =
   422    (Thm.merge_thms (witnesses1, witnesses2),
   423     Thm.merge_thms (intros1, intros2),
   424     Thm.merge_thms (unfolds1, unfolds2));
   425 );
   426 
   427 val get_witnesses = #1 o Thms.get o Context.Proof;
   428 val get_intros = #2 o Thms.get o Context.Proof;
   429 val get_unfolds = #3 o Thms.get o Context.Proof;
   430 
   431 val witness_add =
   432   Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (Thm.add_thm th x, y, z)));
   433 val intro_add =
   434   Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (x, Thm.add_thm th y, z)));
   435 val unfold_add =
   436   Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (x, y, Thm.add_thm th z)));
   437 
   438 
   439 (* Tactic *)
   440 
   441 fun intro_locales_tac eager ctxt =
   442   Method.intros_tac
   443     (get_witnesses ctxt @ get_intros ctxt @ (if eager then get_unfolds ctxt else []));
   444 
   445 val _ = Context.>> (Context.map_theory
   446  (Method.setup (Binding.name "intro_locales") (Scan.succeed (METHOD o intro_locales_tac false))
   447     "back-chain introduction rules of locales without unfolding predicates" #>
   448   Method.setup (Binding.name "unfold_locales") (Scan.succeed (METHOD o intro_locales_tac true))
   449     "back-chain all introduction rules of locales"));
   450 
   451 end;
   452