# HG changeset patch
# User wenzelm
# Date 1371998865 -7200
# Node ID 77075c576d4c749d3461e405785a57a855a6cd34
# Parent  bc5c96c745147a0b2b21165ecc25cf9b5422d4a4
support for XML data representation of proof terms;

diff -r bc5c96c74514 -r 77075c576d4c src/HOL/Proofs/ex/XML_Data.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Proofs/ex/XML_Data.thy	Sun Jun 23 16:47:45 2013 +0200
@@ -0,0 +1,47 @@
+(*  Title:      HOL/Proofs/ex/XML_Data.thy
+    Author:     Makarius
+
+XML data representation of proof terms.
+*)
+
+theory XML_Data
+imports Main
+begin
+
+subsection {* Export and re-import of global proof terms *}
+
+ML {*
+  fun export_proof thm0 =
+    let
+      val thy = Thm.theory_of_thm thm0;
+      val ctxt0 = Proof_Context.init_global thy;
+      val thy = Proof_Context.theory_of ctxt0;
+      val ((_, [thm]), ctxt) = Variable.import true [Thm.transfer thy thm0] ctxt0;
+
+      val prop = Thm.prop_of thm;  (* FIXME proper prop (wrt. import / strip) (!??) *)
+      val prf =
+        Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of thm))
+        |> Proofterm.no_thm_proofs;
+    in XML.Encode.pair Term_XML.Encode.term Proofterm.encode (prop, prf) end;
+
+  fun import_proof thy xml =
+    let
+      val (prop, prf) = XML.Decode.pair Term_XML.Decode.term Proofterm.decode xml;
+      val full_prf = Reconstruct.reconstruct_proof thy prop prf;
+    in Drule.export_without_context (Proof_Checker.thm_of_proof thy full_prf) end;
+*}
+
+
+subsection {* Example *}
+
+ML {* val thy1 = @{theory} *}
+
+lemma ex: "A \<longrightarrow> A" ..
+
+ML {*
+  val xml = export_proof @{thm ex};
+  val thm = import_proof thy1 xml;
+*}
+
+end
+
diff -r bc5c96c74514 -r 77075c576d4c src/HOL/ROOT
--- a/src/HOL/ROOT	Sun Jun 23 14:26:49 2013 +0200
+++ b/src/HOL/ROOT	Sun Jun 23 16:47:45 2013 +0200
@@ -357,7 +357,9 @@
 
 session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
   options [document = false, proofs = 2, skip_proofs = false, parallel_proofs = 0]
-  theories Hilbert_Classical
+  theories
+    Hilbert_Classical
+    XML_Data
 
 session "HOL-Proofs-Extraction" in "Proofs/Extraction" = "HOL-Proofs" +
   description {*
diff -r bc5c96c74514 -r 77075c576d4c src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sun Jun 23 14:26:49 2013 +0200
+++ b/src/Pure/proofterm.ML	Sun Jun 23 16:47:45 2013 +0200
@@ -50,6 +50,13 @@
   val unions_thms: pthm Ord_List.T list -> pthm Ord_List.T
   val all_oracles_of: proof_body -> oracle Ord_List.T
   val approximate_proof_body: proof -> proof_body
+  val no_proof_body: proof_body
+  val no_thm_proofs: proof -> proof
+
+  val encode: proof XML.Encode.T
+  val encode_body: proof_body XML.Encode.T
+  val decode: proof XML.Decode.T
+  val decode_body: proof_body XML.Decode.T
 
   (** primitive operations **)
   val proofs_enabled: unit -> bool
@@ -265,6 +272,87 @@
       proof = prf}
   end;
 
+val no_proof_body = PBody {oracles = [], thms = [], proof = MinProof};
+val no_body = Future.value no_proof_body;
+
+fun no_thm_proofs (PThm (i, (a, _))) = PThm (i, (a, no_body))
+  | no_thm_proofs (Abst (x, T, prf)) = Abst (x, T, no_thm_proofs prf)
+  | no_thm_proofs (AbsP (x, t, prf)) = AbsP (x, t, no_thm_proofs prf)
+  | no_thm_proofs (prf % t) = no_thm_proofs prf % t
+  | no_thm_proofs (prf1 %% prf2) = no_thm_proofs prf1 %% no_thm_proofs prf2
+  | no_thm_proofs a = a;
+
+
+(***** XML data representation *****)
+
+(* encode *)
+
+local
+
+open XML.Encode Term_XML.Encode;
+
+fun proof prf = prf |> variant
+ [fn MinProof => ([], []),
+  fn PBound a => ([int_atom a], []),
+  fn Abst (a, b, c) => ([a], pair (option typ) proof (b, c)),
+  fn AbsP (a, b, c) => ([a], pair (option term) proof (b, c)),
+  fn a % b => ([], pair proof (option term) (a, b)),
+  fn a %% b => ([], pair proof proof (a, b)),
+  fn Hyp a => ([], term a),
+  fn PAxm (a, b, c) => ([a], pair term (option (list typ)) (b, c)),
+  fn OfClass (a, b) => ([b], typ a),
+  fn Oracle (a, b, c) => ([a], pair term (option (list typ)) (b, c)),
+  fn Promise (a, b, c) => ([int_atom a], pair term (list typ) (b, c)),
+  fn PThm (a, ((b, c, d), body)) =>
+    ([int_atom a, b], triple term (option (list typ)) proof_body (c, d, Future.join body))]
+and proof_body (PBody {oracles, thms, proof = prf}) =
+  triple (list (pair string term)) (list pthm) proof (oracles, thms, prf)
+and pthm (a, (b, c, body)) =
+  pair int (triple string term proof_body) (a, (b, c, Future.join body));
+
+in
+
+val encode = proof;
+val encode_body = proof_body;
+
+end;
+
+
+(* decode *)
+
+local
+
+open XML.Decode Term_XML.Decode;
+
+fun proof prf = prf |> variant
+ [fn ([], []) => MinProof,
+  fn ([a], []) => PBound (int_atom a),
+  fn ([a], b) => let val (c, d) = pair (option typ) proof b in Abst (a, c, d) end,
+  fn ([a], b) => let val (c, d) = pair (option term) proof b in AbsP (a, c, d) end,
+  fn ([], a) => op % (pair proof (option term) a),
+  fn ([], a) => op %% (pair proof proof a),
+  fn ([], a) => Hyp (term a),
+  fn ([a], b) => let val (c, d) = pair term (option (list typ)) b in PAxm (a, c, d) end,
+  fn ([b], a) => OfClass (typ a, b),
+  fn ([a], b) => let val (c, d) = pair term (option (list typ)) b in Oracle (a, c, d) end,
+  fn ([a], b) => let val (c, d) = pair term (list typ) b in Promise (int_atom a, c, d) end,
+  fn ([a, b], c) =>
+    let val (d, e, f) = triple term (option (list typ)) proof_body c
+    in PThm (int_atom a, ((b, d, e), Future.value f)) end]
+and proof_body x =
+  let val (a, b, c) = triple (list (pair string term)) (list pthm) proof x
+  in PBody {oracles = a, thms = b, proof = c} end
+and pthm x =
+  let val (a, (b, c, d)) = pair int (triple string term proof_body) x
+  in (a, (b, c, Future.value d)) end;
+
+in
+
+val decode = proof;
+val decode_body = proof_body;
+
+end;
+
 
 (***** proof objects with different levels of detail *****)