325 |
325 |
326 local |
326 local |
327 |
327 |
328 open XML.Encode Term_XML.Encode; |
328 open XML.Encode Term_XML.Encode; |
329 |
329 |
330 fun proof prf = prf |> variant |
330 fun proof consts prf = prf |> variant |
331 [fn MinProof => ([], []), |
331 [fn MinProof => ([], []), |
332 fn PBound a => ([int_atom a], []), |
332 fn PBound a => ([int_atom a], []), |
333 fn Abst (a, b, c) => ([a], pair (option typ) proof (b, c)), |
333 fn Abst (a, b, c) => ([a], pair (option typ) (proof consts) (b, c)), |
334 fn AbsP (a, b, c) => ([a], pair (option term) proof (b, c)), |
334 fn AbsP (a, b, c) => ([a], pair (option (term consts)) (proof consts) (b, c)), |
335 fn a % b => ([], pair proof (option term) (a, b)), |
335 fn a % b => ([], pair (proof consts) (option (term consts)) (a, b)), |
336 fn a %% b => ([], pair proof proof (a, b)), |
336 fn a %% b => ([], pair (proof consts) (proof consts) (a, b)), |
337 fn Hyp a => ([], term a), |
337 fn Hyp a => ([], term consts a), |
338 fn PAxm (a, b, c) => ([a], pair term (option (list typ)) (b, c)), |
338 fn PAxm (a, b, c) => ([a], pair (term consts) (option (list typ)) (b, c)), |
339 fn OfClass (a, b) => ([b], typ a), |
339 fn OfClass (a, b) => ([b], typ a), |
340 fn Oracle (a, b, c) => ([a], pair (option term) (option (list typ)) (b, c)), |
340 fn Oracle (a, b, c) => ([a], pair (option (term consts)) (option (list typ)) (b, c)), |
341 fn PThm ({serial, pos, theory_name, name, prop, types}, Thm_Body {open_proof, body, ...}) => |
341 fn PThm ({serial, pos, theory_name, name, prop, types}, Thm_Body {open_proof, body, ...}) => |
342 ([int_atom serial, theory_name, name], |
342 ([int_atom serial, theory_name, name], |
343 pair (list properties) (pair term (pair (option (list typ)) proof_body)) |
343 pair (list properties) (pair (term consts) (pair (option (list typ)) (proof_body consts))) |
344 (map Position.properties_of pos, (prop, (types, map_proof_of open_proof (Future.join body)))))] |
344 (map Position.properties_of pos, (prop, (types, map_proof_of open_proof (Future.join body)))))] |
345 and proof_body (PBody {oracles, thms, proof = prf}) = |
345 and proof_body consts (PBody {oracles, thms, proof = prf}) = |
346 triple (list (pair string (option term))) (list thm) proof (oracles, thms, prf) |
346 triple (list (pair string (option (term consts)))) (list (thm consts)) (proof consts) |
347 and thm (a, thm_node) = |
347 (oracles, thms, prf) |
348 pair int (pair string (pair string (pair term proof_body))) |
348 and thm consts (a, thm_node) = |
|
349 pair int (pair string (pair string (pair (term consts) (proof_body consts)))) |
349 (a, (thm_node_theory_name thm_node, (thm_node_name thm_node, (thm_node_prop thm_node, |
350 (a, (thm_node_theory_name thm_node, (thm_node_name thm_node, (thm_node_prop thm_node, |
350 (Future.join (thm_node_body thm_node)))))); |
351 (Future.join (thm_node_body thm_node)))))); |
351 |
352 |
352 fun full_proof prf = prf |> variant |
353 fun full_proof consts prf = prf |> variant |
353 [fn MinProof => ([], []), |
354 [fn MinProof => ([], []), |
354 fn PBound a => ([int_atom a], []), |
355 fn PBound a => ([int_atom a], []), |
355 fn Abst (a, SOME b, c) => ([a], pair typ full_proof (b, c)), |
356 fn Abst (a, SOME b, c) => ([a], pair typ (full_proof consts) (b, c)), |
356 fn AbsP (a, SOME b, c) => ([a], pair term full_proof (b, c)), |
357 fn AbsP (a, SOME b, c) => ([a], pair (term consts) (full_proof consts) (b, c)), |
357 fn a % SOME b => ([], pair full_proof term (a, b)), |
358 fn a % SOME b => ([], pair (full_proof consts) (term consts) (a, b)), |
358 fn a %% b => ([], pair full_proof full_proof (a, b)), |
359 fn a %% b => ([], pair (full_proof consts) (full_proof consts) (a, b)), |
359 fn Hyp a => ([], term a), |
360 fn Hyp a => ([], term consts a), |
360 fn PAxm (name, _, SOME Ts) => ([name], list typ Ts), |
361 fn PAxm (name, _, SOME Ts) => ([name], list typ Ts), |
361 fn OfClass (T, c) => ([c], typ T), |
362 fn OfClass (T, c) => ([c], typ T), |
362 fn Oracle (name, prop, SOME Ts) => ([name], pair (option term) (list typ) (prop, Ts)), |
363 fn Oracle (name, prop, SOME Ts) => ([name], pair (option (term consts)) (list typ) (prop, Ts)), |
363 fn PThm ({serial, theory_name, name, types = SOME Ts, ...}, _) => |
364 fn PThm ({serial, theory_name, name, types = SOME Ts, ...}, _) => |
364 ([int_atom serial, theory_name, name], list typ Ts)]; |
365 ([int_atom serial, theory_name, name], list typ Ts)]; |
365 |
366 |
366 in |
367 in |
367 |
368 |
376 |
377 |
377 local |
378 local |
378 |
379 |
379 open XML.Decode Term_XML.Decode; |
380 open XML.Decode Term_XML.Decode; |
380 |
381 |
381 fun proof prf = prf |> variant |
382 fun proof consts prf = prf |> variant |
382 [fn ([], []) => MinProof, |
383 [fn ([], []) => MinProof, |
383 fn ([a], []) => PBound (int_atom a), |
384 fn ([a], []) => PBound (int_atom a), |
384 fn ([a], b) => let val (c, d) = pair (option typ) proof b in Abst (a, c, d) end, |
385 fn ([a], b) => let val (c, d) = pair (option typ) (proof consts) b in Abst (a, c, d) end, |
385 fn ([a], b) => let val (c, d) = pair (option term) proof b in AbsP (a, c, d) end, |
386 fn ([a], b) => let val (c, d) = pair (option (term consts)) (proof consts) b in AbsP (a, c, d) end, |
386 fn ([], a) => op % (pair proof (option term) a), |
387 fn ([], a) => op % (pair (proof consts) (option (term consts)) a), |
387 fn ([], a) => op %% (pair proof proof a), |
388 fn ([], a) => op %% (pair (proof consts) (proof consts) a), |
388 fn ([], a) => Hyp (term a), |
389 fn ([], a) => Hyp (term consts a), |
389 fn ([a], b) => let val (c, d) = pair term (option (list typ)) b in PAxm (a, c, d) end, |
390 fn ([a], b) => let val (c, d) = pair (term consts) (option (list typ)) b in PAxm (a, c, d) end, |
390 fn ([b], a) => OfClass (typ a, b), |
391 fn ([b], a) => OfClass (typ a, b), |
391 fn ([a], b) => let val (c, d) = pair (option term) (option (list typ)) b in Oracle (a, c, d) end, |
392 fn ([a], b) => |
|
393 let val (c, d) = pair (option (term consts)) (option (list typ)) b in Oracle (a, c, d) end, |
392 fn ([a, b, c], d) => |
394 fn ([a, b, c], d) => |
393 let |
395 let |
394 val ((e, (f, (g, h)))) = |
396 val ((e, (f, (g, h)))) = |
395 pair (list properties) (pair term (pair (option (list typ)) proof_body)) d; |
397 pair (list properties) (pair (term consts) (pair (option (list typ)) (proof_body consts))) d; |
396 val header = thm_header (int_atom a) (map Position.of_properties e) b c f g; |
398 val header = thm_header (int_atom a) (map Position.of_properties e) b c f g; |
397 in PThm (header, thm_body h) end] |
399 in PThm (header, thm_body h) end] |
398 and proof_body x = |
400 and proof_body consts x = |
399 let val (a, b, c) = triple (list (pair string (option term))) (list thm) proof x |
401 let |
|
402 val (a, b, c) = |
|
403 triple (list (pair string (option (term consts)))) (list (thm consts)) (proof consts) x; |
400 in PBody {oracles = a, thms = b, proof = c} end |
404 in PBody {oracles = a, thms = b, proof = c} end |
401 and thm x = |
405 and thm consts x = |
402 let val (a, (b, (c, (d, e)))) = pair int (pair string (pair string (pair term proof_body))) x |
406 let |
|
407 val (a, (b, (c, (d, e)))) = |
|
408 pair int (pair string (pair string (pair (term consts) (proof_body consts)))) x |
403 in (a, make_thm_node b c d (Future.value e)) end; |
409 in (a, make_thm_node b c d (Future.value e)) end; |
404 |
410 |
405 in |
411 in |
406 |
412 |
407 val decode = proof; |
413 val decode = proof; |