src/Pure/Isar/bundle.ML
author wenzelm
Wed Apr 01 13:32:32 2015 +0200 (2015-04-01)
changeset 59890 01aff5aa081d
parent 59880 30687c3f2b10
child 59917 9830c944670f
permissions -rw-r--r--
tuned signature;
     1 (*  Title:      Pure/Isar/bundle.ML
     2     Author:     Makarius
     3 
     4 Bundled declarations (notes etc.).
     5 *)
     6 
     7 signature BUNDLE =
     8 sig
     9   type bundle = (thm list * Token.src list) list
    10   val check: Proof.context -> xstring * Position.T -> string
    11   val get_bundle: Proof.context -> string -> bundle
    12   val get_bundle_cmd: Proof.context -> xstring * Position.T -> bundle
    13   val bundle: binding * (thm list * Token.src list) list ->
    14     (binding * typ option * mixfix) list -> local_theory -> local_theory
    15   val bundle_cmd: binding * (Facts.ref * Token.src list) list ->
    16     (binding * string option * mixfix) list -> local_theory -> local_theory
    17   val includes: string list -> Proof.context -> Proof.context
    18   val includes_cmd: (xstring * Position.T) list -> Proof.context -> Proof.context
    19   val include_: string list -> Proof.state -> Proof.state
    20   val include_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
    21   val including: string list -> Proof.state -> Proof.state
    22   val including_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
    23   val context: string list -> Element.context_i list ->
    24     generic_theory -> Binding.scope * local_theory
    25   val context_cmd: (xstring * Position.T) list -> Element.context list ->
    26     generic_theory -> Binding.scope * local_theory
    27   val print_bundles: Proof.context -> unit
    28 end;
    29 
    30 structure Bundle: BUNDLE =
    31 struct
    32 
    33 (* maintain bundles *)
    34 
    35 type bundle = (thm list * Token.src list) list;
    36 
    37 fun transform_bundle phi : bundle -> bundle =
    38   map (fn (fact, atts) => (Morphism.fact phi fact, map (Token.transform_src phi) atts));
    39 
    40 structure Data = Generic_Data
    41 (
    42   type T = bundle Name_Space.table;
    43   val empty : T = Name_Space.empty_table "bundle";
    44   val extend = I;
    45   val merge = Name_Space.merge_tables;
    46 );
    47 
    48 val get_bundles = Data.get o Context.Proof;
    49 
    50 fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_bundles ctxt);
    51 
    52 val get_bundle = Name_Space.get o get_bundles;
    53 fun get_bundle_cmd ctxt = get_bundle ctxt o check ctxt;
    54 
    55 
    56 (* define bundle *)
    57 
    58 local
    59 
    60 fun gen_bundle prep_fact prep_att prep_vars (binding, raw_bundle) fixes lthy =
    61   let
    62     val (_, ctxt') = lthy |> prep_vars fixes |-> Proof_Context.add_fixes;
    63     val bundle0 = raw_bundle
    64       |> map (fn (fact, atts) => (prep_fact ctxt' fact, map (prep_att ctxt') atts));
    65     val bundle =
    66       Attrib.partial_evaluation ctxt' [(Attrib.empty_binding, bundle0)] |> map snd |> flat
    67       |> transform_bundle (Proof_Context.export_morphism ctxt' lthy);
    68   in
    69     lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
    70       (fn phi => fn context =>
    71         context |> Data.map
    72           (#2 o Name_Space.define context true
    73             (Morphism.binding phi binding, transform_bundle phi bundle)))
    74   end;
    75 
    76 in
    77 
    78 val bundle = gen_bundle (K I) (K I) Proof_Context.cert_vars;
    79 val bundle_cmd = gen_bundle Proof_Context.get_fact Attrib.check_src Proof_Context.read_vars;
    80 
    81 end;
    82 
    83 
    84 (* include bundles *)
    85 
    86 local
    87 
    88 fun gen_includes get args ctxt =
    89   let val decls = maps (get ctxt) args
    90   in #2 (Attrib.local_notes "" [((Binding.empty, []), decls)] ctxt) end;
    91 
    92 fun gen_context get prep_decl raw_incls raw_elems gthy =
    93   let
    94     val (after_close, lthy) =
    95       gthy |> Context.cases (pair Local_Theory.exit o Named_Target.theory_init)
    96         (pair I o Local_Theory.assert);
    97     val ((_, _, _, lthy'), _) = lthy
    98       |> gen_includes get raw_incls
    99       |> prep_decl ([], []) I raw_elems;
   100   in
   101     lthy' |> Local_Theory.init_target
   102       (Local_Theory.background_naming_of lthy) (Local_Theory.operations_of lthy) after_close
   103   end;
   104 
   105 in
   106 
   107 val includes = gen_includes get_bundle;
   108 val includes_cmd = gen_includes get_bundle_cmd;
   109 
   110 fun include_ bs = Proof.assert_forward #> Proof.map_context (includes bs) #> Proof.reset_facts;
   111 fun include_cmd bs =
   112   Proof.assert_forward #> Proof.map_context (includes_cmd bs) #> Proof.reset_facts;
   113 
   114 fun including bs = Proof.assert_backward #> Proof.map_context (includes bs);
   115 fun including_cmd bs = Proof.assert_backward #> Proof.map_context (includes_cmd bs);
   116 
   117 val context = gen_context get_bundle Expression.cert_declaration;
   118 val context_cmd = gen_context get_bundle_cmd Expression.read_declaration;
   119 
   120 end;
   121 
   122 
   123 (* print_bundles *)
   124 
   125 fun print_bundles ctxt =
   126   let
   127     val prt_thm = Pretty.backquote o Display.pretty_thm ctxt;
   128 
   129     fun prt_fact (ths, []) = map prt_thm ths
   130       | prt_fact (ths, atts) = Pretty.enclose "(" ")"
   131           (Pretty.breaks (map prt_thm ths)) :: Attrib.pretty_attribs ctxt atts;
   132 
   133     fun prt_bundle (name, bundle) =
   134       Pretty.block (Pretty.keyword1 "bundle" :: Pretty.str " " :: Pretty.mark_str name ::
   135         Pretty.breaks (Pretty.str " =" :: maps prt_fact bundle));
   136   in
   137     map prt_bundle (Name_Space.markup_table ctxt (get_bundles ctxt))
   138   end |> Pretty.writeln_chunks;
   139 
   140 end;