--- 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)
-------------------------------
--- 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)
--- 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
--- 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";
--- 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) =>
--- 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 _ =
--- 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
--- 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)
--- 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;
--- 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)) },
--- 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),