# HG changeset patch
# User wenzelm
# Date 1570195852 -7200
# Node ID 799437173553271829881469d52c59433873db23
# Parent  92f56fbfbab3779047293d12ca98cc39a18c5c8d
Term_XML.Encode/Decode.term uses Const "typargs";

diff -r 92f56fbfbab3 -r 799437173553 NEWS
--- a/NEWS	Wed Oct 02 22:01:04 2019 +0200
+++ b/NEWS	Fri Oct 04 15:30:52 2019 +0200
@@ -58,6 +58,12 @@
 
 *** HOL ***
 
+* Term_XML.Encode/Decode.term uses compact representation of Const
+"typargs" from the given declaration environment. This also makes more
+sense for translations to lambda-calculi with explicit polymorphism.
+INCOMPATIBILITY, use Term_XML.Encode/Decode.term_raw in special
+applications.
+
 * ASCII membership syntax concerning big operators for infimum and
 supremum is gone. INCOMPATIBILITY.
 
@@ -99,6 +105,7 @@
 libraries. See also the module Export_Theory in Isabelle/Scala.
 
 
+
 New in Isabelle2019 (June 2019)
 -------------------------------
 
diff -r 92f56fbfbab3 -r 799437173553 src/HOL/Library/code_test.ML
--- a/src/HOL/Library/code_test.ML	Wed Oct 02 22:01:04 2019 +0200
+++ b/src/HOL/Library/code_test.ML	Fri Oct 04 15:30:52 2019 +0200
@@ -112,7 +112,7 @@
     if size line > size failureN then
       String.extract (line, size failureN, NONE)
       |> YXML.parse_body
-      |> Term_XML.Decode.term
+      |> Term_XML.Decode.term_raw
       |> dest_tuples
       |> SOME
     else NONE)
diff -r 92f56fbfbab3 -r 799437173553 src/HOL/Proofs/ex/XML_Data.thy
--- a/src/HOL/Proofs/ex/XML_Data.thy	Wed Oct 02 22:01:04 2019 +0200
+++ b/src/HOL/Proofs/ex/XML_Data.thy	Fri Oct 04 15:30:52 2019 +0200
@@ -12,12 +12,12 @@
 subsection \<open>Export and re-import of global proof terms\<close>
 
 ML \<open>
-  fun export_proof thm =
-    Proofterm.encode (Thm.clean_proof_of true thm);
+  fun export_proof thy thm =
+    Proofterm.encode (Sign.consts_of thy) (Thm.clean_proof_of true thm);
 
   fun import_proof thy xml =
     let
-      val prf = Proofterm.decode xml;
+      val prf = Proofterm.decode (Sign.consts_of thy) xml;
       val (prf', _) = Proofterm.freeze_thaw_prf prf;
     in Drule.export_without_context (Proof_Checker.thm_of_proof thy prf') end;
 \<close>
@@ -30,26 +30,26 @@
 lemma ex: "A \<longrightarrow> A" ..
 
 ML_val \<open>
-  val xml = export_proof @{thm ex};
+  val xml = export_proof thy1 @{thm ex};
   val thm = import_proof thy1 xml;
 \<close>
 
 ML_val \<open>
-  val xml = export_proof @{thm de_Morgan};
+  val xml = export_proof thy1 @{thm de_Morgan};
   val thm = import_proof thy1 xml;
 \<close>
 
 ML_val \<open>
-  val xml = export_proof @{thm Drinker's_Principle};
+  val xml = export_proof thy1 @{thm Drinker's_Principle};
   val thm = import_proof thy1 xml;
 \<close>
 
 text \<open>Some fairly large proof:\<close>
 
 ML_val \<open>
-  val xml = export_proof @{thm abs_less_iff};
+  val xml = export_proof thy1 @{thm abs_less_iff};
   val thm = import_proof thy1 xml;
-  \<^assert> (size (YXML.string_of_body xml) > 1000000);
+  \<^assert> (size (YXML.string_of_body xml) > 500000);
 \<close>
 
 end
diff -r 92f56fbfbab3 -r 799437173553 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Oct 02 22:01:04 2019 +0200
+++ b/src/Pure/ROOT.ML	Fri Oct 04 15:30:52 2019 +0200
@@ -150,7 +150,6 @@
 
 ML_file "term_ord.ML";
 ML_file "term_subst.ML";
-ML_file "term_xml.ML";
 ML_file "General/completion.ML";
 ML_file "General/name_space.ML";
 ML_file "sorts.ML";
@@ -161,6 +160,7 @@
 ML_file "item_net.ML";
 ML_file "envir.ML";
 ML_file "consts.ML";
+ML_file "term_xml.ML";
 ML_file "primitive_defs.ML";
 ML_file "sign.ML";
 ML_file "defs.ML";
diff -r 92f56fbfbab3 -r 799437173553 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Wed Oct 02 22:01:04 2019 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Fri Oct 04 15:30:52 2019 +0200
@@ -401,7 +401,7 @@
       if is_prop
       then (Markup.language_prop, "prop", "prop", Type.constraint propT)
       else (Markup.language_term, "term", Config.get ctxt Syntax.root, I);
-    val decode = constrain o Term_XML.Decode.term;
+    val decode = constrain o Term_XML.Decode.term (Proof_Context.consts_of ctxt);
   in
     Syntax.parse_input ctxt decode markup
       (fn (syms, pos) =>
diff -r 92f56fbfbab3 -r 799437173553 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Wed Oct 02 22:01:04 2019 +0200
+++ b/src/Pure/Thy/export_theory.ML	Fri Oct 04 15:30:52 2019 +0200
@@ -196,11 +196,14 @@
 
     (* consts *)
 
+    val consts = Sign.consts_of thy;
+    val encode_term = Term_XML.Encode.term consts;
+
     val encode_const =
       let open XML.Encode Term_XML.Encode in
         pair encode_syntax
           (pair (list string)
-            (pair typ (pair (option term) (pair bool (pair (list string) bool)))))
+            (pair typ (pair (option encode_term) (pair bool (pair (list string) bool)))))
       end;
 
     fun export_const c (T, abbrev) =
@@ -211,13 +214,13 @@
         val recursion = primrec_types thy_ctxt (c, U);
         val abbrev' = abbrev
           |> Option.map (Proofterm.standard_vars_term Name.context #> map_types Type.strip_sorts);
-        val args = map (#1 o dest_TFree) (Consts.typargs (Sign.consts_of thy) (c, U0));
+        val args = map (#1 o dest_TFree) (Consts.typargs consts (c, U0));
         val propositional = Object_Logic.is_propositional thy_ctxt (Term.body_type U0);
       in encode_const (syntax, (args, (U0, (abbrev', (propositional, recursion))))) end;
 
     val _ =
       export_entities "consts" (SOME oo export_const) Sign.const_space
-        (#constants (Consts.dest (Sign.consts_of thy)));
+        (#constants (Consts.dest consts));
 
 
     (* axioms *)
@@ -233,7 +236,7 @@
 
     val encode_prop =
       let open XML.Encode Term_XML.Encode
-      in triple (list (pair string sort)) (list (pair string typ)) term end;
+      in triple (list (pair string sort)) (list (pair string typ)) encode_term end;
 
     fun encode_axiom used prop =
       encode_prop (#1 (standard_prop used [] prop NONE));
@@ -268,7 +271,7 @@
       in
         (prop, (deps, proof)) |>
           let open XML.Encode Term_XML.Encode
-          in pair encode_prop (pair (list string) (option Proofterm.encode_full)) end
+          in pair encode_prop (pair (list string) (option (Proofterm.encode_full consts))) end
       end;
 
     fun buffer_export_thm (serial, thm_name) =
@@ -356,7 +359,7 @@
         let
           open XML.Encode Term_XML.Encode;
           val encode_subst =
-            pair (list (pair (pair string sort) typ)) (list (pair (pair string typ) term));
+            pair (list (pair (pair string sort) typ)) (list (pair (pair string typ) (term consts)));
         in pair string (pair string (pair (list (pair string bool)) encode_subst)) end;
 
     val _ =
diff -r 92f56fbfbab3 -r 799437173553 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Wed Oct 02 22:01:04 2019 +0200
+++ b/src/Pure/proofterm.ML	Fri Oct 04 15:30:52 2019 +0200
@@ -59,11 +59,11 @@
   val no_thm_proofs: proof -> proof
   val no_body_proofs: proof -> proof
 
-  val encode: proof XML.Encode.T
-  val encode_body: proof_body XML.Encode.T
-  val encode_full: proof XML.Encode.T
-  val decode: proof XML.Decode.T
-  val decode_body: proof_body XML.Decode.T
+  val encode: Consts.T -> proof XML.Encode.T
+  val encode_body: Consts.T -> proof_body XML.Encode.T
+  val encode_full: Consts.T -> proof XML.Encode.T
+  val decode: Consts.T -> proof XML.Decode.T
+  val decode_body: Consts.T -> proof_body XML.Decode.T
 
   val %> : proof * term -> proof
 
@@ -327,39 +327,40 @@
 
 open XML.Encode Term_XML.Encode;
 
-fun proof prf = prf |> variant
+fun proof consts 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 Abst (a, b, c) => ([a], pair (option typ) (proof consts) (b, c)),
+  fn AbsP (a, b, c) => ([a], pair (option (term consts)) (proof consts) (b, c)),
+  fn a % b => ([], pair (proof consts) (option (term consts)) (a, b)),
+  fn a %% b => ([], pair (proof consts) (proof consts) (a, b)),
+  fn Hyp a => ([], term consts a),
+  fn PAxm (a, b, c) => ([a], pair (term consts) (option (list typ)) (b, c)),
   fn OfClass (a, b) => ([b], typ a),
-  fn Oracle (a, b, c) => ([a], pair (option term) (option (list typ)) (b, c)),
+  fn Oracle (a, b, c) => ([a], pair (option (term consts)) (option (list typ)) (b, c)),
   fn PThm ({serial, pos, theory_name, name, prop, types}, Thm_Body {open_proof, body, ...}) =>
     ([int_atom serial, theory_name, name],
-      pair (list properties) (pair term (pair (option (list typ)) proof_body))
+      pair (list properties) (pair (term consts) (pair (option (list typ)) (proof_body consts)))
         (map Position.properties_of pos, (prop, (types, map_proof_of open_proof (Future.join body)))))]
-and proof_body (PBody {oracles, thms, proof = prf}) =
-  triple (list (pair string (option term))) (list thm) proof (oracles, thms, prf)
-and thm (a, thm_node) =
-  pair int (pair string (pair string (pair term proof_body)))
+and proof_body consts (PBody {oracles, thms, proof = prf}) =
+  triple (list (pair string (option (term consts)))) (list (thm consts)) (proof consts)
+    (oracles, thms, prf)
+and thm consts (a, thm_node) =
+  pair int (pair string (pair string (pair (term consts) (proof_body consts))))
     (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 full_proof prf = prf |> variant
+fun full_proof consts prf = prf |> variant
  [fn MinProof => ([], []),
   fn PBound a => ([int_atom a], []),
-  fn Abst (a, SOME b, c) => ([a], pair typ full_proof (b, c)),
-  fn AbsP (a, SOME b, c) => ([a], pair term full_proof (b, c)),
-  fn a % SOME b => ([], pair full_proof term (a, b)),
-  fn a %% b => ([], pair full_proof full_proof (a, b)),
-  fn Hyp a => ([], term a),
+  fn Abst (a, SOME b, c) => ([a], pair typ (full_proof consts) (b, c)),
+  fn AbsP (a, SOME b, c) => ([a], pair (term consts) (full_proof consts) (b, c)),
+  fn a % SOME b => ([], pair (full_proof consts) (term consts) (a, b)),
+  fn a %% b => ([], pair (full_proof consts) (full_proof consts) (a, b)),
+  fn Hyp a => ([], 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 (option term) (list typ) (prop, Ts)),
+  fn Oracle (name, prop, SOME Ts) => ([name], pair (option (term consts)) (list typ) (prop, Ts)),
   fn PThm ({serial, theory_name, name, types = SOME Ts, ...}, _) =>
     ([int_atom serial, theory_name, name], list typ Ts)];
 
@@ -378,28 +379,33 @@
 
 open XML.Decode Term_XML.Decode;
 
-fun proof prf = prf |> variant
+fun proof consts 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 ([a], b) => let val (c, d) = pair (option typ) (proof consts) b in Abst (a, c, d) end,
+  fn ([a], b) => let val (c, d) = pair (option (term consts)) (proof consts) b in AbsP (a, c, d) end,
+  fn ([], a) => op % (pair (proof consts) (option (term consts)) a),
+  fn ([], a) => op %% (pair (proof consts) (proof consts) a),
+  fn ([], a) => Hyp (term consts a),
+  fn ([a], b) => let val (c, d) = pair (term consts) (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 (option term) (option (list typ)) b in Oracle (a, c, d) end,
+  fn ([a], b) =>
+    let val (c, d) = pair (option (term consts)) (option (list typ)) b in Oracle (a, c, d) end,
   fn ([a, b, c], d) =>
     let
       val ((e, (f, (g, h)))) =
-        pair (list properties) (pair term (pair (option (list typ)) proof_body)) d;
+        pair (list properties) (pair (term consts) (pair (option (list typ)) (proof_body consts))) d;
       val header = thm_header (int_atom a) (map Position.of_properties e) b c f g;
     in PThm (header, thm_body h) end]
-and proof_body x =
-  let val (a, b, c) = triple (list (pair string (option term))) (list thm) proof x
+and proof_body consts x =
+  let
+    val (a, b, c) =
+      triple (list (pair string (option (term consts)))) (list (thm consts)) (proof consts) x;
   in PBody {oracles = a, thms = b, proof = c} end
-and thm x =
-  let val (a, (b, (c, (d, e)))) = pair int (pair string (pair string (pair term proof_body))) x
+and thm consts x =
+  let
+    val (a, (b, (c, (d, e)))) =
+      pair int (pair string (pair string (pair (term consts) (proof_body consts)))) x
   in (a, make_thm_node b c d (Future.value e)) end;
 
 in
@@ -2065,15 +2071,15 @@
 
 fun clean_proof thy = rew_proof thy #> shrink_proof;
 
-fun encode_export prop prf =
+fun encode_export consts prop prf =
   let open XML.Encode Term_XML.Encode
-  in pair term encode_full (prop, prf) end;
+  in pair (term consts) (encode_full consts) (prop, prf) 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 prop' prf';
+    val xml = encode_export (Sign.consts_of thy) prop' prf';
     val chunks = Buffer.chunks (YXML.buffer_body xml Buffer.empty);
   in
     chunks |> Export.export_params
diff -r 92f56fbfbab3 -r 799437173553 src/Pure/term.scala
--- a/src/Pure/term.scala	Wed Oct 02 22:01:04 2019 +0200
+++ b/src/Pure/term.scala	Fri Oct 04 15:30:52 2019 +0200
@@ -40,7 +40,7 @@
   val dummyT = Type("dummy")
 
   sealed abstract class Term
-  case class Const(name: String, typ: Typ = dummyT) extends Term
+  case class Const(name: String, typargs: List[Typ]) extends Term
   case class Free(name: String, typ: Typ = dummyT) extends Term
   case class Var(name: Indexname, typ: Typ = dummyT) extends Term
   case class Bound(index: Int) extends Term
@@ -68,15 +68,14 @@
   val propT: Typ = Type(Pure_Thy.PROP, Nil)
   def funT(ty1: Typ, ty2: Typ): Typ = Type(Pure_Thy.FUN, List(ty1, ty2))
 
-  def mk_type(ty: Typ): Term = Const(Pure_Thy.TYPE, itselfT(ty))
+  def mk_type(ty: Typ): Term = Const(Pure_Thy.TYPE, List(ty))
 
   def const_of_class(c: String): String = c + "_class"
 
   def mk_of_sort(ty: Typ, s: Sort): List[Term] =
   {
-    val class_type = funT(itselfT(ty), propT)
     val t = mk_type(ty)
-    s.map(c => App(Const(const_of_class(c), class_type), t))
+    s.map(c => App(Const(const_of_class(c), List(ty)), t))
   }
 
 
@@ -154,7 +153,7 @@
         case Some(y) => y
         case None =>
           x match {
-            case Const(name, typ) => store(Const(cache_string(name), cache_typ(typ)))
+            case Const(name, typargs) => store(Const(cache_string(name), cache_typs(typargs)))
             case Free(name, typ) => store(Free(cache_string(name), cache_typ(typ)))
             case Var(name, typ) => store(Var(cache_indexname(name), cache_typ(typ)))
             case Bound(_) => store(x)
diff -r 92f56fbfbab3 -r 799437173553 src/Pure/term_xml.ML
--- a/src/Pure/term_xml.ML	Wed Oct 02 22:01:04 2019 +0200
+++ b/src/Pure/term_xml.ML	Fri Oct 04 15:30:52 2019 +0200
@@ -9,7 +9,8 @@
   type 'a T
   val sort: sort T
   val typ: typ T
-  val term: term T
+  val term: Consts.T -> term T
+  val term_raw: term T
 end
 
 signature TERM_XML =
@@ -33,13 +34,21 @@
   fn TFree (a, b) => ([a], sort b),
   fn TVar ((a, b), c) => ([a, int_atom b], sort c)];
 
-fun term t = t |> variant
+fun term consts t = t |> variant
+ [fn Const (a, b) => ([a], list typ (Consts.typargs consts (a, b))),
+  fn Free (a, b) => ([a], typ b),
+  fn Var ((a, b), c) => ([a, int_atom b], typ c),
+  fn Bound a => ([int_atom a], []),
+  fn Abs (a, b, c) => ([a], pair typ (term consts) (b, c)),
+  fn op $ a => ([], pair (term consts) (term consts) a)];
+
+fun term_raw t = t |> variant
  [fn Const (a, b) => ([a], typ b),
   fn Free (a, b) => ([a], typ b),
   fn Var ((a, b), c) => ([a, int_atom b], typ c),
   fn Bound a => ([int_atom a], []),
-  fn Abs (a, b, c) => ([a], pair typ term (b, c)),
-  fn op $ a => ([], pair term term a)];
+  fn Abs (a, b, c) => ([a], pair typ term_raw (b, c)),
+  fn op $ a => ([], pair term_raw term_raw a)];
 
 end;
 
@@ -55,13 +64,21 @@
   fn ([a], b) => TFree (a, sort b),
   fn ([a, b], c) => TVar ((a, int_atom b), sort c)];
 
-fun term t = t |> variant
+fun term consts t = t |> variant
+ [fn ([a], b) => Const (a, Consts.instance consts (a, list typ b)),
+  fn ([a], b) => Free (a, typ b),
+  fn ([a, b], c) => Var ((a, int_atom b), typ c),
+  fn ([a], []) => Bound (int_atom a),
+  fn ([a], b) => let val (c, d) = pair typ (term consts) b in Abs (a, c, d) end,
+  fn ([], a) => op $ (pair (term consts) (term consts) a)];
+
+fun term_raw t = t |> variant
  [fn ([a], b) => Const (a, typ b),
   fn ([a], b) => Free (a, typ b),
   fn ([a, b], c) => Var ((a, int_atom b), typ c),
   fn ([a], []) => Bound (int_atom a),
-  fn ([a], b) => let val (c, d) = pair typ term b in Abs (a, c, d) end,
-  fn ([], a) => op $ (pair term term a)];
+  fn ([a], b) => let val (c, d) = pair typ term_raw b in Abs (a, c, d) end,
+  fn ([], a) => op $ (pair term_raw term_raw a)];
 
 end;
 
diff -r 92f56fbfbab3 -r 799437173553 src/Pure/term_xml.scala
--- a/src/Pure/term_xml.scala	Wed Oct 02 22:01:04 2019 +0200
+++ b/src/Pure/term_xml.scala	Fri Oct 04 15:30:52 2019 +0200
@@ -25,7 +25,7 @@
 
     def term: T[Term] =
       variant[Term](List(
-        { case Const(a, b) => (List(a), typ(b)) },
+        { case Const(a, b) => (List(a), list(typ)(b)) },
         { case Free(a, b) => (List(a), typ(b)) },
         { case Var(Indexname(a, b), c) => (List(a, int_atom(b)), typ(c)) },
         { case Bound(a) => (List(int_atom(a)), Nil) },
@@ -47,7 +47,7 @@
 
     def term: T[Term] =
       variant[Term](List(
-        { case (List(a), b) => Const(a, typ(b)) },
+        { case (List(a), b) => Const(a, list(typ)(b)) },
         { case (List(a), b) => Free(a, typ(b)) },
         { case (List(a, b), c) => Var(Indexname(a, int_atom(b)), typ(c)) },
         { case (List(a), Nil) => Bound(int_atom(a)) },
diff -r 92f56fbfbab3 -r 799437173553 src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Wed Oct 02 22:01:04 2019 +0200
+++ b/src/Tools/Haskell/Haskell.thy	Fri Oct 04 15:30:52 2019 +0200
@@ -1381,7 +1381,7 @@
 
 
 data Term =
-    Const (String, Typ)
+    Const (String, [Typ])
   | Free (String, Typ)
   | Var (Indexname, Typ)
   | Bound Int
@@ -1424,7 +1424,7 @@
 term :: T Term
 term t =
   t |> variant
-   [\case { Const (a, b) -> Just ([a], typ b); _ -> Nothing },
+   [\case { Const (a, b) -> Just ([a], list typ b); _ -> Nothing },
     \case { Free (a, b) -> Just ([a], typ b); _ -> Nothing },
     \case { Var ((a, b), c) -> Just ([a, int_atom b], typ c); _ -> Nothing },
     \case { Bound a -> Just ([int_atom a], []); _ -> Nothing },
@@ -1464,7 +1464,7 @@
 term :: T Term
 term t =
   t |> variant
-   [\([a], b) -> Const (a, typ b),
+   [\([a], b) -> Const (a, list typ b),
     \([a], b) -> Free (a, typ b),
     \([a, b], c) -> Var ((a, int_atom b), typ c),
     \([a], []) -> Bound (int_atom a),