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