src/Pure/Isar/bundle.ML
author wenzelm
Tue, 03 Apr 2012 20:08:08 +0200
changeset 47314 644a3b74cfd0
parent 47311 1addbe2a7458
child 50301 56b4c9afd7be
permissions -rw-r--r--
less intrusive visibility;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
47057
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/bundle.ML
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
     3
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
     4
Bundled declarations (notes etc.).
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
     5
*)
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
     6
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
     7
signature BUNDLE =
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
     8
sig
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
     9
  type bundle = (thm list * Args.src list) list
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    10
  val the_bundle: Proof.context -> string -> bundle
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    11
  val check: Proof.context -> xstring * Position.T -> string
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    12
  val bundle: binding * (thm list * Args.src list) list ->
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    13
    (binding * typ option * mixfix) list -> local_theory -> local_theory
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    14
  val bundle_cmd: binding * (Facts.ref * Args.src list) list ->
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    15
    (binding * string option * mixfix) list -> local_theory -> local_theory
47067
4ef29b0c568f optional 'includes' element for long theorem statements;
wenzelm
parents: 47066
diff changeset
    16
  val includes: string list -> Proof.context -> Proof.context
4ef29b0c568f optional 'includes' element for long theorem statements;
wenzelm
parents: 47066
diff changeset
    17
  val includes_cmd: (xstring * Position.T) list -> Proof.context -> Proof.context
47066
8a6124d09ff5 basic support for nested contexts including bundles;
wenzelm
parents: 47057
diff changeset
    18
  val include_: string list -> Proof.state -> Proof.state
8a6124d09ff5 basic support for nested contexts including bundles;
wenzelm
parents: 47057
diff changeset
    19
  val include_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
8a6124d09ff5 basic support for nested contexts including bundles;
wenzelm
parents: 47057
diff changeset
    20
  val including: string list -> Proof.state -> Proof.state
8a6124d09ff5 basic support for nested contexts including bundles;
wenzelm
parents: 47057
diff changeset
    21
  val including_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
47253
a00c5c88d8f3 more general context command with auxiliary fixes/assumes etc.;
wenzelm
parents: 47251
diff changeset
    22
  val context: string list -> Element.context_i list -> generic_theory -> local_theory
a00c5c88d8f3 more general context command with auxiliary fixes/assumes etc.;
wenzelm
parents: 47251
diff changeset
    23
  val context_cmd: (xstring * Position.T) list -> Element.context list ->
a00c5c88d8f3 more general context command with auxiliary fixes/assumes etc.;
wenzelm
parents: 47251
diff changeset
    24
    generic_theory -> local_theory
47057
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    25
  val print_bundles: Proof.context -> unit
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    26
end;
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    27
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    28
structure Bundle: BUNDLE =
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    29
struct
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    30
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    31
(* maintain bundles *)
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    32
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    33
type bundle = (thm list * Args.src list) list;
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    34
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    35
fun transform_bundle phi : bundle -> bundle =
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    36
  map (fn (fact, atts) => (Morphism.fact phi fact, map (Args.transform_values phi) atts));
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    37
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    38
structure Data = Generic_Data
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    39
(
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    40
  type T = bundle Name_Space.table;
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    41
  val empty : T = Name_Space.empty_table "bundle";
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    42
  val extend = I;
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    43
  val merge = Name_Space.merge_tables;
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    44
);
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    45
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    46
val get_bundles = Data.get o Context.Proof;
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    47
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    48
fun the_bundle ctxt name =
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    49
  (case Symtab.lookup (#2 (get_bundles ctxt)) name of
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    50
    SOME bundle => bundle
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    51
  | NONE => error ("Unknown bundle " ^ quote name));
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    52
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    53
fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_bundles ctxt);
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    54
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    55
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    56
(* define bundle *)
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    57
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    58
local
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    59
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    60
fun gen_bundle prep_fact prep_att prep_vars (binding, raw_bundle) fixes lthy =
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    61
  let
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    62
    val (_, ctxt') = lthy |> prep_vars fixes |-> Proof_Context.add_fixes;
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    63
    val bundle0 = raw_bundle
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    64
      |> map (fn (fact, atts) => (prep_fact lthy fact, map (prep_att lthy) atts));
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    65
    val bundle =
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    66
      Attrib.partial_evaluation ctxt' [(Attrib.empty_binding, bundle0)] |> map snd |> flat
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    67
      |> transform_bundle (Proof_Context.export_morphism ctxt' lthy);
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    68
  in
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    69
    lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    70
      (fn phi => fn context =>
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    71
        context |> Data.map
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    72
          (#2 o Name_Space.define context true
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    73
            (Morphism.binding phi binding, transform_bundle phi bundle)))
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    74
  end;
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    75
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    76
in
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    77
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    78
val bundle = gen_bundle (K I) (K I) Proof_Context.cert_vars;
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    79
val bundle_cmd =
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    80
  gen_bundle Proof_Context.get_fact (Attrib.intern_src o Proof_Context.theory_of)
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    81
    Proof_Context.read_vars;
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    82
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    83
end;
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    84
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    85
47066
8a6124d09ff5 basic support for nested contexts including bundles;
wenzelm
parents: 47057
diff changeset
    86
(* include bundles *)
8a6124d09ff5 basic support for nested contexts including bundles;
wenzelm
parents: 47057
diff changeset
    87
8a6124d09ff5 basic support for nested contexts including bundles;
wenzelm
parents: 47057
diff changeset
    88
local
8a6124d09ff5 basic support for nested contexts including bundles;
wenzelm
parents: 47057
diff changeset
    89
47067
4ef29b0c568f optional 'includes' element for long theorem statements;
wenzelm
parents: 47066
diff changeset
    90
fun gen_includes prep args ctxt =
47249
c0481c3c2a6c added Attrib.global_notes/local_notes/generic_notes convenience;
wenzelm
parents: 47070
diff changeset
    91
  let val decls = maps (the_bundle ctxt o prep ctxt) args
c0481c3c2a6c added Attrib.global_notes/local_notes/generic_notes convenience;
wenzelm
parents: 47070
diff changeset
    92
  in #2 (Attrib.local_notes "" [((Binding.empty, []), decls)] ctxt) end;
47057
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    93
47311
1addbe2a7458 close context elements via Expression.cert/read_declaration;
wenzelm
parents: 47253
diff changeset
    94
fun gen_context prep_bundle prep_decl raw_incls raw_elems gthy =
47253
a00c5c88d8f3 more general context command with auxiliary fixes/assumes etc.;
wenzelm
parents: 47251
diff changeset
    95
  let
a00c5c88d8f3 more general context command with auxiliary fixes/assumes etc.;
wenzelm
parents: 47251
diff changeset
    96
    val lthy = Context.cases Named_Target.theory_init Local_Theory.assert gthy;
47311
1addbe2a7458 close context elements via Expression.cert/read_declaration;
wenzelm
parents: 47253
diff changeset
    97
    fun augment ctxt =
1addbe2a7458 close context elements via Expression.cert/read_declaration;
wenzelm
parents: 47253
diff changeset
    98
      let
1addbe2a7458 close context elements via Expression.cert/read_declaration;
wenzelm
parents: 47253
diff changeset
    99
        val ((_, _, _, ctxt'), _) = ctxt
47314
644a3b74cfd0 less intrusive visibility;
wenzelm
parents: 47311
diff changeset
   100
          |> Context_Position.restore_visible lthy
47311
1addbe2a7458 close context elements via Expression.cert/read_declaration;
wenzelm
parents: 47253
diff changeset
   101
          |> gen_includes prep_bundle raw_incls
1addbe2a7458 close context elements via Expression.cert/read_declaration;
wenzelm
parents: 47253
diff changeset
   102
          |> prep_decl ([], []) I raw_elems;
1addbe2a7458 close context elements via Expression.cert/read_declaration;
wenzelm
parents: 47253
diff changeset
   103
      in ctxt' |> Context_Position.restore_visible ctxt end;
47253
a00c5c88d8f3 more general context command with auxiliary fixes/assumes etc.;
wenzelm
parents: 47251
diff changeset
   104
  in
a00c5c88d8f3 more general context command with auxiliary fixes/assumes etc.;
wenzelm
parents: 47251
diff changeset
   105
    (case gthy of
a00c5c88d8f3 more general context command with auxiliary fixes/assumes etc.;
wenzelm
parents: 47251
diff changeset
   106
      Context.Theory _ => Local_Theory.target augment lthy |> Local_Theory.restore
a00c5c88d8f3 more general context command with auxiliary fixes/assumes etc.;
wenzelm
parents: 47251
diff changeset
   107
    | Context.Proof _ =>
a00c5c88d8f3 more general context command with auxiliary fixes/assumes etc.;
wenzelm
parents: 47251
diff changeset
   108
        augment lthy |>
a00c5c88d8f3 more general context command with auxiliary fixes/assumes etc.;
wenzelm
parents: 47251
diff changeset
   109
        Local_Theory.open_target (Local_Theory.naming_of lthy) (Local_Theory.operations_of lthy))
a00c5c88d8f3 more general context command with auxiliary fixes/assumes etc.;
wenzelm
parents: 47251
diff changeset
   110
  end;
47066
8a6124d09ff5 basic support for nested contexts including bundles;
wenzelm
parents: 47057
diff changeset
   111
8a6124d09ff5 basic support for nested contexts including bundles;
wenzelm
parents: 47057
diff changeset
   112
in
47057
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   113
47067
4ef29b0c568f optional 'includes' element for long theorem statements;
wenzelm
parents: 47066
diff changeset
   114
val includes = gen_includes (K I);
4ef29b0c568f optional 'includes' element for long theorem statements;
wenzelm
parents: 47066
diff changeset
   115
val includes_cmd = gen_includes check;
47066
8a6124d09ff5 basic support for nested contexts including bundles;
wenzelm
parents: 47057
diff changeset
   116
47068
2027ff3136cc tuned signature;
wenzelm
parents: 47067
diff changeset
   117
fun include_ bs = Proof.assert_forward #> Proof.map_context (includes bs) #> Proof.reset_facts;
47067
4ef29b0c568f optional 'includes' element for long theorem statements;
wenzelm
parents: 47066
diff changeset
   118
fun include_cmd bs =
47068
2027ff3136cc tuned signature;
wenzelm
parents: 47067
diff changeset
   119
  Proof.assert_forward #> Proof.map_context (includes_cmd bs) #> Proof.reset_facts;
47066
8a6124d09ff5 basic support for nested contexts including bundles;
wenzelm
parents: 47057
diff changeset
   120
47067
4ef29b0c568f optional 'includes' element for long theorem statements;
wenzelm
parents: 47066
diff changeset
   121
fun including bs = Proof.assert_backward #> Proof.map_context (includes bs);
4ef29b0c568f optional 'includes' element for long theorem statements;
wenzelm
parents: 47066
diff changeset
   122
fun including_cmd bs = Proof.assert_backward #> Proof.map_context (includes_cmd bs);
4ef29b0c568f optional 'includes' element for long theorem statements;
wenzelm
parents: 47066
diff changeset
   123
47311
1addbe2a7458 close context elements via Expression.cert/read_declaration;
wenzelm
parents: 47253
diff changeset
   124
val context = gen_context (K I) Expression.cert_declaration;
1addbe2a7458 close context elements via Expression.cert/read_declaration;
wenzelm
parents: 47253
diff changeset
   125
val context_cmd = gen_context check Expression.read_declaration;
47253
a00c5c88d8f3 more general context command with auxiliary fixes/assumes etc.;
wenzelm
parents: 47251
diff changeset
   126
47066
8a6124d09ff5 basic support for nested contexts including bundles;
wenzelm
parents: 47057
diff changeset
   127
end;
47057
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   128
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   129
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   130
(* print_bundles *)
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   131
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   132
fun print_bundles ctxt =
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   133
  let
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   134
    val prt_thm = Pretty.backquote o Display.pretty_thm ctxt;
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   135
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   136
    fun prt_fact (ths, []) = map prt_thm ths
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   137
      | prt_fact (ths, atts) = Pretty.enclose "(" ")"
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   138
          (Pretty.breaks (map prt_thm ths)) :: Attrib.pretty_attribs ctxt atts;
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   139
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   140
    fun prt_bundle (name, bundle) =
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   141
      Pretty.block (Pretty.command "bundle" :: Pretty.str " " :: Pretty.str name ::
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   142
        Pretty.breaks (Pretty.str " =" :: maps prt_fact bundle));
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   143
  in
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   144
    map prt_bundle (Name_Space.extern_table ctxt (get_bundles ctxt))
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   145
  end |> Pretty.chunks |> Pretty.writeln;
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   146
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   147
end;
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   148