--- a/src/Pure/PIDE/xml.ML Thu Oct 10 15:52:30 2019 +0200
+++ b/src/Pure/PIDE/xml.ML Thu Oct 10 16:51:47 2019 +0200
@@ -11,6 +11,7 @@
type 'a A
type 'a T
type 'a V
+ type 'a P
val int_atom: int A
val bool_atom: bool A
val unit_atom: unit A
@@ -290,6 +291,7 @@
type 'a A = 'a -> string;
type 'a T = 'a -> body;
type 'a V = 'a -> string list * body;
+type 'a P = 'a -> string list;
(* atomic values *)
@@ -347,6 +349,7 @@
type 'a A = string -> 'a;
type 'a T = body -> 'a;
type 'a V = string list * body -> 'a;
+type 'a P = string list -> 'a;
(* atomic values *)
--- a/src/Pure/PIDE/xml.scala Thu Oct 10 15:52:30 2019 +0200
+++ b/src/Pure/PIDE/xml.scala Thu Oct 10 16:51:47 2019 +0200
@@ -241,6 +241,7 @@
{
type T[A] = A => XML.Body
type V[A] = PartialFunction[A, (List[String], XML.Body)]
+ type P[A] = PartialFunction[A, List[String]]
/* atomic values */
@@ -309,6 +310,7 @@
{
type T[A] = XML.Body => A
type V[A] = (List[String], XML.Body) => A
+ type P[A] = PartialFunction[List[String], A]
/* atomic values */
--- a/src/Pure/term_xml.ML Thu Oct 10 15:52:30 2019 +0200
+++ b/src/Pure/term_xml.ML Thu Oct 10 16:51:47 2019 +0200
@@ -7,10 +7,13 @@
signature TERM_XML_OPS =
sig
type 'a T
+ type 'a P
+ val indexname: indexname P
val sort: sort T
+ val typ_raw: typ T
+ val term_raw: term T
val typ: typ T
val term: Consts.T -> term T
- val term_raw: term T
end
signature TERM_XML =
@@ -27,29 +30,33 @@
open XML.Encode;
+fun indexname (a, b) = if b = 0 then [a] else [a, int_atom b];
+
val sort = list string;
-fun typ T = T |> variant
- [fn Type (a, b) => ([a], list typ b),
+fun typ_raw T = T |> variant
+ [fn Type (a, b) => ([a], list typ_raw b),
fn TFree (a, b) => ([a], sort b),
- fn TVar ((a, b), c) => ([a, int_atom b], sort c)];
+ fn TVar (a, b) => (indexname a, sort b)];
+
+fun term_raw t = t |> variant
+ [fn Const (a, b) => ([a], typ_raw b),
+ fn Free (a, b) => ([a], typ_raw b),
+ fn Var (a, b) => (indexname a, typ_raw b),
+ fn Bound a => ([int_atom a], []),
+ fn Abs (a, b, c) => ([a], pair typ_raw term_raw (b, c)),
+ fn op $ a => ([], pair term_raw term_raw a)];
+
+fun typ T = option typ_raw (if T = dummyT then NONE else SOME T);
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 Var (a, b) => (indexname a, typ b),
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_raw (b, c)),
- fn op $ a => ([], pair term_raw term_raw a)];
-
end;
structure Decode =
@@ -57,29 +64,34 @@
open XML.Decode;
+fun indexname [a] = (a, 0)
+ | indexname [a, b] = (a, int_atom b);
+
val sort = list string;
-fun typ T = T |> variant
- [fn ([a], b) => Type (a, list typ b),
+fun typ_raw body = body |> variant
+ [fn ([a], b) => Type (a, list typ_raw b),
fn ([a], b) => TFree (a, sort b),
- fn ([a, b], c) => TVar ((a, int_atom b), sort c)];
+ fn (a, b) => TVar (indexname a, sort b)];
-fun term consts t = t |> variant
+fun term_raw body = body |> variant
+ [fn ([a], b) => Const (a, typ_raw b),
+ fn ([a], b) => Free (a, typ_raw b),
+ fn (a, b) => Var (indexname a, typ_raw b),
+ fn ([a], []) => Bound (int_atom a),
+ fn ([a], b) => let val (c, d) = pair typ_raw term_raw b in Abs (a, c, d) end,
+ fn ([], a) => op $ (pair term_raw term_raw a)];
+
+val typ = option typ_raw #> the_default dummyT;
+
+fun term consts body = body |> 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, b) => Var (indexname a, typ b),
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_raw b in Abs (a, c, d) end,
- fn ([], a) => op $ (pair term_raw term_raw a)];
-
end;
end;
--- a/src/Pure/term_xml.scala Thu Oct 10 15:52:30 2019 +0200
+++ b/src/Pure/term_xml.scala Thu Oct 10 16:51:47 2019 +0200
@@ -15,19 +15,26 @@
{
import XML.Encode._
+ val indexname: P[Indexname] =
+ { case Indexname(a, 0) => List(a)
+ case Indexname(a, b) => List(a, int_atom(b)) }
+
val sort: T[Sort] = list(string)
- def typ: T[Typ] =
+ def typ_raw: T[Typ] =
variant[Typ](List(
- { case Type(a, b) => (List(a), list(typ)(b)) },
+ { case Type(a, b) => (List(a), list(typ_raw)(b)) },
{ case TFree(a, b) => (List(a), sort(b)) },
- { case TVar(Indexname(a, b), c) => (List(a, int_atom(b)), sort(c)) }))
+ { case TVar(a, b) => (indexname(a), sort(b)) }))
+
+ val typ: T[Typ] =
+ { case t => option(typ_raw)(if (t == dummyT) None else Some(t)) }
def term: T[Term] =
variant[Term](List(
{ 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 Var(a, b) => (indexname(a), typ(b)) },
{ case Bound(a) => (List(int_atom(a)), Nil) },
{ case Abs(a, b, c) => (List(a), pair(typ, term)(b, c)) },
{ case App(a, b) => (Nil, pair(term, term)(a, b)) }))
@@ -37,19 +44,25 @@
{
import XML.Decode._
+ val indexname: P[Indexname] =
+ { case List(a) => Indexname(a, 0)
+ case List(a, b) => Indexname(a, int_atom(b)) }
+
val sort: T[Sort] = list(string)
- def typ: T[Typ] =
+ def typ_raw: T[Typ] =
variant[Typ](List(
- { case (List(a), b) => Type(a, list(typ)(b)) },
+ { case (List(a), b) => Type(a, list(typ_raw)(b)) },
{ case (List(a), b) => TFree(a, sort(b)) },
- { case (List(a, b), c) => TVar(Indexname(a, int_atom(b)), sort(c)) }))
+ { case (a, b) => TVar(indexname(a), sort(b)) }))
+
+ def typ(body: XML.Body): Typ = option(typ_raw)(body).getOrElse(dummyT)
def term: T[Term] =
variant[Term](List(
{ 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 (a, b) => Var(indexname(a), typ(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) }))