author | blanchet |
Fri, 20 Dec 2013 20:36:38 +0100 | |
changeset 54838 | 16511f84913c |
parent 43789 | 321ebd051897 |
child 70784 | 799437173553 |
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 sort: sort T |
|
11 |
val typ: typ T |
|
12 |
val term: term T |
|
13 |
end |
|
14 |
||
15 |
signature TERM_XML = |
|
16 |
sig |
|
43779 | 17 |
structure Encode: TERM_XML_OPS |
18 |
structure Decode: TERM_XML_OPS |
|
43729 | 19 |
end; |
20 |
||
21 |
structure Term_XML: TERM_XML = |
|
22 |
struct |
|
23 |
||
43731
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43730
diff
changeset
|
24 |
structure Encode = |
43729 | 25 |
struct |
26 |
||
43767 | 27 |
open XML.Encode; |
43729 | 28 |
|
43730
a0ed7bc688b5
lambda terms with XML data representation in Scala;
wenzelm
parents:
43729
diff
changeset
|
29 |
val sort = list string; |
43729 | 30 |
|
31 |
fun typ T = T |> variant |
|
43789 | 32 |
[fn Type (a, b) => ([a], list typ b), |
43778
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43767
diff
changeset
|
33 |
fn TFree (a, b) => ([a], sort b), |
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43767
diff
changeset
|
34 |
fn TVar ((a, b), c) => ([a, int_atom b], sort c)]; |
43729 | 35 |
|
36 |
fun term t = t |> variant |
|
43778
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43767
diff
changeset
|
37 |
[fn Const (a, b) => ([a], typ b), |
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43767
diff
changeset
|
38 |
fn Free (a, b) => ([a], typ b), |
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43767
diff
changeset
|
39 |
fn Var ((a, b), c) => ([a, int_atom b], typ c), |
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43767
diff
changeset
|
40 |
fn Bound a => ([int_atom a], []), |
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43767
diff
changeset
|
41 |
fn Abs (a, b, c) => ([a], pair typ term (b, c)), |
43789 | 42 |
fn op $ a => ([], pair term term a)]; |
43729 | 43 |
|
44 |
end; |
|
45 |
||
43731
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43730
diff
changeset
|
46 |
structure Decode = |
43729 | 47 |
struct |
48 |
||
43767 | 49 |
open XML.Decode; |
43729 | 50 |
|
43730
a0ed7bc688b5
lambda terms with XML data representation in Scala;
wenzelm
parents:
43729
diff
changeset
|
51 |
val sort = list string; |
43729 | 52 |
|
53 |
fun typ T = T |> variant |
|
43778
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43767
diff
changeset
|
54 |
[fn ([a], b) => Type (a, list typ b), |
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43767
diff
changeset
|
55 |
fn ([a], b) => TFree (a, sort b), |
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43767
diff
changeset
|
56 |
fn ([a, b], c) => TVar ((a, int_atom b), sort c)]; |
43729 | 57 |
|
58 |
fun term t = t |> variant |
|
43778
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43767
diff
changeset
|
59 |
[fn ([a], b) => Const (a, typ b), |
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43767
diff
changeset
|
60 |
fn ([a], b) => Free (a, typ b), |
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43767
diff
changeset
|
61 |
fn ([a, b], c) => Var ((a, int_atom b), typ c), |
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43767
diff
changeset
|
62 |
fn ([a], []) => Bound (int_atom a), |
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43767
diff
changeset
|
63 |
fn ([a], b) => let val (c, d) = pair typ term b in Abs (a, c, d) end, |
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43767
diff
changeset
|
64 |
fn ([], a) => op $ (pair term term a)]; |
43729 | 65 |
|
66 |
end; |
|
67 |
||
68 |
end; |