author | wenzelm |
Tue, 12 Jul 2011 10:44:30 +0200 | |
changeset 43767 | e0219ef7f84c |
parent 43731 | 70072780e095 |
child 43778 | ce9189450447 |
permissions | -rw-r--r-- |
43729 | 1 |
(* Title: Pure/term_xml.ML |
2 |
Author: Makarius |
|
3 |
||
4 |
XML data representation of lambda terms. |
|
5 |
*) |
|
6 |
||
7 |
signature TERM_XML_OPS = |
|
8 |
sig |
|
9 |
type 'a T |
|
10 |
val indexname: indexname T |
|
11 |
val sort: sort T |
|
12 |
val typ: typ T |
|
13 |
val term: term T |
|
14 |
end |
|
15 |
||
16 |
signature TERM_XML = |
|
17 |
sig |
|
43767 | 18 |
structure Encode: TERM_XML_OPS where type 'a T = 'a XML.Encode.T |
19 |
structure Decode: TERM_XML_OPS where type 'a T = 'a XML.Decode.T |
|
43729 | 20 |
end; |
21 |
||
22 |
structure Term_XML: TERM_XML = |
|
23 |
struct |
|
24 |
||
43731
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43730
diff
changeset
|
25 |
(* encode *) |
43729 | 26 |
|
43731
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43730
diff
changeset
|
27 |
structure Encode = |
43729 | 28 |
struct |
29 |
||
43767 | 30 |
open XML.Encode; |
43729 | 31 |
|
32 |
val indexname = pair string int; |
|
43730
a0ed7bc688b5
lambda terms with XML data representation in Scala;
wenzelm
parents:
43729
diff
changeset
|
33 |
|
a0ed7bc688b5
lambda terms with XML data representation in Scala;
wenzelm
parents:
43729
diff
changeset
|
34 |
val sort = list string; |
43729 | 35 |
|
36 |
fun typ T = T |> variant |
|
37 |
[fn Type x => pair string (list typ) x, |
|
38 |
fn TFree x => pair string sort x, |
|
39 |
fn TVar x => pair indexname sort x]; |
|
40 |
||
41 |
fun term t = t |> variant |
|
42 |
[fn Const x => pair string typ x, |
|
43 |
fn Free x => pair string typ x, |
|
44 |
fn Var x => pair indexname typ x, |
|
45 |
fn Bound x => int x, |
|
46 |
fn Abs x => triple string typ term x, |
|
47 |
fn op $ x => pair term term x]; |
|
48 |
||
49 |
end; |
|
50 |
||
51 |
||
43731
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43730
diff
changeset
|
52 |
(* decode *) |
43729 | 53 |
|
43731
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43730
diff
changeset
|
54 |
structure Decode = |
43729 | 55 |
struct |
56 |
||
43767 | 57 |
open XML.Decode; |
43729 | 58 |
|
59 |
val indexname = pair string int; |
|
43730
a0ed7bc688b5
lambda terms with XML data representation in Scala;
wenzelm
parents:
43729
diff
changeset
|
60 |
|
a0ed7bc688b5
lambda terms with XML data representation in Scala;
wenzelm
parents:
43729
diff
changeset
|
61 |
val sort = list string; |
43729 | 62 |
|
63 |
fun typ T = T |> variant |
|
64 |
[Type o pair string (list typ), |
|
65 |
TFree o pair string sort, |
|
66 |
TVar o pair indexname sort]; |
|
67 |
||
68 |
fun term t = t |> variant |
|
69 |
[Const o pair string typ, |
|
70 |
Free o pair string typ, |
|
71 |
Var o pair indexname typ, |
|
72 |
Bound o int, |
|
73 |
Abs o triple string typ term, |
|
74 |
op $ o pair term term]; |
|
75 |
||
76 |
end; |
|
77 |
||
78 |
end; |