--- 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;