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