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