# HG changeset patch
# User wenzelm
# Date 1570880597 -7200
# Node ID cc987440d77622987ff687bb47aa22ab2b231de8
# Parent  c5caf81aa5237229b653e8557f446eeb2878ff9f
more compact XML: separate environment for free variables;
clarified fold_proof_terms vs. fold_proof_terms_types;

diff -r c5caf81aa523 -r cc987440d776 src/Pure/Proof/proof_checker.ML
--- a/src/Pure/Proof/proof_checker.ML	Sat Oct 12 12:25:16 2019 +0200
+++ b/src/Pure/Proof/proof_checker.ML	Sat Oct 12 13:43:17 2019 +0200
@@ -72,7 +72,7 @@
   let val lookup = lookup_thm thy in
     fn prf =>
       let
-        val prf_names = Proofterm.fold_proof_terms Term.declare_term_frees (K I) prf Name.context;
+        val prf_names = Proofterm.fold_proof_terms Term.declare_term_frees prf Name.context;
 
         fun thm_of_atom thm Ts =
           let
diff -r c5caf81aa523 -r cc987440d776 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Sat Oct 12 12:25:16 2019 +0200
+++ b/src/Pure/Thy/export_theory.ML	Sat Oct 12 13:43:17 2019 +0200
@@ -270,8 +270,10 @@
           standard_prop Name.context (Thm.extra_shyps thm) (Thm.full_prop_of thm) (SOME raw_proof);
       in
         (prop, (deps, proof)) |>
-          let open XML.Encode Term_XML.Encode
-          in pair encode_prop (pair (list string) (option (Proofterm.encode_standard consts))) end
+          let
+            open XML.Encode Term_XML.Encode;
+            val encode_proof = Proofterm.encode_standard_proof consts;
+          in pair encode_prop (pair (list string) (option encode_proof)) end
       end;
 
     fun buffer_export_thm (serial, thm_name) =
diff -r c5caf81aa523 -r cc987440d776 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Sat Oct 12 12:25:16 2019 +0200
+++ b/src/Pure/Thy/export_theory.scala	Sat Oct 12 13:43:17 2019 +0200
@@ -357,7 +357,17 @@
   {
     val body = provider.focus(theory_name).uncompressed_yxml(export_prefix_proofs + serial)
     if (body.isEmpty) error("Bad proof export " + serial)
-    val (prop, proof) = XML.Decode.pair(Term_XML.Decode.term, Term_XML.Decode.proof)(body)
+
+    val (vars, prop_body, proof_body) =
+    {
+      import XML.Decode._
+      import Term_XML.Decode._
+      triple(list(pair(string, typ)), x => x, x => x)(body)
+    }
+    val env = vars.toMap
+    val prop = Term_XML.Decode.term_env(env)(prop_body)
+    val proof = Term_XML.Decode.proof_env(env)(proof_body)
+
     cache match {
       case None => (prop, proof)
       case Some(cache) => (cache.term(prop), cache.proof(proof))
diff -r c5caf81aa523 -r cc987440d776 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sat Oct 12 12:25:16 2019 +0200
+++ b/src/Pure/proofterm.ML	Sat Oct 12 13:43:17 2019 +0200
@@ -61,7 +61,8 @@
 
   val encode: Consts.T -> proof XML.Encode.T
   val encode_body: Consts.T -> proof_body XML.Encode.T
-  val encode_standard: Consts.T -> proof XML.Encode.T
+  val encode_standard_term: Consts.T -> term XML.Encode.T
+  val encode_standard_proof: Consts.T -> proof XML.Encode.T
   val decode: Consts.T -> proof XML.Decode.T
   val decode_body: Consts.T -> proof_body XML.Decode.T
 
@@ -84,7 +85,8 @@
   val map_proof_types_same: typ Same.operation -> proof Same.operation
   val map_proof_terms: (term -> term) -> (typ -> typ) -> proof -> proof
   val map_proof_types: (typ -> typ) -> proof -> proof
-  val fold_proof_terms: (term -> 'a -> 'a) -> (typ -> 'a -> 'a) -> proof -> 'a -> 'a
+  val fold_proof_terms: (term -> 'a -> 'a) -> proof -> 'a -> 'a
+  val fold_proof_terms_types: (term -> 'a -> 'a) -> (typ -> 'a -> 'a) -> proof -> 'a -> 'a
   val maxidx_proof: proof -> int -> int
   val size_of_proof: proof -> int
   val change_types: typ list option -> proof -> proof
@@ -163,6 +165,8 @@
 
   val standard_vars: Name.context -> term * proof option -> term * proof option
   val standard_vars_term: Name.context -> term -> term
+  val add_standard_vars: proof -> (string * typ) list -> (string * typ) list
+  val add_standard_vars_term: term -> (string * typ) list -> (string * typ) list
 
   val export_enabled: unit -> bool
   val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
@@ -350,17 +354,25 @@
     (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_atom a], []),
+  fn Abs (a, b, c) => ([a], pair typ (standard_term consts) (b, c)),
+  fn op $ a => ([], pair (standard_term consts) (standard_term consts) a)];
+
 fun standard_proof consts prf = prf |> variant
  [fn MinProof => ([], []),
   fn PBound a => ([int_atom a], []),
   fn Abst (a, SOME b, c) => ([a], pair typ (standard_proof consts) (b, c)),
-  fn AbsP (a, SOME b, c) => ([a], pair (term consts) (standard_proof consts) (b, c)),
-  fn a % SOME b => ([], pair (standard_proof consts) (term consts) (a, b)),
+  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 => ([], term consts a),
+  fn Hyp a => ([], standard_term consts a),
   fn PAxm (name, _, SOME Ts) => ([name], list typ Ts),
   fn OfClass (T, c) => ([c], typ T),
-  fn Oracle (name, prop, SOME Ts) => ([name], pair (term consts) (list typ) (prop, Ts)),
+  fn Oracle (name, prop, SOME Ts) => ([name], pair (standard_term consts) (list typ) (prop, Ts)),
   fn PThm ({serial, theory_name, name, types = SOME Ts, ...}, _) =>
     ([int_atom serial, theory_name, name], list typ Ts)];
 
@@ -368,7 +380,8 @@
 
 val encode = proof;
 val encode_body = proof_body;
-val encode_standard = standard_proof;
+val encode_standard_term = standard_term;
+val encode_standard_proof = standard_proof;
 
 end;
 
@@ -491,21 +504,29 @@
 fun map_proof_terms f g = Same.commit (map_proof_terms_same (same (op =) f) (same (op =) g));
 fun map_proof_types f = Same.commit (map_proof_types_same (same (op =) f));
 
-fun fold_proof_terms f g (Abst (_, SOME T, prf)) = g T #> fold_proof_terms f g prf
-  | fold_proof_terms f g (Abst (_, NONE, prf)) = fold_proof_terms f g prf
-  | fold_proof_terms f g (AbsP (_, SOME t, prf)) = f t #> fold_proof_terms f g prf
-  | fold_proof_terms f g (AbsP (_, NONE, prf)) = fold_proof_terms f g prf
-  | fold_proof_terms f g (prf % SOME t) = fold_proof_terms f g prf #> f t
-  | fold_proof_terms f g (prf % NONE) = fold_proof_terms f g prf
-  | fold_proof_terms f g (prf1 %% prf2) =
-      fold_proof_terms f g prf1 #> fold_proof_terms f g prf2
-  | fold_proof_terms _ g (PAxm (_, _, SOME Ts)) = fold g Ts
-  | fold_proof_terms _ g (OfClass (T, _)) = g T
-  | fold_proof_terms _ g (Oracle (_, _, SOME Ts)) = fold g Ts
-  | fold_proof_terms _ g (PThm ({types = SOME Ts, ...}, _)) = fold g Ts
-  | fold_proof_terms _ _ _ = I;
+fun fold_proof_terms f (Abst (_, _, prf)) = fold_proof_terms f prf
+  | fold_proof_terms f (AbsP (_, SOME t, prf)) = f t #> fold_proof_terms f prf
+  | fold_proof_terms f (AbsP (_, NONE, prf)) = fold_proof_terms f prf
+  | fold_proof_terms f (prf % SOME t) = fold_proof_terms f prf #> f t
+  | fold_proof_terms f (prf % NONE) = fold_proof_terms f prf
+  | fold_proof_terms f (prf1 %% prf2) = fold_proof_terms f prf1 #> fold_proof_terms f prf2
+  | fold_proof_terms _ _ = I;
 
-fun maxidx_proof prf = fold_proof_terms Term.maxidx_term Term.maxidx_typ prf;
+fun fold_proof_terms_types f g (Abst (_, SOME T, prf)) = g T #> fold_proof_terms_types f g prf
+  | fold_proof_terms_types f g (Abst (_, NONE, prf)) = fold_proof_terms_types f g prf
+  | fold_proof_terms_types f g (AbsP (_, SOME t, prf)) = f t #> fold_proof_terms_types f g prf
+  | fold_proof_terms_types f g (AbsP (_, NONE, prf)) = fold_proof_terms_types f g prf
+  | fold_proof_terms_types f g (prf % SOME t) = fold_proof_terms_types f g prf #> f t
+  | fold_proof_terms_types f g (prf % NONE) = fold_proof_terms_types f g prf
+  | fold_proof_terms_types f g (prf1 %% prf2) =
+      fold_proof_terms_types f g prf1 #> fold_proof_terms_types f g prf2
+  | fold_proof_terms_types _ g (PAxm (_, _, SOME Ts)) = fold g Ts
+  | fold_proof_terms_types _ g (OfClass (T, _)) = g T
+  | fold_proof_terms_types _ g (Oracle (_, _, SOME Ts)) = fold g Ts
+  | fold_proof_terms_types _ g (PThm ({types = SOME Ts, ...}, _)) = fold g Ts
+  | fold_proof_terms_types _ _ _ = I;
+
+fun maxidx_proof prf = fold_proof_terms_types Term.maxidx_term Term.maxidx_typ prf;
 
 fun size_of_proof (Abst (_, _, prf)) = 1 + size_of_proof prf
   | size_of_proof (AbsP (_, _, prf)) = 1 + size_of_proof prf
@@ -769,7 +790,7 @@
 
 fun freeze_thaw_prf prf =
   let
-    val (fs, Tfs, vs, Tvs) = fold_proof_terms
+    val (fs, Tfs, vs, Tvs) = fold_proof_terms_types
       (fn t => fn (fs, Tfs, vs, Tvs) =>
          (Term.add_free_names t fs, Term.add_tfree_names t Tfs,
           Term.add_var_names t vs, Term.add_tvar_names t Tvs))
@@ -1991,12 +2012,7 @@
 
 val declare_names_term = Term.declare_term_frees;
 val declare_names_term' = fn SOME t => declare_names_term t | NONE => I;
-
-fun declare_names_proof (Abst (_, _, prf)) = declare_names_proof prf
-  | declare_names_proof (AbsP (_, t, prf)) = declare_names_term' t #> declare_names_proof prf
-  | declare_names_proof (prf % t) = declare_names_proof prf #> declare_names_term' t
-  | declare_names_proof (prf1 %% prf2) = declare_names_proof prf1 #> declare_names_proof prf2
-  | declare_names_proof _ = I;
+val declare_names_proof = fold_proof_terms declare_names_term;
 
 fun variant names bs x =
   #1 (Name.variant x (fold Name.declare bs names));
@@ -2027,7 +2043,7 @@
 
 val used_frees_type = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I);
 fun used_frees_term t = fold_types used_frees_type t #> Term.declare_term_frees t;
-val used_frees_proof = fold_proof_terms used_frees_term used_frees_type;
+val used_frees_proof = fold_proof_terms_types used_frees_term used_frees_type;
 
 val unvarifyT = Term.map_atyps (fn TVar ((a, _), S) => TFree (a, S) | T => T);
 val unvarify = Term.map_aterms (fn Var ((x, _), T) => Free (x, T) | t => t) #> map_types unvarifyT;
@@ -2037,7 +2053,7 @@
   let
     val visible = (fold_types o fold_atyps) (insert (op =)) prop [];
     val add_hiddenT = fold_atyps (fn T => not (member (op =) visible T) ? insert (op =) T);
-  in rev (fold_proof_terms (fold_types add_hiddenT) add_hiddenT proof []) end;
+  in rev (fold_proof_terms_types (fold_types add_hiddenT) add_hiddenT proof []) end;
 
 fun standard_hidden_types term proof =
   let
@@ -2052,7 +2068,7 @@
 fun standard_vars used (term, opt_proof) =
   let
     val proofs = the_list (Option.map (standard_hidden_types term) opt_proof);
-    val proof_terms = rev (fold (fold_proof_terms cons (cons o Logic.mk_type)) proofs []);
+    val proof_terms = rev (fold (fold_proof_terms_types cons (cons o Logic.mk_type)) proofs []);
     val used_frees = used
       |> used_frees_term term
       |> fold used_frees_proof proofs;
@@ -2063,6 +2079,18 @@
 
 fun standard_vars_term used t = #1 (standard_vars used (t, NONE));
 
+val add_standard_vars_term = fold_aterms
+  (fn Free (x, T) =>
+    (fn env =>
+      (case AList.lookup (op =) env x of
+        NONE => (x, T) :: env
+      | SOME T' =>
+          if T = T' then env
+          else raise TYPE ("standard_vars_env: type conflict for variable " ^ quote x, [T, T'], [])))
+    | _ => I);
+
+val add_standard_vars = fold_proof_terms add_standard_vars_term;
+
 end;
 
 
@@ -2090,15 +2118,20 @@
 
 fun clean_proof thy = rew_proof thy #> shrink_proof;
 
-fun encode_export consts prop prf =
-  let open XML.Encode Term_XML.Encode
-  in pair (term consts) (encode_standard consts) (prop, prf) end;
+fun encode_export consts =
+  let
+    open XML.Encode Term_XML.Encode;
+    val encode_vars = list (pair string typ);
+    val encode_term = encode_standard_term consts;
+    val encode_proof = encode_standard_proof consts;
+  in triple encode_vars encode_term encode_proof end;
 
 fun export_proof thy i prop prf =
   let
     val (prop', SOME prf') =
       standard_vars Name.context (prop, SOME (reconstruct_proof thy prop prf));
-    val xml = encode_export (Sign.consts_of thy) prop' prf';
+    val vars = [] |> add_standard_vars_term prop' |> add_standard_vars prf' |> rev;
+    val xml = encode_export (Sign.consts_of thy) (vars, prop', prf');
     val chunks = Buffer.chunks (YXML.buffer_body xml Buffer.empty);
   in
     chunks |> Export.export_params
diff -r c5caf81aa523 -r cc987440d776 src/Pure/term_xml.scala
--- a/src/Pure/term_xml.scala	Sat Oct 12 12:25:16 2019 +0200
+++ b/src/Pure/term_xml.scala	Sat Oct 12 13:43:17 2019 +0200
@@ -66,18 +66,41 @@
         { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) },
         { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) }))
 
-    def proof: T[Proof] =
-      variant[Proof](List(
-        { case (Nil, Nil) => MinProof },
-        { case (List(a), Nil) => PBound(int_atom(a)) },
-        { case (List(a), b) => val (c, d) = pair(typ, proof)(b); Abst(a, c, d) },
-        { case (List(a), b) => val (c, d) = pair(term, proof)(b); AbsP(a, c, d) },
-        { case (Nil, a) => val (b, c) = pair(proof, term)(a); Appt(b, c) },
-        { case (Nil, a) => val (b, c) = pair(proof, proof)(a); AppP(b, c) },
-        { case (Nil, a) => Hyp(term(a)) },
-        { case (List(a), b) => PAxm(a, list(typ)(b)) },
-        { case (List(a), b) => OfClass(typ(b), a) },
-        { case (List(a), b) => val (c, d) = pair(term, list(typ))(b); Oracle(a, c, d) },
-        { case (List(a, b, c), d) => PThm(long_atom(a), b, c, list(typ)(d)) }))
+    def term_env(env: Map[String, Typ]): T[Term] =
+    {
+      def env_type(x: String, t: Typ): Typ =
+        if (t == dummyT && env.isDefinedAt(x)) env(x) else t
+
+      def term: T[Term] =
+        variant[Term](List(
+          { case (List(a), b) => Const(a, list(typ)(b)) },
+          { case (List(a), b) => Free(a, env_type(a, typ_body(b))) },
+          { case (a, b) => Var(indexname(a), typ_body(b)) },
+          { case (List(a), Nil) => Bound(int_atom(a)) },
+          { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) },
+          { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) }))
+      term
+    }
+
+    def proof_env(env: Map[String, Typ]): T[Proof] =
+    {
+      val term = term_env(env)
+      def proof: T[Proof] =
+        variant[Proof](List(
+          { case (Nil, Nil) => MinProof },
+          { case (List(a), Nil) => PBound(int_atom(a)) },
+          { case (List(a), b) => val (c, d) = pair(typ, proof)(b); Abst(a, c, d) },
+          { case (List(a), b) => val (c, d) = pair(term, proof)(b); AbsP(a, c, d) },
+          { case (Nil, a) => val (b, c) = pair(proof, term)(a); Appt(b, c) },
+          { case (Nil, a) => val (b, c) = pair(proof, proof)(a); AppP(b, c) },
+          { case (Nil, a) => Hyp(term(a)) },
+          { case (List(a), b) => PAxm(a, list(typ)(b)) },
+          { case (List(a), b) => OfClass(typ(b), a) },
+          { case (List(a), b) => val (c, d) = pair(term, list(typ))(b); Oracle(a, c, d) },
+          { case (List(a, b, c), d) => PThm(long_atom(a), b, c, list(typ)(d)) }))
+      proof
+    }
+
+    val proof: T[Proof] = proof_env(Map.empty)
   }
 }
diff -r c5caf81aa523 -r cc987440d776 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Sat Oct 12 12:25:16 2019 +0200
+++ b/src/Pure/variable.ML	Sat Oct 12 13:43:17 2019 +0200
@@ -265,7 +265,8 @@
 
 val declare_typ = declare_term o Logic.mk_type;
 
-val declare_prf = Proofterm.fold_proof_terms declare_internal (declare_internal o Logic.mk_type);
+val declare_prf =
+  Proofterm.fold_proof_terms_types declare_internal (declare_internal o Logic.mk_type);
 
 val declare_thm = Thm.fold_terms declare_internal;
 
@@ -616,7 +617,7 @@
 
 fun import_prf is_open prf ctxt =
   let
-    val ts = rev (Proofterm.fold_proof_terms cons (cons o Logic.mk_type) prf []);
+    val ts = rev (Proofterm.fold_proof_terms_types cons (cons o Logic.mk_type) prf []);
     val (insts, ctxt') = import_inst is_open ts ctxt;
   in (Proofterm.instantiate insts prf, ctxt') end;