author  wenzelm 
Fri, 28 Aug 2015 23:21:04 +0200  
changeset 61044  b7af255dd200 
parent 60948  b710a5087116 
child 61045  c7a7f063704a 
permissions  rwrr 
6185  1 
(* Title: Pure/context.ML 
2 
Author: Markus Wenzel, TU Muenchen 

3 

16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

4 
Generic theory contexts with unique identity, arbitrarily typed data, 
24141
73baca986087
improved check_thy: produce a checked theory_ref (threadsafe version);
wenzelm
parents:
23944
diff
changeset

5 
monotonic development graph and history support. Generic proof 
73baca986087
improved check_thy: produce a checked theory_ref (threadsafe version);
wenzelm
parents:
23944
diff
changeset

6 
contexts with arbitrarily typed data. 
33031
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32784
diff
changeset

7 

b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32784
diff
changeset

8 
Firm naming conventions: 
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32784
diff
changeset

9 
thy, thy', thy1, thy2: theory 
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32784
diff
changeset

10 
ctxt, ctxt', ctxt1, ctxt2: Proof.context 
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32784
diff
changeset

11 
context: Context.generic 
6185  12 
*) 
13 

14 
signature BASIC_CONTEXT = 

15 
sig 

16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

16 
type theory 
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

17 
exception THEORY of string * theory list 
33031
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32784
diff
changeset

18 
structure Proof: sig type context end 
42360  19 
structure Proof_Context: 
33031
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32784
diff
changeset

20 
sig 
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32784
diff
changeset

21 
val theory_of: Proof.context > theory 
36610
bafd82950e24
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
wenzelm
parents:
34259
diff
changeset

22 
val init_global: theory > Proof.context 
51686  23 
val get_global: theory > string > Proof.context 
33031
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32784
diff
changeset

24 
end 
6185  25 
end; 
26 

27 
signature CONTEXT = 

28 
sig 

29 
include BASIC_CONTEXT 

16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

30 
(*theory context*) 
60947  31 
type theory_id 
32 
val theory_id: theory > theory_id 

42818
128cc195ced3
timing of Theory_Data operations, with implicit thread positions when functor is applied;
wenzelm
parents:
42383
diff
changeset

33 
val timing: bool Unsynchronized.ref 
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42360
diff
changeset

34 
type pretty 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

35 
val parents_of: theory > theory list 
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

36 
val ancestors_of: theory > theory list 
60948  37 
val theory_id_name: theory_id > string 
29069
c7ba485581ae
unified ids for ancestors and checkpoints, removed obsolete history of checkpoints;
wenzelm
parents:
29001
diff
changeset

38 
val theory_name: theory > string 
29093
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

39 
val PureN: string 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

40 
val display_name: theory_id > string 
29093
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

41 
val display_names: theory > string list 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

42 
val pretty_thy: theory > Pretty.T 
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

43 
val string_of_thy: theory > string 
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

44 
val pretty_abbrev_thy: theory > Pretty.T 
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

45 
val str_of_thy: theory > string 
37867
b9783e9e96e1
added Context.get_theory  avoid referring to accidental theory loader state (cf. Thy_Info.get_theory);
wenzelm
parents:
37852
diff
changeset

46 
val get_theory: theory > string > theory 
37871
c7ce7685e087
replaced Thy_Info.the_theory by Context.this_theory  avoid referring to accidental theory loader state;
wenzelm
parents:
37867
diff
changeset

47 
val this_theory: theory > string > theory 
60947  48 
val eq_thy_id: theory_id * theory_id > bool 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

49 
val eq_thy: theory * theory > bool 
60947  50 
val proper_subthy_id: theory_id * theory_id > bool 
51 
val proper_subthy: theory * theory > bool 

52 
val subthy_id: theory_id * theory_id > bool 

16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

53 
val subthy: theory * theory > bool 
16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

54 
val finish_thy: theory > theory 
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42360
diff
changeset

55 
val begin_thy: (theory > pretty) > string > theory list > theory 
16533  56 
(*proof context*) 
33031
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32784
diff
changeset

57 
val raw_transfer: theory > Proof.context > Proof.context 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

58 
(*certificate*) 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

59 
datatype certificate = Certificate of theory  Certificate_Id of theory_id 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

60 
val certificate_theory: certificate > theory 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

61 
val certificate_theory_id: certificate > theory_id 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

62 
val eq_certificate: certificate * certificate > bool 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

63 
val join_certificate: certificate * certificate > certificate 
16533  64 
(*generic context*) 
33031
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32784
diff
changeset

65 
datatype generic = Theory of theory  Proof of Proof.context 
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32784
diff
changeset

66 
val cases: (theory > 'a) > (Proof.context > 'a) > generic > 'a 
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32784
diff
changeset

67 
val mapping: (theory > theory) > (Proof.context > Proof.context) > generic > generic 
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32784
diff
changeset

68 
val mapping_result: (theory > 'a * theory) > (Proof.context > 'a * Proof.context) > 
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32784
diff
changeset

69 
generic > 'a * generic 
18632  70 
val the_theory: generic > theory 
33031
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32784
diff
changeset

71 
val the_proof: generic > Proof.context 
18731  72 
val map_theory: (theory > theory) > generic > generic 
33031
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32784
diff
changeset

73 
val map_proof: (Proof.context > Proof.context) > generic > generic 
26486  74 
val map_theory_result: (theory > 'a * theory) > generic > 'a * generic 
33031
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32784
diff
changeset

75 
val map_proof_result: (Proof.context > 'a * Proof.context) > generic > 'a * generic 
18731  76 
val theory_map: (generic > generic) > theory > theory 
33031
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32784
diff
changeset

77 
val proof_map: (generic > generic) > Proof.context > Proof.context 
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32784
diff
changeset

78 
val theory_of: generic > theory (*total*) 
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32784
diff
changeset

79 
val proof_of: generic > Proof.context (*total*) 
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42360
diff
changeset

80 
(*pretty printing context*) 
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42360
diff
changeset

81 
val pretty: Proof.context > pretty 
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42360
diff
changeset

82 
val pretty_global: theory > pretty 
47005
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
43684
diff
changeset

83 
val pretty_generic: generic > pretty 
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42360
diff
changeset

84 
val pretty_context: (theory > Proof.context) > pretty > Proof.context 
26413
003dd6155870
added thread data (formerly global ref in ML/ml_context.ML);
wenzelm
parents:
24559
diff
changeset

85 
(*thread data*) 
003dd6155870
added thread data (formerly global ref in ML/ml_context.ML);
wenzelm
parents:
24559
diff
changeset

86 
val thread_data: unit > generic option 
003dd6155870
added thread data (formerly global ref in ML/ml_context.ML);
wenzelm
parents:
24559
diff
changeset

87 
val the_thread_data: unit > generic 
003dd6155870
added thread data (formerly global ref in ML/ml_context.ML);
wenzelm
parents:
24559
diff
changeset

88 
val set_thread_data: generic option > unit 
003dd6155870
added thread data (formerly global ref in ML/ml_context.ML);
wenzelm
parents:
24559
diff
changeset

89 
val setmp_thread_data: generic option > ('a > 'b) > 'a > 'b 
26463  90 
val >> : (generic > generic) > unit 
91 
val >>> : (generic > 'a * generic) > 'a 

6185  92 
end; 
93 

16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

94 
signature PRIVATE_CONTEXT = 
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

95 
sig 
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

96 
include CONTEXT 
33033  97 
structure Theory_Data: 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

98 
sig 
51368
2ea5c7c2d825
tuned signature  prefer terminology of Scala and Axiom;
wenzelm
parents:
50431
diff
changeset

99 
val declare: Position.T > Any.T > (Any.T > Any.T) > 
2ea5c7c2d825
tuned signature  prefer terminology of Scala and Axiom;
wenzelm
parents:
50431
diff
changeset

100 
(pretty > Any.T * Any.T > Any.T) > serial 
2ea5c7c2d825
tuned signature  prefer terminology of Scala and Axiom;
wenzelm
parents:
50431
diff
changeset

101 
val get: serial > (Any.T > 'a) > theory > 'a 
2ea5c7c2d825
tuned signature  prefer terminology of Scala and Axiom;
wenzelm
parents:
50431
diff
changeset

102 
val put: serial > ('a > Any.T) > 'a > theory > theory 
16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

103 
end 
33033  104 
structure Proof_Data: 
16533  105 
sig 
51368
2ea5c7c2d825
tuned signature  prefer terminology of Scala and Axiom;
wenzelm
parents:
50431
diff
changeset

106 
val declare: (theory > Any.T) > serial 
2ea5c7c2d825
tuned signature  prefer terminology of Scala and Axiom;
wenzelm
parents:
50431
diff
changeset

107 
val get: serial > (Any.T > 'a) > Proof.context > 'a 
2ea5c7c2d825
tuned signature  prefer terminology of Scala and Axiom;
wenzelm
parents:
50431
diff
changeset

108 
val put: serial > ('a > Any.T) > 'a > Proof.context > Proof.context 
16533  109 
end 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

110 
end; 
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

111 

7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

112 
structure Context: PRIVATE_CONTEXT = 
6185  113 
struct 
114 

16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

115 
(*** theory context ***) 
6185  116 

16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

117 
(** theory data **) 
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

118 

f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

119 
(* data kinds and access methods *) 
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

120 

42818
128cc195ced3
timing of Theory_Data operations, with implicit thread positions when functor is applied;
wenzelm
parents:
42383
diff
changeset

121 
val timing = Unsynchronized.ref false; 
128cc195ced3
timing of Theory_Data operations, with implicit thread positions when functor is applied;
wenzelm
parents:
42383
diff
changeset

122 

19028
6c238953f66c
structure Datatab: private copy avoids potential conflict of table exceptions;
wenzelm
parents:
18931
diff
changeset

123 
(*private copy avoids potential conflict of table exceptions*) 
31971
8c1b845ed105
renamed functor TableFun to Table, and GraphFun to Graph;
wenzelm
parents:
30628
diff
changeset

124 
structure Datatab = Table(type key = int val ord = int_ord); 
19028
6c238953f66c
structure Datatab: private copy avoids potential conflict of table exceptions;
wenzelm
parents:
18931
diff
changeset

125 

51368
2ea5c7c2d825
tuned signature  prefer terminology of Scala and Axiom;
wenzelm
parents:
50431
diff
changeset

126 
datatype pretty = Pretty of Any.T; 
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42360
diff
changeset

127 

16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

128 
local 
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

129 

f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

130 
type kind = 
42818
128cc195ced3
timing of Theory_Data operations, with implicit thread positions when functor is applied;
wenzelm
parents:
42383
diff
changeset

131 
{pos: Position.T, 
51368
2ea5c7c2d825
tuned signature  prefer terminology of Scala and Axiom;
wenzelm
parents:
50431
diff
changeset

132 
empty: Any.T, 
2ea5c7c2d825
tuned signature  prefer terminology of Scala and Axiom;
wenzelm
parents:
50431
diff
changeset

133 
extend: Any.T > Any.T, 
2ea5c7c2d825
tuned signature  prefer terminology of Scala and Axiom;
wenzelm
parents:
50431
diff
changeset

134 
merge: pretty > Any.T * Any.T > Any.T}; 
16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

135 

43684  136 
val kinds = Synchronized.var "Theory_Data" (Datatab.empty: kind Datatab.table); 
16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

137 

42818
128cc195ced3
timing of Theory_Data operations, with implicit thread positions when functor is applied;
wenzelm
parents:
42383
diff
changeset

138 
fun invoke name f k x = 
43684  139 
(case Datatab.lookup (Synchronized.value kinds) k of 
42818
128cc195ced3
timing of Theory_Data operations, with implicit thread positions when functor is applied;
wenzelm
parents:
42383
diff
changeset

140 
SOME kind => 
128cc195ced3
timing of Theory_Data operations, with implicit thread positions when functor is applied;
wenzelm
parents:
42383
diff
changeset

141 
if ! timing andalso name <> "" then 
48992  142 
Timing.cond_timeit true ("Theory_Data." ^ name ^ Position.here (#pos kind)) 
42818
128cc195ced3
timing of Theory_Data operations, with implicit thread positions when functor is applied;
wenzelm
parents:
42383
diff
changeset

143 
(fn () => f kind x) 
128cc195ced3
timing of Theory_Data operations, with implicit thread positions when functor is applied;
wenzelm
parents:
42383
diff
changeset

144 
else f kind x 
37852
a902f158b4fc
eliminated oldstyle sys_error/SYS_ERROR in favour of exception Fail  after careful checking that there is no overlap with existing handling of that;
wenzelm
parents:
37216
diff
changeset

145 
 NONE => raise Fail "Invalid theory data identifier"); 
16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

146 

f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

147 
in 
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

148 

42818
128cc195ced3
timing of Theory_Data operations, with implicit thread positions when functor is applied;
wenzelm
parents:
42383
diff
changeset

149 
fun invoke_empty k = invoke "" (K o #empty) k (); 
128cc195ced3
timing of Theory_Data operations, with implicit thread positions when functor is applied;
wenzelm
parents:
42383
diff
changeset

150 
val invoke_extend = invoke "extend" #extend; 
128cc195ced3
timing of Theory_Data operations, with implicit thread positions when functor is applied;
wenzelm
parents:
42383
diff
changeset

151 
fun invoke_merge pp = invoke "merge" (fn kind => #merge kind pp); 
16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

152 

42818
128cc195ced3
timing of Theory_Data operations, with implicit thread positions when functor is applied;
wenzelm
parents:
42383
diff
changeset

153 
fun declare_theory_data pos empty extend merge = 
16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

154 
let 
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

155 
val k = serial (); 
42818
128cc195ced3
timing of Theory_Data operations, with implicit thread positions when functor is applied;
wenzelm
parents:
42383
diff
changeset

156 
val kind = {pos = pos, empty = empty, extend = extend, merge = merge}; 
43684  157 
val _ = Synchronized.change kinds (Datatab.update (k, kind)); 
16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

158 
in k end; 
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

159 

39020  160 
val extend_data = Datatab.map invoke_extend; 
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
55547
diff
changeset

161 
fun merge_data pp = Datatab.join (invoke_merge pp) o apply2 extend_data; 
16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

162 

f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

163 
end; 
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

164 

f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

165 

f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

166 

f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

167 
(** datatype theory **) 
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

168 

60947  169 
datatype theory_id = 
170 
Theory_Id of 

16533  171 
(*identity*) 
52696
38466f4f3483
immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 > 100000, JinjaThreads: 65000 > 300000)  minimal measurable impact on inference kernel performance;
wenzelm
parents:
52682
diff
changeset

172 
{id: serial, (*identifier*) 
38466f4f3483
immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 > 100000, JinjaThreads: 65000 > 300000)  minimal measurable impact on inference kernel performance;
wenzelm
parents:
52682
diff
changeset

173 
ids: Inttab.set} * (*cumulative identifiers  symbolic body content*) 
29095  174 
(*history*) 
29093
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

175 
{name: string, (*official theory name*) 
52696
38466f4f3483
immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 > 100000, JinjaThreads: 65000 > 300000)  minimal measurable impact on inference kernel performance;
wenzelm
parents:
52682
diff
changeset

176 
stage: int}; (*counter for anonymous updates*) 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

177 

60947  178 
datatype theory = 
179 
Theory of 

180 
theory_id * 

181 
(*ancestry*) 

182 
{parents: theory list, (*immediate predecessors*) 

183 
ancestors: theory list} * (*all predecessors  canonical reverse order*) 

184 
(*data*) 

185 
Any.T Datatab.table; (*body content*) 

186 

16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

187 
exception THEORY of string * theory list; 
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

188 

60947  189 
fun rep_theory_id (Theory_Id args) = args; 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

190 
fun rep_theory (Theory args) = args; 
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

191 

60947  192 
val theory_id = #1 o rep_theory; 
193 

194 
val identity_of_id = #1 o rep_theory_id; 

195 
val identity_of = identity_of_id o theory_id; 

196 
val history_of_id = #2 o rep_theory_id; 

197 
val history_of = history_of_id o theory_id; 

198 
val ancestry_of = #2 o rep_theory; 

199 
val data_of = #3 o rep_theory; 

16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

200 

52696
38466f4f3483
immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 > 100000, JinjaThreads: 65000 > 300000)  minimal measurable impact on inference kernel performance;
wenzelm
parents:
52682
diff
changeset

201 
fun make_identity id ids = {id = id, ids = ids}; 
60947  202 
fun make_history name stage = {name = name, stage = stage}; 
16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

203 
fun make_ancestry parents ancestors = {parents = parents, ancestors = ancestors}; 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

204 

60948  205 
val theory_id_name = #name o history_of_id; 
60947  206 
val theory_name = #name o history_of; 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

207 
val parents_of = #parents o ancestry_of; 
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

208 
val ancestors_of = #ancestors o ancestry_of; 
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

209 

7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

210 

29093
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

211 
(* names *) 
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

212 

1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

213 
val PureN = "Pure"; 
29095  214 
val finished = ~1; 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

215 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

216 
fun display_name thy_id = 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

217 
let val {name, stage} = history_of_id thy_id 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

218 
in if stage = finished then name else name ^ ":" ^ string_of_int stage end; 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

219 

29093
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

220 
fun display_names thy = 
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

221 
let 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

222 
val name = display_name (theory_id thy); 
29093
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

223 
val ancestor_names = map theory_name (ancestors_of thy); 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

224 
in rev (name :: ancestor_names) end; 
29069
c7ba485581ae
unified ids for ancestors and checkpoints, removed obsolete history of checkpoints;
wenzelm
parents:
29001
diff
changeset

225 

29093
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

226 
val pretty_thy = Pretty.str_list "{" "}" o display_names; 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

227 
val string_of_thy = Pretty.string_of o pretty_thy; 
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

228 

7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

229 
fun pretty_abbrev_thy thy = 
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

230 
let 
29093
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

231 
val names = display_names thy; 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

232 
val n = length names; 
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

233 
val abbrev = if n > 5 then "..." :: List.drop (names, n  5) else names; 
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

234 
in Pretty.str_list "{" "}" abbrev end; 
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

235 

7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

236 
val str_of_thy = Pretty.str_of o pretty_abbrev_thy; 
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

237 

37867
b9783e9e96e1
added Context.get_theory  avoid referring to accidental theory loader state (cf. Thy_Info.get_theory);
wenzelm
parents:
37852
diff
changeset

238 
fun get_theory thy name = 
b9783e9e96e1
added Context.get_theory  avoid referring to accidental theory loader state (cf. Thy_Info.get_theory);
wenzelm
parents:
37852
diff
changeset

239 
if theory_name thy <> name then 
b9783e9e96e1
added Context.get_theory  avoid referring to accidental theory loader state (cf. Thy_Info.get_theory);
wenzelm
parents:
37852
diff
changeset

240 
(case find_first (fn thy' => theory_name thy' = name) (ancestors_of thy) of 
b9783e9e96e1
added Context.get_theory  avoid referring to accidental theory loader state (cf. Thy_Info.get_theory);
wenzelm
parents:
37852
diff
changeset

241 
SOME thy' => thy' 
b9783e9e96e1
added Context.get_theory  avoid referring to accidental theory loader state (cf. Thy_Info.get_theory);
wenzelm
parents:
37852
diff
changeset

242 
 NONE => error ("Unknown ancestor theory " ^ quote name)) 
b9783e9e96e1
added Context.get_theory  avoid referring to accidental theory loader state (cf. Thy_Info.get_theory);
wenzelm
parents:
37852
diff
changeset

243 
else if #stage (history_of thy) = finished then thy 
b9783e9e96e1
added Context.get_theory  avoid referring to accidental theory loader state (cf. Thy_Info.get_theory);
wenzelm
parents:
37852
diff
changeset

244 
else error ("Unfinished theory " ^ quote name); 
b9783e9e96e1
added Context.get_theory  avoid referring to accidental theory loader state (cf. Thy_Info.get_theory);
wenzelm
parents:
37852
diff
changeset

245 

37871
c7ce7685e087
replaced Thy_Info.the_theory by Context.this_theory  avoid referring to accidental theory loader state;
wenzelm
parents:
37867
diff
changeset

246 
fun this_theory thy name = 
c7ce7685e087
replaced Thy_Info.the_theory by Context.this_theory  avoid referring to accidental theory loader state;
wenzelm
parents:
37867
diff
changeset

247 
if theory_name thy = name then thy 
c7ce7685e087
replaced Thy_Info.the_theory by Context.this_theory  avoid referring to accidental theory loader state;
wenzelm
parents:
37867
diff
changeset

248 
else get_theory thy name; 
c7ce7685e087
replaced Thy_Info.the_theory by Context.this_theory  avoid referring to accidental theory loader state;
wenzelm
parents:
37867
diff
changeset

249 

16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

250 

29093
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

251 
(* build ids *) 
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

252 

52696
38466f4f3483
immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 > 100000, JinjaThreads: 65000 > 300000)  minimal measurable impact on inference kernel performance;
wenzelm
parents:
52682
diff
changeset

253 
fun insert_id id ids = Inttab.update (id, ()) ids; 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

254 

29093
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

255 
fun merge_ids 
60947  256 
(Theory (Theory_Id ({id = id1, ids = ids1, ...}, _), _, _)) 
257 
(Theory (Theory_Id ({id = id2, ids = ids2, ...}, _), _, _)) = 

29093
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

258 
Inttab.merge (K true) (ids1, ids2) 
52696
38466f4f3483
immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 > 100000, JinjaThreads: 65000 > 300000)  minimal measurable impact on inference kernel performance;
wenzelm
parents:
52682
diff
changeset

259 
> insert_id id1 
38466f4f3483
immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 > 100000, JinjaThreads: 65000 > 300000)  minimal measurable impact on inference kernel performance;
wenzelm
parents:
52682
diff
changeset

260 
> insert_id id2; 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

261 

7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

262 

16533  263 
(* equality and inclusion *) 
264 

60947  265 
val eq_thy_id = op = o apply2 (#id o identity_of_id); 
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
55547
diff
changeset

266 
val eq_thy = op = o apply2 (#id o identity_of); 
16533  267 

60947  268 
fun proper_subthy_id (Theory_Id ({id, ...}, _), Theory_Id ({ids, ...}, _)) = Inttab.defined ids id; 
269 
val proper_subthy = proper_subthy_id o apply2 theory_id; 

16533  270 

60947  271 
fun subthy_id p = eq_thy_id p orelse proper_subthy_id p; 
272 
val subthy = subthy_id o apply2 theory_id; 

16533  273 

274 

29093
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

275 
(* consistent ancestors *) 
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

276 

50431
955c4aa44f60
check consistent theory names for direct imports as well  as claimed in the comments (see also 1cc36c0ec9eb);
wenzelm
parents:
48992
diff
changeset

277 
fun eq_thy_consistent (thy1, thy2) = 
955c4aa44f60
check consistent theory names for direct imports as well  as claimed in the comments (see also 1cc36c0ec9eb);
wenzelm
parents:
48992
diff
changeset

278 
eq_thy (thy1, thy2) orelse 
955c4aa44f60
check consistent theory names for direct imports as well  as claimed in the comments (see also 1cc36c0ec9eb);
wenzelm
parents:
48992
diff
changeset

279 
(theory_name thy1 = theory_name thy2 andalso 
955c4aa44f60
check consistent theory names for direct imports as well  as claimed in the comments (see also 1cc36c0ec9eb);
wenzelm
parents:
48992
diff
changeset

280 
raise THEORY ("Duplicate theory name", [thy1, thy2])); 
955c4aa44f60
check consistent theory names for direct imports as well  as claimed in the comments (see also 1cc36c0ec9eb);
wenzelm
parents:
48992
diff
changeset

281 

29093
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

282 
fun extend_ancestors thy thys = 
50431
955c4aa44f60
check consistent theory names for direct imports as well  as claimed in the comments (see also 1cc36c0ec9eb);
wenzelm
parents:
48992
diff
changeset

283 
if member eq_thy_consistent thys thy then 
33033  284 
raise THEORY ("Duplicate theory node", thy :: thys) 
29093
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

285 
else thy :: thys; 
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

286 

50431
955c4aa44f60
check consistent theory names for direct imports as well  as claimed in the comments (see also 1cc36c0ec9eb);
wenzelm
parents:
48992
diff
changeset

287 
val merge_ancestors = merge eq_thy_consistent; 
29093
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

288 

1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

289 

16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

290 

f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

291 
(** build theories **) 
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

292 

f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

293 
(* primitives *) 
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

294 

60947  295 
fun create_thy ids history ancestry data = 
296 
Theory (Theory_Id (make_identity (serial ()) ids, history), ancestry, data); 

33606
2b27020ffcb2
local mutex for theory content/identity operations;
wenzelm
parents:
33517
diff
changeset

297 

52696
38466f4f3483
immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 > 100000, JinjaThreads: 65000 > 300000)  minimal measurable impact on inference kernel performance;
wenzelm
parents:
52682
diff
changeset

298 
val pre_pure_thy = 
60947  299 
create_thy Inttab.empty (make_history PureN 0) (make_ancestry [] []) Datatab.empty; 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

300 

52696
38466f4f3483
immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 > 100000, JinjaThreads: 65000 > 300000)  minimal measurable impact on inference kernel performance;
wenzelm
parents:
52682
diff
changeset

301 
local 
38466f4f3483
immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 > 100000, JinjaThreads: 65000 > 300000)  minimal measurable impact on inference kernel performance;
wenzelm
parents:
52682
diff
changeset

302 

38466f4f3483
immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 > 100000, JinjaThreads: 65000 > 300000)  minimal measurable impact on inference kernel performance;
wenzelm
parents:
52682
diff
changeset

303 
fun change_thy finish f thy = 
16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

304 
let 
60947  305 
val Theory (Theory_Id ({id, ids}, {name, stage}), ancestry, data) = thy; 
306 
val (ancestry', data') = 

52696
38466f4f3483
immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 > 100000, JinjaThreads: 65000 > 300000)  minimal measurable impact on inference kernel performance;
wenzelm
parents:
52682
diff
changeset

307 
if stage = finished then 
60947  308 
(make_ancestry [thy] (extend_ancestors thy (ancestors_of thy)), extend_data data) 
309 
else (ancestry, data); 

52696
38466f4f3483
immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 > 100000, JinjaThreads: 65000 > 300000)  minimal measurable impact on inference kernel performance;
wenzelm
parents:
52682
diff
changeset

310 
val history' = {name = name, stage = if finish then finished else stage + 1}; 
38466f4f3483
immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 > 100000, JinjaThreads: 65000 > 300000)  minimal measurable impact on inference kernel performance;
wenzelm
parents:
52682
diff
changeset

311 
val ids' = insert_id id ids; 
16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

312 
val data'' = f data'; 
60947  313 
in create_thy ids' history' ancestry' data'' end; 
16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

314 

52696
38466f4f3483
immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 > 100000, JinjaThreads: 65000 > 300000)  minimal measurable impact on inference kernel performance;
wenzelm
parents:
52682
diff
changeset

315 
in 
16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

316 

52696
38466f4f3483
immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 > 100000, JinjaThreads: 65000 > 300000)  minimal measurable impact on inference kernel performance;
wenzelm
parents:
52682
diff
changeset

317 
val update_thy = change_thy false; 
38466f4f3483
immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 > 100000, JinjaThreads: 65000 > 300000)  minimal measurable impact on inference kernel performance;
wenzelm
parents:
52682
diff
changeset

318 
val extend_thy = update_thy I; 
38466f4f3483
immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 > 100000, JinjaThreads: 65000 > 300000)  minimal measurable impact on inference kernel performance;
wenzelm
parents:
52682
diff
changeset

319 
val finish_thy = change_thy true I; 
16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

320 

52696
38466f4f3483
immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 > 100000, JinjaThreads: 65000 > 300000)  minimal measurable impact on inference kernel performance;
wenzelm
parents:
52682
diff
changeset

321 
end; 
16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

322 

f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

323 

f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

324 
(* named theory nodes *) 
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

325 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

326 
local 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

327 

16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

328 
fun merge_thys pp (thy1, thy2) = 
26957  329 
let 
29093
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

330 
val ids = merge_ids thy1 thy2; 
60947  331 
val history = make_history "" 0; 
26957  332 
val ancestry = make_ancestry [] []; 
60947  333 
val data = merge_data (pp thy1) (data_of thy1, data_of thy2); 
334 
in create_thy ids history ancestry data end; 

16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

335 

16533  336 
fun maximal_thys thys = 
28617  337 
thys > filter_out (fn thy => exists (fn thy' => proper_subthy (thy, thy')) thys); 
16533  338 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

339 
in 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

340 

16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

341 
fun begin_thy pp name imports = 
52696
38466f4f3483
immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 > 100000, JinjaThreads: 65000 > 300000)  minimal measurable impact on inference kernel performance;
wenzelm
parents:
52682
diff
changeset

342 
if name = "" then error ("Bad theory name: " ^ quote name) 
24369  343 
else 
16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

344 
let 
24141
73baca986087
improved check_thy: produce a checked theory_ref (threadsafe version);
wenzelm
parents:
23944
diff
changeset

345 
val parents = maximal_thys (distinct eq_thy imports); 
29093
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

346 
val ancestors = 
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

347 
Library.foldl merge_ancestors ([], map ancestors_of parents) 
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

348 
> fold extend_ancestors parents; 
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

349 

60947  350 
val Theory (Theory_Id ({ids, ...}, _), _, data) = 
16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

351 
(case parents of 
48638  352 
[] => error "Missing theory imports" 
16533  353 
 [thy] => extend_thy thy 
354 
 thy :: thys => Library.foldl (merge_thys pp) (thy, thys)); 

29093
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

355 

60947  356 
val history = make_history name 0; 
16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

357 
val ancestry = make_ancestry parents ancestors; 
60947  358 
in create_thy ids history ancestry data end; 
16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

359 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

360 
end; 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

361 

16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

362 

f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

363 
(* theory data *) 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

364 

33033  365 
structure Theory_Data = 
16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

366 
struct 
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

367 

f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

368 
val declare = declare_theory_data; 
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

369 

f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

370 
fun get k dest thy = 
34253
5930c6391126
removed further remains of mutable theory data (cf. 25bd3ed2ac9f);
wenzelm
parents:
34245
diff
changeset

371 
(case Datatab.lookup (data_of thy) k of 
22847
22da6c4bc422
simplified DataFun interfaces: removed name/print, use adhoc value for uninitialized data, init only required for impure data;
wenzelm
parents:
22827
diff
changeset

372 
SOME x => x 
34253
5930c6391126
removed further remains of mutable theory data (cf. 25bd3ed2ac9f);
wenzelm
parents:
34245
diff
changeset

373 
 NONE => invoke_empty k) > dest; 
16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

374 

52696
38466f4f3483
immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 > 100000, JinjaThreads: 65000 > 300000)  minimal measurable impact on inference kernel performance;
wenzelm
parents:
52682
diff
changeset

375 
fun put k mk x = update_thy (Datatab.update (k, mk x)); 
16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

376 

f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

377 
end; 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

378 

7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

379 

7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

380 

16533  381 
(*** proof context ***) 
382 

33031
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32784
diff
changeset

383 
(* datatype Proof.context *) 
17060
cca2f3938443
type proof: theory_ref instead of theory (make proof contexts independent entities);
wenzelm
parents:
16894
diff
changeset

384 

33031
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32784
diff
changeset

385 
structure Proof = 
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32784
diff
changeset

386 
struct 
52788  387 
datatype context = Context of Any.T Datatab.table * theory; 
33031
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32784
diff
changeset

388 
end; 
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32784
diff
changeset

389 

16533  390 

391 
(* proof data kinds *) 

392 

393 
local 

394 

51368
2ea5c7c2d825
tuned signature  prefer terminology of Scala and Axiom;
wenzelm
parents:
50431
diff
changeset

395 
val kinds = Synchronized.var "Proof_Data" (Datatab.empty: (theory > Any.T) Datatab.table); 
16533  396 

59163  397 
fun init_data thy = 
398 
Synchronized.value kinds > Datatab.map (fn _ => fn init => init thy); 

16533  399 

59163  400 
fun init_new_data thy = 
401 
Synchronized.value kinds > Datatab.fold (fn (k, init) => fn data => 

402 
if Datatab.defined data k then data 

403 
else Datatab.update (k, init thy) data); 

22847
22da6c4bc422
simplified DataFun interfaces: removed name/print, use adhoc value for uninitialized data, init only required for impure data;
wenzelm
parents:
22827
diff
changeset

404 

59163  405 
fun init_fallback k thy = 
406 
(case Datatab.lookup (Synchronized.value kinds) k of 

407 
SOME init => init thy 

408 
 NONE => raise Fail "Invalid proof data identifier"); 

16533  409 

410 
in 

411 

52788  412 
fun raw_transfer thy' (Proof.Context (data, thy)) = 
24141
73baca986087
improved check_thy: produce a checked theory_ref (threadsafe version);
wenzelm
parents:
23944
diff
changeset

413 
let 
52682  414 
val _ = subthy (thy, thy') orelse error "Cannot transfer proof context: not a super theory"; 
59163  415 
val data' = init_new_data thy' data; 
52788  416 
in Proof.Context (data', thy') end; 
22847
22da6c4bc422
simplified DataFun interfaces: removed name/print, use adhoc value for uninitialized data, init only required for impure data;
wenzelm
parents:
22827
diff
changeset

417 

42360  418 
structure Proof_Context = 
33031
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32784
diff
changeset

419 
struct 
59163  420 
fun theory_of (Proof.Context (_, thy)) = thy; 
52788  421 
fun init_global thy = Proof.Context (init_data thy, thy); 
51686  422 
fun get_global thy name = init_global (get_theory thy name); 
33031
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32784
diff
changeset

423 
end; 
16533  424 

33033  425 
structure Proof_Data = 
16533  426 
struct 
427 

22847
22da6c4bc422
simplified DataFun interfaces: removed name/print, use adhoc value for uninitialized data, init only required for impure data;
wenzelm
parents:
22827
diff
changeset

428 
fun declare init = 
16533  429 
let 
430 
val k = serial (); 

43684  431 
val _ = Synchronized.change kinds (Datatab.update (k, init)); 
16533  432 
in k end; 
433 

59163  434 
fun get k dest (Proof.Context (data, thy)) = 
435 
(case Datatab.lookup data k of 

22847
22da6c4bc422
simplified DataFun interfaces: removed name/print, use adhoc value for uninitialized data, init only required for impure data;
wenzelm
parents:
22827
diff
changeset

436 
SOME x => x 
59163  437 
 NONE => init_fallback k thy) > dest; 
16533  438 

59163  439 
fun put k mk x (Proof.Context (data, thy)) = 
440 
Proof.Context (Datatab.update (k, mk x) data, thy); 

16533  441 

442 
end; 

443 

444 
end; 

445 

446 

18632  447 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

448 
(*** theory certificate ***) 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

449 

b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

450 
datatype certificate = Certificate of theory  Certificate_Id of theory_id; 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

451 

b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

452 
fun certificate_theory (Certificate thy) = thy 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

453 
 certificate_theory (Certificate_Id thy_id) = 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

454 
raise Fail ("No content for theory certificate " ^ quote (display_name thy_id)); 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

455 

b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

456 
fun certificate_theory_id (Certificate thy) = theory_id thy 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

457 
 certificate_theory_id (Certificate_Id thy_id) = thy_id; 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

458 

b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

459 
fun eq_certificate (Certificate thy1, Certificate thy2) = eq_thy (thy1, thy2) 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

460 
 eq_certificate (Certificate_Id thy_id1, Certificate_Id thy_id2) = eq_thy_id (thy_id1, thy_id2) 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

461 
 eq_certificate _ = false; 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

462 

b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

463 
fun join_certificate (cert1, cert2) = 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

464 
let val (thy_id1, thy_id2) = apply2 certificate_theory_id (cert1, cert2) in 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

465 
if eq_thy_id (thy_id1, thy_id2) then (case cert1 of Certificate _ => cert1  _ => cert2) 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

466 
else if proper_subthy_id (thy_id2, thy_id1) then cert1 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

467 
else if proper_subthy_id (thy_id1, thy_id2) then cert2 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

468 
else 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

469 
raise Fail ("Cannot join unrelated theory certificates " ^ 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

470 
quote (display_name thy_id1) ^ " and " ^ quote (display_name thy_id2)) 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

471 
end; 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

472 

b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

473 

b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

474 

16533  475 
(*** generic context ***) 
476 

33031
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32784
diff
changeset

477 
datatype generic = Theory of theory  Proof of Proof.context; 
18632  478 

479 
fun cases f _ (Theory thy) = f thy 

480 
 cases _ g (Proof prf) = g prf; 

16533  481 

19678  482 
fun mapping f g = cases (Theory o f) (Proof o g); 
21660  483 
fun mapping_result f g = cases (apsnd Theory o f) (apsnd Proof o g); 
19678  484 

23595
7ca68a2c8575
the_theory/proof: error instead of exception Fail;
wenzelm
parents:
23355
diff
changeset

485 
val the_theory = cases I (fn _ => error "Illtyped context: theory expected"); 
7ca68a2c8575
the_theory/proof: error instead of exception Fail;
wenzelm
parents:
23355
diff
changeset

486 
val the_proof = cases (fn _ => error "Illtyped context: proof expected") I; 
16533  487 

18731  488 
fun map_theory f = Theory o f o the_theory; 
489 
fun map_proof f = Proof o f o the_proof; 

490 

26486  491 
fun map_theory_result f = apsnd Theory o f o the_theory; 
492 
fun map_proof_result f = apsnd Proof o f o the_proof; 

493 

18731  494 
fun theory_map f = the_theory o f o Theory; 
495 
fun proof_map f = the_proof o f o Proof; 

18665  496 

42360  497 
val theory_of = cases I Proof_Context.theory_of; 
498 
val proof_of = cases Proof_Context.init_global I; 

16533  499 

22085
c138cfd500f7
ML context: full generic context, tuned signature;
wenzelm
parents:
21962
diff
changeset

500 

42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42360
diff
changeset

501 
(* pretty printing context *) 
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42360
diff
changeset

502 

0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42360
diff
changeset

503 
exception PRETTY of generic; 
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42360
diff
changeset

504 

47005
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
43684
diff
changeset

505 
val pretty_generic = Pretty o PRETTY; 
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
43684
diff
changeset

506 
val pretty = pretty_generic o Proof; 
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
43684
diff
changeset

507 
val pretty_global = pretty_generic o Theory; 
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42360
diff
changeset

508 

0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42360
diff
changeset

509 
fun pretty_context init (Pretty (PRETTY context)) = cases init I context; 
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42360
diff
changeset

510 

0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42360
diff
changeset

511 

22085
c138cfd500f7
ML context: full generic context, tuned signature;
wenzelm
parents:
21962
diff
changeset

512 

26413
003dd6155870
added thread data (formerly global ref in ML/ml_context.ML);
wenzelm
parents:
24559
diff
changeset

513 
(** thread data **) 
003dd6155870
added thread data (formerly global ref in ML/ml_context.ML);
wenzelm
parents:
24559
diff
changeset

514 

003dd6155870
added thread data (formerly global ref in ML/ml_context.ML);
wenzelm
parents:
24559
diff
changeset

515 
local val tag = Universal.tag () : generic option Universal.tag in 
003dd6155870
added thread data (formerly global ref in ML/ml_context.ML);
wenzelm
parents:
24559
diff
changeset

516 

003dd6155870
added thread data (formerly global ref in ML/ml_context.ML);
wenzelm
parents:
24559
diff
changeset

517 
fun thread_data () = 
28122  518 
(case Thread.getLocal tag of 
26413
003dd6155870
added thread data (formerly global ref in ML/ml_context.ML);
wenzelm
parents:
24559
diff
changeset

519 
SOME (SOME context) => SOME context 
003dd6155870
added thread data (formerly global ref in ML/ml_context.ML);
wenzelm
parents:
24559
diff
changeset

520 
 _ => NONE); 
003dd6155870
added thread data (formerly global ref in ML/ml_context.ML);
wenzelm
parents:
24559
diff
changeset

521 

003dd6155870
added thread data (formerly global ref in ML/ml_context.ML);
wenzelm
parents:
24559
diff
changeset

522 
fun the_thread_data () = 
003dd6155870
added thread data (formerly global ref in ML/ml_context.ML);
wenzelm
parents:
24559
diff
changeset

523 
(case thread_data () of 
003dd6155870
added thread data (formerly global ref in ML/ml_context.ML);
wenzelm
parents:
24559
diff
changeset

524 
SOME context => context 
003dd6155870
added thread data (formerly global ref in ML/ml_context.ML);
wenzelm
parents:
24559
diff
changeset

525 
 _ => error "Unknown context"); 
003dd6155870
added thread data (formerly global ref in ML/ml_context.ML);
wenzelm
parents:
24559
diff
changeset

526 

28122  527 
fun set_thread_data context = Thread.setLocal (tag, context); 
26413
003dd6155870
added thread data (formerly global ref in ML/ml_context.ML);
wenzelm
parents:
24559
diff
changeset

528 
fun setmp_thread_data context = Library.setmp_thread_data tag (thread_data ()) context; 
003dd6155870
added thread data (formerly global ref in ML/ml_context.ML);
wenzelm
parents:
24559
diff
changeset

529 

26428  530 
end; 
531 

532 
fun >>> f = 

533 
let 

26463  534 
val (res, context') = f (the_thread_data ()); 
535 
val _ = set_thread_data (SOME context'); 

26428  536 
in res end; 
537 

26421  538 
nonfix >>; 
26463  539 
fun >> f = >>> (fn context => ((), f context)); 
26413
003dd6155870
added thread data (formerly global ref in ML/ml_context.ML);
wenzelm
parents:
24559
diff
changeset

540 

26428  541 
val _ = set_thread_data (SOME (Theory pre_pure_thy)); 
26413
003dd6155870
added thread data (formerly global ref in ML/ml_context.ML);
wenzelm
parents:
24559
diff
changeset

542 

6185  543 
end; 
544 

33031
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32784
diff
changeset

545 
structure Basic_Context: BASIC_CONTEXT = Context; 
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32784
diff
changeset

546 
open Basic_Context; 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

547 

7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

548 

7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

549 

16533  550 
(*** typesafe interfaces for data declarations ***) 
551 

552 
(** theory data **) 

16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

553 

34259
2ba492b8b6e8
discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations  hard to get rid of);
wenzelm
parents:
34253
diff
changeset

554 
signature THEORY_DATA_PP_ARGS = 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

555 
sig 
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

556 
type T 
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

557 
val empty: T 
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

558 
val extend: T > T 
42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42360
diff
changeset

559 
val merge: Context.pretty > T * T > T 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

560 
end; 
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

561 

34259
2ba492b8b6e8
discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations  hard to get rid of);
wenzelm
parents:
34253
diff
changeset

562 
signature THEORY_DATA_ARGS = 
2ba492b8b6e8
discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations  hard to get rid of);
wenzelm
parents:
34253
diff
changeset

563 
sig 
2ba492b8b6e8
discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations  hard to get rid of);
wenzelm
parents:
34253
diff
changeset

564 
type T 
2ba492b8b6e8
discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations  hard to get rid of);
wenzelm
parents:
34253
diff
changeset

565 
val empty: T 
2ba492b8b6e8
discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations  hard to get rid of);
wenzelm
parents:
34253
diff
changeset

566 
val extend: T > T 
2ba492b8b6e8
discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations  hard to get rid of);
wenzelm
parents:
34253
diff
changeset

567 
val merge: T * T > T 
2ba492b8b6e8
discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations  hard to get rid of);
wenzelm
parents:
34253
diff
changeset

568 
end; 
2ba492b8b6e8
discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations  hard to get rid of);
wenzelm
parents:
34253
diff
changeset

569 

34253
5930c6391126
removed further remains of mutable theory data (cf. 25bd3ed2ac9f);
wenzelm
parents:
34245
diff
changeset

570 
signature THEORY_DATA = 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

571 
sig 
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

572 
type T 
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

573 
val get: theory > T 
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

574 
val put: T > theory > theory 
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

575 
val map: (T > T) > theory > theory 
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

576 
end; 
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

577 

34259
2ba492b8b6e8
discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations  hard to get rid of);
wenzelm
parents:
34253
diff
changeset

578 
functor Theory_Data_PP(Data: THEORY_DATA_PP_ARGS): THEORY_DATA = 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

579 
struct 
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

580 

7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

581 
type T = Data.T; 
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

582 
exception Data of T; 
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

583 

42818
128cc195ced3
timing of Theory_Data operations, with implicit thread positions when functor is applied;
wenzelm
parents:
42383
diff
changeset

584 
val kind = 
128cc195ced3
timing of Theory_Data operations, with implicit thread positions when functor is applied;
wenzelm
parents:
42383
diff
changeset

585 
Context.Theory_Data.declare 
128cc195ced3
timing of Theory_Data operations, with implicit thread positions when functor is applied;
wenzelm
parents:
42383
diff
changeset

586 
(Position.thread_data ()) 
128cc195ced3
timing of Theory_Data operations, with implicit thread positions when functor is applied;
wenzelm
parents:
42383
diff
changeset

587 
(Data Data.empty) 
128cc195ced3
timing of Theory_Data operations, with implicit thread positions when functor is applied;
wenzelm
parents:
42383
diff
changeset

588 
(fn Data x => Data (Data.extend x)) 
128cc195ced3
timing of Theory_Data operations, with implicit thread positions when functor is applied;
wenzelm
parents:
42383
diff
changeset

589 
(fn pp => fn (Data x1, Data x2) => Data (Data.merge pp (x1, x2))); 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

590 

33033  591 
val get = Context.Theory_Data.get kind (fn Data x => x); 
592 
val put = Context.Theory_Data.put kind Data; 

16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

593 
fun map f thy = put (f (get thy)) thy; 
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

594 

7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

595 
end; 
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

596 

33517
d064fa48f305
modernized/simplified functor Theory_Data, Proof_Data, Generic_Data: eliminated Pretty.pp, discontinued mutable data;
wenzelm
parents:
33033
diff
changeset

597 
functor Theory_Data(Data: THEORY_DATA_ARGS): THEORY_DATA = 
34259
2ba492b8b6e8
discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations  hard to get rid of);
wenzelm
parents:
34253
diff
changeset

598 
Theory_Data_PP 
2ba492b8b6e8
discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations  hard to get rid of);
wenzelm
parents:
34253
diff
changeset

599 
( 
2ba492b8b6e8
discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations  hard to get rid of);
wenzelm
parents:
34253
diff
changeset

600 
type T = Data.T; 
2ba492b8b6e8
discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations  hard to get rid of);
wenzelm
parents:
34253
diff
changeset

601 
val empty = Data.empty; 
2ba492b8b6e8
discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations  hard to get rid of);
wenzelm
parents:
34253
diff
changeset

602 
val extend = Data.extend; 
2ba492b8b6e8
discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations  hard to get rid of);
wenzelm
parents:
34253
diff
changeset

603 
fun merge _ = Data.merge; 
2ba492b8b6e8
discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations  hard to get rid of);
wenzelm
parents:
34253
diff
changeset

604 
); 
33517
d064fa48f305
modernized/simplified functor Theory_Data, Proof_Data, Generic_Data: eliminated Pretty.pp, discontinued mutable data;
wenzelm
parents:
33033
diff
changeset

605 

16533  606 

607 

608 
(** proof data **) 

609 

610 
signature PROOF_DATA_ARGS = 

611 
sig 

612 
type T 

613 
val init: theory > T 

614 
end; 

615 

616 
signature PROOF_DATA = 

617 
sig 

618 
type T 

33031
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32784
diff
changeset

619 
val get: Proof.context > T 
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32784
diff
changeset

620 
val put: T > Proof.context > Proof.context 
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32784
diff
changeset

621 
val map: (T > T) > Proof.context > Proof.context 
16533  622 
end; 
623 

33517
d064fa48f305
modernized/simplified functor Theory_Data, Proof_Data, Generic_Data: eliminated Pretty.pp, discontinued mutable data;
wenzelm
parents:
33033
diff
changeset

624 
functor Proof_Data(Data: PROOF_DATA_ARGS): PROOF_DATA = 
16533  625 
struct 
626 

627 
type T = Data.T; 

628 
exception Data of T; 

629 

33033  630 
val kind = Context.Proof_Data.declare (Data o Data.init); 
16533  631 

33033  632 
val get = Context.Proof_Data.get kind (fn Data x => x); 
633 
val put = Context.Proof_Data.put kind Data; 

16533  634 
fun map f prf = put (f (get prf)) prf; 
635 

636 
end; 

637 

18632  638 

639 

640 
(** generic data **) 

641 

642 
signature GENERIC_DATA_ARGS = 

643 
sig 

644 
type T 

645 
val empty: T 

646 
val extend: T > T 

33517
d064fa48f305
modernized/simplified functor Theory_Data, Proof_Data, Generic_Data: eliminated Pretty.pp, discontinued mutable data;
wenzelm
parents:
33033
diff
changeset

647 
val merge: T * T > T 
18632  648 
end; 
649 

650 
signature GENERIC_DATA = 

651 
sig 

652 
type T 

653 
val get: Context.generic > T 

654 
val put: T > Context.generic > Context.generic 

655 
val map: (T > T) > Context.generic > Context.generic 

656 
end; 

657 

33517
d064fa48f305
modernized/simplified functor Theory_Data, Proof_Data, Generic_Data: eliminated Pretty.pp, discontinued mutable data;
wenzelm
parents:
33033
diff
changeset

658 
functor Generic_Data(Data: GENERIC_DATA_ARGS): GENERIC_DATA = 
18632  659 
struct 
660 

33517
d064fa48f305
modernized/simplified functor Theory_Data, Proof_Data, Generic_Data: eliminated Pretty.pp, discontinued mutable data;
wenzelm
parents:
33033
diff
changeset

661 
structure Thy_Data = Theory_Data(Data); 
d064fa48f305
modernized/simplified functor Theory_Data, Proof_Data, Generic_Data: eliminated Pretty.pp, discontinued mutable data;
wenzelm
parents:
33033
diff
changeset

662 
structure Prf_Data = Proof_Data(type T = Data.T val init = Thy_Data.get); 
18632  663 

664 
type T = Data.T; 

665 

33033  666 
fun get (Context.Theory thy) = Thy_Data.get thy 
667 
 get (Context.Proof prf) = Prf_Data.get prf; 

18632  668 

33033  669 
fun put x (Context.Theory thy) = Context.Theory (Thy_Data.put x thy) 
670 
 put x (Context.Proof prf) = Context.Proof (Prf_Data.put x prf); 

18632  671 

672 
fun map f ctxt = put (f (get ctxt)) ctxt; 

673 

674 
end; 

675 

16533  676 
(*hide private interface*) 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

677 
structure Context: CONTEXT = Context; 