1 (* Title: Pure/General/xml_data.ML |
|
2 Author: Makarius |
|
3 |
|
4 XML as basic data representation language. |
|
5 *) |
|
6 |
|
7 signature XML_DATA_OPS = |
|
8 sig |
|
9 type 'a T |
|
10 val properties: Properties.T T |
|
11 val string: string T |
|
12 val int: int T |
|
13 val bool: bool T |
|
14 val unit: unit T |
|
15 val pair: 'a T -> 'b T -> ('a * 'b) T |
|
16 val triple: 'a T -> 'b T -> 'c T -> ('a * 'b * 'c) T |
|
17 val list: 'a T -> 'a list T |
|
18 val option: 'a T -> 'a option T |
|
19 val variant: 'a T list -> 'a T |
|
20 end; |
|
21 |
|
22 signature XML_DATA = |
|
23 sig |
|
24 structure Encode: XML_DATA_OPS where type 'a T = 'a -> XML.body |
|
25 exception XML_ATOM of string |
|
26 exception XML_BODY of XML.body |
|
27 structure Decode: XML_DATA_OPS where type 'a T = XML.body -> 'a |
|
28 end; |
|
29 |
|
30 structure XML_Data: XML_DATA = |
|
31 struct |
|
32 |
|
33 (** encode **) |
|
34 |
|
35 structure Encode = |
|
36 struct |
|
37 |
|
38 type 'a T = 'a -> XML.body; |
|
39 |
|
40 |
|
41 (* basic values *) |
|
42 |
|
43 fun int_atom i = signed_string_of_int i; |
|
44 |
|
45 fun bool_atom false = "0" |
|
46 | bool_atom true = "1"; |
|
47 |
|
48 fun unit_atom () = ""; |
|
49 |
|
50 |
|
51 (* structural nodes *) |
|
52 |
|
53 fun node ts = XML.Elem ((":", []), ts); |
|
54 |
|
55 fun tagged (tag, ts) = XML.Elem ((int_atom tag, []), ts); |
|
56 |
|
57 |
|
58 (* representation of standard types *) |
|
59 |
|
60 fun properties props = [XML.Elem ((":", props), [])]; |
|
61 |
|
62 fun string "" = [] |
|
63 | string s = [XML.Text s]; |
|
64 |
|
65 val int = string o int_atom; |
|
66 |
|
67 val bool = string o bool_atom; |
|
68 |
|
69 val unit = string o unit_atom; |
|
70 |
|
71 fun pair f g (x, y) = [node (f x), node (g y)]; |
|
72 |
|
73 fun triple f g h (x, y, z) = [node (f x), node (g y), node (h z)]; |
|
74 |
|
75 fun list f xs = map (node o f) xs; |
|
76 |
|
77 fun option _ NONE = [] |
|
78 | option f (SOME x) = [node (f x)]; |
|
79 |
|
80 fun variant fs x = [tagged (the (get_index (fn f => try f x) fs))]; |
|
81 |
|
82 end; |
|
83 |
|
84 |
|
85 |
|
86 (** decode **) |
|
87 |
|
88 exception XML_ATOM of string; |
|
89 exception XML_BODY of XML.tree list; |
|
90 |
|
91 structure Decode = |
|
92 struct |
|
93 |
|
94 type 'a T = XML.body -> 'a; |
|
95 |
|
96 |
|
97 (* basic values *) |
|
98 |
|
99 fun int_atom s = |
|
100 (case Int.fromString s of |
|
101 SOME i => i |
|
102 | NONE => raise XML_ATOM s); |
|
103 |
|
104 fun bool_atom "0" = false |
|
105 | bool_atom "1" = true |
|
106 | bool_atom s = raise XML_ATOM s; |
|
107 |
|
108 fun unit_atom "" = () |
|
109 | unit_atom s = raise XML_ATOM s; |
|
110 |
|
111 |
|
112 (* structural nodes *) |
|
113 |
|
114 fun node (XML.Elem ((":", []), ts)) = ts |
|
115 | node t = raise XML_BODY [t]; |
|
116 |
|
117 fun tagged (XML.Elem ((s, []), ts)) = (int_atom s, ts) |
|
118 | tagged t = raise XML_BODY [t]; |
|
119 |
|
120 |
|
121 (* representation of standard types *) |
|
122 |
|
123 fun properties [XML.Elem ((":", props), [])] = props |
|
124 | properties ts = raise XML_BODY ts; |
|
125 |
|
126 fun string [] = "" |
|
127 | string [XML.Text s] = s |
|
128 | string ts = raise XML_BODY ts; |
|
129 |
|
130 val int = int_atom o string; |
|
131 |
|
132 val bool = bool_atom o string; |
|
133 |
|
134 val unit = unit_atom o string; |
|
135 |
|
136 fun pair f g [t1, t2] = (f (node t1), g (node t2)) |
|
137 | pair _ _ ts = raise XML_BODY ts; |
|
138 |
|
139 fun triple f g h [t1, t2, t3] = (f (node t1), g (node t2), h (node t3)) |
|
140 | triple _ _ _ ts = raise XML_BODY ts; |
|
141 |
|
142 fun list f ts = map (f o node) ts; |
|
143 |
|
144 fun option _ [] = NONE |
|
145 | option f [t] = SOME (f (node t)) |
|
146 | option _ ts = raise XML_BODY ts; |
|
147 |
|
148 fun variant fs [t] = uncurry (nth fs) (tagged t) |
|
149 | variant _ ts = raise XML_BODY ts; |
|
150 |
|
151 end; |
|
152 |
|
153 end; |
|
154 |
|