author  wenzelm 
Mon, 20 Jul 2020 23:45:29 +0200  
changeset 72290  efb7fd4a6d1f 
parent 70772  57df8a85317a 
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 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

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

35 
val ancestors_of: theory > theory list 
70772  36 
val theory_id_ord: theory_id ord 
65459
da59e8e0a663
clarified theory_long_name (for qualified access to Thy_Info) vs. short theory_name (which is unique within any given theory context);
wenzelm
parents:
62889
diff
changeset

37 
val theory_id_long_name: theory_id > string 
60948  38 
val theory_id_name: theory_id > string 
65459
da59e8e0a663
clarified theory_long_name (for qualified access to Thy_Info) vs. short theory_name (which is unique within any given theory context);
wenzelm
parents:
62889
diff
changeset

39 
val theory_long_name: theory > string 
29069
c7ba485581ae
unified ids for ancestors and checkpoints, removed obsolete history of checkpoints;
wenzelm
parents:
29001
diff
changeset

40 
val theory_name: theory > string 
68482  41 
val theory_name': {long: bool} > 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

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

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

44 
val pretty_abbrev_thy: theory > Pretty.T 
68482  45 
val get_theory: {long: bool} > theory > string > theory 
60947  46 
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

47 
val eq_thy: theory * theory > bool 
60947  48 
val proper_subthy_id: theory_id * theory_id > bool 
49 
val proper_subthy: theory * theory > bool 

50 
val subthy_id: theory_id * theory_id > bool 

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

51 
val subthy: theory * theory > bool 
67623  52 
val trace_theories: bool Unsynchronized.ref 
67640  53 
val theories_trace: unit > {active_positions: Position.T list, active: int, total: int} 
70546
34b271c4f400
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents:
70545
diff
changeset

54 
val join_thys: theory * theory > theory 
67623  55 
val begin_thy: string > theory list > theory 
16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

56 
val finish_thy: theory > theory 
67621  57 
val theory_data_size: theory > (Position.T * int) list 
16533  58 
(*proof context*) 
33031
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32784
diff
changeset

59 
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

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

61 
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

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

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

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

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

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

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

69 
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

70 
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

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

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

75 
val map_proof: (Proof.context > Proof.context) > generic > generic 
26486  76 
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

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

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

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

81 
val proof_of: generic > Proof.context (*total*) 
26413
003dd6155870
added thread data (formerly global ref in ML/ml_context.ML);
wenzelm
parents:
24559
diff
changeset

82 
(*thread data*) 
62889  83 
val get_generic_context: unit > generic option 
84 
val put_generic_context: generic option > unit 

85 
val setmp_generic_context: generic option > ('a > 'b) > 'a > 'b 

62876  86 
val the_generic_context: unit > generic 
87 
val the_global_context: unit > theory 

88 
val the_local_context: unit > Proof.context 

26463  89 
val >> : (generic > generic) > unit 
90 
val >>> : (generic > 'a * generic) > 'a 

6185  91 
end; 
92 

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

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

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

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

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

98 
val declare: Position.T > Any.T > (Any.T > Any.T) > 
61262
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

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

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

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

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

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

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

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

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

110 

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

111 
structure Context: PRIVATE_CONTEXT = 
6185  112 
struct 
113 

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

114 
(*** theory context ***) 
6185  115 

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

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

117 
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

118 

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

119 

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

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

121 

70545
03430649a7d2
clarified history stage: allow independent updates that are merged later;
wenzelm
parents:
68482
diff
changeset

122 
type stage = int * int Synchronized.var; 
03430649a7d2
clarified history stage: allow independent updates that are merged later;
wenzelm
parents:
68482
diff
changeset

123 
fun init_stage () : stage = (0, Synchronized.var "Context.stage" 1); 
03430649a7d2
clarified history stage: allow independent updates that are merged later;
wenzelm
parents:
68482
diff
changeset

124 
fun next_stage ((_, state): stage) = (Synchronized.change_result state (fn n => (n, n + 1)), state); 
03430649a7d2
clarified history stage: allow independent updates that are merged later;
wenzelm
parents:
68482
diff
changeset

125 

70638
70019ab5e57f
abstract type theory_id  ensure nonequality type independently of implementation;
wenzelm
parents:
70546
diff
changeset

126 
abstype theory_id = 
60947  127 
Theory_Id of 
16533  128 
(*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

129 
{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

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

132 
{name: string, (*official theory name*) 
70638
70019ab5e57f
abstract type theory_id  ensure nonequality type independently of implementation;
wenzelm
parents:
70546
diff
changeset

133 
stage: stage option} (*index and counter for anonymous updates*) 
70019ab5e57f
abstract type theory_id  ensure nonequality type independently of implementation;
wenzelm
parents:
70546
diff
changeset

134 
with 
70019ab5e57f
abstract type theory_id  ensure nonequality type independently of implementation;
wenzelm
parents:
70546
diff
changeset

135 

70019ab5e57f
abstract type theory_id  ensure nonequality type independently of implementation;
wenzelm
parents:
70546
diff
changeset

136 
fun rep_theory_id (Theory_Id args) = args; 
70019ab5e57f
abstract type theory_id  ensure nonequality type independently of implementation;
wenzelm
parents:
70546
diff
changeset

137 
val make_theory_id = Theory_Id; 
70019ab5e57f
abstract type theory_id  ensure nonequality type independently of implementation;
wenzelm
parents:
70546
diff
changeset

138 

70019ab5e57f
abstract type theory_id  ensure nonequality type independently of implementation;
wenzelm
parents:
70546
diff
changeset

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

140 

60947  141 
datatype theory = 
142 
Theory of 

67623  143 
(*identity*) 
144 
{theory_id: theory_id, 

67640  145 
token: Position.T Unsynchronized.ref} * 
60947  146 
(*ancestry*) 
147 
{parents: theory list, (*immediate predecessors*) 

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

149 
(*data*) 

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

151 

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

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

153 

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

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

155 

67623  156 
val theory_identity = #1 o rep_theory; 
157 
val theory_id = #theory_id o theory_identity; 

60947  158 

159 
val identity_of_id = #1 o rep_theory_id; 

160 
val identity_of = identity_of_id o theory_id; 

161 
val history_of_id = #2 o rep_theory_id; 

162 
val history_of = history_of_id o theory_id; 

163 
val ancestry_of = #2 o rep_theory; 

164 
val data_of = #3 o rep_theory; 

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

165 

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

166 
fun make_identity id ids = {id = id, ids = ids}; 
70545
03430649a7d2
clarified history stage: allow independent updates that are merged later;
wenzelm
parents:
68482
diff
changeset

167 
fun make_history name = {name = name, stage = SOME (init_stage ())}; 
16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

168 
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

169 

70645
f0a445c5a82c
maintain sort constraints from type instantiations, with proforma derivation to collect oracles/thms;
wenzelm
parents:
70638
diff
changeset

170 
val theory_id_ord = int_ord o apply2 (#id o identity_of_id); 
65459
da59e8e0a663
clarified theory_long_name (for qualified access to Thy_Info) vs. short theory_name (which is unique within any given theory context);
wenzelm
parents:
62889
diff
changeset

171 
val theory_id_long_name = #name o history_of_id; 
da59e8e0a663
clarified theory_long_name (for qualified access to Thy_Info) vs. short theory_name (which is unique within any given theory context);
wenzelm
parents:
62889
diff
changeset

172 
val theory_id_name = Long_Name.base_name o theory_id_long_name; 
da59e8e0a663
clarified theory_long_name (for qualified access to Thy_Info) vs. short theory_name (which is unique within any given theory context);
wenzelm
parents:
62889
diff
changeset

173 
val theory_long_name = #name o history_of; 
da59e8e0a663
clarified theory_long_name (for qualified access to Thy_Info) vs. short theory_name (which is unique within any given theory context);
wenzelm
parents:
62889
diff
changeset

174 
val theory_name = Long_Name.base_name o theory_long_name; 
68482  175 
fun theory_name' {long} = if long then theory_long_name else theory_name; 
65459
da59e8e0a663
clarified theory_long_name (for qualified access to Thy_Info) vs. short theory_name (which is unique within any given theory context);
wenzelm
parents:
62889
diff
changeset

176 

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

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

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

179 

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

180 

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

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

182 

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

183 
val PureN = "Pure"; 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

184 

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

185 
fun display_name thy_id = 
70545
03430649a7d2
clarified history stage: allow independent updates that are merged later;
wenzelm
parents:
68482
diff
changeset

186 
(case history_of_id thy_id of 
03430649a7d2
clarified history stage: allow independent updates that are merged later;
wenzelm
parents:
68482
diff
changeset

187 
{name, stage = NONE} => name 
03430649a7d2
clarified history stage: allow independent updates that are merged later;
wenzelm
parents:
68482
diff
changeset

188 
 {name, stage = SOME (i, _)} => name ^ ":" ^ string_of_int i); 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

189 

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

190 
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

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

192 
val name = display_name (theory_id thy); 
68192  193 
val ancestor_names = map theory_long_name (ancestors_of thy); 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

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

195 

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

196 
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

197 

62819
d3ff367a16a0
careful export of typedependent functions, without losing their special status;
wenzelm
parents:
62663
diff
changeset

198 
val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty_thy); 
62663  199 

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

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

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

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

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

204 
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

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

206 

68482  207 
fun get_theory long thy name = 
208 
if theory_name' long thy <> name then 

209 
(case find_first (fn thy' => theory_name' long thy' = name) (ancestors_of thy) of 

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

210 
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

211 
 NONE => error ("Unknown ancestor theory " ^ quote name)) 
70545
03430649a7d2
clarified history stage: allow independent updates that are merged later;
wenzelm
parents:
68482
diff
changeset

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

213 
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

214 

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

215 

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

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

217 

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

218 
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

219 

67623  220 
val merge_ids = 
70638
70019ab5e57f
abstract type theory_id  ensure nonequality type independently of implementation;
wenzelm
parents:
70546
diff
changeset

221 
apply2 (theory_id #> rep_theory_id #> #1) #> 
70019ab5e57f
abstract type theory_id  ensure nonequality type independently of implementation;
wenzelm
parents:
70546
diff
changeset

222 
(fn ({id = id1, ids = ids1, ...}, {id = id2, ids = ids2, ...}) => 
67623  223 
Inttab.merge (K true) (ids1, ids2) 
224 
> insert_id id1 

225 
> insert_id id2); 

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

226 

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

227 

16533  228 
(* equality and inclusion *) 
229 

60947  230 
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:
55549
diff
changeset

231 
val eq_thy = op = o apply2 (#id o identity_of); 
16533  232 

70638
70019ab5e57f
abstract type theory_id  ensure nonequality type independently of implementation;
wenzelm
parents:
70546
diff
changeset

233 
val proper_subthy_id = 
70019ab5e57f
abstract type theory_id  ensure nonequality type independently of implementation;
wenzelm
parents:
70546
diff
changeset

234 
apply2 (rep_theory_id #> #1) #> (fn ({id, ...}, {ids, ...}) => Inttab.defined ids id); 
60947  235 
val proper_subthy = proper_subthy_id o apply2 theory_id; 
16533  236 

60947  237 
fun subthy_id p = eq_thy_id p orelse proper_subthy_id p; 
238 
val subthy = subthy_id o apply2 theory_id; 

16533  239 

240 

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

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

242 

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

243 
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

244 
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

245 
(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

246 
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

247 

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

248 
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

249 
if member eq_thy_consistent thys thy then 
33033  250 
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

251 
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

252 

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

253 
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

254 

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

255 

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

256 

61262
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

257 
(** theory data **) 
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

258 

7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

259 
(* data kinds and access methods *) 
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

260 

7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

261 
val timing = Unsynchronized.ref false; 
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

262 

7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

263 
local 
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

264 

7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

265 
type kind = 
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

266 
{pos: Position.T, 
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

267 
empty: Any.T, 
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

268 
extend: Any.T > Any.T, 
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

269 
merge: theory * theory > Any.T * Any.T > Any.T}; 
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

270 

7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

271 
val kinds = Synchronized.var "Theory_Data" (Datatab.empty: kind Datatab.table); 
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

272 

7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

273 
fun invoke name f k x = 
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

274 
(case Datatab.lookup (Synchronized.value kinds) k of 
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

275 
SOME kind => 
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

276 
if ! timing andalso name <> "" then 
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

277 
Timing.cond_timeit true ("Theory_Data." ^ name ^ Position.here (#pos kind)) 
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

278 
(fn () => f kind x) 
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

279 
else f kind x 
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

280 
 NONE => raise Fail "Invalid theory data identifier"); 
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

281 

7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

282 
in 
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

283 

67621  284 
fun invoke_pos k = invoke "" (K o #pos) k (); 
61262
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

285 
fun invoke_empty k = invoke "" (K o #empty) k (); 
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

286 
val invoke_extend = invoke "extend" #extend; 
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

287 
fun invoke_merge thys = invoke "merge" (fn kind => #merge kind thys); 
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

288 

7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

289 
fun declare_theory_data pos empty extend merge = 
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

290 
let 
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

291 
val k = serial (); 
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

292 
val kind = {pos = pos, empty = empty, extend = extend, merge = merge}; 
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

293 
val _ = Synchronized.change kinds (Datatab.update (k, kind)); 
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

294 
in k end; 
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

295 

7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

296 
val extend_data = Datatab.map invoke_extend; 
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

297 
fun merge_data thys = Datatab.join (invoke_merge thys) o apply2 extend_data; 
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

298 

7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

299 
end; 
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

300 

7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

301 

7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

302 

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

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

304 

67623  305 
(* create theory *) 
306 

307 
val trace_theories = Unsynchronized.ref false; 

308 

309 
local 

310 

311 
val theories = 

67640  312 
Synchronized.var "theory_tokens" 
313 
([]: Position.T Unsynchronized.ref option Unsynchronized.ref list); 

67623  314 

67640  315 
val dummy_token = Unsynchronized.ref Position.none; 
67623  316 

317 
fun make_token () = 

318 
if ! trace_theories then 

319 
let 

67640  320 
val token = Unsynchronized.ref (Position.thread_data ()); 
67623  321 
val _ = Synchronized.change theories (cons (Weak.weak (SOME token))); 
322 
in token end 

323 
else dummy_token; 

324 

325 
in 

326 

327 
fun theories_trace () = 

328 
let 

329 
val trace = Synchronized.value theories; 

330 
val _ = ML_Heap.full_gc (); 

67640  331 
val active_positions = 
332 
fold (fn Unsynchronized.ref (SOME pos) => cons (! pos)  _ => I) trace []; 

333 
in 

334 
{active_positions = active_positions, 

335 
active = length active_positions, 

336 
total = length trace} 

337 
end; 

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

338 

60947  339 
fun create_thy ids history ancestry data = 
67623  340 
let 
70638
70019ab5e57f
abstract type theory_id  ensure nonequality type independently of implementation;
wenzelm
parents:
70546
diff
changeset

341 
val theory_id = make_theory_id (make_identity (serial ()) ids, history); 
67623  342 
val token = make_token (); 
343 
in Theory ({theory_id = theory_id, token = token}, ancestry, data) end; 

344 

345 
end; 

346 

347 

348 
(* primitives *) 

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

349 

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

350 
val pre_pure_thy = 
70545
03430649a7d2
clarified history stage: allow independent updates that are merged later;
wenzelm
parents:
68482
diff
changeset

351 
create_thy Inttab.empty (make_history PureN) (make_ancestry [] []) Datatab.empty; 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

352 

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

353 
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

354 

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

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

356 
let 
70638
70019ab5e57f
abstract type theory_id  ensure nonequality type independently of implementation;
wenzelm
parents:
70546
diff
changeset

357 
val ({id, ids}, {name, stage}) = rep_theory_id (theory_id thy); 
67623  358 
val Theory (_, ancestry, data) = thy; 
60947  359 
val (ancestry', data') = 
70545
03430649a7d2
clarified history stage: allow independent updates that are merged later;
wenzelm
parents:
68482
diff
changeset

360 
if is_none stage then 
60947  361 
(make_ancestry [thy] (extend_ancestors thy (ancestors_of thy)), extend_data data) 
362 
else (ancestry, data); 

70545
03430649a7d2
clarified history stage: allow independent updates that are merged later;
wenzelm
parents:
68482
diff
changeset

363 
val history' = {name = name, stage = if finish then NONE else Option.map next_stage stage}; 
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

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

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

367 

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

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

369 

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

370 
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

371 
val extend_thy = update_thy I; 
68193
14dd78f036ba
more thorough checks for theory name consistency (for extend, not just merge);
wenzelm
parents:
68192
diff
changeset

372 
val finish_thy = change_thy true I #> tap extend_thy; 
16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

373 

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

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

375 

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

376 

70546
34b271c4f400
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents:
70545
diff
changeset

377 
(* join: anonymous theory nodes *) 
34b271c4f400
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents:
70545
diff
changeset

378 

34b271c4f400
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents:
70545
diff
changeset

379 
local 
34b271c4f400
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents:
70545
diff
changeset

380 

34b271c4f400
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents:
70545
diff
changeset

381 
fun bad_join (thy1, thy2) = raise THEORY ("Cannot join theories", [thy1, thy2]); 
34b271c4f400
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents:
70545
diff
changeset

382 

34b271c4f400
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents:
70545
diff
changeset

383 
fun join_history thys = 
34b271c4f400
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents:
70545
diff
changeset

384 
apply2 history_of thys > 
34b271c4f400
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents:
70545
diff
changeset

385 
(fn ({name, stage}, {name = name', stage = stage'}) => 
34b271c4f400
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents:
70545
diff
changeset

386 
if name = name' andalso is_some stage andalso is_some stage' then 
34b271c4f400
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents:
70545
diff
changeset

387 
{name = name, stage = Option.map next_stage stage} 
34b271c4f400
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents:
70545
diff
changeset

388 
else bad_join thys); 
34b271c4f400
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents:
70545
diff
changeset

389 

34b271c4f400
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents:
70545
diff
changeset

390 
fun join_ancestry thys = 
34b271c4f400
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents:
70545
diff
changeset

391 
apply2 ancestry_of thys > 
34b271c4f400
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents:
70545
diff
changeset

392 
(fn (ancestry as {parents, ancestors}, {parents = parents', ancestors = ancestors'}) => 
34b271c4f400
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents:
70545
diff
changeset

393 
if eq_list eq_thy (parents, parents') andalso eq_list eq_thy (ancestors, ancestors') 
34b271c4f400
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents:
70545
diff
changeset

394 
then ancestry else bad_join thys); 
34b271c4f400
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents:
70545
diff
changeset

395 

34b271c4f400
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents:
70545
diff
changeset

396 
in 
34b271c4f400
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents:
70545
diff
changeset

397 

34b271c4f400
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents:
70545
diff
changeset

398 
fun join_thys thys = 
34b271c4f400
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents:
70545
diff
changeset

399 
let 
34b271c4f400
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents:
70545
diff
changeset

400 
val ids = merge_ids thys; 
34b271c4f400
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents:
70545
diff
changeset

401 
val history = join_history thys; 
34b271c4f400
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents:
70545
diff
changeset

402 
val ancestry = join_ancestry thys; 
34b271c4f400
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents:
70545
diff
changeset

403 
val data = merge_data thys (apply2 data_of thys); 
34b271c4f400
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents:
70545
diff
changeset

404 
in create_thy ids history ancestry data end; 
34b271c4f400
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents:
70545
diff
changeset

405 

34b271c4f400
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents:
70545
diff
changeset

406 
end; 
34b271c4f400
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents:
70545
diff
changeset

407 

34b271c4f400
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents:
70545
diff
changeset

408 

34b271c4f400
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents:
70545
diff
changeset

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

410 

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

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

412 

67623  413 
fun merge_thys thys = 
26957  414 
let 
67623  415 
val ids = merge_ids thys; 
70545
03430649a7d2
clarified history stage: allow independent updates that are merged later;
wenzelm
parents:
68482
diff
changeset

416 
val history = make_history ""; 
26957  417 
val ancestry = make_ancestry [] []; 
67623  418 
val data = merge_data thys (apply2 data_of thys); 
60947  419 
in create_thy ids history ancestry data end; 
16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

420 

16533  421 
fun maximal_thys thys = 
28617  422 
thys > filter_out (fn thy => exists (fn thy' => proper_subthy (thy, thy')) thys); 
16533  423 

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

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

425 

61262
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

426 
fun begin_thy 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

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

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

430 
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

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

432 
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

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

434 

67623  435 
val thy0 = 
16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

436 
(case parents of 
48638  437 
[] => error "Missing theory imports" 
16533  438 
 [thy] => extend_thy thy 
61262
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

439 
 thy :: thys => Library.foldl merge_thys (thy, thys)); 
70638
70019ab5e57f
abstract type theory_id  ensure nonequality type independently of implementation;
wenzelm
parents:
70546
diff
changeset

440 
val ({ids, ...}, _) = rep_theory_id (theory_id thy0); 
29093
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

441 

70545
03430649a7d2
clarified history stage: allow independent updates that are merged later;
wenzelm
parents:
68482
diff
changeset

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

443 
val ancestry = make_ancestry parents ancestors; 
68193
14dd78f036ba
more thorough checks for theory name consistency (for extend, not just merge);
wenzelm
parents:
68192
diff
changeset

444 
in create_thy ids history ancestry (data_of thy0) > tap finish_thy end; 
16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

445 

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

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

447 

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

448 

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

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

450 

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

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

453 

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

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

455 

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

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

457 
(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

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

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

460 

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

461 
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

462 

67621  463 
fun obj_size k thy = 
464 
Datatab.lookup (data_of thy) k > Option.map ML_Heap.obj_size; 

465 

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

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

467 

67621  468 
fun theory_data_size thy = 
469 
(data_of thy, []) > Datatab.fold_rev (fn (k, _) => 

470 
(case Theory_Data.obj_size k thy of 

471 
NONE => I 

472 
 SOME n => (cons (invoke_pos k, n)))); 

473 

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

474 

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

475 

16533  476 
(*** proof context ***) 
477 

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

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

479 

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

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

481 
struct 
52788  482 
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

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

484 

16533  485 

486 
(* proof data kinds *) 

487 

488 
local 

489 

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

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

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

16533  494 

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

497 
if Datatab.defined data k then data 

498 
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

499 

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

502 
SOME init => init thy 

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

16533  504 

505 
in 

506 

52788  507 
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

508 
let 
52682  509 
val _ = subthy (thy, thy') orelse error "Cannot transfer proof context: not a super theory"; 
59163  510 
val data' = init_new_data thy' data; 
52788  511 
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

512 

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

514 
struct 
59163  515 
fun theory_of (Proof.Context (_, thy)) = thy; 
52788  516 
fun init_global thy = Proof.Context (init_data thy, thy); 
68482  517 
fun get_global thy name = init_global (get_theory {long = false} thy name); 
33031
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32784
diff
changeset

518 
end; 
16533  519 

33033  520 
structure Proof_Data = 
16533  521 
struct 
522 

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

523 
fun declare init = 
16533  524 
let 
525 
val k = serial (); 

43684  526 
val _ = Synchronized.change kinds (Datatab.update (k, init)); 
16533  527 
in k end; 
528 

59163  529 
fun get k dest (Proof.Context (data, thy)) = 
530 
(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

531 
SOME x => x 
59163  532 
 NONE => init_fallback k thy) > dest; 
16533  533 

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

16533  536 

537 
end; 

538 

539 
end; 

540 

541 

18632  542 

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

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

544 

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

545 
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

546 

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

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

548 
 certificate_theory (Certificate_Id thy_id) = 
61062  549 
error ("No content for theory certificate " ^ display_name thy_id); 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

550 

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

551 
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

552 
 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

553 

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

554 
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

555 
 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

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

557 

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

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

559 
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

560 
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

561 
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

562 
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

563 
else 
61045
c7a7f063704a
clarified exceptions: avoid interference of formal context failure with regular rule application failure (which is routinely handled in userspace);
wenzelm
parents:
61044
diff
changeset

564 
error ("Cannot join unrelated theory certificates " ^ 
61062  565 
display_name thy_id1 ^ " and " ^ display_name thy_id2) 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
60948
diff
changeset

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

567 

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

568 

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

569 

16533  570 
(*** generic context ***) 
571 

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

572 
datatype generic = Theory of theory  Proof of Proof.context; 
18632  573 

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

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

16533  576 

19678  577 
fun mapping f g = cases (Theory o f) (Proof o g); 
21660  578 
fun mapping_result f g = cases (apsnd Theory o f) (apsnd Proof o g); 
19678  579 

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

580 
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

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

18731  583 
fun map_theory f = Theory o f o the_theory; 
584 
fun map_proof f = Proof o f o the_proof; 

585 

26486  586 
fun map_theory_result f = apsnd Theory o f o the_theory; 
587 
fun map_proof_result f = apsnd Proof o f o the_proof; 

588 

18731  589 
fun theory_map f = the_theory o f o Theory; 
590 
fun proof_map f = the_proof o f o Proof; 

18665  591 

42360  592 
val theory_of = cases I Proof_Context.theory_of; 
593 
val proof_of = cases Proof_Context.init_global I; 

16533  594 

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

595 

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

596 

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

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

598 

62889  599 
local val generic_context_var = Thread_Data.var () : generic Thread_Data.var in 
26413
003dd6155870
added thread data (formerly global ref in ML/ml_context.ML);
wenzelm
parents:
24559
diff
changeset

600 

62889  601 
fun get_generic_context () = Thread_Data.get generic_context_var; 
602 
val put_generic_context = Thread_Data.put generic_context_var; 

603 
fun setmp_generic_context opt_context = Thread_Data.setmp generic_context_var opt_context; 

62876  604 

605 
fun the_generic_context () = 

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

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

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

609 

62876  610 
val the_global_context = theory_of o the_generic_context; 
611 
val the_local_context = proof_of o the_generic_context; 

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

612 

26428  613 
end; 
614 

615 
fun >>> f = 

616 
let 

62876  617 
val (res, context') = f (the_generic_context ()); 
62889  618 
val _ = put_generic_context (SOME context'); 
26428  619 
in res end; 
620 

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

623 

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

625 

6185  626 
end; 
627 

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

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

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

630 

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

631 

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

632 

16533  633 
(*** typesafe interfaces for data declarations ***) 
634 

635 
(** theory data **) 

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

636 

61262
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

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

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

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

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

641 
val extend: T > T 
61262
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

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

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

644 

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

645 
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

646 
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

647 
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

648 
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

649 
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

650 
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

651 
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

652 

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

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

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

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

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

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

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

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

660 

61262
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

661 
functor Theory_Data'(Data: THEORY_DATA'_ARGS): THEORY_DATA = 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

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

663 

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

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

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

666 

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

667 
val kind = 
72290
efb7fd4a6d1f
subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;
wenzelm
parents:
70772
diff
changeset

668 
let val pos = Position.thread_data () in 
efb7fd4a6d1f
subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;
wenzelm
parents:
70772
diff
changeset

669 
Context.Theory_Data.declare 
efb7fd4a6d1f
subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;
wenzelm
parents:
70772
diff
changeset

670 
pos 
efb7fd4a6d1f
subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;
wenzelm
parents:
70772
diff
changeset

671 
(Data Data.empty) 
efb7fd4a6d1f
subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;
wenzelm
parents:
70772
diff
changeset

672 
(fn Data x => 
efb7fd4a6d1f
subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;
wenzelm
parents:
70772
diff
changeset

673 
let 
efb7fd4a6d1f
subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;
wenzelm
parents:
70772
diff
changeset

674 
val y = Data.extend x; 
efb7fd4a6d1f
subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;
wenzelm
parents:
70772
diff
changeset

675 
val _ = 
efb7fd4a6d1f
subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;
wenzelm
parents:
70772
diff
changeset

676 
if pointer_eq (x, y) then () 
efb7fd4a6d1f
subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;
wenzelm
parents:
70772
diff
changeset

677 
else raise Fail ("Theory_Data extend needs to be identity" ^ Position.here pos) 
efb7fd4a6d1f
subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;
wenzelm
parents:
70772
diff
changeset

678 
in Data y end) 
efb7fd4a6d1f
subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;
wenzelm
parents:
70772
diff
changeset

679 
(fn thys => fn (Data x1, Data x2) => Data (Data.merge thys (x1, x2))) 
efb7fd4a6d1f
subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;
wenzelm
parents:
70772
diff
changeset

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

681 

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

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

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

685 

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

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

687 

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

688 
functor Theory_Data(Data: THEORY_DATA_ARGS): THEORY_DATA = 
61262
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61062
diff
changeset

689 
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

690 
( 
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

691 
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

692 
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

693 
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

694 
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

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

696 

16533  697 

698 

699 
(** proof data **) 

700 

701 
signature PROOF_DATA_ARGS = 

702 
sig 

703 
type T 

704 
val init: theory > T 

705 
end; 

706 

707 
signature PROOF_DATA = 

708 
sig 

709 
type T 

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

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

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

712 
val map: (T > T) > Proof.context > Proof.context 
16533  713 
end; 
714 

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

715 
functor Proof_Data(Data: PROOF_DATA_ARGS): PROOF_DATA = 
16533  716 
struct 
717 

718 
type T = Data.T; 

719 
exception Data of T; 

720 

33033  721 
val kind = Context.Proof_Data.declare (Data o Data.init); 
16533  722 

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

16533  725 
fun map f prf = put (f (get prf)) prf; 
726 

727 
end; 

728 

18632  729 

730 

731 
(** generic data **) 

732 

733 
signature GENERIC_DATA_ARGS = 

734 
sig 

735 
type T 

736 
val empty: T 

737 
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

738 
val merge: T * T > T 
18632  739 
end; 
740 

741 
signature GENERIC_DATA = 

742 
sig 

743 
type T 

744 
val get: Context.generic > T 

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

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

747 
end; 

748 

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

749 
functor Generic_Data(Data: GENERIC_DATA_ARGS): GENERIC_DATA = 
18632  750 
struct 
751 

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

752 
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

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

755 
type T = Data.T; 

756 

33033  757 
fun get (Context.Theory thy) = Thy_Data.get thy 
758 
 get (Context.Proof prf) = Prf_Data.get prf; 

18632  759 

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

18632  762 

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

764 

765 
end; 

766 

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

768 
structure Context: CONTEXT = Context; 