wenzelm@6185
|
1 |
(* Title: Pure/context.ML
|
wenzelm@6185
|
2 |
ID: $Id$
|
wenzelm@6185
|
3 |
Author: Markus Wenzel, TU Muenchen
|
wenzelm@6185
|
4 |
|
wenzelm@16436
|
5 |
Generic theory contexts with unique identity, arbitrarily typed data,
|
wenzelm@22095
|
6 |
development graph and history support. Generic proof contexts with
|
wenzelm@22095
|
7 |
arbitrarily typed data.
|
wenzelm@6185
|
8 |
*)
|
wenzelm@6185
|
9 |
|
wenzelm@6185
|
10 |
signature BASIC_CONTEXT =
|
wenzelm@6185
|
11 |
sig
|
wenzelm@16436
|
12 |
type theory
|
wenzelm@16436
|
13 |
type theory_ref
|
wenzelm@16436
|
14 |
exception THEORY of string * theory list
|
wenzelm@6185
|
15 |
end;
|
wenzelm@6185
|
16 |
|
wenzelm@6185
|
17 |
signature CONTEXT =
|
wenzelm@6185
|
18 |
sig
|
wenzelm@6185
|
19 |
include BASIC_CONTEXT
|
wenzelm@16436
|
20 |
(*theory context*)
|
wenzelm@16489
|
21 |
val theory_name: theory -> string
|
wenzelm@16436
|
22 |
val parents_of: theory -> theory list
|
wenzelm@16436
|
23 |
val ancestors_of: theory -> theory list
|
wenzelm@16436
|
24 |
val is_stale: theory -> bool
|
wenzelm@16436
|
25 |
val ProtoPureN: string
|
wenzelm@16436
|
26 |
val PureN: string
|
wenzelm@16436
|
27 |
val CPureN: string
|
wenzelm@16436
|
28 |
val draftN: string
|
wenzelm@16436
|
29 |
val exists_name: string -> theory -> bool
|
wenzelm@16436
|
30 |
val names_of: theory -> string list
|
wenzelm@16436
|
31 |
val pretty_thy: theory -> Pretty.T
|
wenzelm@16436
|
32 |
val string_of_thy: theory -> string
|
wenzelm@16436
|
33 |
val pprint_thy: theory -> pprint_args -> unit
|
wenzelm@16436
|
34 |
val pretty_abbrev_thy: theory -> Pretty.T
|
wenzelm@16436
|
35 |
val str_of_thy: theory -> string
|
wenzelm@16719
|
36 |
val check_thy: theory -> theory
|
wenzelm@16436
|
37 |
val eq_thy: theory * theory -> bool
|
wenzelm@16436
|
38 |
val subthy: theory * theory -> bool
|
wenzelm@16594
|
39 |
val joinable: theory * theory -> bool
|
wenzelm@16489
|
40 |
val merge: theory * theory -> theory (*exception TERM*)
|
wenzelm@16489
|
41 |
val merge_refs: theory_ref * theory_ref -> theory_ref (*exception TERM*)
|
wenzelm@16436
|
42 |
val self_ref: theory -> theory_ref
|
wenzelm@16436
|
43 |
val deref: theory_ref -> theory
|
wenzelm@16436
|
44 |
val copy_thy: theory -> theory
|
wenzelm@16436
|
45 |
val checkpoint_thy: theory -> theory
|
wenzelm@16489
|
46 |
val finish_thy: theory -> theory
|
wenzelm@22131
|
47 |
val is_finished_thy: theory -> bool
|
wenzelm@16533
|
48 |
val theory_data_of: theory -> string list
|
wenzelm@16489
|
49 |
val pre_pure_thy: theory
|
wenzelm@16489
|
50 |
val begin_thy: (theory -> Pretty.pp) -> string -> theory list -> theory
|
wenzelm@16533
|
51 |
(*proof context*)
|
wenzelm@16533
|
52 |
type proof
|
wenzelm@16533
|
53 |
val theory_of_proof: proof -> theory
|
wenzelm@17060
|
54 |
val transfer_proof: theory -> proof -> proof
|
wenzelm@16533
|
55 |
val init_proof: theory -> proof
|
wenzelm@16533
|
56 |
val proof_data_of: theory -> string list
|
wenzelm@16533
|
57 |
(*generic context*)
|
wenzelm@18632
|
58 |
datatype generic = Theory of theory | Proof of proof
|
wenzelm@18632
|
59 |
val cases: (theory -> 'a) -> (proof -> 'a) -> generic -> 'a
|
wenzelm@19678
|
60 |
val mapping: (theory -> theory) -> (proof -> proof) -> generic -> generic
|
wenzelm@21660
|
61 |
val mapping_result: (theory -> 'a * theory) -> (proof -> 'a * proof) -> generic -> 'a * generic
|
wenzelm@18632
|
62 |
val the_theory: generic -> theory
|
wenzelm@18632
|
63 |
val the_proof: generic -> proof
|
wenzelm@18731
|
64 |
val map_theory: (theory -> theory) -> generic -> generic
|
wenzelm@18731
|
65 |
val map_proof: (proof -> proof) -> generic -> generic
|
wenzelm@18731
|
66 |
val theory_map: (generic -> generic) -> theory -> theory
|
wenzelm@18731
|
67 |
val proof_map: (generic -> generic) -> proof -> proof
|
wenzelm@18665
|
68 |
val theory_of: generic -> theory (*total*)
|
wenzelm@18665
|
69 |
val proof_of: generic -> proof (*total*)
|
wenzelm@22095
|
70 |
(*delayed setup*)
|
wenzelm@22085
|
71 |
val add_setup: (theory -> theory) -> unit
|
wenzelm@22085
|
72 |
val setup: unit -> theory -> theory
|
wenzelm@6185
|
73 |
end;
|
wenzelm@6185
|
74 |
|
wenzelm@16436
|
75 |
signature PRIVATE_CONTEXT =
|
wenzelm@16436
|
76 |
sig
|
wenzelm@16436
|
77 |
include CONTEXT
|
wenzelm@16436
|
78 |
structure TheoryData:
|
wenzelm@16436
|
79 |
sig
|
wenzelm@16489
|
80 |
val declare: string -> Object.T -> (Object.T -> Object.T) -> (Object.T -> Object.T) ->
|
wenzelm@16489
|
81 |
(Pretty.pp -> Object.T * Object.T -> Object.T) -> serial
|
wenzelm@16436
|
82 |
val init: serial -> theory -> theory
|
wenzelm@16436
|
83 |
val get: serial -> (Object.T -> 'a) -> theory -> 'a
|
wenzelm@16436
|
84 |
val put: serial -> ('a -> Object.T) -> 'a -> theory -> theory
|
wenzelm@16489
|
85 |
end
|
wenzelm@16533
|
86 |
structure ProofData:
|
wenzelm@16533
|
87 |
sig
|
wenzelm@16533
|
88 |
val declare: string -> (theory -> Object.T) -> serial
|
wenzelm@16533
|
89 |
val init: serial -> theory -> theory
|
wenzelm@16533
|
90 |
val get: serial -> (Object.T -> 'a) -> proof -> 'a
|
wenzelm@16533
|
91 |
val put: serial -> ('a -> Object.T) -> 'a -> proof -> proof
|
wenzelm@16533
|
92 |
end
|
wenzelm@16436
|
93 |
end;
|
wenzelm@16436
|
94 |
|
wenzelm@16436
|
95 |
structure Context: PRIVATE_CONTEXT =
|
wenzelm@6185
|
96 |
struct
|
wenzelm@6185
|
97 |
|
wenzelm@16436
|
98 |
(*** theory context ***)
|
wenzelm@6185
|
99 |
|
wenzelm@16489
|
100 |
(** theory data **)
|
wenzelm@16489
|
101 |
|
wenzelm@16489
|
102 |
(* data kinds and access methods *)
|
wenzelm@16489
|
103 |
|
wenzelm@19028
|
104 |
(*private copy avoids potential conflict of table exceptions*)
|
wenzelm@19028
|
105 |
structure Datatab = TableFun(type key = int val ord = int_ord);
|
wenzelm@19028
|
106 |
|
wenzelm@16489
|
107 |
local
|
wenzelm@16489
|
108 |
|
wenzelm@16489
|
109 |
type kind =
|
wenzelm@16489
|
110 |
{name: string,
|
wenzelm@16489
|
111 |
empty: Object.T,
|
wenzelm@16489
|
112 |
copy: Object.T -> Object.T,
|
wenzelm@16489
|
113 |
extend: Object.T -> Object.T,
|
wenzelm@16489
|
114 |
merge: Pretty.pp -> Object.T * Object.T -> Object.T};
|
wenzelm@16489
|
115 |
|
wenzelm@19028
|
116 |
val kinds = ref (Datatab.empty: kind Datatab.table);
|
wenzelm@16489
|
117 |
|
wenzelm@16489
|
118 |
fun invoke meth_name meth_fn k =
|
wenzelm@19028
|
119 |
(case Datatab.lookup (! kinds) k of
|
wenzelm@16489
|
120 |
SOME kind => meth_fn kind |> transform_failure (fn exn =>
|
wenzelm@17340
|
121 |
EXCEPTION (exn, "Theory data method " ^ #name kind ^ "." ^ meth_name ^ " failed"))
|
wenzelm@16489
|
122 |
| NONE => sys_error ("Invalid theory data identifier " ^ string_of_int k));
|
wenzelm@16489
|
123 |
|
wenzelm@16489
|
124 |
in
|
wenzelm@16489
|
125 |
|
wenzelm@16489
|
126 |
fun invoke_name k = invoke "name" (K o #name) k ();
|
wenzelm@16489
|
127 |
fun invoke_empty k = invoke "empty" (K o #empty) k ();
|
wenzelm@16489
|
128 |
val invoke_copy = invoke "copy" #copy;
|
wenzelm@16489
|
129 |
val invoke_extend = invoke "extend" #extend;
|
wenzelm@16489
|
130 |
fun invoke_merge pp = invoke "merge" (fn kind => #merge kind pp);
|
wenzelm@16489
|
131 |
|
wenzelm@16533
|
132 |
fun declare_theory_data name empty copy extend merge =
|
wenzelm@16489
|
133 |
let
|
wenzelm@16489
|
134 |
val k = serial ();
|
wenzelm@16533
|
135 |
val kind = {name = name, empty = empty, copy = copy, extend = extend, merge = merge};
|
wenzelm@21962
|
136 |
val _ =
|
wenzelm@21962
|
137 |
if Datatab.exists (equal name o #name o #2) (! kinds) then
|
wenzelm@21962
|
138 |
warning ("Duplicate declaration of theory data " ^ quote name)
|
wenzelm@21962
|
139 |
else ();
|
wenzelm@19028
|
140 |
val _ = change kinds (Datatab.update (k, kind));
|
wenzelm@16489
|
141 |
in k end;
|
wenzelm@16489
|
142 |
|
wenzelm@19028
|
143 |
val copy_data = Datatab.map' invoke_copy;
|
wenzelm@19028
|
144 |
val extend_data = Datatab.map' invoke_extend;
|
wenzelm@19028
|
145 |
fun merge_data pp = Datatab.join (invoke_merge pp) o pairself extend_data;
|
wenzelm@16489
|
146 |
|
wenzelm@16489
|
147 |
end;
|
wenzelm@16489
|
148 |
|
wenzelm@16489
|
149 |
|
wenzelm@16489
|
150 |
|
wenzelm@16489
|
151 |
(** datatype theory **)
|
wenzelm@16489
|
152 |
|
wenzelm@16436
|
153 |
datatype theory =
|
wenzelm@16436
|
154 |
Theory of
|
wenzelm@16533
|
155 |
(*identity*)
|
wenzelm@16489
|
156 |
{self: theory ref option, (*dynamic self reference -- follows theory changes*)
|
wenzelm@16489
|
157 |
id: serial * string, (*identifier of this theory*)
|
wenzelm@16489
|
158 |
ids: string Inttab.table, (*identifiers of ancestors*)
|
wenzelm@16489
|
159 |
iids: string Inttab.table} * (*identifiers of intermediate checkpoints*)
|
wenzelm@16533
|
160 |
(*data*)
|
wenzelm@19028
|
161 |
{theory: Object.T Datatab.table, (*theory data record*)
|
wenzelm@19028
|
162 |
proof: unit Datatab.table} * (*proof data kinds*)
|
wenzelm@16533
|
163 |
(*ancestry*)
|
wenzelm@16489
|
164 |
{parents: theory list, (*immediate predecessors*)
|
wenzelm@16489
|
165 |
ancestors: theory list} * (*all predecessors*)
|
wenzelm@16533
|
166 |
(*history*)
|
wenzelm@16489
|
167 |
{name: string, (*prospective name of finished theory*)
|
wenzelm@16489
|
168 |
version: int, (*checkpoint counter*)
|
wenzelm@16489
|
169 |
intermediates: theory list}; (*intermediate checkpoints*)
|
wenzelm@16436
|
170 |
|
wenzelm@16436
|
171 |
exception THEORY of string * theory list;
|
wenzelm@16436
|
172 |
|
wenzelm@16436
|
173 |
fun rep_theory (Theory args) = args;
|
wenzelm@16436
|
174 |
|
wenzelm@16436
|
175 |
val identity_of = #1 o rep_theory;
|
wenzelm@16436
|
176 |
val data_of = #2 o rep_theory;
|
wenzelm@16489
|
177 |
val ancestry_of = #3 o rep_theory;
|
wenzelm@16489
|
178 |
val history_of = #4 o rep_theory;
|
wenzelm@16436
|
179 |
|
wenzelm@16489
|
180 |
fun make_identity self id ids iids = {self = self, id = id, ids = ids, iids = iids};
|
wenzelm@16533
|
181 |
fun make_data theory proof = {theory = theory, proof = proof};
|
wenzelm@16489
|
182 |
fun make_ancestry parents ancestors = {parents = parents, ancestors = ancestors};
|
wenzelm@16436
|
183 |
fun make_history name vers ints = {name = name, version = vers, intermediates = ints};
|
wenzelm@16436
|
184 |
|
wenzelm@18731
|
185 |
fun map_theory_data f {theory, proof} = make_data (f theory) proof;
|
wenzelm@18731
|
186 |
fun map_proof_data f {theory, proof} = make_data theory (f proof);
|
wenzelm@16533
|
187 |
|
wenzelm@16533
|
188 |
val the_self = the o #self o identity_of;
|
wenzelm@16436
|
189 |
val parents_of = #parents o ancestry_of;
|
wenzelm@16436
|
190 |
val ancestors_of = #ancestors o ancestry_of;
|
wenzelm@16489
|
191 |
val theory_name = #name o history_of;
|
wenzelm@16436
|
192 |
|
wenzelm@16436
|
193 |
|
wenzelm@16436
|
194 |
(* staleness *)
|
wenzelm@16436
|
195 |
|
wenzelm@16533
|
196 |
fun eq_id ((i: int, _), (j, _)) = (i = j);
|
wenzelm@16436
|
197 |
|
wenzelm@16436
|
198 |
fun is_stale
|
wenzelm@16436
|
199 |
(Theory ({self = SOME (ref (Theory ({id = id', ...}, _, _, _))), id, ...}, _, _, _)) =
|
wenzelm@16436
|
200 |
not (eq_id (id, id'))
|
wenzelm@16436
|
201 |
| is_stale (Theory ({self = NONE, ...}, _, _, _)) = true;
|
wenzelm@16436
|
202 |
|
wenzelm@16436
|
203 |
fun vitalize (thy as Theory ({self = SOME r, ...}, _, _, _)) = (r := thy; thy)
|
wenzelm@16489
|
204 |
| vitalize (thy as Theory ({self = NONE, id, ids, iids}, data, ancestry, history)) =
|
wenzelm@16436
|
205 |
let
|
wenzelm@16436
|
206 |
val r = ref thy;
|
wenzelm@16489
|
207 |
val thy' = Theory (make_identity (SOME r) id ids iids, data, ancestry, history);
|
wenzelm@16436
|
208 |
in r := thy'; thy' end;
|
wenzelm@16436
|
209 |
|
wenzelm@16436
|
210 |
|
wenzelm@16436
|
211 |
(* names *)
|
wenzelm@16436
|
212 |
|
wenzelm@16436
|
213 |
val ProtoPureN = "ProtoPure";
|
wenzelm@16436
|
214 |
val PureN = "Pure";
|
wenzelm@16436
|
215 |
val CPureN = "CPure";
|
wenzelm@16436
|
216 |
|
wenzelm@16436
|
217 |
val draftN = "#";
|
wenzelm@16436
|
218 |
fun draft_id (_, name) = (name = draftN);
|
wenzelm@16436
|
219 |
val is_draft = draft_id o #id o identity_of;
|
wenzelm@16436
|
220 |
|
wenzelm@20821
|
221 |
fun exists_name name (thy as Theory ({id, ids, iids, ...}, _, _, _)) =
|
wenzelm@20821
|
222 |
name = theory_name thy orelse
|
wenzelm@16489
|
223 |
name = #2 id orelse
|
wenzelm@16489
|
224 |
Inttab.exists (equal name o #2) ids orelse
|
wenzelm@16489
|
225 |
Inttab.exists (equal name o #2) iids;
|
wenzelm@16436
|
226 |
|
wenzelm@16489
|
227 |
fun names_of (Theory ({id, ids, iids, ...}, _, _, _)) =
|
wenzelm@16489
|
228 |
rev (#2 id :: Inttab.fold (cons o #2) iids (Inttab.fold (cons o #2) ids []));
|
wenzelm@16436
|
229 |
|
wenzelm@16436
|
230 |
fun pretty_thy thy =
|
wenzelm@16436
|
231 |
Pretty.str_list "{" "}" (names_of thy @ (if is_stale thy then ["!"] else []));
|
wenzelm@16436
|
232 |
|
wenzelm@16436
|
233 |
val string_of_thy = Pretty.string_of o pretty_thy;
|
wenzelm@16436
|
234 |
val pprint_thy = Pretty.pprint o pretty_thy;
|
wenzelm@16436
|
235 |
|
wenzelm@16436
|
236 |
fun pretty_abbrev_thy thy =
|
wenzelm@16436
|
237 |
let
|
wenzelm@16436
|
238 |
val names = names_of thy;
|
wenzelm@16436
|
239 |
val n = length names;
|
wenzelm@16436
|
240 |
val abbrev = if n > 5 then "..." :: List.drop (names, n - 5) else names;
|
wenzelm@16436
|
241 |
in Pretty.str_list "{" "}" abbrev end;
|
wenzelm@16436
|
242 |
|
wenzelm@16436
|
243 |
val str_of_thy = Pretty.str_of o pretty_abbrev_thy;
|
wenzelm@16436
|
244 |
|
wenzelm@16436
|
245 |
|
wenzelm@16533
|
246 |
(* consistency *) (*exception TERM*)
|
wenzelm@16436
|
247 |
|
wenzelm@16719
|
248 |
fun check_thy thy =
|
wenzelm@16436
|
249 |
if is_stale thy then
|
wenzelm@16719
|
250 |
raise TERM ("Stale theory encountered:\n" ^ string_of_thy thy, [])
|
wenzelm@16436
|
251 |
else thy;
|
wenzelm@16436
|
252 |
|
wenzelm@16489
|
253 |
fun check_ins id ids =
|
wenzelm@16894
|
254 |
if draft_id id orelse Inttab.defined ids (#1 id) then ids
|
wenzelm@16436
|
255 |
else if Inttab.exists (equal (#2 id) o #2) ids then
|
wenzelm@16436
|
256 |
raise TERM ("Different versions of theory component " ^ quote (#2 id), [])
|
wenzelm@17412
|
257 |
else Inttab.update id ids;
|
wenzelm@16436
|
258 |
|
wenzelm@16489
|
259 |
fun check_insert intermediate id (ids, iids) =
|
wenzelm@16489
|
260 |
let val ids' = check_ins id ids and iids' = check_ins id iids
|
wenzelm@16489
|
261 |
in if intermediate then (ids, iids') else (ids', iids) end;
|
wenzelm@16436
|
262 |
|
wenzelm@16489
|
263 |
fun check_merge
|
wenzelm@16489
|
264 |
(Theory ({id = id1, ids = ids1, iids = iids1, ...}, _, _, history1))
|
wenzelm@16489
|
265 |
(Theory ({id = id2, ids = ids2, iids = iids2, ...}, _, _, history2)) =
|
wenzelm@16489
|
266 |
(Inttab.fold check_ins ids2 ids1, Inttab.fold check_ins iids2 iids1)
|
wenzelm@16489
|
267 |
|> check_insert (#version history1 > 0) id1
|
wenzelm@16489
|
268 |
|> check_insert (#version history2 > 0) id2;
|
wenzelm@16436
|
269 |
|
wenzelm@16489
|
270 |
|
wenzelm@16533
|
271 |
(* equality and inclusion *)
|
wenzelm@16533
|
272 |
|
wenzelm@16719
|
273 |
val eq_thy = eq_id o pairself (#id o identity_of o check_thy);
|
wenzelm@16533
|
274 |
|
wenzelm@16533
|
275 |
fun proper_subthy
|
wenzelm@16719
|
276 |
(Theory ({id = (i, _), ...}, _, _, _), Theory ({ids, iids, ...}, _, _, _)) =
|
wenzelm@16894
|
277 |
Inttab.defined ids i orelse Inttab.defined iids i;
|
wenzelm@16533
|
278 |
|
wenzelm@16533
|
279 |
fun subthy thys = eq_thy thys orelse proper_subthy thys;
|
wenzelm@16533
|
280 |
|
wenzelm@16594
|
281 |
fun joinable (thy1, thy2) = subthy (thy1, thy2) orelse subthy (thy2, thy1);
|
wenzelm@16594
|
282 |
|
wenzelm@16533
|
283 |
|
wenzelm@16489
|
284 |
(* theory references *)
|
wenzelm@16489
|
285 |
|
wenzelm@16489
|
286 |
(*theory_ref provides a safe way to store dynamic references to a
|
wenzelm@16533
|
287 |
theory in external data structures -- a plain theory value would
|
wenzelm@16533
|
288 |
become stale as the self reference moves on*)
|
wenzelm@16489
|
289 |
|
wenzelm@16489
|
290 |
datatype theory_ref = TheoryRef of theory ref;
|
wenzelm@16489
|
291 |
|
wenzelm@16719
|
292 |
val self_ref = TheoryRef o the_self o check_thy;
|
wenzelm@16489
|
293 |
fun deref (TheoryRef (ref thy)) = thy;
|
wenzelm@16489
|
294 |
|
wenzelm@16489
|
295 |
|
wenzelm@16533
|
296 |
(* trivial merge *) (*exception TERM*)
|
wenzelm@16436
|
297 |
|
wenzelm@16436
|
298 |
fun merge (thy1, thy2) =
|
wenzelm@16719
|
299 |
if eq_thy (thy1, thy2) then thy1
|
wenzelm@16719
|
300 |
else if proper_subthy (thy2, thy1) then thy1
|
wenzelm@16719
|
301 |
else if proper_subthy (thy1, thy2) then thy2
|
wenzelm@16436
|
302 |
else (check_merge thy1 thy2;
|
wenzelm@16436
|
303 |
raise TERM (cat_lines ["Attempt to perform non-trivial merge of theories:",
|
wenzelm@16436
|
304 |
str_of_thy thy1, str_of_thy thy2], []));
|
wenzelm@16436
|
305 |
|
wenzelm@16719
|
306 |
fun merge_refs (ref1, ref2) =
|
wenzelm@16719
|
307 |
if ref1 = ref2 then ref1
|
wenzelm@16719
|
308 |
else self_ref (merge (deref ref1, deref ref2));
|
wenzelm@16436
|
309 |
|
wenzelm@16436
|
310 |
|
wenzelm@16436
|
311 |
|
wenzelm@16489
|
312 |
(** build theories **)
|
wenzelm@16489
|
313 |
|
wenzelm@16489
|
314 |
(* primitives *)
|
wenzelm@16489
|
315 |
|
wenzelm@16489
|
316 |
fun create_thy name self id ids iids data ancestry history =
|
wenzelm@16489
|
317 |
let
|
wenzelm@17756
|
318 |
val {version, name = _, intermediates = _} = history;
|
wenzelm@17756
|
319 |
val intermediate = version > 0;
|
wenzelm@16489
|
320 |
val (ids', iids') = check_insert intermediate id (ids, iids);
|
wenzelm@16489
|
321 |
val id' = (serial (), name);
|
wenzelm@16489
|
322 |
val _ = check_insert intermediate id' (ids', iids');
|
wenzelm@16489
|
323 |
val identity' = make_identity self id' ids' iids';
|
wenzelm@16489
|
324 |
in vitalize (Theory (identity', data, ancestry, history)) end;
|
wenzelm@16489
|
325 |
|
wenzelm@16489
|
326 |
fun change_thy name f (thy as Theory ({self, id, ids, iids}, data, ancestry, history)) =
|
wenzelm@16489
|
327 |
let
|
wenzelm@16719
|
328 |
val _ = check_thy thy;
|
wenzelm@16489
|
329 |
val (self', data', ancestry') =
|
wenzelm@16489
|
330 |
if is_draft thy then (self, data, ancestry) (*destructive change!*)
|
wenzelm@16489
|
331 |
else if #version history > 0
|
wenzelm@18731
|
332 |
then (NONE, map_theory_data copy_data data, ancestry)
|
wenzelm@18731
|
333 |
else (NONE, map_theory_data extend_data data,
|
wenzelm@18731
|
334 |
make_ancestry [thy] (thy :: #ancestors ancestry));
|
wenzelm@16489
|
335 |
val data'' = f data';
|
wenzelm@16489
|
336 |
in create_thy name self' id ids iids data'' ancestry' history end;
|
wenzelm@16489
|
337 |
|
wenzelm@16489
|
338 |
fun name_thy name = change_thy name I;
|
wenzelm@16489
|
339 |
val modify_thy = change_thy draftN;
|
wenzelm@16489
|
340 |
val extend_thy = modify_thy I;
|
wenzelm@16489
|
341 |
|
wenzelm@16489
|
342 |
fun copy_thy (thy as Theory ({id, ids, iids, ...}, data, ancestry, history)) =
|
wenzelm@16719
|
343 |
(check_thy thy;
|
wenzelm@18731
|
344 |
create_thy draftN NONE id ids iids (map_theory_data copy_data data) ancestry history);
|
wenzelm@16489
|
345 |
|
wenzelm@16489
|
346 |
val pre_pure_thy = create_thy draftN NONE (serial (), draftN) Inttab.empty Inttab.empty
|
wenzelm@19028
|
347 |
(make_data Datatab.empty Datatab.empty) (make_ancestry [] []) (make_history ProtoPureN 0 []);
|
wenzelm@16489
|
348 |
|
wenzelm@16489
|
349 |
|
wenzelm@16489
|
350 |
(* named theory nodes *)
|
wenzelm@16489
|
351 |
|
wenzelm@16489
|
352 |
fun merge_thys pp (thy1, thy2) =
|
wenzelm@16533
|
353 |
if exists_name CPureN thy1 <> exists_name CPureN thy2 then
|
wenzelm@16436
|
354 |
error "Cannot merge Pure and CPure developments"
|
wenzelm@16436
|
355 |
else
|
wenzelm@16436
|
356 |
let
|
wenzelm@16489
|
357 |
val (ids, iids) = check_merge thy1 thy2;
|
wenzelm@16533
|
358 |
val data1 = data_of thy1 and data2 = data_of thy2;
|
wenzelm@16533
|
359 |
val data = make_data
|
wenzelm@16533
|
360 |
(merge_data (pp thy1) (#theory data1, #theory data2))
|
wenzelm@19028
|
361 |
(Datatab.merge (K true) (#proof data1, #proof data2));
|
wenzelm@16489
|
362 |
val ancestry = make_ancestry [] [];
|
wenzelm@16436
|
363 |
val history = make_history "" 0 [];
|
wenzelm@16489
|
364 |
in create_thy draftN NONE (serial (), draftN) ids iids data ancestry history end;
|
wenzelm@16436
|
365 |
|
wenzelm@16533
|
366 |
fun maximal_thys thys =
|
wenzelm@16533
|
367 |
thys |> filter (fn thy => not (exists (fn thy' => proper_subthy (thy, thy')) thys));
|
wenzelm@16533
|
368 |
|
wenzelm@16489
|
369 |
fun begin_thy pp name imports =
|
wenzelm@16489
|
370 |
if name = draftN then error ("Illegal theory name: " ^ quote draftN)
|
wenzelm@16436
|
371 |
else
|
wenzelm@16436
|
372 |
let
|
wenzelm@16533
|
373 |
val parents =
|
wenzelm@19046
|
374 |
maximal_thys (distinct eq_thy (map check_thy imports));
|
wenzelm@19482
|
375 |
val ancestors = distinct eq_thy (parents @ maps ancestors_of parents);
|
wenzelm@16489
|
376 |
val Theory ({id, ids, iids, ...}, data, _, _) =
|
wenzelm@16436
|
377 |
(case parents of
|
wenzelm@16436
|
378 |
[] => error "No parent theories"
|
wenzelm@16533
|
379 |
| [thy] => extend_thy thy
|
wenzelm@16533
|
380 |
| thy :: thys => Library.foldl (merge_thys pp) (thy, thys));
|
wenzelm@16489
|
381 |
val ancestry = make_ancestry parents ancestors;
|
wenzelm@16436
|
382 |
val history = make_history name 0 [];
|
wenzelm@16489
|
383 |
in create_thy draftN NONE id ids iids data ancestry history end;
|
wenzelm@16436
|
384 |
|
wenzelm@16436
|
385 |
|
wenzelm@16489
|
386 |
(* undoable checkpoints *)
|
wenzelm@16436
|
387 |
|
wenzelm@16489
|
388 |
fun checkpoint_thy thy =
|
wenzelm@16489
|
389 |
if not (is_draft thy) then thy
|
wenzelm@16489
|
390 |
else
|
wenzelm@16489
|
391 |
let
|
wenzelm@16489
|
392 |
val {name, version, intermediates} = history_of thy;
|
wenzelm@16489
|
393 |
val thy' as Theory (identity', data', ancestry', _) =
|
wenzelm@16489
|
394 |
name_thy (name ^ ":" ^ string_of_int version) thy;
|
wenzelm@16489
|
395 |
val history' = make_history name (version + 1) (thy' :: intermediates);
|
wenzelm@16489
|
396 |
in vitalize (Theory (identity', data', ancestry', history')) end;
|
wenzelm@16436
|
397 |
|
wenzelm@16489
|
398 |
fun finish_thy thy =
|
wenzelm@16489
|
399 |
let
|
wenzelm@16489
|
400 |
val {name, version, intermediates} = history_of thy;
|
wenzelm@16719
|
401 |
val rs = map (the_self o check_thy) intermediates;
|
wenzelm@16489
|
402 |
val thy' as Theory ({self, id, ids, ...}, data', ancestry', _) = name_thy name thy;
|
wenzelm@16489
|
403 |
val identity' = make_identity self id ids Inttab.empty;
|
wenzelm@16489
|
404 |
val history' = make_history name 0 [];
|
wenzelm@16489
|
405 |
val thy'' = vitalize (Theory (identity', data', ancestry', history'));
|
wenzelm@16533
|
406 |
val _ = List.app (fn r => r := thy'') rs;
|
wenzelm@16533
|
407 |
in thy'' end;
|
wenzelm@16436
|
408 |
|
wenzelm@22131
|
409 |
fun is_finished_thy thy =
|
wenzelm@22131
|
410 |
(check_thy thy; not (is_draft thy) andalso #version (history_of thy) = 0);
|
wenzelm@22131
|
411 |
|
wenzelm@16489
|
412 |
|
wenzelm@16489
|
413 |
(* theory data *)
|
wenzelm@16489
|
414 |
|
wenzelm@16533
|
415 |
fun dest_data name_of tab =
|
wenzelm@19028
|
416 |
map name_of (Datatab.keys tab)
|
wenzelm@18931
|
417 |
|> map (rpair ()) |> Symtab.make_list |> Symtab.dest
|
wenzelm@16489
|
418 |
|> map (apsnd length)
|
wenzelm@16489
|
419 |
|> map (fn (name, 1) => name | (name, n) => name ^ enclose "[" "]" (string_of_int n));
|
wenzelm@16489
|
420 |
|
wenzelm@16533
|
421 |
val theory_data_of = dest_data invoke_name o #theory o data_of;
|
wenzelm@16533
|
422 |
|
wenzelm@16489
|
423 |
structure TheoryData =
|
wenzelm@16489
|
424 |
struct
|
wenzelm@16489
|
425 |
|
wenzelm@16489
|
426 |
val declare = declare_theory_data;
|
wenzelm@16489
|
427 |
|
wenzelm@16489
|
428 |
fun get k dest thy =
|
wenzelm@19028
|
429 |
(case Datatab.lookup (#theory (data_of thy)) k of
|
wenzelm@16489
|
430 |
SOME x => (dest x handle Match =>
|
wenzelm@16489
|
431 |
error ("Failed to access theory data " ^ quote (invoke_name k)))
|
wenzelm@16489
|
432 |
| NONE => error ("Uninitialized theory data " ^ quote (invoke_name k)));
|
wenzelm@16489
|
433 |
|
wenzelm@19028
|
434 |
fun put k mk x = modify_thy (map_theory_data (Datatab.update (k, mk x)));
|
wenzelm@16489
|
435 |
fun init k = put k I (invoke_empty k);
|
wenzelm@16489
|
436 |
|
wenzelm@16489
|
437 |
end;
|
wenzelm@16489
|
438 |
|
wenzelm@16489
|
439 |
|
wenzelm@16489
|
440 |
|
wenzelm@16533
|
441 |
(*** proof context ***)
|
wenzelm@16533
|
442 |
|
wenzelm@16533
|
443 |
(* datatype proof *)
|
wenzelm@16533
|
444 |
|
wenzelm@19028
|
445 |
datatype proof = Proof of theory_ref * Object.T Datatab.table;
|
wenzelm@16533
|
446 |
|
wenzelm@17060
|
447 |
fun theory_of_proof (Proof (thy_ref, _)) = deref thy_ref;
|
wenzelm@16533
|
448 |
fun data_of_proof (Proof (_, data)) = data;
|
wenzelm@17060
|
449 |
fun map_prf f (Proof (thy_ref, data)) = Proof (thy_ref, f data);
|
wenzelm@17060
|
450 |
|
wenzelm@17060
|
451 |
fun transfer_proof thy' (prf as Proof (thy_ref, data)) =
|
wenzelm@17060
|
452 |
if not (subthy (deref thy_ref, thy')) then
|
haftmann@19815
|
453 |
error "transfer proof context: not a super theory"
|
wenzelm@17060
|
454 |
else Proof (self_ref thy', data);
|
wenzelm@16533
|
455 |
|
wenzelm@16533
|
456 |
|
wenzelm@16533
|
457 |
(* proof data kinds *)
|
wenzelm@16533
|
458 |
|
wenzelm@16533
|
459 |
local
|
wenzelm@16533
|
460 |
|
wenzelm@16533
|
461 |
type kind =
|
wenzelm@16533
|
462 |
{name: string,
|
wenzelm@16533
|
463 |
init: theory -> Object.T};
|
wenzelm@16533
|
464 |
|
wenzelm@19028
|
465 |
val kinds = ref (Datatab.empty: kind Datatab.table);
|
wenzelm@16533
|
466 |
|
wenzelm@16533
|
467 |
fun invoke meth_name meth_fn k =
|
wenzelm@19028
|
468 |
(case Datatab.lookup (! kinds) k of
|
wenzelm@16533
|
469 |
SOME kind => meth_fn kind |> transform_failure (fn exn =>
|
wenzelm@17340
|
470 |
EXCEPTION (exn, "Proof data method " ^ #name kind ^ "." ^ meth_name ^ " failed"))
|
wenzelm@16533
|
471 |
| NONE => sys_error ("Invalid proof data identifier " ^ string_of_int k));
|
wenzelm@16533
|
472 |
|
wenzelm@16533
|
473 |
fun invoke_name k = invoke "name" (K o #name) k ();
|
wenzelm@16533
|
474 |
val invoke_init = invoke "init" #init;
|
wenzelm@16533
|
475 |
|
wenzelm@16533
|
476 |
in
|
wenzelm@16533
|
477 |
|
wenzelm@16533
|
478 |
val proof_data_of = dest_data invoke_name o #proof o data_of;
|
wenzelm@16533
|
479 |
|
wenzelm@16533
|
480 |
fun init_proof thy =
|
wenzelm@19028
|
481 |
Proof (self_ref thy, Datatab.map' (fn k => fn _ => invoke_init k thy) (#proof (data_of thy)));
|
wenzelm@16533
|
482 |
|
wenzelm@16533
|
483 |
structure ProofData =
|
wenzelm@16533
|
484 |
struct
|
wenzelm@16533
|
485 |
|
wenzelm@16533
|
486 |
fun declare name init =
|
wenzelm@16533
|
487 |
let
|
wenzelm@16533
|
488 |
val k = serial ();
|
wenzelm@16533
|
489 |
val kind = {name = name, init = init};
|
wenzelm@21962
|
490 |
val _ =
|
wenzelm@21962
|
491 |
if Datatab.exists (equal name o #name o #2) (! kinds) then
|
wenzelm@21962
|
492 |
warning ("Duplicate declaration of proof data " ^ quote name)
|
wenzelm@21962
|
493 |
else ();
|
wenzelm@19028
|
494 |
val _ = change kinds (Datatab.update (k, kind));
|
wenzelm@16533
|
495 |
in k end;
|
wenzelm@16533
|
496 |
|
wenzelm@19028
|
497 |
fun init k = modify_thy (map_proof_data (Datatab.update (k, ())));
|
wenzelm@16533
|
498 |
|
wenzelm@16533
|
499 |
fun get k dest prf =
|
wenzelm@19028
|
500 |
(case Datatab.lookup (data_of_proof prf) k of
|
wenzelm@16533
|
501 |
SOME x => (dest x handle Match =>
|
wenzelm@16533
|
502 |
error ("Failed to access proof data " ^ quote (invoke_name k)))
|
wenzelm@16533
|
503 |
| NONE => error ("Uninitialized proof data " ^ quote (invoke_name k)));
|
wenzelm@16533
|
504 |
|
wenzelm@19028
|
505 |
fun put k mk x = map_prf (Datatab.update (k, mk x));
|
wenzelm@16533
|
506 |
|
wenzelm@16533
|
507 |
end;
|
wenzelm@16533
|
508 |
|
wenzelm@16533
|
509 |
end;
|
wenzelm@16533
|
510 |
|
wenzelm@16533
|
511 |
|
wenzelm@18632
|
512 |
|
wenzelm@16533
|
513 |
(*** generic context ***)
|
wenzelm@16533
|
514 |
|
wenzelm@18632
|
515 |
datatype generic = Theory of theory | Proof of proof;
|
wenzelm@16533
|
516 |
|
wenzelm@18632
|
517 |
fun cases f _ (Theory thy) = f thy
|
wenzelm@18632
|
518 |
| cases _ g (Proof prf) = g prf;
|
wenzelm@16533
|
519 |
|
wenzelm@19678
|
520 |
fun mapping f g = cases (Theory o f) (Proof o g);
|
wenzelm@21660
|
521 |
fun mapping_result f g = cases (apsnd Theory o f) (apsnd Proof o g);
|
wenzelm@19678
|
522 |
|
wenzelm@18731
|
523 |
val the_theory = cases I (fn _ => raise Fail "Ill-typed context: theory expected");
|
wenzelm@18731
|
524 |
val the_proof = cases (fn _ => raise Fail "Ill-typed context: proof expected") I;
|
wenzelm@18632
|
525 |
|
wenzelm@18731
|
526 |
fun map_theory f = Theory o f o the_theory;
|
wenzelm@18731
|
527 |
fun map_proof f = Proof o f o the_proof;
|
wenzelm@18731
|
528 |
|
wenzelm@18731
|
529 |
fun theory_map f = the_theory o f o Theory;
|
wenzelm@18731
|
530 |
fun proof_map f = the_proof o f o Proof;
|
wenzelm@18665
|
531 |
|
wenzelm@18632
|
532 |
val theory_of = cases I theory_of_proof;
|
wenzelm@18632
|
533 |
val proof_of = cases init_proof I;
|
wenzelm@16533
|
534 |
|
wenzelm@22085
|
535 |
|
wenzelm@22085
|
536 |
|
wenzelm@22095
|
537 |
(** delayed theory setup **)
|
wenzelm@22085
|
538 |
|
wenzelm@22085
|
539 |
local
|
wenzelm@22085
|
540 |
val setup_fn = ref (I: theory -> theory);
|
wenzelm@22085
|
541 |
in
|
wenzelm@22085
|
542 |
fun add_setup f = setup_fn := (! setup_fn #> f);
|
wenzelm@22085
|
543 |
fun setup () = let val f = ! setup_fn in setup_fn := I; f end;
|
wenzelm@22085
|
544 |
end;
|
wenzelm@22085
|
545 |
|
wenzelm@6185
|
546 |
end;
|
wenzelm@6185
|
547 |
|
wenzelm@6185
|
548 |
structure BasicContext: BASIC_CONTEXT = Context;
|
wenzelm@6185
|
549 |
open BasicContext;
|
wenzelm@16436
|
550 |
|
wenzelm@16436
|
551 |
|
wenzelm@16436
|
552 |
|
wenzelm@16533
|
553 |
(*** type-safe interfaces for data declarations ***)
|
wenzelm@16533
|
554 |
|
wenzelm@16533
|
555 |
(** theory data **)
|
wenzelm@16436
|
556 |
|
wenzelm@16436
|
557 |
signature THEORY_DATA_ARGS =
|
wenzelm@16436
|
558 |
sig
|
wenzelm@16436
|
559 |
val name: string
|
wenzelm@16436
|
560 |
type T
|
wenzelm@16436
|
561 |
val empty: T
|
wenzelm@16436
|
562 |
val copy: T -> T
|
wenzelm@16436
|
563 |
val extend: T -> T
|
wenzelm@16436
|
564 |
val merge: Pretty.pp -> T * T -> T
|
wenzelm@16436
|
565 |
val print: theory -> T -> unit
|
wenzelm@16436
|
566 |
end;
|
wenzelm@16436
|
567 |
|
wenzelm@16436
|
568 |
signature THEORY_DATA =
|
wenzelm@16436
|
569 |
sig
|
wenzelm@16436
|
570 |
type T
|
wenzelm@16436
|
571 |
val init: theory -> theory
|
wenzelm@16436
|
572 |
val print: theory -> unit
|
wenzelm@16436
|
573 |
val get: theory -> T
|
wenzelm@16489
|
574 |
val get_sg: theory -> T (*obsolete*)
|
wenzelm@16436
|
575 |
val put: T -> theory -> theory
|
wenzelm@16436
|
576 |
val map: (T -> T) -> theory -> theory
|
wenzelm@16436
|
577 |
end;
|
wenzelm@16436
|
578 |
|
wenzelm@16436
|
579 |
functor TheoryDataFun(Data: THEORY_DATA_ARGS): THEORY_DATA =
|
wenzelm@16436
|
580 |
struct
|
wenzelm@16436
|
581 |
|
wenzelm@16436
|
582 |
structure TheoryData = Context.TheoryData;
|
wenzelm@16436
|
583 |
|
wenzelm@16436
|
584 |
type T = Data.T;
|
wenzelm@16436
|
585 |
exception Data of T;
|
wenzelm@16436
|
586 |
|
wenzelm@16436
|
587 |
val kind = TheoryData.declare Data.name
|
wenzelm@16436
|
588 |
(Data Data.empty)
|
wenzelm@16436
|
589 |
(fn Data x => Data (Data.copy x))
|
wenzelm@16436
|
590 |
(fn Data x => Data (Data.extend x))
|
wenzelm@16489
|
591 |
(fn pp => fn (Data x1, Data x2) => Data (Data.merge pp (x1, x2)));
|
wenzelm@16436
|
592 |
|
wenzelm@16436
|
593 |
val init = TheoryData.init kind;
|
wenzelm@16436
|
594 |
val get = TheoryData.get kind (fn Data x => x);
|
wenzelm@16489
|
595 |
val get_sg = get;
|
wenzelm@16489
|
596 |
fun print thy = Data.print thy (get thy);
|
wenzelm@16436
|
597 |
val put = TheoryData.put kind Data;
|
wenzelm@16436
|
598 |
fun map f thy = put (f (get thy)) thy;
|
wenzelm@16436
|
599 |
|
wenzelm@16436
|
600 |
end;
|
wenzelm@16436
|
601 |
|
wenzelm@16533
|
602 |
|
wenzelm@16533
|
603 |
|
wenzelm@16533
|
604 |
(** proof data **)
|
wenzelm@16533
|
605 |
|
wenzelm@16533
|
606 |
signature PROOF_DATA_ARGS =
|
wenzelm@16533
|
607 |
sig
|
wenzelm@16533
|
608 |
val name: string
|
wenzelm@16533
|
609 |
type T
|
wenzelm@16533
|
610 |
val init: theory -> T
|
wenzelm@16533
|
611 |
val print: Context.proof -> T -> unit
|
wenzelm@16533
|
612 |
end;
|
wenzelm@16533
|
613 |
|
wenzelm@16533
|
614 |
signature PROOF_DATA =
|
wenzelm@16533
|
615 |
sig
|
wenzelm@16533
|
616 |
type T
|
wenzelm@16533
|
617 |
val init: theory -> theory
|
wenzelm@16533
|
618 |
val print: Context.proof -> unit
|
wenzelm@16533
|
619 |
val get: Context.proof -> T
|
wenzelm@16533
|
620 |
val put: T -> Context.proof -> Context.proof
|
wenzelm@16533
|
621 |
val map: (T -> T) -> Context.proof -> Context.proof
|
wenzelm@16533
|
622 |
end;
|
wenzelm@16533
|
623 |
|
wenzelm@16533
|
624 |
functor ProofDataFun(Data: PROOF_DATA_ARGS): PROOF_DATA =
|
wenzelm@16533
|
625 |
struct
|
wenzelm@16533
|
626 |
|
wenzelm@16533
|
627 |
structure ProofData = Context.ProofData;
|
wenzelm@16533
|
628 |
|
wenzelm@16533
|
629 |
type T = Data.T;
|
wenzelm@16533
|
630 |
exception Data of T;
|
wenzelm@16533
|
631 |
|
wenzelm@16533
|
632 |
val kind = ProofData.declare Data.name (Data o Data.init);
|
wenzelm@16533
|
633 |
|
wenzelm@16533
|
634 |
val init = ProofData.init kind;
|
wenzelm@16533
|
635 |
val get = ProofData.get kind (fn Data x => x);
|
wenzelm@16533
|
636 |
fun print prf = Data.print prf (get prf);
|
wenzelm@16533
|
637 |
val put = ProofData.put kind Data;
|
wenzelm@16533
|
638 |
fun map f prf = put (f (get prf)) prf;
|
wenzelm@16533
|
639 |
|
wenzelm@16533
|
640 |
end;
|
wenzelm@16533
|
641 |
|
wenzelm@18632
|
642 |
|
wenzelm@18632
|
643 |
|
wenzelm@18632
|
644 |
(** generic data **)
|
wenzelm@18632
|
645 |
|
wenzelm@18632
|
646 |
signature GENERIC_DATA_ARGS =
|
wenzelm@18632
|
647 |
sig
|
wenzelm@18632
|
648 |
val name: string
|
wenzelm@18632
|
649 |
type T
|
wenzelm@18632
|
650 |
val empty: T
|
wenzelm@18632
|
651 |
val extend: T -> T
|
wenzelm@18632
|
652 |
val merge: Pretty.pp -> T * T -> T
|
wenzelm@18632
|
653 |
val print: Context.generic -> T -> unit
|
wenzelm@18632
|
654 |
end;
|
wenzelm@18632
|
655 |
|
wenzelm@18632
|
656 |
signature GENERIC_DATA =
|
wenzelm@18632
|
657 |
sig
|
wenzelm@18632
|
658 |
type T
|
wenzelm@18632
|
659 |
val init: theory -> theory
|
wenzelm@18632
|
660 |
val get: Context.generic -> T
|
wenzelm@18632
|
661 |
val put: T -> Context.generic -> Context.generic
|
wenzelm@18632
|
662 |
val map: (T -> T) -> Context.generic -> Context.generic
|
wenzelm@18632
|
663 |
val print: Context.generic -> unit
|
wenzelm@18632
|
664 |
end;
|
wenzelm@18632
|
665 |
|
wenzelm@18632
|
666 |
functor GenericDataFun(Data: GENERIC_DATA_ARGS): GENERIC_DATA =
|
wenzelm@18632
|
667 |
struct
|
wenzelm@18632
|
668 |
|
wenzelm@18632
|
669 |
structure ThyData = TheoryDataFun(open Data val copy = I fun print _ _ = ());
|
wenzelm@18632
|
670 |
structure PrfData =
|
wenzelm@18632
|
671 |
ProofDataFun(val name = Data.name type T = Data.T val init = ThyData.get fun print _ _ = ());
|
wenzelm@18632
|
672 |
|
wenzelm@18632
|
673 |
type T = Data.T;
|
wenzelm@18632
|
674 |
val init = ThyData.init #> PrfData.init;
|
wenzelm@18632
|
675 |
|
wenzelm@18632
|
676 |
fun get (Context.Theory thy) = ThyData.get thy
|
wenzelm@18632
|
677 |
| get (Context.Proof prf) = PrfData.get prf;
|
wenzelm@18632
|
678 |
|
wenzelm@18632
|
679 |
fun put x (Context.Theory thy) = Context.Theory (ThyData.put x thy)
|
wenzelm@18632
|
680 |
| put x (Context.Proof prf) = Context.Proof (PrfData.put x prf);
|
wenzelm@18632
|
681 |
|
wenzelm@18632
|
682 |
fun map f ctxt = put (f (get ctxt)) ctxt;
|
wenzelm@18632
|
683 |
|
wenzelm@18632
|
684 |
fun print ctxt = Data.print ctxt (get ctxt);
|
wenzelm@18632
|
685 |
|
wenzelm@18632
|
686 |
end;
|
wenzelm@18632
|
687 |
|
wenzelm@18632
|
688 |
|
wenzelm@16533
|
689 |
(*hide private interface*)
|
wenzelm@16436
|
690 |
structure Context: CONTEXT = Context;
|
wenzelm@20297
|
691 |
|
wenzelm@21518
|
692 |
(*fake predeclarations*)
|
wenzelm@20297
|
693 |
structure Proof = struct type context = Context.proof end;
|
wenzelm@21518
|
694 |
structure ProofContext =
|
wenzelm@21518
|
695 |
struct val theory_of = Context.theory_of_proof val init = Context.init_proof end;
|