2 Author: David Aspinall |
2 Author: David Aspinall |
3 |
3 |
4 PGIP abstraction: types and conversions. |
4 PGIP abstraction: types and conversions. |
5 *) |
5 *) |
6 |
6 |
7 (* TODO: PGML, proverflag *) |
|
8 signature PGIPTYPES = |
7 signature PGIPTYPES = |
9 sig |
8 sig |
10 (* Object types: the types of values which can be manipulated externally. |
|
11 Ideally a list of other types would be configured as a parameter. *) |
|
12 datatype objtype = ObjFile | ObjTheory | ObjTheorem | ObjComment |
|
13 | ObjTerm | ObjType | ObjOther of string |
|
14 |
|
15 (* Names for values of objtypes (i.e. prover identifiers). Could be a parameter. |
|
16 Names for ObjFiles are URIs. *) |
|
17 type objname = string |
|
18 |
|
19 type idtable = { context: objname option, (* container's objname *) |
|
20 objtype: objtype, |
|
21 ids: objname list } |
|
22 |
|
23 (* Types and values (used for preferences and dialogs) *) |
9 (* Types and values (used for preferences and dialogs) *) |
24 |
10 |
25 datatype pgiptype = |
11 datatype pgiptype = |
26 Pgipnull | Pgipbool | Pgipint of int option * int option | Pgipnat | Pgipreal |
12 Pgipnull | Pgipbool | Pgipint of int option * int option | Pgipnat | Pgipreal |
27 | Pgipstring | Pgipconst of string | Pgipchoice of pgipdtype list |
13 | Pgipstring | Pgipconst of string | Pgipchoice of pgipdtype list |
28 |
14 |
29 and pgipdtype = Pgipdtype of string option * pgiptype (* type with opt. description *) |
15 and pgipdtype = Pgipdtype of string option * pgiptype (* type with opt. description *) |
30 |
16 |
31 type pgipval (* typed value *) |
|
32 |
|
33 (* URLs we can cope with *) |
|
34 type pgipurl |
|
35 |
|
36 (* Representation error in reading/writing PGIP *) |
|
37 exception PGIP of string |
17 exception PGIP of string |
38 |
|
39 (* Interface areas for message output *) |
|
40 datatype displayarea = Status | Message | Display | Tracing | Internal | Other of string |
|
41 |
|
42 (* Error levels *) |
|
43 datatype fatality = Info | Warning | Nonfatal | Fatal | Panic | Log | Debug |
|
44 |
|
45 (* File location *) |
|
46 type location = { descr: string option, |
|
47 url: pgipurl option, |
|
48 line: int option, |
|
49 column: int option, |
|
50 char: int option, |
|
51 length: int option } |
|
52 end |
|
53 |
|
54 signature PGIPTYPES_OPNS = |
|
55 sig |
|
56 include PGIPTYPES |
|
57 |
18 |
58 (* Object types *) |
|
59 val name_of_objtype : objtype -> string |
|
60 val attrs_of_objtype : objtype -> XML.attributes |
|
61 val objtype_of_attrs : XML.attributes -> objtype (* raises PGIP *) |
|
62 val idtable_to_xml : idtable -> XML.tree |
|
63 |
|
64 (* Values as XML strings *) |
19 (* Values as XML strings *) |
65 val read_pgipint : (int option * int option) -> string -> int (* raises PGIP *) |
20 val read_pgipint : (int option * int option) -> string -> int (* raises PGIP *) |
66 val read_pgipnat : string -> int (* raises PGIP *) |
21 val read_pgipnat : string -> int (* raises PGIP *) |
67 val read_pgipbool : string -> bool (* raises PGIP *) |
22 val read_pgipbool : string -> bool (* raises PGIP *) |
68 val read_pgipreal : string -> real (* raises PGIP *) |
23 val read_pgipreal : string -> real (* raises PGIP *) |
72 val bool_to_pgstring : bool -> string |
27 val bool_to_pgstring : bool -> string |
73 val string_to_pgstring : string -> string |
28 val string_to_pgstring : string -> string |
74 |
29 |
75 (* PGIP datatypes *) |
30 (* PGIP datatypes *) |
76 val pgiptype_to_xml : pgiptype -> XML.tree |
31 val pgiptype_to_xml : pgiptype -> XML.tree |
77 val read_pgval : pgiptype -> string -> pgipval (* raises PGIP *) |
|
78 val pgval_to_string : pgipval -> string |
|
79 |
|
80 val attrs_of_displayarea : displayarea -> XML.attributes |
|
81 val attrs_of_fatality : fatality -> XML.attributes |
|
82 val attrs_of_location : location -> XML.attributes |
|
83 val location_of_attrs : XML.attributes -> location (* raises PGIP *) |
|
84 |
|
85 val pgipurl_of_url : Url.T -> pgipurl (* raises PGIP *) |
|
86 val pgipurl_of_string : string -> pgipurl (* raises PGIP *) |
|
87 val pgipurl_of_path : Path.T -> pgipurl |
|
88 val path_of_pgipurl : pgipurl -> Path.T |
|
89 val string_of_pgipurl : pgipurl -> string |
|
90 val attrs_of_pgipurl : pgipurl -> XML.attributes |
|
91 val pgipurl_of_attrs : XML.attributes -> pgipurl (* raises PGIP *) |
|
92 |
32 |
93 (* XML utils, only for PGIP code *) |
33 (* XML utils, only for PGIP code *) |
94 val attr : string -> string -> XML.attributes |
34 val attr : string -> string -> XML.attributes |
95 val opt_attr : string -> string option -> XML.attributes |
35 val opt_attr : string -> string option -> XML.attributes |
96 val opt_attr_map : ('a -> string) -> string -> 'a option -> XML.attributes |
36 val opt_attr_map : ('a -> string) -> string -> 'a option -> XML.attributes |
97 val get_attr : string -> XML.attributes -> string (* raises PGIP *) |
37 val get_attr : string -> XML.attributes -> string (* raises PGIP *) |
98 val get_attr_opt : string -> XML.attributes -> string option |
38 val get_attr_opt : string -> XML.attributes -> string option |
99 val get_attr_dflt : string -> string -> XML.attributes -> string |
39 val get_attr_dflt : string -> string -> XML.attributes -> string |
100 end |
40 end |
101 |
41 |
102 structure PgipTypes : PGIPTYPES_OPNS = |
42 structure PgipTypes : PGIPTYPES = |
103 struct |
43 struct |
|
44 |
104 exception PGIP of string |
45 exception PGIP of string |
105 |
46 |
106 (** XML utils **) |
47 (** XML utils **) |
107 |
48 |
108 fun get_attr_opt attr attrs = Properties.get attrs attr |
49 fun get_attr_opt attr attrs = Properties.get attrs attr |
121 (* or, if you've got function-itis: |
62 (* or, if you've got function-itis: |
122 the_default [] (Option.map (single o (pair attr_name) o f) opt_val) |
63 the_default [] (Option.map (single o (pair attr_name) o f) opt_val) |
123 *) |
64 *) |
124 |
65 |
125 fun opt_attr attr_name = opt_attr_map I attr_name |
66 fun opt_attr attr_name = opt_attr_map I attr_name |
126 |
|
127 |
|
128 (** Objtypes **) |
|
129 |
|
130 datatype objtype = ObjFile | ObjTheory | ObjTheorem | ObjComment |
|
131 | ObjTerm | ObjType | ObjOther of string |
|
132 |
|
133 fun name_of_objtype obj = |
|
134 case obj of |
|
135 ObjFile => "file" |
|
136 | ObjTheory => "theory" |
|
137 | ObjTheorem => "theorem" |
|
138 | ObjComment => "comment" |
|
139 | ObjTerm => "term" |
|
140 | ObjType => "type" |
|
141 | ObjOther s => s |
|
142 |
|
143 val attrs_of_objtype = attr "objtype" o name_of_objtype |
|
144 |
|
145 fun objtype_of_attrs attrs = case get_attr "objtype" attrs of |
|
146 "file" => ObjFile |
|
147 | "theory" => ObjTheory |
|
148 | "theorem" => ObjTheorem |
|
149 | "comment" => ObjComment |
|
150 | "term" => ObjTerm |
|
151 | "type" => ObjType |
|
152 | s => ObjOther s (* where s mem other_objtypes_parameter *) |
|
153 |
|
154 type objname = string |
|
155 type idtable = { context: objname option, (* container's objname *) |
|
156 objtype: objtype, |
|
157 ids: objname list } |
|
158 |
|
159 fun idtable_to_xml {context, objtype, ids} = |
|
160 let |
|
161 val objtype_attrs = attrs_of_objtype objtype |
|
162 val context_attrs = opt_attr "context" context |
|
163 val ids_content = map (fn x => XML.Elem(("identifier", []), [XML.Text x])) ids |
|
164 in |
|
165 XML.Elem (("idtable", objtype_attrs @ context_attrs), ids_content) |
|
166 end |
|
167 |
67 |
168 |
68 |
169 (** Types and values **) |
69 (** Types and values **) |
170 |
70 |
171 (* readers and writers for values represented in XML strings *) |
71 (* readers and writers for values represented in XML strings *) |
286 XML.Elem ((elt, desc_attr @ attrs), map pgipdtype_to_xml typargs) |
186 XML.Elem ((elt, desc_attr @ attrs), map pgipdtype_to_xml typargs) |
287 end |
187 end |
288 |
188 |
289 val pgiptype_to_xml = pgipdtype_to_xml o pair NONE |
189 val pgiptype_to_xml = pgipdtype_to_xml o pair NONE |
290 |
190 |
291 fun read_pguval Pgipnull s = |
|
292 if s="" then Pgvalnull |
|
293 else raise PGIP ("Expecting empty string for null type, not: " ^ quote s) |
|
294 | read_pguval Pgipbool s = Pgvalbool (read_pgipbool s) |
|
295 | read_pguval (Pgipint range) s = Pgvalint (read_pgipint range s) |
|
296 | read_pguval Pgipnat s = Pgvalnat (read_pgipnat s) |
|
297 | read_pguval Pgipreal s = Pgvalreal (read_pgipreal s) |
|
298 | read_pguval (Pgipconst c) s = |
|
299 if c=s then Pgvalconst c |
|
300 else raise PGIP ("Given string: "^quote s^" doesn't match expected string: "^quote c) |
|
301 | read_pguval Pgipstring s = |
|
302 if s<>"" then Pgvalstring s |
|
303 else raise PGIP ("Expecting non-empty string, empty string illegal.") |
|
304 | read_pguval (Pgipchoice tydescs) s = |
|
305 let |
|
306 (* Union type: match first in list *) |
|
307 fun getty (Pgipdtype(_, ty)) = ty |
|
308 val uval = get_first |
|
309 (fn ty => SOME (read_pguval ty s) handle PGIP _ => NONE) |
|
310 (map getty tydescs) |
|
311 in |
|
312 case uval of SOME pgv => pgv | NONE => raise PGIP ("Can't match string: "^quote s^ |
|
313 " against any allowed types.") |
|
314 end |
|
315 |
|
316 fun read_pgval ty s = (ty, read_pguval ty s) |
|
317 |
|
318 fun pgval_to_string (_, Pgvalnull) = "" |
|
319 | pgval_to_string (_, Pgvalbool b) = bool_to_pgstring b |
|
320 | pgval_to_string (_, Pgvalnat n) = int_to_pgstring n |
|
321 | pgval_to_string (_, Pgvalint i) = int_to_pgstring i |
|
322 | pgval_to_string (_, Pgvalreal x) = real_to_pgstring x |
|
323 | pgval_to_string (_, Pgvalconst c) = string_to_pgstring c |
|
324 | pgval_to_string (_, Pgvalstring s) = string_to_pgstring s |
|
325 |
|
326 |
|
327 type pgipurl = Path.T (* URLs: only local files *) |
|
328 |
|
329 datatype displayarea = Status | Message | Display | Tracing | Internal | Other of string |
|
330 |
|
331 datatype fatality = Info | Warning | Nonfatal | Fatal | Panic | Log | Debug |
|
332 |
|
333 type location = { descr: string option, |
|
334 url: pgipurl option, |
|
335 line: int option, |
|
336 column: int option, |
|
337 char: int option, |
|
338 length: int option } |
|
339 |
|
340 |
|
341 |
|
342 (** Url operations **) |
|
343 |
|
344 |
|
345 fun pgipurl_of_string url = (* only handle file:/// or file://localhost/ *) |
|
346 case Url.explode url of |
|
347 (Url.File path) => path |
|
348 | _ => raise PGIP ("Cannot access non-local URL " ^ quote url) |
|
349 |
|
350 fun pgipurl_of_path p = p |
|
351 |
|
352 fun path_of_pgipurl p = p (* potentially raises PGIP, but not with this implementation *) |
|
353 |
|
354 fun string_of_pgipurl p = Path.implode p |
|
355 |
|
356 fun attrval_of_pgipurl purl = |
|
357 "file:" ^ XML.text (File.platform_path (File.full_path Path.current purl)) |
|
358 |
|
359 fun attrs_of_pgipurl purl = [("url", attrval_of_pgipurl purl)] |
|
360 |
|
361 val pgipurl_of_attrs = pgipurl_of_string o get_attr "url" |
|
362 |
|
363 fun pgipurl_of_url (Url.File p) = p |
|
364 | pgipurl_of_url url = |
|
365 raise PGIP ("Cannot access non-local/non-file URL " ^ quote (Url.implode url)) |
|
366 |
|
367 |
|
368 (** Messages and errors **) |
|
369 |
|
370 local |
|
371 fun string_of_area Status = "status" |
|
372 | string_of_area Message = "message" |
|
373 | string_of_area Display = "display" |
|
374 | string_of_area Tracing = "tracing" |
|
375 | string_of_area Internal = "internal" |
|
376 | string_of_area (Other s) = s |
|
377 |
|
378 fun string_of_fatality Info = "info" |
|
379 | string_of_fatality Warning = "warning" |
|
380 | string_of_fatality Nonfatal = "nonfatal" |
|
381 | string_of_fatality Fatal = "fatal" |
|
382 | string_of_fatality Panic = "panic" |
|
383 | string_of_fatality Log = "log" |
|
384 | string_of_fatality Debug = "debug" |
|
385 in |
|
386 fun attrs_of_displayarea area = [("area", string_of_area area)] |
|
387 |
|
388 fun attrs_of_fatality fatality = [("fatality", string_of_fatality fatality)] |
|
389 |
|
390 fun attrs_of_location ({ descr, url, line, column, char, length }:location) = |
|
391 let |
|
392 val descr = opt_attr "location_descr" descr |
|
393 val url = opt_attr_map attrval_of_pgipurl "location_url" url |
|
394 val line = opt_attr_map int_to_pgstring "locationline" line |
|
395 val column = opt_attr_map int_to_pgstring "locationcolumn" column |
|
396 val char = opt_attr_map int_to_pgstring "locationcharacter" char |
|
397 val length = opt_attr_map int_to_pgstring "locationlength" length |
|
398 in |
|
399 descr @ url @ line @ column @ char @ length |
|
400 end |
|
401 |
|
402 fun pgipint_of_string err s = |
|
403 case Int.fromString s of |
|
404 SOME i => i |
|
405 | NONE => raise PGIP ("Type error in " ^ quote err ^ ": expected integer.") |
|
406 |
|
407 fun location_of_attrs attrs = |
|
408 let |
|
409 val descr = get_attr_opt "location_descr" attrs |
|
410 val url = Option.map pgipurl_of_string (get_attr_opt "location_url" attrs) |
|
411 val line = Option.map (pgipint_of_string "location element line attribute") |
|
412 (get_attr_opt "locationline" attrs) |
|
413 val column = Option.map (pgipint_of_string "location element column attribute") |
|
414 (get_attr_opt "locationcolumn" attrs) |
|
415 val char = Option.map (pgipint_of_string "location element char attribute") |
|
416 (get_attr_opt "locationcharacter" attrs) |
|
417 val length = Option.map (pgipint_of_string "location element length attribute") |
|
418 (get_attr_opt "locationlength" attrs) |
|
419 in |
|
420 {descr=descr, url=url, line=line, column=column, char=char, length=length} |
|
421 end |
|
422 end |
191 end |
423 |
192 |
424 end |
|
425 |
|