author  wenzelm 
Wed, 21 Mar 2012 23:41:58 +0100  
changeset 47070  15cd66da537f 
parent 47069  451fc10a81f3 
child 47249  c0481c3c2a6c 
permissions  rwrr 
47057  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 * Args.src list) list 

10 
val the_bundle: Proof.context > string > bundle 

11 
val check: Proof.context > xstring * Position.T > string 

12 
val bundle: binding * (thm list * Args.src list) list > 

13 
(binding * typ option * mixfix) list > local_theory > local_theory 

14 
val bundle_cmd: binding * (Facts.ref * Args.src list) list > 

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  18 
val context_includes: string list > generic_theory > local_theory 
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  24 
val print_bundles: Proof.context > unit 
25 
end; 

26 

27 
structure Bundle: BUNDLE = 

28 
struct 

29 

30 
(* maintain bundles *) 

31 

32 
type bundle = (thm list * Args.src list) list; 

33 

34 
fun transform_bundle phi : bundle > bundle = 

35 
map (fn (fact, atts) => (Morphism.fact phi fact, map (Args.transform_values phi) atts)); 

36 

37 
structure Data = Generic_Data 

38 
( 

39 
type T = bundle Name_Space.table; 

40 
val empty : T = Name_Space.empty_table "bundle"; 

41 
val extend = I; 

42 
val merge = Name_Space.merge_tables; 

43 
); 

44 

45 
val get_bundles = Data.get o Context.Proof; 

46 

47 
fun the_bundle ctxt name = 

48 
(case Symtab.lookup (#2 (get_bundles ctxt)) name of 

49 
SOME bundle => bundle 

50 
 NONE => error ("Unknown bundle " ^ quote name)); 

51 

52 
fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_bundles 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 lthy fact, map (prep_att lthy) 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 = 

79 
gen_bundle Proof_Context.get_fact (Attrib.intern_src o Proof_Context.theory_of) 

80 
Proof_Context.read_vars; 

81 

82 
end; 

83 

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  95 

47069  96 
fun gen_context prep args (Context.Theory thy) = 
97 
Named_Target.theory_init thy 

98 
> Local_Theory.target (gen_includes prep args) 

47070  99 
> Local_Theory.restore 
47069  100 
 gen_context prep args (Context.Proof lthy) = 
101 
Named_Target.assert lthy 

102 
> gen_includes prep args 

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  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  110 
val context_includes = gen_context (K I); 
111 
val context_includes_cmd = gen_context check; 

112 

47068  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  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  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.command "bundle" :: Pretty.str " " :: Pretty.str name :: 

135 
Pretty.breaks (Pretty.str " =" :: maps prt_fact bundle)); 

136 
in 

137 
map prt_bundle (Name_Space.extern_table ctxt (get_bundles ctxt)) 

138 
end > Pretty.chunks > Pretty.writeln; 

139 

140 
end; 

141 