1(*  Title:      Pure/term_xml.ML
2    Author:     Makarius
3
4XML data representation of lambda terms.
5*)
6
7signature TERM_XML_OPS =
8sig
9  type 'a T
10  type 'a P
11  val indexname: indexname P
12  val sort: sort T
13  val typ: typ T
14  val term_raw: term T
15  val typ_body: typ T
16  val term: Consts.T -> term T
17end
18
19signature TERM_XML =
20sig
21  structure Encode: TERM_XML_OPS
22  structure Decode: TERM_XML_OPS
23end;
24
25structure Term_XML: TERM_XML =
26struct
27
28structure Encode =
29struct
30
31open XML.Encode;
32
33fun indexname (a, b) = if b = 0 then [a] else [a, int_atom b];
34
35val sort = list string;
36
37fun typ T = T |> variant
38 [fn Type (a, b) => ([a], list typ b),
39  fn TFree (a, b) => ([a], sort b),
40  fn TVar (a, b) => (indexname a, sort b)];
41
42fun term_raw t = t |> variant
43 [fn Const (a, b) => ([a], typ b),
44  fn Free (a, b) => ([a], typ b),
45  fn Var (a, b) => (indexname a, typ b),
46  fn Bound a => ([], int a),
47  fn Abs (a, b, c) => ([a], pair typ term_raw (b, c)),
48  fn op $ a => ([], pair term_raw term_raw a)];
49
50fun typ_body T = if T = dummyT then [] else typ T;
51
52fun term consts t = t |> variant
53 [fn Const (a, b) => ([a], list typ (Consts.typargs consts (a, b))),
54  fn Free (a, b) => ([a], typ_body b),
55  fn Var (a, b) => (indexname a, typ_body b),
56  fn Bound a => ([], int a),
57  fn Abs (a, b, c) => ([a], pair typ (term consts) (b, c)),
58  fn op $ a => ([], pair (term consts) (term consts) a)];
59
60end;
61
62structure Decode =
63struct
64
65open XML.Decode;
66
67fun indexname [a] = (a, 0)
68  | indexname [a, b] = (a, int_atom b);
69
70val sort = list string;
71
72fun typ body = body |> variant
73 [fn ([a], b) => Type (a, list typ b),
74  fn ([a], b) => TFree (a, sort b),
75  fn (a, b) => TVar (indexname a, sort b)];
76
77fun term_raw body = body |> variant
78 [fn ([a], b) => Const (a, typ b),
79  fn ([a], b) => Free (a, typ b),
80  fn (a, b) => Var (indexname a, typ b),
81  fn ([], a) => Bound (int a),
82  fn ([a], b) => let val (c, d) = pair typ term_raw b in Abs (a, c, d) end,
83  fn ([], a) => op $ (pair term_raw term_raw a)];
84
85fun typ_body [] = dummyT
86  | typ_body body = typ body;
87
88fun term consts body = body |> variant
89 [fn ([a], b) => Const (a, Consts.instance consts (a, list typ b)),
90  fn ([a], b) => Free (a, typ_body b),
91  fn (a, b) => Var (indexname a, typ_body b),
92  fn ([], a) => Bound (int a),
93  fn ([a], b) => let val (c, d) = pair typ (term consts) b in Abs (a, c, d) end,
94  fn ([], a) => op $ (pair (term consts) (term consts) a)];
95
96end;
97
98end;
99