2001 #> fold_rev (implies_intr_proof o snd) (#constraints ucontext) |
2001 #> fold_rev (implies_intr_proof o snd) (#constraints ucontext) |
2002 end; |
2002 end; |
2003 |
2003 |
2004 fun clean_proof thy = rew_proof thy #> shrink_proof; |
2004 fun clean_proof thy = rew_proof thy #> shrink_proof; |
2005 |
2005 |
2006 val export_proof_term = |
2006 fun export_proof thy i prop prf = |
2007 term_of {thm_const = K o string_of_int, axm_const = axm_const_default}; |
2007 let |
2008 |
2008 val xml = |
2009 fun export_proof thy main_prop main_proof = |
2009 reconstruct_proof thy prop prf |
2010 let |
2010 |> term_of {thm_const = K o string_of_int, axm_const = axm_const_default} |
2011 fun add_proof_boxes (AbsP (_, _, prf)) = add_proof_boxes prf |
2011 |> Term_XML.Encode.term; |
2012 | add_proof_boxes (Abst (_, _, prf)) = add_proof_boxes prf |
2012 val chunks = Buffer.chunks (YXML.buffer_body xml Buffer.empty); |
2013 | add_proof_boxes (prf1 %% prf2) = add_proof_boxes prf1 #> add_proof_boxes prf2 |
2013 in |
2014 | add_proof_boxes (prf % _) = add_proof_boxes prf |
2014 chunks |> Export.export_params |
2015 | add_proof_boxes (PThm ({serial = i, name = "", prop, ...}, thm_body)) = |
2015 {theory = thy, |
2016 (fn boxes => |
2016 binding = Path.binding0 (Path.make ["proofs", string_of_int i]), |
2017 if Inttab.defined boxes i then boxes |
2017 executable = false, |
|
2018 compress = true, |
|
2019 strict = false} |
|
2020 end; |
|
2021 |
|
2022 fun export_proof_boxes thy proof = |
|
2023 let |
|
2024 fun export_boxes (AbsP (_, _, prf)) = export_boxes prf |
|
2025 | export_boxes (Abst (_, _, prf)) = export_boxes prf |
|
2026 | export_boxes (prf1 %% prf2) = export_boxes prf1 #> export_boxes prf2 |
|
2027 | export_boxes (prf % _) = export_boxes prf |
|
2028 | export_boxes (PThm ({serial = i, name = "", prop, ...}, thm_body)) = |
|
2029 (fn seen => |
|
2030 if Inttab.defined seen i then seen |
2018 else |
2031 else |
2019 let val prf = thm_body_proof_open thm_body |> reconstruct_proof thy prop; |
2032 let |
2020 in add_proof_boxes prf boxes |> Inttab.update (i, prf) end) |
2033 val proof = thm_body_proof_open thm_body; |
2021 | add_proof_boxes _ = I; |
2034 val _ = export_proof thy i prop proof; |
2022 |
2035 val boxes' = Inttab.update (i, ()) seen; |
2023 val proof = reconstruct_proof thy main_prop main_proof; |
2036 in export_boxes proof boxes' end) |
2024 val proof_boxes = |
2037 | export_boxes _ = I; |
2025 (proof, Inttab.empty) |-> add_proof_boxes |> Inttab.dest |
2038 in (proof, Inttab.empty) |-> export_boxes |> ignore end; |
2026 |> map (apsnd export_proof_term); |
2039 |
2027 in (proof_boxes, export_proof_term proof) end; |
2040 fun export thy i prop prf = |
2028 |
|
2029 fun export thy i prop proof = |
|
2030 if Options.default_bool "export_proofs" then |
2041 if Options.default_bool "export_proofs" then |
2031 let |
2042 (export_proof_boxes thy prf; export_proof thy i prop prf) |
2032 val xml = export_proof thy prop proof |
|
2033 |> let open XML.Encode Term_XML.Encode in pair (list (pair int term)) term end; |
|
2034 in |
|
2035 Export.export thy (Path.binding0 (Path.make ["proofs", string_of_int i])) |
|
2036 (Buffer.chunks (YXML.buffer_body xml Buffer.empty)) |
|
2037 end |
|
2038 else (); |
2043 else (); |
2039 |
2044 |
2040 fun prune proof = |
2045 fun prune proof = |
2041 if Options.default_bool "prune_proofs" then MinProof |
2046 if Options.default_bool "prune_proofs" then MinProof |
2042 else proof; |
2047 else proof; |