# HG changeset patch
# User wenzelm
# Date 1721312753 -7200
# Node ID b8733a141c268c383794e28c65d3966bdd1b4d10
# Parent  9c6cfac291f4f81f765d86a9c344f91086e0d21f
uniform export via ztyp/zterm/zproof;

diff -r 9c6cfac291f4 -r b8733a141c26 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Thu Jul 18 15:26:36 2024 +0200
+++ b/src/Pure/proofterm.ML	Thu Jul 18 16:25:53 2024 +0200
@@ -65,10 +65,11 @@
   val no_thm_proofs: proof -> proof
   val no_body_proofs: proof -> proof
 
+  val proof_to_zproof: theory -> proof -> zproof
+  val encode_standard_term: theory -> term XML.Encode.T
+  val encode_standard_proof: theory -> proof XML.Encode.T
   val encode: theory -> proof XML.Encode.T
   val encode_body: theory -> proof_body XML.Encode.T
-  val encode_standard_term: theory -> term XML.Encode.T
-  val encode_standard_proof: theory -> proof XML.Encode.T
   val decode: theory -> proof XML.Decode.T
   val decode_body: theory -> proof_body XML.Decode.T
 
@@ -369,6 +370,40 @@
 
 (** XML data representation **)
 
+(* encode as zterm/zproof *)
+
+fun proof_to_zproof thy =
+  let
+    val {ztyp, zterm} = ZTerm.zterm_cache thy;
+    val ztvar = ztyp #> (fn ZTVar v => v);
+
+    fun zproof_const name prop typargs =
+      let
+        val vs = rev ((fold_types o fold_atyps) (insert (op =) o ztvar) prop []);
+        val Ts = map ztyp typargs
+      in ZConstp ((name, zterm prop), (ZTVars.make (vs ~~ Ts), ZVars.empty)) end;
+
+    fun zproof MinProof = ZNop
+      | zproof (PBound i) = ZBoundp i
+      | zproof (Abst (a, SOME T, p)) = ZAbst (a, ztyp T, zproof p)
+      | zproof (AbsP (a, SOME t, p)) = ZAbsp (a, zterm t, zproof p)
+      | zproof (p % SOME t) = ZAppt (zproof p, zterm t)
+      | zproof (p %% q) = ZAppp (zproof p, zproof q)
+      | zproof (Hyp t) = ZHyp (zterm t)
+      | zproof (PAxm (a, prop, SOME Ts)) = zproof_const (ZAxiom a) prop Ts
+      | zproof (PClass (T, c)) = OFCLASSp (ztyp T, c)
+      | zproof (Oracle (a, prop, SOME Ts)) = zproof_const (ZOracle a) prop Ts
+      | zproof (PThm ({serial, pos, theory_name, thm_name, prop, types = SOME Ts, ...}, _)) =
+          let
+            val name = (thm_name, try hd pos |> the_default Position.none);
+            val proof_name = ZThm {theory_name = theory_name, thm_name = name, serial = serial};
+          in zproof_const proof_name prop Ts end;
+  in zproof end;
+
+fun encode_standard_term thy = ZTerm.zterm_of thy #> ZTerm.encode_zterm {typed_vars = false};
+fun encode_standard_proof thy = proof_to_zproof thy #> ZTerm.encode_zproof {typed_vars = false};
+
+
 (* encode *)
 
 local
@@ -399,39 +434,10 @@
     (a, (thm_node_theory_name thm_node, (thm_node_name thm_node, (thm_node_prop thm_node,
       (Future.join (thm_node_body thm_node))))));
 
-fun standard_term consts t = t |> variant
- [fn Const (a, b) => ([a], list typ (Consts.typargs consts (a, b))),
-  fn Free (a, _) => ([a], []),
-  fn Var (a, _) => (indexname a, []),
-  fn Bound a => ([], int a),
-  fn Abs (a, b, c) => ([a], pair typ (standard_term consts) (b, c)),
-  fn t as op $ a =>
-    if can Logic.match_of_class t then raise Match
-    else ([], pair (standard_term consts) (standard_term consts) a),
-  fn t =>
-    let val (T, c) = Logic.match_of_class t
-    in ([c], typ T) end];
-
-fun standard_proof consts prf = prf |> variant
- [fn MinProof => ([], []),
-  fn PBound a => ([], int a),
-  fn Abst (a, SOME b, c) => ([a], pair typ (standard_proof consts) (b, c)),
-  fn AbsP (a, SOME b, c) => ([a], pair (standard_term consts) (standard_proof consts) (b, c)),
-  fn a % SOME b => ([], pair (standard_proof consts) (standard_term consts) (a, b)),
-  fn a %% b => ([], pair (standard_proof consts) (standard_proof consts) (a, b)),
-  fn Hyp a => ([], standard_term consts a),
-  fn PAxm (name, _, SOME Ts) => ([name], list typ Ts),
-  fn PClass (T, c) => ([c], typ T),
-  fn Oracle (name, prop, SOME Ts) => ([name], pair (standard_term consts) (list typ) (prop, Ts)),
-  fn PThm ({serial, theory_name, thm_name, types = SOME Ts, ...}, _) =>
-    ([int_atom serial, theory_name, #1 thm_name, int_atom (#2 thm_name)], list typ Ts)];
-
 in
 
 val encode = proof o Sign.consts_of;
 val encode_body = proof_body o Sign.consts_of;
-val encode_standard_term = standard_term o Sign.consts_of;
-val encode_standard_proof = standard_proof o Sign.consts_of;
 
 end;
 
diff -r 9c6cfac291f4 -r b8733a141c26 src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Thu Jul 18 15:26:36 2024 +0200
+++ b/src/Pure/zterm.ML	Thu Jul 18 16:25:53 2024 +0200
@@ -251,6 +251,7 @@
   val map_proof_types: {hyps: bool} -> ztyp Same.operation -> zproof -> zproof
   val map_class_proof: (ztyp * class, zproof) Same.function -> zproof -> zproof
   val ztyp_of: typ -> ztyp
+  val ztyp_dummy: ztyp
   val typ_of_tvar: indexname * sort -> typ
   val typ_of: ztyp -> typ
   val reset_cache: theory -> theory
@@ -314,6 +315,9 @@
   val of_sort_proof: Sorts.algebra -> sorts_proof -> (typ * class -> zproof) ->
     typ * sort -> zproof list
   val unconstrainT_proof: theory -> sorts_proof -> Logic.unconstrain_context -> zproof -> zproof
+  val encode_ztyp: ztyp XML.Encode.T
+  val encode_zterm: {typed_vars: bool} -> zterm XML.Encode.T
+  val encode_zproof: {typed_vars: bool} -> zproof XML.Encode.T
 end;
 
 structure ZTerm: ZTERM =
@@ -591,6 +595,8 @@
   | ztyp_of (Type (c, [T])) = ZType1 (c, ztyp_of T)
   | ztyp_of (Type (c, ts)) = ZType (c, map ztyp_of ts);
 
+val ztyp_dummy = ztyp_of dummyT;
+
 fun typ_of_tvar ((a, ~1), S) = TFree (a, S)
   | typ_of_tvar v = TVar v;
 
@@ -1365,4 +1371,60 @@
     #> fold_rev (implies_intr_proof' o #zterm cache o #2) (#constraints ucontext)
   end;
 
+
+
+(** XML data representation **)
+
+(* encode *)
+
+local
+
+open XML.Encode Term_XML.Encode;
+
+fun ztyp T = T |> variant
+ [fn ZFun args => (["fun"], pair ztyp ztyp args)
+   | ZProp => (["prop"], [])
+   | ZType0 a => ([a], [])
+   | ZType1 (a, b) => ([a], list ztyp [b])
+   | ZType (a, b) => ([a], list ztyp b),
+  fn ZTVar ((a, ~1), b) => ([a], sort b),
+  fn ZTVar (a, b) => (indexname a, sort b)];
+
+fun zvar_type {typed_vars} T =
+  if typed_vars andalso T <> ztyp_dummy then ztyp T else [];
+
+fun zterm flag t = t |> variant
+ [fn ZConst0 a => ([a], [])
+   | ZConst1 (a, b) => ([a], list ztyp [b])
+   | ZConst (a, b) => ([a], list ztyp b),
+  fn ZVar ((a, ~1), b) => ([a], zvar_type flag b),
+  fn ZVar (a, b) => (indexname a, zvar_type flag b),
+  fn ZBound a => ([], int a),
+  fn ZAbs (a, b, c) => ([a], pair ztyp (zterm flag) (b, c)),
+  fn ZApp a => ([], pair (zterm flag) (zterm flag) a),
+  fn OFCLASS (a, b) => ([b], ztyp a)];
+
+fun zproof flag prf = prf |> variant
+ [fn ZNop => ([], []),
+  fn ZBoundp a => ([], int a),
+  fn ZAbst (a, b, c) => ([a], pair ztyp (zproof flag) (b, c)),
+  fn ZAbsp (a, b, c) => ([a], pair (zterm flag) (zproof flag) (b, c)),
+  fn ZAppt a => ([], pair (zproof flag) (zterm flag) a),
+  fn ZAppp a => ([], pair (zproof flag) (zproof flag) a),
+  fn ZHyp a => ([], zterm flag a),
+  fn ZConstp (c as ((ZAxiom a, b), _)) => ([a], list (ztyp o #2) (zproof_const_typargs c)),
+  fn OFCLASSp (a, b) => ([b], ztyp a),
+  fn ZConstp (c as ((ZOracle a, b), _)) => ([a], list (ztyp o #2) (zproof_const_typargs c)),
+  fn ZConstp (c as ((ZThm {theory_name, thm_name = (name, _), serial}, b), _)) =>
+    ([int_atom serial, theory_name, #1 name, int_atom (#2 name)],
+      list (ztyp o #2) (zproof_const_typargs c))];
+
+in
+
+val encode_ztyp = ztyp;
+val encode_zterm = zterm;
+val encode_zproof = zproof;
+
 end;
+
+end;
\ No newline at end of file