src/Pure/Isar/bundle.ML
author wenzelm
Wed, 21 Mar 2012 23:41:58 +0100
changeset 47070 15cd66da537f
parent 47069 451fc10a81f3
child 47249 c0481c3c2a6c
permissions -rw-r--r--
actually expose target context;
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
47069
451fc10a81f3 more explicit Toplevel.open_target/close_target;
wenzelm
parents: 47068
diff changeset
    18
  val context_includes: string list -> generic_theory -> local_theory
451fc10a81f3 more explicit Toplevel.open_target/close_target;
wenzelm
parents: 47068
diff changeset
    19
  val context_includes_cmd: (xstring * Position.T) list -> generic_theory -> local_theory
47066
8a6124d09ff5 basic support for nested contexts including bundles;
wenzelm
parents: 47057
diff changeset
    20
  val include_: string list -> Proof.state -> Proof.state
8a6124d09ff5 basic support for nested contexts including bundles;
wenzelm
parents: 47057
diff changeset
    21
  val include_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
8a6124d09ff5 basic support for nested contexts including bundles;
wenzelm
parents: 47057
diff changeset
    22
  val including: string list -> Proof.state -> Proof.state
8a6124d09ff5 basic support for nested contexts including bundles;
wenzelm
parents: 47057
diff changeset
    23
  val including_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
47057
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    24
  val print_bundles: Proof.context -> unit
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    25
end;
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    26
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    27
structure Bundle: BUNDLE =
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    28
struct
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    29
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    30
(* maintain bundles *)
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    31
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    32
type bundle = (thm list * Args.src list) list;
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    33
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    34
fun transform_bundle phi : bundle -> bundle =
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    35
  map (fn (fact, atts) => (Morphism.fact phi fact, map (Args.transform_values phi) atts));
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    36
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    37
structure Data = Generic_Data
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    38
(
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    39
  type T = bundle Name_Space.table;
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    40
  val empty : T = Name_Space.empty_table "bundle";
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    41
  val extend = I;
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    42
  val merge = Name_Space.merge_tables;
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    43
);
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    44
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    45
val get_bundles = Data.get o Context.Proof;
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    46
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    47
fun the_bundle ctxt name =
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    48
  (case Symtab.lookup (#2 (get_bundles ctxt)) name of
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    49
    SOME bundle => bundle
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    50
  | NONE => error ("Unknown bundle " ^ quote name));
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    51
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    52
fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_bundles ctxt);
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    53
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    54
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    55
(* define bundle *)
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    56
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    57
local
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    58
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    59
fun gen_bundle prep_fact prep_att prep_vars (binding, raw_bundle) fixes lthy =
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    60
  let
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    61
    val (_, ctxt') = lthy |> prep_vars fixes |-> Proof_Context.add_fixes;
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    62
    val bundle0 = raw_bundle
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    63
      |> map (fn (fact, atts) => (prep_fact lthy fact, map (prep_att lthy) atts));
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    64
    val bundle =
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    65
      Attrib.partial_evaluation ctxt' [(Attrib.empty_binding, bundle0)] |> map snd |> flat
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    66
      |> transform_bundle (Proof_Context.export_morphism ctxt' lthy);
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    67
  in
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    68
    lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    69
      (fn phi => fn context =>
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    70
        context |> Data.map
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    71
          (#2 o Name_Space.define context true
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    72
            (Morphism.binding phi binding, transform_bundle phi bundle)))
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    73
  end;
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    74
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    75
in
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    76
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    77
val bundle = gen_bundle (K I) (K I) Proof_Context.cert_vars;
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    78
val bundle_cmd =
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    79
  gen_bundle Proof_Context.get_fact (Attrib.intern_src o Proof_Context.theory_of)
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    80
    Proof_Context.read_vars;
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    81
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    82
end;
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    83
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    84
47066
8a6124d09ff5 basic support for nested contexts including bundles;
wenzelm
parents: 47057
diff changeset
    85
(* include bundles *)
8a6124d09ff5 basic support for nested contexts including bundles;
wenzelm
parents: 47057
diff changeset
    86
8a6124d09ff5 basic support for nested contexts including bundles;
wenzelm
parents: 47057
diff changeset
    87
local
8a6124d09ff5 basic support for nested contexts including bundles;
wenzelm
parents: 47057
diff changeset
    88
47067
4ef29b0c568f optional 'includes' element for long theorem statements;
wenzelm
parents: 47066
diff changeset
    89
fun gen_includes prep args ctxt =
47066
8a6124d09ff5 basic support for nested contexts including bundles;
wenzelm
parents: 47057
diff changeset
    90
  let
47067
4ef29b0c568f optional 'includes' element for long theorem statements;
wenzelm
parents: 47066
diff changeset
    91
    val decls = maps (the_bundle ctxt o prep ctxt) args;
47066
8a6124d09ff5 basic support for nested contexts including bundles;
wenzelm
parents: 47057
diff changeset
    92
    val attrib = Attrib.attribute_i (Proof_Context.theory_of ctxt);
47067
4ef29b0c568f optional 'includes' element for long theorem statements;
wenzelm
parents: 47066
diff changeset
    93
    val note = ((Binding.empty, []), map (apsnd (map attrib)) decls);
47066
8a6124d09ff5 basic support for nested contexts including bundles;
wenzelm
parents: 47057
diff changeset
    94
  in #2 (Proof_Context.note_thmss "" [note] ctxt) end;
47057
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
    95
47069
451fc10a81f3 more explicit Toplevel.open_target/close_target;
wenzelm
parents: 47068
diff changeset
    96
fun gen_context prep args (Context.Theory thy) =
451fc10a81f3 more explicit Toplevel.open_target/close_target;
wenzelm
parents: 47068
diff changeset
    97
      Named_Target.theory_init thy
451fc10a81f3 more explicit Toplevel.open_target/close_target;
wenzelm
parents: 47068
diff changeset
    98
      |> Local_Theory.target (gen_includes prep args)
47070
15cd66da537f actually expose target context;
wenzelm
parents: 47069
diff changeset
    99
      |> Local_Theory.restore
47069
451fc10a81f3 more explicit Toplevel.open_target/close_target;
wenzelm
parents: 47068
diff changeset
   100
  | gen_context prep args (Context.Proof lthy) =
451fc10a81f3 more explicit Toplevel.open_target/close_target;
wenzelm
parents: 47068
diff changeset
   101
      Named_Target.assert lthy
451fc10a81f3 more explicit Toplevel.open_target/close_target;
wenzelm
parents: 47068
diff changeset
   102
      |> gen_includes prep args
451fc10a81f3 more explicit Toplevel.open_target/close_target;
wenzelm
parents: 47068
diff changeset
   103
      |> Local_Theory.open_target (Local_Theory.naming_of lthy) (Local_Theory.operations_of lthy);
47066
8a6124d09ff5 basic support for nested contexts including bundles;
wenzelm
parents: 47057
diff changeset
   104
8a6124d09ff5 basic support for nested contexts including bundles;
wenzelm
parents: 47057
diff changeset
   105
in
47057
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   106
47067
4ef29b0c568f optional 'includes' element for long theorem statements;
wenzelm
parents: 47066
diff changeset
   107
val includes = gen_includes (K I);
4ef29b0c568f optional 'includes' element for long theorem statements;
wenzelm
parents: 47066
diff changeset
   108
val includes_cmd = gen_includes check;
47066
8a6124d09ff5 basic support for nested contexts including bundles;
wenzelm
parents: 47057
diff changeset
   109
47069
451fc10a81f3 more explicit Toplevel.open_target/close_target;
wenzelm
parents: 47068
diff changeset
   110
val context_includes = gen_context (K I);
451fc10a81f3 more explicit Toplevel.open_target/close_target;
wenzelm
parents: 47068
diff changeset
   111
val context_includes_cmd = gen_context check;
451fc10a81f3 more explicit Toplevel.open_target/close_target;
wenzelm
parents: 47068
diff changeset
   112
47068
2027ff3136cc tuned signature;
wenzelm
parents: 47067
diff changeset
   113
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
   114
fun include_cmd bs =
47068
2027ff3136cc tuned signature;
wenzelm
parents: 47067
diff changeset
   115
  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
   116
47067
4ef29b0c568f optional 'includes' element for long theorem statements;
wenzelm
parents: 47066
diff changeset
   117
fun including bs = Proof.assert_backward #> Proof.map_context (includes bs);
4ef29b0c568f optional 'includes' element for long theorem statements;
wenzelm
parents: 47066
diff changeset
   118
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
   119
47066
8a6124d09ff5 basic support for nested contexts including bundles;
wenzelm
parents: 47057
diff changeset
   120
end;
47057
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   121
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   122
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   123
(* print_bundles *)
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   124
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   125
fun print_bundles ctxt =
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   126
  let
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   127
    val prt_thm = Pretty.backquote o Display.pretty_thm ctxt;
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   128
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   129
    fun prt_fact (ths, []) = map prt_thm ths
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   130
      | prt_fact (ths, atts) = Pretty.enclose "(" ")"
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   131
          (Pretty.breaks (map prt_thm ths)) :: Attrib.pretty_attribs ctxt atts;
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   132
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   133
    fun prt_bundle (name, bundle) =
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   134
      Pretty.block (Pretty.command "bundle" :: Pretty.str " " :: Pretty.str name ::
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   135
        Pretty.breaks (Pretty.str " =" :: maps prt_fact bundle));
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   136
  in
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   137
    map prt_bundle (Name_Space.extern_table ctxt (get_bundles ctxt))
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   138
  end |> Pretty.chunks |> Pretty.writeln;
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   139
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   140
end;
12423b36fcc4 basic support for bundled declarations;
wenzelm
parents:
diff changeset
   141