19064
|
1 |
signature XML_CONV =
|
|
2 |
sig
|
|
3 |
type 'a input = XML.tree -> 'a
|
|
4 |
type 'a output = 'a -> XML.tree
|
|
5 |
|
|
6 |
exception ParseException of string
|
|
7 |
|
|
8 |
val xml_of_typ: typ output
|
|
9 |
val typ_of_xml: typ input
|
|
10 |
|
|
11 |
val xml_of_term: term output
|
|
12 |
val term_of_xml : term input
|
|
13 |
|
|
14 |
val xml_of_mixfix: mixfix output
|
|
15 |
val mixfix_of_xml: mixfix input
|
|
16 |
|
|
17 |
val xml_of_proof: Proofterm.proof output
|
|
18 |
|
|
19 |
val xml_of_bool: bool output
|
|
20 |
val bool_of_xml: bool input
|
|
21 |
|
|
22 |
val xml_of_int: int output
|
|
23 |
val int_of_xml: int input
|
|
24 |
|
|
25 |
val xml_of_string: string output
|
|
26 |
val string_of_xml: string input
|
|
27 |
|
|
28 |
val xml_of_list: 'a output -> 'a list output
|
|
29 |
val list_of_xml: 'a input -> 'a list input
|
|
30 |
|
|
31 |
val xml_of_tuple : 'a output -> 'a list output
|
|
32 |
val tuple_of_xml: 'a input -> int -> 'a list input
|
|
33 |
|
|
34 |
val xml_of_option: 'a output -> 'a option output
|
|
35 |
val option_of_xml: 'a input -> 'a option input
|
|
36 |
|
|
37 |
val xml_of_pair: 'a output -> 'b output -> ('a * 'b) output
|
|
38 |
val pair_of_xml: 'a input -> 'b input -> ('a * 'b) input
|
|
39 |
|
|
40 |
val xml_of_triple: 'a output -> 'b output -> 'c output -> ('a * 'b * 'c) output
|
|
41 |
val triple_of_xml: 'a input -> 'b input -> 'c input -> ('a * 'b * 'c) input
|
|
42 |
|
|
43 |
val xml_of_unit: unit output
|
|
44 |
val unit_of_xml: unit input
|
|
45 |
|
|
46 |
val xml_of_quadruple: 'a output -> 'b output -> 'c output -> 'd output -> ('a * 'b * 'c * 'd) output
|
|
47 |
val quadruple_of_xml: 'a input -> 'b input -> 'c input -> 'd input -> ('a * 'b * 'c * 'd) input
|
|
48 |
|
|
49 |
val xml_of_quintuple: 'a output -> 'b output -> 'c output -> 'd output -> 'e output -> ('a * 'b * 'c * 'd * 'e) output
|
|
50 |
val quintuple_of_xml: 'a input -> 'b input -> 'c input -> 'd input -> 'e input -> ('a * 'b * 'c * 'd * 'e) input
|
|
51 |
|
|
52 |
val wrap : string -> 'a output -> 'a output
|
|
53 |
val unwrap : ('a -> 'b) -> 'a input -> 'b input
|
|
54 |
val wrap_empty : string output
|
|
55 |
val unwrap_empty : 'a -> 'a input
|
|
56 |
val name_of_wrap : XML.tree -> string
|
|
57 |
|
|
58 |
val write_to_file: 'a output -> string -> 'a -> unit
|
|
59 |
val read_from_file: 'a input -> string -> 'a
|
19089
|
60 |
|
|
61 |
val serialize_to_file : 'a output -> string -> 'a -> unit
|
|
62 |
val deserialize_from_file : 'a input -> string -> 'a
|
19064
|
63 |
end;
|
|
64 |
|
|
65 |
structure XMLConv : XML_CONV =
|
|
66 |
struct
|
|
67 |
|
|
68 |
type 'a input = XML.tree -> 'a
|
|
69 |
type 'a output = 'a -> XML.tree
|
|
70 |
exception ParseException of string
|
|
71 |
|
|
72 |
fun parse_err s = raise ParseException s
|
|
73 |
|
|
74 |
fun xml_of_class name = XML.Elem ("class", [("name", name)], []);
|
|
75 |
|
|
76 |
fun class_of_xml (XML.Elem ("class", [("name", name)], [])) = name
|
|
77 |
| class_of_xml _ = parse_err "class"
|
|
78 |
|
|
79 |
fun xml_of_typ (TVar ((s, i), S)) = XML.Elem ("TVar",
|
|
80 |
("name", s) :: (if i=0 then [] else [("index", string_of_int i)]),
|
|
81 |
map xml_of_class S)
|
|
82 |
| xml_of_typ (TFree (s, S)) =
|
|
83 |
XML.Elem ("TFree", [("name", s)], map xml_of_class S)
|
|
84 |
| xml_of_typ (Type (s, Ts)) =
|
|
85 |
XML.Elem ("Type", [("name", s)], map xml_of_typ Ts);
|
|
86 |
|
|
87 |
fun intofstr s i =
|
|
88 |
case Int.fromString i of
|
|
89 |
NONE => parse_err (s^", invalid index: "^i)
|
|
90 |
| SOME i => i
|
|
91 |
|
|
92 |
fun typ_of_xml (XML.Elem ("TVar", [("name", s)], cs)) = TVar ((s,0), map class_of_xml cs)
|
|
93 |
| typ_of_xml (XML.Elem ("TVar", [("name", s), ("index", i)], cs)) =
|
|
94 |
TVar ((s, intofstr "TVar" i), map class_of_xml cs)
|
|
95 |
| typ_of_xml (XML.Elem ("TFree", [("name", s)], cs)) = TFree (s, map class_of_xml cs)
|
|
96 |
| typ_of_xml (XML.Elem ("Type", [("name", s)], ts)) = Type (s, map typ_of_xml ts)
|
|
97 |
| typ_of_xml _ = parse_err "type"
|
|
98 |
|
|
99 |
fun xml_of_term (Bound i) =
|
|
100 |
XML.Elem ("Bound", [("index", string_of_int i)], [])
|
|
101 |
| xml_of_term (Free (s, T)) =
|
|
102 |
XML.Elem ("Free", [("name", s)], [xml_of_typ T])
|
|
103 |
| xml_of_term (Var ((s, i), T)) = XML.Elem ("Var",
|
|
104 |
("name", s) :: (if i=0 then [] else [("index", string_of_int i)]),
|
|
105 |
[xml_of_typ T])
|
|
106 |
| xml_of_term (Const (s, T)) =
|
|
107 |
XML.Elem ("Const", [("name", s)], [xml_of_typ T])
|
|
108 |
| xml_of_term (t $ u) =
|
|
109 |
XML.Elem ("App", [], [xml_of_term t, xml_of_term u])
|
|
110 |
| xml_of_term (Abs (s, T, t)) =
|
|
111 |
XML.Elem ("Abs", [("vname", s)], [xml_of_typ T, xml_of_term t]);
|
|
112 |
|
|
113 |
fun term_of_xml (XML.Elem ("Bound", [("index", i)], [])) = Bound (intofstr "Bound" i)
|
|
114 |
| term_of_xml (XML.Elem ("Free", [("name", s)], [T])) = Free (s, typ_of_xml T)
|
|
115 |
| term_of_xml (XML.Elem ("Var",[("name", s)], [T])) = Var ((s,0), typ_of_xml T)
|
|
116 |
| term_of_xml (XML.Elem ("Var",[("name", s), ("index", i)], [T])) = Var ((s,intofstr "Var" i), typ_of_xml T)
|
|
117 |
| term_of_xml (XML.Elem ("Const", [("name", s)], [T])) = Const (s, typ_of_xml T)
|
|
118 |
| term_of_xml (XML.Elem ("App", [], [t, u])) = (term_of_xml t) $ (term_of_xml u)
|
|
119 |
| term_of_xml (XML.Elem ("Abs", [("vname", s)], [T, t])) = Abs (s, typ_of_xml T, term_of_xml t)
|
|
120 |
| term_of_xml _ = parse_err "term"
|
|
121 |
|
|
122 |
fun xml_of_opttypes NONE = []
|
|
123 |
| xml_of_opttypes (SOME Ts) = [XML.Elem ("types", [], map xml_of_typ Ts)];
|
|
124 |
|
|
125 |
(* FIXME: the t argument of PThm and PAxm is actually redundant, since *)
|
|
126 |
(* it can be looked up in the theorem database. Thus, it could be *)
|
|
127 |
(* omitted from the xml representation. *)
|
|
128 |
|
|
129 |
fun xml_of_proof (PBound i) =
|
|
130 |
XML.Elem ("PBound", [("index", string_of_int i)], [])
|
|
131 |
| xml_of_proof (Abst (s, optT, prf)) =
|
|
132 |
XML.Elem ("Abst", [("vname", s)],
|
|
133 |
(case optT of NONE => [] | SOME T => [xml_of_typ T]) @
|
|
134 |
[xml_of_proof prf])
|
|
135 |
| xml_of_proof (AbsP (s, optt, prf)) =
|
|
136 |
XML.Elem ("AbsP", [("vname", s)],
|
|
137 |
(case optt of NONE => [] | SOME t => [xml_of_term t]) @
|
|
138 |
[xml_of_proof prf])
|
|
139 |
| xml_of_proof (prf % optt) =
|
|
140 |
XML.Elem ("Appt", [],
|
|
141 |
xml_of_proof prf ::
|
|
142 |
(case optt of NONE => [] | SOME t => [xml_of_term t]))
|
|
143 |
| xml_of_proof (prf %% prf') =
|
|
144 |
XML.Elem ("AppP", [], [xml_of_proof prf, xml_of_proof prf'])
|
|
145 |
| xml_of_proof (Hyp t) = XML.Elem ("Hyp", [], [xml_of_term t])
|
|
146 |
| xml_of_proof (PThm ((s, _), _, t, optTs)) =
|
|
147 |
XML.Elem ("PThm", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
|
|
148 |
| xml_of_proof (PAxm (s, t, optTs)) =
|
|
149 |
XML.Elem ("PAxm", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
|
|
150 |
| xml_of_proof (Oracle (s, t, optTs)) =
|
|
151 |
XML.Elem ("Oracle", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
|
|
152 |
| xml_of_proof (MinProof _) = XML.Elem ("MinProof", [], []);
|
|
153 |
|
|
154 |
fun xml_of_bool b = XML.Elem ("bool", [("value", if b then "true" else "false")], [])
|
|
155 |
fun xml_of_int i = XML.Elem ("int", [("value", string_of_int i)], [])
|
|
156 |
fun xml_of_string s = XML.Elem ("string", [("value", s)], [])
|
|
157 |
fun xml_of_unit () = XML.Elem ("unit", [], [])
|
|
158 |
fun xml_of_list output ls = XML.Elem ("list", [], map output ls)
|
|
159 |
fun xml_of_tuple output ls = XML.Elem ("tuple", [], map output ls)
|
|
160 |
fun xml_of_option output opt = XML.Elem ("option", [], case opt of NONE => [] | SOME x => [output x])
|
|
161 |
fun wrap s output x = XML.Elem (s, [], [output x])
|
|
162 |
fun wrap_empty s = XML.Elem (s, [], [])
|
|
163 |
fun xml_of_pair output1 output2 (x1, x2) = XML.Elem ("pair", [], [output1 x1, output2 x2])
|
|
164 |
fun xml_of_triple output1 output2 output3 (x1, x2, x3) = XML.Elem ("triple", [], [output1 x1, output2 x2, output3 x3])
|
|
165 |
fun xml_of_quadruple output1 output2 output3 output4 (x1, x2, x3, x4) =
|
|
166 |
XML.Elem ("quadruple", [], [output1 x1, output2 x2, output3 x3, output4 x4])
|
|
167 |
fun xml_of_quintuple output1 output2 output3 output4 output5 (x1, x2, x3, x4, x5) =
|
|
168 |
XML.Elem ("quintuple", [], [output1 x1, output2 x2, output3 x3, output4 x4, output5 x5])
|
|
169 |
|
|
170 |
fun bool_of_xml (XML.Elem ("bool", [("value", "true")], [])) = true
|
|
171 |
| bool_of_xml (XML.Elem ("bool", [("value", "false")], [])) = false
|
|
172 |
| bool_of_xml _ = parse_err "bool"
|
|
173 |
|
|
174 |
fun int_of_xml (XML.Elem ("int", [("value", i)], [])) = intofstr "int" i
|
|
175 |
| int_of_xml _ = parse_err "int"
|
|
176 |
|
|
177 |
fun unit_of_xml (XML.Elem ("unit", [], [])) = ()
|
|
178 |
| unit_of_xml _ = parse_err "unit"
|
|
179 |
|
|
180 |
fun list_of_xml input (XML.Elem ("list", [], ls)) = map input ls
|
|
181 |
| list_of_xml _ _ = parse_err "list"
|
|
182 |
|
|
183 |
fun tuple_of_xml input i (XML.Elem ("tuple", [], ls)) =
|
|
184 |
if i = length ls then map input ls else parse_err "tuple"
|
|
185 |
| tuple_of_xml _ _ _ = parse_err "tuple"
|
|
186 |
|
|
187 |
fun option_of_xml input (XML.Elem ("option", [], [])) = NONE
|
|
188 |
| option_of_xml input (XML.Elem ("option", [], [opt])) = SOME (input opt)
|
|
189 |
| option_of_xml _ _ = parse_err "option"
|
|
190 |
|
|
191 |
fun pair_of_xml input1 input2 (XML.Elem ("pair", [], [x1, x2])) = (input1 x1, input2 x2)
|
|
192 |
| pair_of_xml _ _ _ = parse_err "pair"
|
|
193 |
|
|
194 |
fun triple_of_xml input1 input2 input3 (XML.Elem ("triple", [], [x1, x2, x3])) = (input1 x1, input2 x2, input3 x3)
|
|
195 |
| triple_of_xml _ _ _ _ = parse_err "triple"
|
|
196 |
|
|
197 |
fun quadruple_of_xml input1 input2 input3 input4 (XML.Elem ("quadruple", [], [x1, x2, x3, x4])) =
|
|
198 |
(input1 x1, input2 x2, input3 x3, input4 x4)
|
|
199 |
| quadruple_of_xml _ _ _ _ _ = parse_err "quadruple"
|
|
200 |
|
|
201 |
fun quintuple_of_xml input1 input2 input3 input4 input5 (XML.Elem ("quintuple", [], [x1, x2, x3, x4, x5])) =
|
|
202 |
(input1 x1, input2 x2, input3 x3, input4 x4, input5 x5)
|
|
203 |
| quintuple_of_xml _ _ _ _ _ _ = parse_err "quintuple"
|
|
204 |
|
|
205 |
fun unwrap f input (XML.Elem (_, [], [x])) = f (input x)
|
|
206 |
| unwrap _ _ _ = parse_err "unwrap"
|
|
207 |
|
|
208 |
fun unwrap_empty x (XML.Elem (_, [], [])) = x
|
|
209 |
| unwrap_empty _ _ = parse_err "unwrap_unit"
|
|
210 |
|
|
211 |
fun name_of_wrap (XML.Elem (name, _, _)) = name
|
|
212 |
| name_of_wrap _ = parse_err "name_of_wrap"
|
|
213 |
|
|
214 |
fun string_of_xml (XML.Elem ("string", [("value", s)], [])) = s
|
|
215 |
| string_of_xml _ = parse_err "string"
|
|
216 |
|
|
217 |
fun xml_of_mixfix NoSyn = wrap_empty "nosyn"
|
|
218 |
| xml_of_mixfix Structure = wrap_empty "structure"
|
|
219 |
| xml_of_mixfix (Mixfix args) = wrap "mixfix" (xml_of_triple xml_of_string (xml_of_list xml_of_int) xml_of_int) args
|
|
220 |
| xml_of_mixfix (Delimfix s) = wrap "delimfix" xml_of_string s
|
|
221 |
| xml_of_mixfix (InfixName args) = wrap "infixname" (xml_of_pair xml_of_string xml_of_int) args
|
|
222 |
| xml_of_mixfix (InfixlName args) = wrap "infixlname" (xml_of_pair xml_of_string xml_of_int) args
|
|
223 |
| xml_of_mixfix (InfixrName args) = wrap "infixrname" (xml_of_pair xml_of_string xml_of_int) args
|
|
224 |
| xml_of_mixfix (Infix i) = wrap "infix" xml_of_int i
|
|
225 |
| xml_of_mixfix (Infixl i) = wrap "infixl" xml_of_int i
|
|
226 |
| xml_of_mixfix (Infixr i) = wrap "infixr" xml_of_int i
|
|
227 |
| xml_of_mixfix (Binder args) = wrap "binder" (xml_of_triple xml_of_string xml_of_int xml_of_int) args
|
|
228 |
|
|
229 |
fun mixfix_of_xml e =
|
|
230 |
(case name_of_wrap e of
|
|
231 |
"nosyn" => unwrap_empty NoSyn
|
|
232 |
| "structure" => unwrap_empty Structure
|
|
233 |
| "mixfix" => unwrap Mixfix (triple_of_xml string_of_xml (list_of_xml int_of_xml) int_of_xml)
|
|
234 |
| "delimfix" => unwrap Delimfix string_of_xml
|
|
235 |
| "infixname" => unwrap InfixName (pair_of_xml string_of_xml int_of_xml)
|
|
236 |
| "infixlname" => unwrap InfixlName (pair_of_xml string_of_xml int_of_xml)
|
|
237 |
| "infixrname" => unwrap InfixrName (pair_of_xml string_of_xml int_of_xml)
|
|
238 |
| "infix" => unwrap Infix int_of_xml
|
|
239 |
| "infixl" => unwrap Infixl int_of_xml
|
|
240 |
| "infixr" => unwrap Infixr int_of_xml
|
|
241 |
| "binder" => unwrap Binder (triple_of_xml string_of_xml int_of_xml int_of_xml)
|
|
242 |
| _ => parse_err "mixfix"
|
|
243 |
) e
|
|
244 |
|
|
245 |
|
19089
|
246 |
fun to_file f output fname x = File.write (Path.unpack fname) (f (output x))
|
19064
|
247 |
|
19089
|
248 |
fun from_file f input fname =
|
19064
|
249 |
let
|
|
250 |
val _ = writeln "read_from_file enter"
|
|
251 |
val s = File.read (Path.unpack fname)
|
|
252 |
val _ = writeln "done: read file"
|
19089
|
253 |
val tree = timeit (fn () => f s)
|
19064
|
254 |
val _ = writeln "done: tree"
|
|
255 |
val x = timeit (fn () => input tree)
|
|
256 |
val _ = writeln "done: input"
|
|
257 |
in
|
|
258 |
x
|
|
259 |
end
|
|
260 |
|
19089
|
261 |
fun write_to_file x = to_file XML.string_of_tree x
|
|
262 |
fun read_from_file x = timeit (fn () => (writeln "read_from_file"; from_file XML.tree_of_string x))
|
|
263 |
|
|
264 |
fun serialize_to_file x = to_file XML.encoded_string_of_tree x
|
|
265 |
fun deserialize_from_file x = timeit (fn () => (writeln "deserialize_from_file"; from_file XML.tree_of_encoded_string x))
|
|
266 |
|
19064
|
267 |
end;
|
|
268 |
|
|
269 |
structure XMLConvOutput =
|
|
270 |
struct
|
|
271 |
open XMLConv
|
|
272 |
|
|
273 |
val typ = xml_of_typ
|
|
274 |
val term = xml_of_term
|
|
275 |
val mixfix = xml_of_mixfix
|
|
276 |
val proof = xml_of_proof
|
|
277 |
val bool = xml_of_bool
|
|
278 |
val int = xml_of_int
|
|
279 |
val string = xml_of_string
|
|
280 |
val unit = xml_of_unit
|
|
281 |
val list = xml_of_list
|
|
282 |
val pair = xml_of_pair
|
|
283 |
val option = xml_of_option
|
|
284 |
val triple = xml_of_triple
|
|
285 |
val quadruple = xml_of_quadruple
|
|
286 |
val quintuple = xml_of_quintuple
|
|
287 |
|
|
288 |
end
|
|
289 |
|
|
290 |
structure XMLConvInput =
|
|
291 |
struct
|
|
292 |
open XMLConv
|
|
293 |
|
|
294 |
val typ = typ_of_xml
|
|
295 |
val term = term_of_xml
|
|
296 |
val mixfix = mixfix_of_xml
|
|
297 |
val bool = bool_of_xml
|
|
298 |
val int = int_of_xml
|
|
299 |
val string = string_of_xml
|
|
300 |
val unit = unit_of_xml
|
|
301 |
val list = list_of_xml
|
|
302 |
val pair = pair_of_xml
|
|
303 |
val option = option_of_xml
|
|
304 |
val triple = triple_of_xml
|
|
305 |
val quadruple = quadruple_of_xml
|
|
306 |
val quintuple = quintuple_of_xml
|
|
307 |
|
|
308 |
end
|
|
309 |
|