author | wenzelm |
Fri, 04 Oct 2019 15:30:52 +0200 | |
changeset 70784 | 799437173553 |
parent 43789 | 321ebd051897 |
child 70828 | cb70d84a9f5e |
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 |
|
70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
43789
diff
changeset
|
12 |
val term: Consts.T -> term T |
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
43789
diff
changeset
|
13 |
val term_raw: term T |
43729 | 14 |
end |
15 |
||
16 |
signature TERM_XML = |
|
17 |
sig |
|
43779 | 18 |
structure Encode: TERM_XML_OPS |
19 |
structure Decode: TERM_XML_OPS |
|
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 |
structure Encode = |
43729 | 26 |
struct |
27 |
||
43767 | 28 |
open XML.Encode; |
43729 | 29 |
|
43730
a0ed7bc688b5
lambda terms with XML data representation in Scala;
wenzelm
parents:
43729
diff
changeset
|
30 |
val sort = list string; |
43729 | 31 |
|
32 |
fun typ T = T |> variant |
|
43789 | 33 |
[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
|
34 |
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
|
35 |
fn TVar ((a, b), c) => ([a, int_atom b], sort c)]; |
43729 | 36 |
|
70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
43789
diff
changeset
|
37 |
fun term consts t = t |> variant |
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
43789
diff
changeset
|
38 |
[fn Const (a, b) => ([a], list typ (Consts.typargs consts (a, b))), |
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
43789
diff
changeset
|
39 |
fn Free (a, b) => ([a], typ b), |
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
43789
diff
changeset
|
40 |
fn Var ((a, b), c) => ([a, int_atom b], typ c), |
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
43789
diff
changeset
|
41 |
fn Bound a => ([int_atom a], []), |
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
43789
diff
changeset
|
42 |
fn Abs (a, b, c) => ([a], pair typ (term consts) (b, c)), |
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
43789
diff
changeset
|
43 |
fn op $ a => ([], pair (term consts) (term consts) a)]; |
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
43789
diff
changeset
|
44 |
|
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
43789
diff
changeset
|
45 |
fun term_raw 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
|
46 |
[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
|
47 |
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
|
48 |
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
|
49 |
fn Bound a => ([int_atom a], []), |
70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
43789
diff
changeset
|
50 |
fn Abs (a, b, c) => ([a], pair typ term_raw (b, c)), |
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
43789
diff
changeset
|
51 |
fn op $ a => ([], pair term_raw term_raw a)]; |
43729 | 52 |
|
53 |
end; |
|
54 |
||
43731
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43730
diff
changeset
|
55 |
structure Decode = |
43729 | 56 |
struct |
57 |
||
43767 | 58 |
open XML.Decode; |
43729 | 59 |
|
43730
a0ed7bc688b5
lambda terms with XML data representation in Scala;
wenzelm
parents:
43729
diff
changeset
|
60 |
val sort = list string; |
43729 | 61 |
|
62 |
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
|
63 |
[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
|
64 |
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
|
65 |
fn ([a, b], c) => TVar ((a, int_atom b), sort c)]; |
43729 | 66 |
|
70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
43789
diff
changeset
|
67 |
fun term consts t = t |> variant |
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
43789
diff
changeset
|
68 |
[fn ([a], b) => Const (a, Consts.instance consts (a, list typ b)), |
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
43789
diff
changeset
|
69 |
fn ([a], b) => Free (a, typ b), |
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
43789
diff
changeset
|
70 |
fn ([a, b], c) => Var ((a, int_atom b), typ c), |
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
43789
diff
changeset
|
71 |
fn ([a], []) => Bound (int_atom a), |
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
43789
diff
changeset
|
72 |
fn ([a], b) => let val (c, d) = pair typ (term consts) b in Abs (a, c, d) end, |
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
43789
diff
changeset
|
73 |
fn ([], a) => op $ (pair (term consts) (term consts) a)]; |
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
43789
diff
changeset
|
74 |
|
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
43789
diff
changeset
|
75 |
fun term_raw 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
|
76 |
[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
|
77 |
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
|
78 |
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
|
79 |
fn ([a], []) => Bound (int_atom a), |
70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
43789
diff
changeset
|
80 |
fn ([a], b) => let val (c, d) = pair typ term_raw b in Abs (a, c, d) end, |
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
43789
diff
changeset
|
81 |
fn ([], a) => op $ (pair term_raw term_raw a)]; |
43729 | 82 |
|
83 |
end; |
|
84 |
||
85 |
end; |