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