basic support for bundled declarations;
authorwenzelm
Tue Mar 20 20:00:13 2012 +0100 (2012-03-20)
changeset 4705712423b36fcc4
parent 47051 b32e6de4a39b
child 47058 34761733526c
basic support for bundled declarations;
etc/isar-keywords-ZF.el
etc/isar-keywords.el
src/Pure/IsaMakefile
src/Pure/Isar/bundle.ML
src/Pure/Isar/isar_syn.ML
src/Pure/ROOT.ML
     1.1 --- a/etc/isar-keywords-ZF.el	Tue Mar 20 18:01:34 2012 +0100
     1.2 +++ b/etc/isar-keywords-ZF.el	Tue Mar 20 20:00:13 2012 +0100
     1.3 @@ -29,6 +29,7 @@
     1.4      "axiomatization"
     1.5      "axioms"
     1.6      "back"
     1.7 +    "bundle"
     1.8      "by"
     1.9      "cannot_undo"
    1.10      "case"
    1.11 @@ -76,6 +77,8 @@
    1.12      "hide_const"
    1.13      "hide_fact"
    1.14      "hide_type"
    1.15 +    "include"
    1.16 +    "including"
    1.17      "inductive"
    1.18      "inductive_cases"
    1.19      "init_toplevel"
    1.20 @@ -120,6 +123,7 @@
    1.21      "print_ast_translation"
    1.22      "print_attributes"
    1.23      "print_binds"
    1.24 +    "print_bundles"
    1.25      "print_cases"
    1.26      "print_claset"
    1.27      "print_classes"
    1.28 @@ -287,6 +291,7 @@
    1.29      "print_antiquotations"
    1.30      "print_attributes"
    1.31      "print_binds"
    1.32 +    "print_bundles"
    1.33      "print_cases"
    1.34      "print_claset"
    1.35      "print_classes"
    1.36 @@ -342,6 +347,7 @@
    1.37      "attribute_setup"
    1.38      "axiomatization"
    1.39      "axioms"
    1.40 +    "bundle"
    1.41      "class"
    1.42      "classes"
    1.43      "classrel"
    1.44 @@ -458,6 +464,8 @@
    1.45  (defconst isar-keywords-proof-decl
    1.46    '("ML_prf"
    1.47      "also"
    1.48 +    "include"
    1.49 +    "including"
    1.50      "let"
    1.51      "moreover"
    1.52      "note"
     2.1 --- a/etc/isar-keywords.el	Tue Mar 20 18:01:34 2012 +0100
     2.2 +++ b/etc/isar-keywords.el	Tue Mar 20 20:00:13 2012 +0100
     2.3 @@ -35,6 +35,7 @@
     2.4      "boogie_open"
     2.5      "boogie_status"
     2.6      "boogie_vc"
     2.7 +    "bundle"
     2.8      "by"
     2.9      "cannot_undo"
    2.10      "case"
    2.11 @@ -108,6 +109,8 @@
    2.12      "hide_fact"
    2.13      "hide_type"
    2.14      "import_tptp"
    2.15 +    "include"
    2.16 +    "including"
    2.17      "inductive"
    2.18      "inductive_cases"
    2.19      "inductive_set"
    2.20 @@ -162,6 +165,7 @@
    2.21      "print_ast_translation"
    2.22      "print_attributes"
    2.23      "print_binds"
    2.24 +    "print_bundles"
    2.25      "print_cases"
    2.26      "print_claset"
    2.27      "print_classes"
    2.28 @@ -372,6 +376,7 @@
    2.29      "print_antiquotations"
    2.30      "print_attributes"
    2.31      "print_binds"
    2.32 +    "print_bundles"
    2.33      "print_cases"
    2.34      "print_claset"
    2.35      "print_classes"
    2.36 @@ -446,6 +451,7 @@
    2.37      "axioms"
    2.38      "boogie_end"
    2.39      "boogie_open"
    2.40 +    "bundle"
    2.41      "class"
    2.42      "classes"
    2.43      "classrel"
    2.44 @@ -613,6 +619,8 @@
    2.45  (defconst isar-keywords-proof-decl
    2.46    '("ML_prf"
    2.47      "also"
    2.48 +    "include"
    2.49 +    "including"
    2.50      "let"
    2.51      "moreover"
    2.52      "note"
     3.1 --- a/src/Pure/IsaMakefile	Tue Mar 20 18:01:34 2012 +0100
     3.2 +++ b/src/Pure/IsaMakefile	Tue Mar 20 20:00:13 2012 +0100
     3.3 @@ -108,6 +108,7 @@
     3.4    Isar/args.ML						\
     3.5    Isar/attrib.ML					\
     3.6    Isar/auto_bind.ML					\
     3.7 +  Isar/bundle.ML					\
     3.8    Isar/calculation.ML					\
     3.9    Isar/class.ML						\
    3.10    Isar/class_declaration.ML				\
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/Isar/bundle.ML	Tue Mar 20 20:00:13 2012 +0100
     4.3 @@ -0,0 +1,115 @@
     4.4 +(*  Title:      Pure/Isar/bundle.ML
     4.5 +    Author:     Makarius
     4.6 +
     4.7 +Bundled declarations (notes etc.).
     4.8 +*)
     4.9 +
    4.10 +signature BUNDLE =
    4.11 +sig
    4.12 +  type bundle = (thm list * Args.src list) list
    4.13 +  val the_bundle: Proof.context -> string -> bundle
    4.14 +  val check: Proof.context -> xstring * Position.T -> string
    4.15 +  val bundle: binding * (thm list * Args.src list) list ->
    4.16 +    (binding * typ option * mixfix) list -> local_theory -> local_theory
    4.17 +  val bundle_cmd: binding * (Facts.ref * Args.src list) list ->
    4.18 +    (binding * string option * mixfix) list -> local_theory -> local_theory
    4.19 +  val include_: string -> Proof.state -> Proof.state
    4.20 +  val include_cmd: xstring * Position.T -> Proof.state -> Proof.state
    4.21 +  val including: string -> Proof.state -> Proof.state
    4.22 +  val including_cmd: xstring * Position.T -> Proof.state -> Proof.state
    4.23 +  val print_bundles: Proof.context -> unit
    4.24 +end;
    4.25 +
    4.26 +structure Bundle: BUNDLE =
    4.27 +struct
    4.28 +
    4.29 +(* maintain bundles *)
    4.30 +
    4.31 +type bundle = (thm list * Args.src list) list;
    4.32 +
    4.33 +fun transform_bundle phi : bundle -> bundle =
    4.34 +  map (fn (fact, atts) => (Morphism.fact phi fact, map (Args.transform_values phi) atts));
    4.35 +
    4.36 +structure Data = Generic_Data
    4.37 +(
    4.38 +  type T = bundle Name_Space.table;
    4.39 +  val empty : T = Name_Space.empty_table "bundle";
    4.40 +  val extend = I;
    4.41 +  val merge = Name_Space.merge_tables;
    4.42 +);
    4.43 +
    4.44 +val get_bundles = Data.get o Context.Proof;
    4.45 +
    4.46 +fun the_bundle ctxt name =
    4.47 +  (case Symtab.lookup (#2 (get_bundles ctxt)) name of
    4.48 +    SOME bundle => bundle
    4.49 +  | NONE => error ("Unknown bundle " ^ quote name));
    4.50 +
    4.51 +fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_bundles ctxt);
    4.52 +
    4.53 +
    4.54 +(* define bundle *)
    4.55 +
    4.56 +local
    4.57 +
    4.58 +fun gen_bundle prep_fact prep_att prep_vars (binding, raw_bundle) fixes lthy =
    4.59 +  let
    4.60 +    val (_, ctxt') = lthy |> prep_vars fixes |-> Proof_Context.add_fixes;
    4.61 +    val bundle0 = raw_bundle
    4.62 +      |> map (fn (fact, atts) => (prep_fact lthy fact, map (prep_att lthy) atts));
    4.63 +    val bundle =
    4.64 +      Attrib.partial_evaluation ctxt' [(Attrib.empty_binding, bundle0)] |> map snd |> flat
    4.65 +      |> transform_bundle (Proof_Context.export_morphism ctxt' lthy);
    4.66 +  in
    4.67 +    lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
    4.68 +      (fn phi => fn context =>
    4.69 +        context |> Data.map
    4.70 +          (#2 o Name_Space.define context true
    4.71 +            (Morphism.binding phi binding, transform_bundle phi bundle)))
    4.72 +  end;
    4.73 +
    4.74 +in
    4.75 +
    4.76 +val bundle = gen_bundle (K I) (K I) Proof_Context.cert_vars;
    4.77 +val bundle_cmd =
    4.78 +  gen_bundle Proof_Context.get_fact (Attrib.intern_src o Proof_Context.theory_of)
    4.79 +    Proof_Context.read_vars;
    4.80 +
    4.81 +end;
    4.82 +
    4.83 +
    4.84 +(* include bundle *)
    4.85 +
    4.86 +fun gen_include prep raw_name =
    4.87 +  Proof.map_context (fn ctxt =>
    4.88 +    let
    4.89 +      val bundle = the_bundle ctxt (prep ctxt raw_name);
    4.90 +      val attrib = Attrib.attribute_i (Proof_Context.theory_of ctxt);
    4.91 +      val note = ((Binding.empty, []), map (apsnd (map attrib)) bundle);
    4.92 +    in #2 (Proof_Context.note_thmss "" [note] ctxt) end);
    4.93 +
    4.94 +fun include_ name = Proof.assert_forward #> gen_include (K I) name #> Proof.put_facts NONE;
    4.95 +fun include_cmd name = Proof.assert_forward #> gen_include check name #> Proof.put_facts NONE;
    4.96 +fun including name = Proof.assert_backward #> gen_include (K I) name;
    4.97 +fun including_cmd name = Proof.assert_backward #> gen_include check name;
    4.98 +
    4.99 +
   4.100 +(* print_bundles *)
   4.101 +
   4.102 +fun print_bundles ctxt =
   4.103 +  let
   4.104 +    val prt_thm = Pretty.backquote o Display.pretty_thm ctxt;
   4.105 +
   4.106 +    fun prt_fact (ths, []) = map prt_thm ths
   4.107 +      | prt_fact (ths, atts) = Pretty.enclose "(" ")"
   4.108 +          (Pretty.breaks (map prt_thm ths)) :: Attrib.pretty_attribs ctxt atts;
   4.109 +
   4.110 +    fun prt_bundle (name, bundle) =
   4.111 +      Pretty.block (Pretty.command "bundle" :: Pretty.str " " :: Pretty.str name ::
   4.112 +        Pretty.breaks (Pretty.str " =" :: maps prt_fact bundle));
   4.113 +  in
   4.114 +    map prt_bundle (Name_Space.extern_table ctxt (get_bundles ctxt))
   4.115 +  end |> Pretty.chunks |> Pretty.writeln;
   4.116 +
   4.117 +end;
   4.118 +
     5.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Mar 20 18:01:34 2012 +0100
     5.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Mar 20 20:00:13 2012 +0100
     5.3 @@ -414,6 +414,29 @@
     5.4        Toplevel.print o Toplevel.begin_local_theory true (Named_Target.context_cmd name)));
     5.5  
     5.6  
     5.7 +(* bundled declarations *)
     5.8 +
     5.9 +val _ =
    5.10 +  Outer_Syntax.local_theory ("bundle", Keyword.thy_decl) "define bundle of declarations"
    5.11 +    ((Parse.binding --| Parse.$$$ "=") -- Parse_Spec.xthms1 -- Parse.for_fixes
    5.12 +      >> (uncurry Bundle.bundle_cmd));
    5.13 +
    5.14 +val _ =
    5.15 +  Outer_Syntax.command ("include", Keyword.prf_decl)
    5.16 +    "include declarations from bundle in proof body"
    5.17 +    (Parse.position Parse.xname >> (Toplevel.print oo (Toplevel.proof o Bundle.include_cmd)));
    5.18 +
    5.19 +val _ =
    5.20 +  Outer_Syntax.command ("including", Keyword.prf_decl)
    5.21 +    "include declarations from bundle in goal refinement"
    5.22 +    (Parse.position Parse.xname >> (Toplevel.print oo (Toplevel.proof o Bundle.including_cmd)));
    5.23 +
    5.24 +val _ =
    5.25 +  Outer_Syntax.improper_command ("print_bundles", Keyword.diag) "print bundles of declarations"
    5.26 +    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
    5.27 +      Toplevel.keep (Bundle.print_bundles o Toplevel.context_of)));
    5.28 +
    5.29 +
    5.30  (* locales *)
    5.31  
    5.32  val locale_val =
     6.1 --- a/src/Pure/ROOT.ML	Tue Mar 20 18:01:34 2012 +0100
     6.2 +++ b/src/Pure/ROOT.ML	Tue Mar 20 20:00:13 2012 +0100
     6.3 @@ -224,6 +224,7 @@
     6.4  use "Isar/named_target.ML";
     6.5  use "Isar/expression.ML";
     6.6  use "Isar/class_declaration.ML";
     6.7 +use "Isar/bundle.ML";
     6.8  
     6.9  use "simplifier.ML";
    6.10