src/Pure/Isar/locale.ML
author haftmann
Tue Jan 06 08:50:12 2009 +0100 (2009-01-06)
changeset 29363 c1f024b4d76d
parent 29275 9fa69e3858d6
parent 29361 764d51ab0198
child 29392 aa3a30b625d1
permissions -rw-r--r--
merged
     1 (*  Title:      Pure/Isar/locale.ML
     2     Author:     Clemens Ballarin, TU Muenchen
     3 
     4 Locales -- Isar proof contexts as meta-level predicates, with local
     5 syntax and implicit structures.
     6 
     7 Draws basic ideas from Florian Kammueller's original version of
     8 locales, but uses the richer infrastructure of Isar instead of the raw
     9 meta-logic.  Furthermore, structured import of contexts (with merge
    10 and rename operations) are provided, as well as type-inference of the
    11 signature parts, and predicate definitions of the specification text.
    12 
    13 Interpretation enables the reuse of theorems of locales in other
    14 contexts, namely those defined by theories, structured proofs and
    15 locales themselves.
    16 
    17 See also:
    18 
    19 [1] Clemens Ballarin. Locales and Locale Expressions in Isabelle/Isar.
    20     In Stefano Berardi et al., Types for Proofs and Programs: International
    21     Workshop, TYPES 2003, Torino, Italy, LNCS 3085, pages 34-50, 2004.
    22 [2] Clemens Ballarin. Interpretation of Locales in Isabelle: Managing
    23     Dependencies between Locales. Technical Report TUM-I0607, Technische
    24     Universitaet Muenchen, 2006.
    25 [3] Clemens Ballarin. Interpretation of Locales in Isabelle: Theories and
    26     Proof Contexts. In J.M. Borwein and W.M. Farmer, MKM 2006, LNAI 4108,
    27     pages 31-43, 2006.
    28 *)
    29 
    30 signature LOCALE =
    31 sig
    32   type locale
    33 
    34   val test_locale: theory -> string -> bool
    35   val register_locale: bstring ->
    36     (string * sort) list * (Binding.T * typ option * mixfix) list ->
    37     term option * term list ->
    38     (declaration * stamp) list * (declaration * stamp) list ->
    39     ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * stamp) list ->
    40     ((string * Morphism.morphism) * stamp) list -> theory -> theory
    41 
    42   (* Locale name space *)
    43   val intern: theory -> xstring -> string
    44   val extern: theory -> string -> xstring
    45 
    46   (* Specification *)
    47   val params_of: theory -> string -> (Binding.T * typ option * mixfix) list
    48   val instance_of: theory -> string -> Morphism.morphism -> term list
    49   val specification_of: theory -> string -> term option * term list
    50   val declarations_of: theory -> string -> declaration list * declaration list
    51 
    52   (* Storing results *)
    53   val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
    54     Proof.context -> Proof.context
    55   val add_type_syntax: string -> declaration -> Proof.context -> Proof.context
    56   val add_term_syntax: string -> declaration -> Proof.context -> Proof.context
    57   val add_declaration: string -> declaration -> Proof.context -> Proof.context
    58   val add_dependency: string -> (string * Morphism.morphism) -> theory -> theory
    59 
    60   (* Activation *)
    61   val activate_declarations: theory -> string * Morphism.morphism ->
    62     Proof.context -> Proof.context
    63   val activate_global_facts: string * Morphism.morphism -> theory -> theory
    64   val activate_local_facts: string * Morphism.morphism -> Proof.context -> Proof.context
    65   val init: string -> theory -> Proof.context
    66 
    67   (* Reasoning about locales *)
    68   val witness_attrib: attribute
    69   val intro_attrib: attribute
    70   val unfold_attrib: attribute
    71   val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
    72 
    73   (* Registrations *)
    74   val add_global_registration: (string * (Morphism.morphism * Morphism.morphism)) ->
    75     theory -> theory
    76   val amend_global_registration: Morphism.morphism -> (string * Morphism.morphism) ->
    77     theory -> theory
    78   val get_global_registrations: theory -> (string * Morphism.morphism) list
    79 
    80   (* Diagnostic *)
    81   val print_locales: theory -> unit
    82   val print_locale: theory -> bool -> bstring -> unit
    83 end;
    84 
    85 
    86 (*** Theorem list extensible via attribute --- to control intro_locales_tac ***)
    87 
    88 (* FIXME: consider moving named_thms.ML up in the build hierarchy and using that *)
    89 functor ThmsFun() =
    90 struct
    91 
    92 structure Data = GenericDataFun
    93 (
    94   type T = thm list;
    95   val empty = [];
    96   val extend = I;
    97   fun merge _ = Thm.merge_thms;
    98 );
    99 
   100 val get = Data.get o Context.Proof;
   101 val add = Thm.declaration_attribute (Data.map o Thm.add_thm);
   102 
   103 end;
   104 
   105 
   106 structure Locale: LOCALE =
   107 struct
   108 
   109 datatype ctxt = datatype Element.ctxt;
   110 
   111 
   112 (*** Basics ***)
   113 
   114 datatype locale = Loc of {
   115   (* extensible lists are in reverse order: decls, notes, dependencies *)
   116   parameters: (string * sort) list * (Binding.T * typ option * mixfix) list,
   117     (* type and term parameters *)
   118   spec: term option * term list,
   119     (* assumptions (as a single predicate expression) and defines *)
   120   decls: (declaration * stamp) list * (declaration * stamp) list,
   121     (* type and term syntax declarations *)
   122   notes: ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * stamp) list,
   123     (* theorem declarations *)
   124   dependencies: ((string * Morphism.morphism) * stamp) list
   125     (* locale dependencies (sublocale relation) *)
   126 }
   127 
   128 
   129 (*** Theory data ***)
   130 
   131 structure LocalesData = TheoryDataFun
   132 (
   133   type T = NameSpace.T * locale Symtab.table;
   134     (* locale namespace and locales of the theory *)
   135 
   136   val empty = NameSpace.empty_table;
   137   val copy = I;
   138   val extend = I;
   139 
   140   fun join_locales _
   141    (Loc {parameters, spec, decls = (decls1, decls2), notes, dependencies},
   142     Loc {decls = (decls1', decls2'), notes = notes', dependencies = dependencies', ...}) =
   143       Loc {
   144         parameters = parameters,
   145         spec = spec,
   146         decls =
   147          (merge (eq_snd op =) (decls1, decls1'),
   148           merge (eq_snd op =) (decls2, decls2')),
   149         notes = merge (eq_snd op =) (notes, notes'),
   150         dependencies = merge (eq_snd op =) (dependencies, dependencies')};
   151 
   152   fun merge _ = NameSpace.join_tables join_locales;
   153 );
   154 
   155 val intern = NameSpace.intern o #1 o LocalesData.get;
   156 val extern = NameSpace.extern o #1 o LocalesData.get;
   157 
   158 fun get_locale thy name = Symtab.lookup (#2 (LocalesData.get thy)) name;
   159 
   160 fun the_locale thy name = case get_locale thy name
   161  of SOME loc => loc
   162   | NONE => error ("Unknown locale " ^ quote name);
   163 
   164 fun test_locale thy name = case get_locale thy name
   165  of SOME _ => true | NONE => false;
   166 
   167 fun register_locale bname parameters spec decls notes dependencies thy =
   168   thy |> LocalesData.map (NameSpace.bind (Sign.naming_of thy) (Binding.name bname,
   169     Loc {parameters = parameters, spec = spec, decls = decls, notes = notes,
   170       dependencies = dependencies}) #> snd);
   171 
   172 fun change_locale name f thy =
   173   let
   174     val Loc {parameters, spec, decls, notes, dependencies} =
   175         the_locale thy name;
   176     val (parameters', spec', decls', notes', dependencies') =
   177       f (parameters, spec, decls, notes, dependencies);
   178   in
   179     thy
   180     |> (LocalesData.map o apsnd) (Symtab.update (name, Loc {parameters = parameters',
   181       spec = spec', decls = decls', notes = notes', dependencies = dependencies'}))
   182   end;
   183 
   184 fun print_locales thy =
   185   let val (space, locs) = LocalesData.get thy in
   186     Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs)))
   187     |> Pretty.writeln
   188   end;
   189 
   190 
   191 (*** Primitive operations ***)
   192 
   193 fun params_of thy name =
   194   let
   195     val Loc {parameters = (_, params), ...} = the_locale thy name
   196   in params end;
   197 
   198 fun instance_of thy name morph =
   199   params_of thy name |>
   200     map ((fn (b, T, _) => Free (Binding.base_name b, the T)) #> Morphism.term morph);
   201 
   202 fun specification_of thy name =
   203   let
   204     val Loc {spec, ...} = the_locale thy name
   205   in spec end;
   206 
   207 fun declarations_of thy name =
   208   let
   209     val Loc {decls, ...} = the_locale thy name
   210   in
   211     decls |> apfst (map fst) |> apsnd (map fst)
   212   end;
   213 
   214 
   215 (*** Activate context elements of locale ***)
   216 
   217 (** Identifiers: activated locales in theory or proof context **)
   218 
   219 type identifiers = (string * term list) list;
   220 
   221 val empty = ([] : identifiers);
   222 
   223 fun ident_eq thy ((n: string, ts), (m, ss)) = (m = n) andalso Pattern.matchess thy (ss, ts);
   224 
   225 local
   226 
   227 datatype 'a delayed = Ready of 'a | ToDo of ('a delayed * 'a delayed);
   228 
   229 structure IdentifiersData = GenericDataFun
   230 (
   231   type T = identifiers delayed;
   232   val empty = Ready empty;
   233   val extend = I;
   234   fun merge _ = ToDo;
   235 );
   236 
   237 in
   238 
   239 fun finish thy (ToDo (i1, i2)) = merge (ident_eq thy) (finish thy i1, finish thy i2)
   240   | finish _ (Ready ids) = ids;
   241 
   242 val _ = Context.>> (Context.map_theory (Theory.at_begin (fn thy =>
   243   (case IdentifiersData.get (Context.Theory thy) of
   244     Ready _ => NONE |
   245     ids => SOME (Context.theory_map (IdentifiersData.put (Ready (finish thy ids))) thy))
   246   )));
   247 
   248 fun get_global_idents thy =
   249   let val (Ready ids) = (IdentifiersData.get o Context.Theory) thy in ids end;
   250 val put_global_idents = Context.theory_map o IdentifiersData.put o Ready;
   251 
   252 fun get_local_idents ctxt =
   253   let val (Ready ids) = (IdentifiersData.get o Context.Proof) ctxt in ids end;
   254 val put_local_idents = Context.proof_map o IdentifiersData.put o Ready;
   255 
   256 end;
   257 
   258 
   259 (** Resolve locale dependencies in a depth-first fashion **)
   260 
   261 local
   262 
   263 val roundup_bound = 120;
   264 
   265 fun add thy depth (name, morph) (deps, marked) =
   266   if depth > roundup_bound
   267   then error "Roundup bound exceeded (sublocale relation probably not terminating)."
   268   else
   269     let
   270       val Loc {parameters = (_, params), dependencies, ...} = the_locale thy name;
   271       val instance = instance_of thy name morph;
   272     in
   273       if member (ident_eq thy) marked (name, instance)
   274       then (deps, marked)
   275       else
   276         let
   277           val dependencies' =
   278             map (fn ((name, morph'), _) => (name, morph' $>  morph)) dependencies;
   279           val marked' = (name, instance) :: marked;
   280           val (deps', marked'') = fold_rev (add thy (depth + 1)) dependencies' ([], marked');
   281         in
   282           ((name, morph) :: deps' @ deps, marked'')
   283         end
   284     end;
   285 
   286 in
   287 
   288 fun roundup thy activate_dep (name, morph) (marked, input) =
   289   let
   290     (* Find all dependencies incuding new ones (which are dependencies enriching
   291       existing registrations). *)
   292     val (dependencies, marked') = add thy 0 (name, morph) ([], empty);
   293     (* Filter out exisiting fragments. *)
   294     val dependencies' = filter_out (fn (name, morph) =>
   295       member (ident_eq thy) marked (name, instance_of thy name morph)) dependencies;
   296   in
   297     (merge (ident_eq thy) (marked, marked'), input |> fold_rev (activate_dep thy) dependencies')
   298   end;
   299 
   300 end;
   301 
   302 
   303 (* Declarations, facts and entire locale content *)
   304 
   305 fun activate_decls thy (name, morph) ctxt =
   306   let
   307     val Loc {decls = (typ_decls, term_decls), ...} = the_locale thy name;
   308   in
   309     ctxt |> fold_rev (fn (decl, _) => Context.proof_map (decl morph)) typ_decls |>
   310       fold_rev (fn (decl, _) => Context.proof_map (decl morph)) term_decls
   311   end;
   312 
   313 fun activate_notes activ_elem transfer thy (name, morph) input =
   314   let
   315     val Loc {notes, ...} = the_locale thy name;
   316     fun activate ((kind, facts), _) input =
   317       let
   318         val facts' = facts |> Element.facts_map (Element.morph_ctxt (transfer input $> morph))
   319       in activ_elem (Notes (kind, facts')) input end;
   320   in
   321     fold_rev activate notes input
   322   end;
   323 
   324 fun activate_all name thy activ_elem transfer (marked, input) =
   325   let
   326     val Loc {parameters = (_, params), spec = (asm, defs), ...} =
   327       the_locale thy name;
   328   in
   329     input |>
   330       (if not (null params) then activ_elem (Fixes params) else I) |>
   331       (* FIXME type parameters *)
   332       (if is_some asm then activ_elem (Assumes [(Attrib.empty_binding, [(the asm, [])])]) else I) |>
   333       (if not (null defs)
   334         then activ_elem (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs))
   335         else I) |>
   336       pair marked |> roundup thy (activate_notes activ_elem transfer) (name, Morphism.identity)
   337   end;
   338 
   339 
   340 (** Public activation functions **)
   341 
   342 local
   343 
   344 fun init_global_elem (Notes (kind, facts)) thy =
   345       let
   346         val facts' = Attrib.map_facts (Attrib.attribute_i thy) facts
   347       in Old_Locale.global_note_qualified kind facts' thy |> snd end
   348 
   349 fun init_local_elem (Fixes fixes) ctxt = ctxt |>
   350       ProofContext.add_fixes_i fixes |> snd
   351   | init_local_elem (Assumes assms) ctxt =
   352       let
   353         val assms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) assms
   354       in
   355         ctxt |> fold Variable.auto_fixes (maps (map fst o snd) assms') |>
   356           ProofContext.add_assms_i Assumption.assume_export assms' |> snd
   357      end
   358   | init_local_elem (Defines defs) ctxt =
   359       let
   360         val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs
   361       in
   362         ctxt |> fold Variable.auto_fixes (map (fst o snd) defs') |>
   363           ProofContext.add_assms_i LocalDefs.def_export (map (fn (attn, t) => (attn, [t])) defs') |>
   364           snd
   365       end
   366   | init_local_elem (Notes (kind, facts)) ctxt =
   367       let
   368         val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts
   369       in Old_Locale.local_note_qualified kind facts' ctxt |> snd end
   370 
   371 fun cons_elem false (Notes notes) elems = elems
   372   | cons_elem _ elem elems = elem :: elems
   373 
   374 in
   375 
   376 fun activate_declarations thy dep ctxt =
   377   roundup thy activate_decls dep (get_local_idents ctxt, ctxt) |> uncurry put_local_idents;
   378 
   379 fun activate_global_facts dep thy =
   380   roundup thy (activate_notes init_global_elem Element.transfer_morphism)
   381     dep (get_global_idents thy, thy) |>
   382   uncurry put_global_idents;
   383 
   384 fun activate_local_facts dep ctxt =
   385   roundup (ProofContext.theory_of ctxt)
   386   (activate_notes init_local_elem (Element.transfer_morphism o ProofContext.theory_of)) dep
   387     (get_local_idents ctxt, ctxt) |>
   388   uncurry put_local_idents;
   389 
   390 fun init name thy =
   391   activate_all name thy init_local_elem (Element.transfer_morphism o ProofContext.theory_of)
   392     (empty, ProofContext.init thy) |>
   393   uncurry put_local_idents;
   394 
   395 fun print_locale thy show_facts name =
   396   let
   397     val name' = intern thy name;
   398     val ctxt = init name' thy
   399   in
   400     Pretty.big_list "locale elements:"
   401       (activate_all name' thy (cons_elem show_facts) (K (Element.transfer_morphism thy))
   402         (empty, []) |> snd |> rev |>
   403         map (Element.pretty_ctxt ctxt) |> map Pretty.chunks) |> Pretty.writeln
   404   end
   405 
   406 end;
   407 
   408 
   409 (*** Registrations: interpretations in theories ***)
   410 
   411 (* FIXME only global variant needed *)
   412 structure RegistrationsData = GenericDataFun
   413 (
   414   type T = ((string * (Morphism.morphism * Morphism.morphism)) * stamp) list;
   415 (* FIXME mixins need to be stamped *)
   416     (* registrations, in reverse order of declaration *)
   417   val empty = [];
   418   val extend = I;
   419   fun merge _ data : T = Library.merge (eq_snd op =) data;
   420     (* FIXME consolidate with dependencies, consider one data slot only *)
   421 );
   422 
   423 val get_global_registrations =
   424   Context.Theory #> RegistrationsData.get #> map fst #> map (apsnd op $>);
   425 
   426 fun add_global reg =
   427   (Context.theory_map o RegistrationsData.map) (cons (reg, stamp ()));
   428 
   429 fun add_global_registration (name, (base_morph, export)) thy =
   430   roundup thy (fn _ => fn (name', morph') => fn thy => add_global (name', (morph', export)) thy)
   431     (name, base_morph) (get_global_idents thy, thy) |>
   432     snd (* FIXME ?? uncurry put_global_idents *);
   433 
   434 fun amend_global_registration morph (name, base_morph) thy =
   435   let
   436     val regs = (Context.Theory #> RegistrationsData.get #> map fst) thy;
   437     val base = instance_of thy name base_morph;
   438     fun match (name', (morph', _)) =
   439       name = name' andalso eq_list (op aconv) (base, instance_of thy name' morph');
   440     val i = find_index match (rev regs);
   441     val _ = if i = ~1 then error ("No interpretation of locale " ^
   442         quote (extern thy name) ^ " and parameter instantiation " ^
   443         space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^ " available.")
   444       else ();
   445   in
   446     (Context.theory_map o RegistrationsData.map) (nth_map (length regs - 1 - i)
   447       (fn ((name, (base, export)), stamp) => ((name, (base $> morph, export)), stamp))) thy
   448   end;
   449 
   450 
   451 (*** Storing results ***)
   452 
   453 (* Theorems *)
   454 
   455 fun add_thmss loc kind args ctxt =
   456   let
   457     val ([Notes args'], ctxt') = Element.activate_i [Notes (kind, args)] ctxt;
   458     val ctxt'' = ctxt' |> ProofContext.theory (
   459       change_locale loc
   460         (fn (parameters, spec, decls, notes, dependencies) =>
   461           (parameters, spec, decls, (args', stamp ()) :: notes, dependencies)) #>
   462       (* Registrations *)
   463       (fn thy => fold_rev (fn (name, morph) =>
   464             let
   465               val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |>
   466                 Attrib.map_facts (Attrib.attribute_i thy)
   467             in Old_Locale.global_note_qualified kind args'' #> snd end)
   468         (get_global_registrations thy |> filter (fn (name, _) => name = loc)) thy))
   469   in ctxt'' end;
   470 
   471 
   472 (* Declarations *)
   473 
   474 local
   475 
   476 fun decl_attrib decl phi = Thm.declaration_attribute (K (decl phi));
   477 
   478 fun add_decls add loc decl =
   479   ProofContext.theory (change_locale loc
   480     (fn (parameters, spec, decls, notes, dependencies) =>
   481       (parameters, spec, add (decl, stamp ()) decls, notes, dependencies))) #>
   482   add_thmss loc Thm.internalK
   483     [((Binding.empty, [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
   484 
   485 in
   486 
   487 val add_type_syntax = add_decls (apfst o cons);
   488 val add_term_syntax = add_decls (apsnd o cons);
   489 val add_declaration = add_decls (K I);
   490 
   491 end;
   492 
   493 (* Dependencies *)
   494 
   495 fun add_dependency loc dep =
   496   change_locale loc
   497     (fn (parameters, spec, decls, notes, dependencies) =>
   498       (parameters, spec, decls, notes, (dep, stamp ()) :: dependencies));
   499 
   500 
   501 (*** Reasoning about locales ***)
   502 
   503 (** Storage for witnesses, intro and unfold rules **)
   504 
   505 structure Witnesses = ThmsFun();
   506 structure Intros = ThmsFun();
   507 structure Unfolds = ThmsFun();
   508 
   509 val witness_attrib = Witnesses.add;
   510 val intro_attrib = Intros.add;
   511 val unfold_attrib = Unfolds.add;
   512 
   513 (** Tactic **)
   514 
   515 fun intro_locales_tac eager ctxt facts st =
   516   Method.intros_tac
   517     (Witnesses.get ctxt @ Intros.get ctxt @ (if eager then Unfolds.get ctxt else [])) facts st;
   518 
   519 val _ = Context.>> (Context.map_theory
   520   (Method.add_methods
   521     [("intro_locales",
   522       Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac false ctxt ORELSE'
   523         Old_Locale.intro_locales_tac false ctxt)),
   524       "back-chain introduction rules of locales without unfolding predicates"),
   525      ("unfold_locales",
   526       Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac true ctxt ORELSE'
   527         Old_Locale.intro_locales_tac true ctxt)),
   528       "back-chain all introduction rules of locales")]));
   529 
   530 end;
   531