--- a/src/Pure/term_xml.ML Fri Oct 11 22:06:49 2019 +0200
+++ b/src/Pure/term_xml.ML Sat Oct 12 12:25:16 2019 +0200
@@ -10,9 +10,9 @@
type 'a P
val indexname: indexname P
val sort: sort T
- val typ_raw: typ T
+ val typ: typ T
val term_raw: term T
- val typ: typ T
+ val typ_body: typ T
val term: Consts.T -> term T
end
@@ -34,25 +34,25 @@
val sort = list string;
-fun typ_raw T = T |> variant
- [fn Type (a, b) => ([a], list typ_raw b),
+fun typ T = T |> variant
+ [fn Type (a, b) => ([a], list typ b),
fn TFree (a, b) => ([a], sort b),
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 Const (a, b) => ([a], typ b),
+ fn Free (a, b) => ([a], typ b),
+ fn Var (a, b) => (indexname a, typ b),
fn Bound a => ([int_atom a], []),
- fn Abs (a, b, c) => ([a], pair typ_raw term_raw (b, c)),
+ fn Abs (a, b, c) => ([a], pair typ 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 typ_body T = if T = dummyT then [] else typ 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) => (indexname a, typ b),
+ fn Free (a, b) => ([a], typ_body b),
+ fn Var (a, b) => (indexname a, typ_body 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)];
@@ -69,25 +69,26 @@
val sort = list string;
-fun typ_raw body = body |> variant
- [fn ([a], b) => Type (a, list typ_raw b),
+fun typ body = body |> variant
+ [fn ([a], b) => Type (a, list typ b),
fn ([a], b) => TFree (a, sort b),
fn (a, b) => TVar (indexname a, sort b)];
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], b) => Const (a, typ b),
+ fn ([a], b) => Free (a, typ b),
+ fn (a, b) => Var (indexname a, typ 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], 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)];
-val typ = option typ_raw #> the_default dummyT;
+fun typ_body [] = dummyT
+ | typ_body body = typ body;
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) => Var (indexname a, typ b),
+ fn ([a], b) => Free (a, typ_body b),
+ fn (a, b) => Var (indexname a, typ_body 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)];
--- a/src/Pure/term_xml.scala Fri Oct 11 22:06:49 2019 +0200
+++ b/src/Pure/term_xml.scala Sat Oct 12 12:25:16 2019 +0200
@@ -21,20 +21,19 @@
val sort: T[Sort] = list(string)
- def typ_raw: T[Typ] =
+ def typ: T[Typ] =
variant[Typ](List(
- { case Type(a, b) => (List(a), list(typ_raw)(b)) },
+ { case Type(a, b) => (List(a), list(typ)(b)) },
{ case TFree(a, b) => (List(a), sort(b)) },
{ case TVar(a, b) => (indexname(a), sort(b)) }))
- val typ: T[Typ] =
- { case t => option(typ_raw)(if (t == dummyT) None else Some(t)) }
+ val typ_body: T[Typ] = (t: Typ) => if (t == dummyT) Nil else typ(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(a, b) => (indexname(a), typ(b)) },
+ { case Free(a, b) => (List(a), typ_body(b)) },
+ { case Var(a, b) => (indexname(a), typ_body(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)) }))
@@ -50,19 +49,19 @@
val sort: T[Sort] = list(string)
- def typ_raw: T[Typ] =
+ def typ: T[Typ] =
variant[Typ](List(
- { case (List(a), b) => Type(a, list(typ_raw)(b)) },
+ { case (List(a), b) => Type(a, list(typ)(b)) },
{ case (List(a), b) => TFree(a, sort(b)) },
{ case (a, b) => TVar(indexname(a), sort(b)) }))
- def typ(body: XML.Body): Typ = option(typ_raw)(body).getOrElse(dummyT)
+ val typ_body: T[Typ] = { case Nil => dummyT case body => typ(body) }
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 (a, b) => Var(indexname(a), typ(b)) },
+ { case (List(a), b) => Free(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) }))