author  wenzelm 
Wed, 10 Apr 2013 17:02:47 +0200  
changeset 51686  532e0ac5a66d 
parent 51368  2ea5c7c2d825 
child 52682  77146b576ac7 
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 
type theory_ref 
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

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

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

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

22 
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

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

25 
end 
6185  26 
end; 
27 

28 
signature CONTEXT = 

29 
sig 

30 
include BASIC_CONTEXT 

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

31 
(*theory context*) 
42818
128cc195ced3
timing of Theory_Data operations, with implicit thread positions when functor is applied;
wenzelm
parents:
42383
diff
changeset

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

33 
type pretty 
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 
29069
c7ba485581ae
unified ids for ancestors and checkpoints, removed obsolete history of checkpoints;
wenzelm
parents:
29001
diff
changeset

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

37 
val is_stale: theory > bool 
26623  38 
val is_draft: theory > bool 
28317  39 
val reject_draft: theory > theory 
29093
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

40 
val PureN: string 
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 
24141
73baca986087
improved check_thy: produce a checked theory_ref (threadsafe version);
wenzelm
parents:
23944
diff
changeset

48 
val deref: theory_ref > theory 
73baca986087
improved check_thy: produce a checked theory_ref (threadsafe version);
wenzelm
parents:
23944
diff
changeset

49 
val check_thy: theory > theory_ref 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

50 
val eq_thy: theory * theory > bool 
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

51 
val subthy: theory * theory > bool 
16594  52 
val joinable: theory * theory > bool 
23355
d2c033fd4514
merge/merge_refs: plain error instead of exception TERM;
wenzelm
parents:
22847
diff
changeset

53 
val merge: theory * theory > theory 
d2c033fd4514
merge/merge_refs: plain error instead of exception TERM;
wenzelm
parents:
22847
diff
changeset

54 
val merge_refs: theory_ref * theory_ref > theory_ref 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

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

56 
val checkpoint_thy: theory > theory 
16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

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

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

60 
val raw_transfer: theory > Proof.context > Proof.context 
16533  61 
(*generic context*) 
33031
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32784
diff
changeset

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

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

64 
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

65 
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

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

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

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

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

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

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

76 
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

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

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

79 
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

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

81 
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

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

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

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

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

86 
val setmp_thread_data: generic option > ('a > 'b) > 'a > 'b 
26463  87 
val >> : (generic > generic) > unit 
88 
val >>> : (generic > 'a * generic) > 'a 

6185  89 
end; 
90 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

108 

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

109 
structure Context: PRIVATE_CONTEXT = 
6185  110 
struct 
111 

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

112 
(*** theory context ***) 
6185  113 

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

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

115 

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

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

117 

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

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

119 

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

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

121 
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

122 

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

123 
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

124 

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

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

126 

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

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

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

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

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

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

132 

43684  133 
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

134 

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

135 
fun invoke name f k x = 
43684  136 
(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

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

138 
if ! timing andalso name <> "" then 
48992  139 
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

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

141 
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

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

143 

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

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

145 

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

146 
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

147 
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

148 
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

149 

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

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

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

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

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

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

156 

39020  157 
val extend_data = Datatab.map invoke_extend; 
43610
16482dc641d4
back to sequential merge_data, reverting 741373421318 (NB: expensive Parser.merge_gram is already asynchronous since 3daff3cc2214);
wenzelm
parents:
42818
diff
changeset

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

159 

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

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

161 

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 

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

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

165 

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

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

167 
Theory of 
16533  168 
(*identity*) 
32738  169 
{self: theory Unsynchronized.ref option, (*dynamic self reference  follows theory changes*) 
29095  170 
draft: bool, (*draft mode  linear destructive changes*) 
29093
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

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

172 
ids: unit Inttab.table} * (*cumulative identifiers of nondrafts  symbolic body content*) 
29095  173 
(*data*) 
51368
2ea5c7c2d825
tuned signature  prefer terminology of Scala and Axiom;
wenzelm
parents:
50431
diff
changeset

174 
Any.T Datatab.table * (*body content*) 
29095  175 
(*ancestry*) 
29093
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

176 
{parents: theory list, (*immediate predecessors*) 
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

177 
ancestors: theory list} * (*all predecessors  canonical reverse order*) 
29095  178 
(*history*) 
29093
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

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

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

181 

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

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

183 

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

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

185 

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

186 
val identity_of = #1 o rep_theory; 
33033  187 
val data_of = #2 o rep_theory; 
16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

188 
val ancestry_of = #3 o rep_theory; 
33033  189 
val history_of = #4 o rep_theory; 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

190 

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

191 
fun make_identity self draft id ids = {self = self, draft = draft, id = id, ids = ids}; 
16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

192 
fun make_ancestry parents ancestors = {parents = parents, ancestors = ancestors}; 
29093
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

193 
fun make_history name stage = {name = name, stage = stage}; 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

194 

16533  195 
val the_self = the o #self o identity_of; 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

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

197 
val ancestors_of = #ancestors o ancestry_of; 
16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

198 
val theory_name = #name o history_of; 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

199 

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

200 

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

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

202 

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

203 
fun eq_id (i: int, j) = i = j; 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

204 

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

205 
fun is_stale 
32738  206 
(Theory ({self = 
207 
SOME (Unsynchronized.ref (Theory ({id = id', ...}, _, _, _))), id, ...}, _, _, _)) = 

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

208 
not (eq_id (id, id')) 
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

209 
 is_stale (Theory ({self = NONE, ...}, _, _, _)) = true; 
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

210 

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

211 
fun vitalize (thy as Theory ({self = SOME r, ...}, _, _, _)) = (r := thy; thy) 
29093
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

212 
 vitalize (thy as Theory ({self = NONE, draft, id, ids}, data, ancestry, history)) = 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

213 
let 
32738  214 
val r = Unsynchronized.ref thy; 
29093
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

215 
val thy' = Theory (make_identity (SOME r) draft id ids, data, ancestry, history); 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

216 
in r := thy'; thy' end; 
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

217 

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

218 

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

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

220 

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

221 
val is_draft = #draft o identity_of; 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

222 

28317  223 
fun reject_draft thy = 
33031
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32784
diff
changeset

224 
if is_draft thy then 
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32784
diff
changeset

225 
raise THEORY ("Illegal draft theory  stable checkpoint required", [thy]) 
28317  226 
else thy; 
227 

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

228 

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

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

230 

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

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

232 
val draftN = "#"; 
29095  233 
val finished = ~1; 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

234 

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

235 
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

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

237 
val draft = if is_draft thy then [draftN] else []; 
29095  238 
val {stage, ...} = history_of thy; 
29093
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

239 
val name = 
29095  240 
if stage = finished then theory_name thy 
241 
else theory_name thy ^ ":" ^ string_of_int stage; 

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

242 
val ancestor_names = map theory_name (ancestors_of thy); 
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

243 
val stale = if is_stale thy then ["!"] else []; 
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

244 
in rev (stale @ draft @ [name] @ ancestor_names) end; 
29069
c7ba485581ae
unified ids for ancestors and checkpoints, removed obsolete history of checkpoints;
wenzelm
parents:
29001
diff
changeset

245 

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

246 
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

247 
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

248 

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

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

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

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

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

253 
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

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

255 

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

256 
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

257 

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

258 
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

259 
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

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

261 
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

262 
 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

263 
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

264 
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

265 

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

266 
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

267 
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

268 
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

269 

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

270 

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

271 
(* theory references *) 
73baca986087
improved check_thy: produce a checked theory_ref (threadsafe version);
wenzelm
parents:
23944
diff
changeset

272 

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

273 
(*theory_ref provides a safe way to store dynamic references to a 
73baca986087
improved check_thy: produce a checked theory_ref (threadsafe version);
wenzelm
parents:
23944
diff
changeset

274 
theory in external data structures  a plain theory value would 
73baca986087
improved check_thy: produce a checked theory_ref (threadsafe version);
wenzelm
parents:
23944
diff
changeset

275 
become stale as the self reference moves on*) 
73baca986087
improved check_thy: produce a checked theory_ref (threadsafe version);
wenzelm
parents:
23944
diff
changeset

276 

33033  277 
datatype theory_ref = Theory_Ref of theory Unsynchronized.ref; 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

278 

33033  279 
fun deref (Theory_Ref (Unsynchronized.ref thy)) = thy; 
24141
73baca986087
improved check_thy: produce a checked theory_ref (threadsafe version);
wenzelm
parents:
23944
diff
changeset

280 

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

281 
fun check_thy thy = (*threadsafe version*) 
33033  282 
let val thy_ref = Theory_Ref (the_self thy) in 
24141
73baca986087
improved check_thy: produce a checked theory_ref (threadsafe version);
wenzelm
parents:
23944
diff
changeset

283 
if is_stale thy then error ("Stale theory encountered:\n" ^ string_of_thy thy) 
73baca986087
improved check_thy: produce a checked theory_ref (threadsafe version);
wenzelm
parents:
23944
diff
changeset

284 
else thy_ref 
73baca986087
improved check_thy: produce a checked theory_ref (threadsafe version);
wenzelm
parents:
23944
diff
changeset

285 
end; 
73baca986087
improved check_thy: produce a checked theory_ref (threadsafe version);
wenzelm
parents:
23944
diff
changeset

286 

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

287 

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

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

289 

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

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

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

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

293 

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

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

295 
(Theory ({draft = draft1, id = id1, ids = ids1, ...}, _, _, _)) 
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

296 
(Theory ({draft = draft2, id = id2, ids = ids2, ...}, _, _, _)) = 
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

297 
Inttab.merge (K true) (ids1, ids2) 
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

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

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

300 

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

301 

16533  302 
(* equality and inclusion *) 
303 

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

304 
val eq_thy = eq_id o pairself (#id o identity_of); 
16533  305 

29069
c7ba485581ae
unified ids for ancestors and checkpoints, removed obsolete history of checkpoints;
wenzelm
parents:
29001
diff
changeset

306 
fun proper_subthy (Theory ({id, ...}, _, _, _), Theory ({ids, ...}, _, _, _)) = 
29093
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

307 
Inttab.defined ids id; 
16533  308 

309 
fun subthy thys = eq_thy thys orelse proper_subthy thys; 

310 

16594  311 
fun joinable (thy1, thy2) = subthy (thy1, thy2) orelse subthy (thy2, thy1); 
312 

16533  313 

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

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

315 

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

316 
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

317 
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

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

319 
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

320 

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

321 
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

322 
if member eq_thy_consistent thys thy then 
33033  323 
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

324 
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

325 

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

326 
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

327 

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

328 

23355
d2c033fd4514
merge/merge_refs: plain error instead of exception TERM;
wenzelm
parents:
22847
diff
changeset

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

330 

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

331 
fun merge (thy1, thy2) = 
16719  332 
if eq_thy (thy1, thy2) then thy1 
333 
else if proper_subthy (thy2, thy1) then thy1 

334 
else if proper_subthy (thy1, thy2) then thy2 

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

335 
else error (cat_lines ["Attempt to perform nontrivial merge of theories:", 
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

336 
str_of_thy thy1, str_of_thy thy2]); 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

337 

16719  338 
fun merge_refs (ref1, ref2) = 
339 
if ref1 = ref2 then ref1 

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

340 
else check_thy (merge (deref ref1, deref ref2)); 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

341 

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

342 

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

343 

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

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

345 

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

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

347 

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

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

349 
val lock = Mutex.mutex (); 
2b27020ffcb2
local mutex for theory content/identity operations;
wenzelm
parents:
33517
diff
changeset

350 
in 
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36610
diff
changeset

351 
fun SYNCHRONIZED e = Simple_Thread.synchronized "theory" lock e; 
33606
2b27020ffcb2
local mutex for theory content/identity operations;
wenzelm
parents:
33517
diff
changeset

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

353 

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

354 
fun create_thy self draft ids data ancestry history = 
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

355 
let val identity = make_identity self draft (serial ()) ids; 
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

356 
in vitalize (Theory (identity, data, ancestry, history)) end; 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

357 

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

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

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

360 
val Theory ({self, draft, id, ids}, data, ancestry, history) = thy; 
16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

361 
val (self', data', ancestry') = 
29093
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

362 
if draft then (self, data, ancestry) (*destructive change!*) 
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

363 
else if #stage history > 0 
34245  364 
then (NONE, data, ancestry) 
50431
955c4aa44f60
check consistent theory names for direct imports as well  as claimed in the comments (see also 1cc36c0ec9eb);
wenzelm
parents:
48992
diff
changeset

365 
else (NONE, extend_data data, make_ancestry [thy] (extend_ancestors thy (ancestors_of thy))); 
29093
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

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

367 
val data'' = f data'; 
33606
2b27020ffcb2
local mutex for theory content/identity operations;
wenzelm
parents:
33517
diff
changeset

368 
val thy' = SYNCHRONIZED (fn () => 
29093
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

369 
(check_thy thy; create_thy self' draft' ids' data'' ancestry' history)); 
24369  370 
in thy' end; 
16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

371 

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

372 
val name_thy = change_thy false I; 
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

373 
val extend_thy = change_thy true I; 
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

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

375 

24369  376 
fun copy_thy thy = 
24141
73baca986087
improved check_thy: produce a checked theory_ref (threadsafe version);
wenzelm
parents:
23944
diff
changeset

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

378 
val Theory ({draft, id, ids, ...}, data, ancestry, history) = thy; 
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

379 
val ids' = insert_id draft id ids; 
33606
2b27020ffcb2
local mutex for theory content/identity operations;
wenzelm
parents:
33517
diff
changeset

380 
val thy' = SYNCHRONIZED (fn () => 
34245  381 
(check_thy thy; create_thy NONE true ids' data ancestry history)); 
24369  382 
in thy' end; 
16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

383 

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

384 
val pre_pure_thy = create_thy NONE true Inttab.empty 
29069
c7ba485581ae
unified ids for ancestors and checkpoints, removed obsolete history of checkpoints;
wenzelm
parents:
29001
diff
changeset

385 
Datatab.empty (make_ancestry [] []) (make_history PureN 0); 
16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

386 

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

387 

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

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

389 

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

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

392 
val ids = merge_ids thy1 thy2; 
26957  393 
val data = merge_data (pp thy1) (data_of thy1, data_of thy2); 
394 
val ancestry = make_ancestry [] []; 

29069
c7ba485581ae
unified ids for ancestors and checkpoints, removed obsolete history of checkpoints;
wenzelm
parents:
29001
diff
changeset

395 
val history = make_history "" 0; 
33606
2b27020ffcb2
local mutex for theory content/identity operations;
wenzelm
parents:
33517
diff
changeset

396 
val thy' = SYNCHRONIZED (fn () => 
29093
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

397 
(check_thy thy1; check_thy thy2; create_thy NONE true ids data ancestry history)); 
26957  398 
in thy' end; 
16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

399 

16533  400 
fun maximal_thys thys = 
28617  401 
thys > filter_out (fn thy => exists (fn thy' => proper_subthy (thy, thy')) thys); 
16533  402 

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

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

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

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

407 
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

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

409 
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

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

411 

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

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

413 
(case parents of 
48638  414 
[] => error "Missing theory imports" 
16533  415 
 [thy] => extend_thy thy 
416 
 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

417 

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

418 
val ancestry = make_ancestry parents ancestors; 
29069
c7ba485581ae
unified ids for ancestors and checkpoints, removed obsolete history of checkpoints;
wenzelm
parents:
29001
diff
changeset

419 
val history = make_history name 0; 
33606
2b27020ffcb2
local mutex for theory content/identity operations;
wenzelm
parents:
33517
diff
changeset

420 
val thy' = SYNCHRONIZED (fn () => 
29093
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

421 
(map check_thy imports; create_thy NONE true ids data ancestry history)); 
24369  422 
in thy' end; 
16436
7eb6b6cbd166
added type theory: generic theory contexts with unique identity,
wenzelm
parents:
15801
diff
changeset

423 

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

424 

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

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

426 

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

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

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

429 
val {name, stage} = history_of thy; 
29095  430 
val _ = stage = finished andalso raise THEORY ("Theory already finished", [thy]); 
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 history' = make_history name (f stage); 
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

432 
val thy' as Theory (identity', data', ancestry', _) = name_thy thy; 
33606
2b27020ffcb2
local mutex for theory content/identity operations;
wenzelm
parents:
33517
diff
changeset

433 
val thy'' = SYNCHRONIZED (fn () => 
29093
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

434 
(check_thy thy'; vitalize (Theory (identity', data', ancestry', history')))); 
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

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

436 

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

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

438 
if is_draft thy then history_stage (fn stage => stage + 1) thy 
1cc36c0ec9eb
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
wenzelm
parents:
29069
diff
changeset

439 
else thy; 
16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

440 

29095  441 
val finish_thy = history_stage (fn _ => finished); 
16489
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

442 

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

443 

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

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

445 

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

447 
struct 
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 
val declare = declare_theory_data; 
f66ab8a4e98f
improved treatment of intermediate checkpoints: actual copy
wenzelm
parents:
16436
diff
changeset

450 

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

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

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

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

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

455 

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

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

457 

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

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

459 

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

460 

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

461 

16533  462 
(*** proof context ***) 
463 

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

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

465 

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

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

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

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

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

470 

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

471 
fun theory_of_proof (Proof.Context (_, thy_ref)) = deref thy_ref; 
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32784
diff
changeset

472 
fun data_of_proof (Proof.Context (data, _)) = data; 
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32784
diff
changeset

473 
fun map_prf f (Proof.Context (data, thy_ref)) = Proof.Context (f data, thy_ref); 
17060
cca2f3938443
type proof: theory_ref instead of theory (make proof contexts independent entities);
wenzelm
parents:
16894
diff
changeset

474 

16533  475 

476 
(* proof data kinds *) 

477 

478 
local 

479 

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

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

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

482 
fun invoke_init k = 
43684  483 
(case Datatab.lookup (Synchronized.value kinds) 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

484 
SOME init => init 
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

485 
 NONE => raise Fail "Invalid proof data identifier"); 
16533  486 

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

487 
fun init_data thy = 
43684  488 
Datatab.map (fn k => fn _ => invoke_init k thy) (Synchronized.value kinds); 
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

489 

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

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

491 
Datatab.merge (K true) (data, init_data thy); 
16533  492 

493 
in 

494 

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

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

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

497 
val thy = deref thy_ref; 
73baca986087
improved check_thy: produce a checked theory_ref (threadsafe version);
wenzelm
parents:
23944
diff
changeset

498 
val _ = subthy (thy, thy') orelse error "transfer proof context: not a super theory"; 
73baca986087
improved check_thy: produce a checked theory_ref (threadsafe version);
wenzelm
parents:
23944
diff
changeset

499 
val _ = check_thy thy; 
24184
19cb051154fd
threadsafeness: when creating certified items, perform Theory.check_thy *last*;
wenzelm
parents:
24141
diff
changeset

500 
val data' = init_new_data data thy'; 
24141
73baca986087
improved check_thy: produce a checked theory_ref (threadsafe version);
wenzelm
parents:
23944
diff
changeset

501 
val thy_ref' = check_thy thy'; 
33031
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32784
diff
changeset

502 
in Proof.Context (data', thy_ref') 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

503 

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

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

506 
val theory_of = theory_of_proof; 
36610
bafd82950e24
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
wenzelm
parents:
34259
diff
changeset

507 
fun init_global thy = Proof.Context (init_data thy, check_thy thy); 
51686  508 
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

509 
end; 
16533  510 

33033  511 
structure Proof_Data = 
16533  512 
struct 
513 

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

514 
fun declare init = 
16533  515 
let 
516 
val k = serial (); 

43684  517 
val _ = Synchronized.change kinds (Datatab.update (k, init)); 
16533  518 
in k end; 
519 

520 
fun get k dest prf = 

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

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

522 
SOME x => x 
42360  523 
 NONE => invoke_init k (Proof_Context.theory_of prf)); (*adhoc value*) 
16533  524 

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

525 
fun put k mk x = map_prf (Datatab.update (k, mk x)); 
16533  526 

527 
end; 

528 

529 
end; 

530 

531 

18632  532 

16533  533 
(*** generic context ***) 
534 

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

535 
datatype generic = Theory of theory  Proof of Proof.context; 
18632  536 

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

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

16533  539 

19678  540 
fun mapping f g = cases (Theory o f) (Proof o g); 
21660  541 
fun mapping_result f g = cases (apsnd Theory o f) (apsnd Proof o g); 
19678  542 

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

543 
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

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

18731  546 
fun map_theory f = Theory o f o the_theory; 
547 
fun map_proof f = Proof o f o the_proof; 

548 

26486  549 
fun map_theory_result f = apsnd Theory o f o the_theory; 
550 
fun map_proof_result f = apsnd Proof o f o the_proof; 

551 

18731  552 
fun theory_map f = the_theory o f o Theory; 
553 
fun proof_map f = the_proof o f o Proof; 

18665  554 

42360  555 
val theory_of = cases I Proof_Context.theory_of; 
556 
val proof_of = cases Proof_Context.init_global I; 

16533  557 

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

558 

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

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

560 

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

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

562 

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

563 
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

564 
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

565 
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

566 

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

567 
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

568 

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

569 

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

570 

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

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

572 

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

573 
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

574 

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

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

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

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

579 

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

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

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

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

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

584 

28122  585 
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

586 
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

587 

26428  588 
end; 
589 

590 
fun >>> f = 

591 
let 

26463  592 
val (res, context') = f (the_thread_data ()); 
593 
val _ = set_thread_data (SOME context'); 

26428  594 
in res end; 
595 

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

598 

26428  599 
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

600 

6185  601 
end; 
602 

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

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

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

605 

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

606 

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

607 

16533  608 
(*** typesafe interfaces for data declarations ***) 
609 

610 
(** theory data **) 

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

611 

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

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

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

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

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

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

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

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

619 

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

620 
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

621 
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

622 
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

623 
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

624 
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

625 
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

626 
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

627 

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

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

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

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

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

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

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

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

635 

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

636 
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

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

638 

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

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

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

641 

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

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

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

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

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

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

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

648 

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

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

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

652 

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

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

654 

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

655 
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

656 
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

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

658 
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

659 
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

660 
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

661 
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

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

663 

16533  664 

665 

666 
(** proof data **) 

667 

668 
signature PROOF_DATA_ARGS = 

669 
sig 

670 
type T 

671 
val init: theory > T 

672 
end; 

673 

674 
signature PROOF_DATA = 

675 
sig 

676 
type T 

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

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

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

679 
val map: (T > T) > Proof.context > Proof.context 
16533  680 
end; 
681 

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

682 
functor Proof_Data(Data: PROOF_DATA_ARGS): PROOF_DATA = 
16533  683 
struct 
684 

685 
type T = Data.T; 

686 
exception Data of T; 

687 

33033  688 
val kind = Context.Proof_Data.declare (Data o Data.init); 
16533  689 

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

16533  692 
fun map f prf = put (f (get prf)) prf; 
693 

694 
end; 

695 

18632  696 

697 

698 
(** generic data **) 

699 

700 
signature GENERIC_DATA_ARGS = 

701 
sig 

702 
type T 

703 
val empty: T 

704 
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

705 
val merge: T * T > T 
18632  706 
end; 
707 

708 
signature GENERIC_DATA = 

709 
sig 

710 
type T 

711 
val get: Context.generic > T 

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

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

714 
end; 

715 

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

716 
functor Generic_Data(Data: GENERIC_DATA_ARGS): GENERIC_DATA = 
18632  717 
struct 
718 

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

719 
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

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

722 
type T = Data.T; 

723 

33033  724 
fun get (Context.Theory thy) = Thy_Data.get thy 
725 
 get (Context.Proof prf) = Prf_Data.get prf; 

18632  726 

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

18632  729 

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

731 

732 
end; 

733 

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

735 
structure Context: CONTEXT = Context; 
20297  736 