48 val thm_ord: pthm * pthm -> order |
48 val thm_ord: pthm * pthm -> order |
49 val unions_oracles: oracle Ord_List.T list -> oracle Ord_List.T |
49 val unions_oracles: oracle Ord_List.T list -> oracle Ord_List.T |
50 val unions_thms: pthm Ord_List.T list -> pthm Ord_List.T |
50 val unions_thms: pthm Ord_List.T list -> pthm Ord_List.T |
51 val all_oracles_of: proof_body -> oracle Ord_List.T |
51 val all_oracles_of: proof_body -> oracle Ord_List.T |
52 val approximate_proof_body: proof -> proof_body |
52 val approximate_proof_body: proof -> proof_body |
|
53 val no_proof_body: proof_body |
|
54 val no_thm_proofs: proof -> proof |
|
55 |
|
56 val encode: proof XML.Encode.T |
|
57 val encode_body: proof_body XML.Encode.T |
|
58 val decode: proof XML.Decode.T |
|
59 val decode_body: proof_body XML.Decode.T |
53 |
60 |
54 (** primitive operations **) |
61 (** primitive operations **) |
55 val proofs_enabled: unit -> bool |
62 val proofs_enabled: unit -> bool |
56 val proof_combt: proof * term list -> proof |
63 val proof_combt: proof * term list -> proof |
57 val proof_combt': proof * term option list -> proof |
64 val proof_combt': proof * term option list -> proof |
262 PBody |
269 PBody |
263 {oracles = Ord_List.make oracle_ord oracles, |
270 {oracles = Ord_List.make oracle_ord oracles, |
264 thms = Ord_List.make thm_ord thms, |
271 thms = Ord_List.make thm_ord thms, |
265 proof = prf} |
272 proof = prf} |
266 end; |
273 end; |
|
274 |
|
275 val no_proof_body = PBody {oracles = [], thms = [], proof = MinProof}; |
|
276 val no_body = Future.value no_proof_body; |
|
277 |
|
278 fun no_thm_proofs (PThm (i, (a, _))) = PThm (i, (a, no_body)) |
|
279 | no_thm_proofs (Abst (x, T, prf)) = Abst (x, T, no_thm_proofs prf) |
|
280 | no_thm_proofs (AbsP (x, t, prf)) = AbsP (x, t, no_thm_proofs prf) |
|
281 | no_thm_proofs (prf % t) = no_thm_proofs prf % t |
|
282 | no_thm_proofs (prf1 %% prf2) = no_thm_proofs prf1 %% no_thm_proofs prf2 |
|
283 | no_thm_proofs a = a; |
|
284 |
|
285 |
|
286 (***** XML data representation *****) |
|
287 |
|
288 (* encode *) |
|
289 |
|
290 local |
|
291 |
|
292 open XML.Encode Term_XML.Encode; |
|
293 |
|
294 fun proof prf = prf |> variant |
|
295 [fn MinProof => ([], []), |
|
296 fn PBound a => ([int_atom a], []), |
|
297 fn Abst (a, b, c) => ([a], pair (option typ) proof (b, c)), |
|
298 fn AbsP (a, b, c) => ([a], pair (option term) proof (b, c)), |
|
299 fn a % b => ([], pair proof (option term) (a, b)), |
|
300 fn a %% b => ([], pair proof proof (a, b)), |
|
301 fn Hyp a => ([], term a), |
|
302 fn PAxm (a, b, c) => ([a], pair term (option (list typ)) (b, c)), |
|
303 fn OfClass (a, b) => ([b], typ a), |
|
304 fn Oracle (a, b, c) => ([a], pair term (option (list typ)) (b, c)), |
|
305 fn Promise (a, b, c) => ([int_atom a], pair term (list typ) (b, c)), |
|
306 fn PThm (a, ((b, c, d), body)) => |
|
307 ([int_atom a, b], triple term (option (list typ)) proof_body (c, d, Future.join body))] |
|
308 and proof_body (PBody {oracles, thms, proof = prf}) = |
|
309 triple (list (pair string term)) (list pthm) proof (oracles, thms, prf) |
|
310 and pthm (a, (b, c, body)) = |
|
311 pair int (triple string term proof_body) (a, (b, c, Future.join body)); |
|
312 |
|
313 in |
|
314 |
|
315 val encode = proof; |
|
316 val encode_body = proof_body; |
|
317 |
|
318 end; |
|
319 |
|
320 |
|
321 (* decode *) |
|
322 |
|
323 local |
|
324 |
|
325 open XML.Decode Term_XML.Decode; |
|
326 |
|
327 fun proof prf = prf |> variant |
|
328 [fn ([], []) => MinProof, |
|
329 fn ([a], []) => PBound (int_atom a), |
|
330 fn ([a], b) => let val (c, d) = pair (option typ) proof b in Abst (a, c, d) end, |
|
331 fn ([a], b) => let val (c, d) = pair (option term) proof b in AbsP (a, c, d) end, |
|
332 fn ([], a) => op % (pair proof (option term) a), |
|
333 fn ([], a) => op %% (pair proof proof a), |
|
334 fn ([], a) => Hyp (term a), |
|
335 fn ([a], b) => let val (c, d) = pair term (option (list typ)) b in PAxm (a, c, d) end, |
|
336 fn ([b], a) => OfClass (typ a, b), |
|
337 fn ([a], b) => let val (c, d) = pair term (option (list typ)) b in Oracle (a, c, d) end, |
|
338 fn ([a], b) => let val (c, d) = pair term (list typ) b in Promise (int_atom a, c, d) end, |
|
339 fn ([a, b], c) => |
|
340 let val (d, e, f) = triple term (option (list typ)) proof_body c |
|
341 in PThm (int_atom a, ((b, d, e), Future.value f)) end] |
|
342 and proof_body x = |
|
343 let val (a, b, c) = triple (list (pair string term)) (list pthm) proof x |
|
344 in PBody {oracles = a, thms = b, proof = c} end |
|
345 and pthm x = |
|
346 let val (a, (b, c, d)) = pair int (triple string term proof_body) x |
|
347 in (a, (b, c, Future.value d)) end; |
|
348 |
|
349 in |
|
350 |
|
351 val decode = proof; |
|
352 val decode_body = proof_body; |
|
353 |
|
354 end; |
267 |
355 |
268 |
356 |
269 (***** proof objects with different levels of detail *****) |
357 (***** proof objects with different levels of detail *****) |
270 |
358 |
271 fun (prf %> t) = prf % SOME t; |
359 fun (prf %> t) = prf % SOME t; |