author  wenzelm 
Tue, 03 Apr 2012 20:08:08 +0200  
changeset 47314  644a3b74cfd0 
parent 47311  1addbe2a7458 
child 50301  56b4c9afd7be 
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 
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  25 
val print_bundles: Proof.context > unit 
26 
end; 

27 

28 
structure Bundle: BUNDLE = 

29 
struct 

30 

31 
(* maintain bundles *) 

32 

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

34 

35 
fun transform_bundle phi : bundle > bundle = 

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

37 

38 
structure Data = Generic_Data 

39 
( 

40 
type T = bundle Name_Space.table; 

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

42 
val extend = I; 

43 
val merge = Name_Space.merge_tables; 

44 
); 

45 

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

47 

48 
fun the_bundle ctxt name = 

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

50 
SOME bundle => bundle 

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

52 

53 
fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_bundles ctxt); 

54 

55 

56 
(* define bundle *) 

57 

58 
local 

59 

60 
fun gen_bundle prep_fact prep_att prep_vars (binding, raw_bundle) fixes lthy = 

61 
let 

62 
val (_, ctxt') = lthy > prep_vars fixes > Proof_Context.add_fixes; 

63 
val bundle0 = raw_bundle 

64 
> map (fn (fact, atts) => (prep_fact lthy fact, map (prep_att lthy) atts)); 

65 
val bundle = 

66 
Attrib.partial_evaluation ctxt' [(Attrib.empty_binding, bundle0)] > map snd > flat 

67 
> transform_bundle (Proof_Context.export_morphism ctxt' lthy); 

68 
in 

69 
lthy > Local_Theory.declaration {syntax = false, pervasive = true} 

70 
(fn phi => fn context => 

71 
context > Data.map 

72 
(#2 o Name_Space.define context true 

73 
(Morphism.binding phi binding, transform_bundle phi bundle))) 

74 
end; 

75 

76 
in 

77 

78 
val bundle = gen_bundle (K I) (K I) Proof_Context.cert_vars; 

79 
val bundle_cmd = 

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

81 
Proof_Context.read_vars; 

82 

83 
end; 

84 

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  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  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  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  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  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  128 

129 

130 
(* print_bundles *) 

131 

132 
fun print_bundles ctxt = 

133 
let 

134 
val prt_thm = Pretty.backquote o Display.pretty_thm ctxt; 

135 

136 
fun prt_fact (ths, []) = map prt_thm ths 

137 
 prt_fact (ths, atts) = Pretty.enclose "(" ")" 

138 
(Pretty.breaks (map prt_thm ths)) :: Attrib.pretty_attribs ctxt atts; 

139 

140 
fun prt_bundle (name, bundle) = 

141 
Pretty.block (Pretty.command "bundle" :: Pretty.str " " :: Pretty.str name :: 

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

143 
in 

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

145 
end > Pretty.chunks > Pretty.writeln; 

146 

147 
end; 

148 