1 (* Title: Pure/ProofGeneral/pgip_types.ML |
1 (* Title: Pure/ProofGeneral/pgip_types.ML |
2 Author: David Aspinall |
2 Author: David Aspinall |
3 |
3 |
4 PGIP abstraction: types and conversions. |
4 Some PGIP types and conversions. |
5 *) |
5 *) |
6 |
6 |
7 signature PGIPTYPES = |
7 signature PGIPTYPES = |
8 sig |
8 sig |
9 (* Types and values (used for preferences and dialogs) *) |
9 val attr: string -> string -> XML.attributes |
|
10 val opt_attr: string -> string option -> XML.attributes |
|
11 val get_attr: XML.attributes -> string -> string (* raises PGIP *) |
10 |
12 |
11 datatype pgiptype = |
13 datatype pgiptype = |
12 Pgipnull | Pgipbool | Pgipint of int option * int option | Pgipnat | Pgipreal |
14 Pgipnull | Pgipbool | Pgipint of int option * int option | Pgipnat | Pgipreal |
13 | Pgipstring | Pgipconst of string | Pgipchoice of pgipdtype list |
15 | Pgipstring | Pgipconst of string | Pgipchoice of pgipdtype list |
14 |
16 |
15 and pgipdtype = Pgipdtype of string option * pgiptype (* type with opt. description *) |
17 and pgipdtype = Pgipdtype of string option * pgiptype (* type with opt. description *) |
16 |
18 |
17 exception PGIP of string |
19 exception PGIP of string |
18 |
|
19 (* Values as XML strings *) |
|
20 val read_pgipint : (int option * int option) -> string -> int (* raises PGIP *) |
|
21 val read_pgipnat : string -> int (* raises PGIP *) |
|
22 val read_pgipbool : string -> bool (* raises PGIP *) |
|
23 val read_pgipreal : string -> real (* raises PGIP *) |
|
24 val read_pgipstring : string -> string (* raises PGIP *) |
|
25 val real_to_pgstring : real -> string |
|
26 val int_to_pgstring : int -> string |
|
27 val bool_to_pgstring : bool -> string |
|
28 val string_to_pgstring : string -> string |
|
29 |
20 |
30 (* PGIP datatypes *) |
21 (* Values as XML strings *) |
31 val pgiptype_to_xml : pgiptype -> XML.tree |
22 val read_pgipint : (int option * int option) -> string -> int (* raises PGIP *) |
|
23 val read_pgipnat : string -> int (* raises PGIP *) |
|
24 val read_pgipbool : string -> bool (* raises PGIP *) |
|
25 val read_pgipreal : string -> real (* raises PGIP *) |
|
26 val read_pgipstring : string -> string (* raises PGIP *) |
|
27 val real_to_pgstring : real -> string |
|
28 val int_to_pgstring : int -> string |
|
29 val bool_to_pgstring : bool -> string |
|
30 val string_to_pgstring : string -> string |
32 |
31 |
33 (* XML utils, only for PGIP code *) |
32 (* PGIP datatypes *) |
34 val attr : string -> string -> XML.attributes |
33 val pgiptype_to_xml : pgiptype -> XML.tree |
35 val opt_attr : string -> string option -> XML.attributes |
|
36 val opt_attr_map : ('a -> string) -> string -> 'a option -> XML.attributes |
|
37 val get_attr : string -> XML.attributes -> string (* raises PGIP *) |
|
38 val get_attr_opt : string -> XML.attributes -> string option |
|
39 val get_attr_dflt : string -> string -> XML.attributes -> string |
|
40 end |
34 end |
41 |
35 |
42 structure PgipTypes : PGIPTYPES = |
36 structure PgipTypes : PGIPTYPES = |
43 struct |
37 struct |
44 |
38 |
45 exception PGIP of string |
39 exception PGIP of string |
46 |
40 |
47 (** XML utils **) |
41 (** XML utils **) |
48 |
42 |
49 fun get_attr_opt attr attrs = Properties.get attrs attr |
43 fun get_attr attrs name = |
50 |
44 (case Properties.get attrs name of |
51 fun get_attr attr attrs = |
45 SOME value => value |
52 (case get_attr_opt attr attrs of |
46 | NONE => raise PGIP ("Missing attribute: " ^ quote name)); |
53 SOME value => value |
|
54 | NONE => raise PGIP ("Missing attribute: " ^ quote attr)) |
|
55 |
|
56 fun get_attr_dflt attr dflt attrs = the_default dflt (get_attr_opt attr attrs) |
|
57 |
47 |
58 fun attr x y = [(x,y)] : XML.attributes |
48 fun attr x y = [(x,y)] : XML.attributes |
59 |
49 |
60 fun opt_attr_map f attr_name opt_val = |
50 fun opt_attr _ NONE = [] |
61 case opt_val of NONE => [] | SOME v => [(attr_name,f v)] |
51 | opt_attr name (SOME value) = attr name value; |
62 (* or, if you've got function-itis: |
|
63 the_default [] (Option.map (single o (pair attr_name) o f) opt_val) |
|
64 *) |
|
65 |
|
66 fun opt_attr attr_name = opt_attr_map I attr_name |
|
67 |
52 |
68 |
53 |
69 (** Types and values **) |
54 (** Types and values **) |
70 |
55 |
71 (* readers and writers for values represented in XML strings *) |
|
72 |
|
73 fun read_pgipbool s = |
56 fun read_pgipbool s = |
74 (case s of |
57 (case s of |
75 "false" => false |
58 "false" => false |
76 | "true" => true |
59 | "true" => true |
77 | _ => raise PGIP ("Invalid boolean value: " ^ quote s)) |
60 | _ => raise PGIP ("Invalid boolean value: " ^ quote s)) |
78 |
61 |
79 local |
62 local |
80 fun int_in_range (NONE,NONE) (_: int) = true |
63 fun int_in_range (NONE,NONE) (_: int) = true |
81 | int_in_range (SOME min,NONE) i = min<= i |
64 | int_in_range (SOME min,NONE) i = min<= i |
82 | int_in_range (NONE,SOME max) i = i<=max |
65 | int_in_range (NONE,SOME max) i = i<=max |
83 | int_in_range (SOME min,SOME max) i = min<= i andalso i<=max |
66 | int_in_range (SOME min,SOME max) i = min<= i andalso i<=max |
84 in |
67 in |
85 fun read_pgipint range s = |
68 fun read_pgipint range s = |
86 (case Int.fromString s of |
69 (case Int.fromString s of |
87 SOME i => if int_in_range range i then i |
70 SOME i => if int_in_range range i then i |
88 else raise PGIP ("Out of range integer value: " ^ quote s) |
71 else raise PGIP ("Out of range integer value: " ^ quote s) |
89 | NONE => raise PGIP ("Invalid integer value: " ^ quote s)) |
72 | NONE => raise PGIP ("Invalid integer value: " ^ quote s)) |
90 end; |
73 end; |
91 |
74 |
92 fun read_pgipnat s = |
75 fun read_pgipnat s = |
93 (case Int.fromString s of |
76 (case Int.fromString s of |
94 SOME i => if i >= 0 then i |
77 SOME i => if i >= 0 then i |
95 else raise PGIP ("Invalid natural number: " ^ quote s) |
78 else raise PGIP ("Invalid natural number: " ^ quote s) |
96 | NONE => raise PGIP ("Invalid natural number: " ^ quote s)) |
79 | NONE => raise PGIP ("Invalid natural number: " ^ quote s)) |
97 |
80 |
98 fun read_pgipreal s = |
81 fun read_pgipreal s = |
116 |
99 |
117 fun bool_to_pgstring b = if b then "true" else "false" |
100 fun bool_to_pgstring b = if b then "true" else "false" |
118 |
101 |
119 |
102 |
120 (* PGIP datatypes. |
103 (* PGIP datatypes. |
121 |
104 |
122 This is a reflection of the type structure of PGIP configuration, |
105 This is a reflection of the type structure of PGIP configuration, |
123 which is meant for setting up user dialogs and preference settings. |
106 which is meant for setting up user dialogs and preference settings. |
124 These are configured declaratively in XML, using a syntax for types |
107 These are configured declaratively in XML, using a syntax for types |
125 and values which is like a (vastly cut down) form of XML Schema |
108 and values which is like a (vastly cut down) form of XML Schema |
126 Datatypes. |
109 Datatypes. |
127 |
110 |
128 The prover needs to interpret the strings representing the typed |
111 The prover needs to interpret the strings representing the typed |
129 values, at least for the types it expects from the dialogs it |
112 values, at least for the types it expects from the dialogs it |
130 configures. Here we go further and construct a type-safe |
113 configures. Here we go further and construct a type-safe |
131 encapsulation of these values, which would be useful for more |
114 encapsulation of these values, which would be useful for more |
132 advanced cases (e.g. generating and processing forms). |
115 advanced cases (e.g. generating and processing forms). |
133 *) |
116 *) |
134 |
117 |
135 |
118 |
136 datatype pgiptype = |
119 datatype pgiptype = |
137 Pgipnull (* unit type: unique element is empty string *) |
120 Pgipnull (* unit type: unique element is empty string *) |
138 | Pgipbool (* booleans: "true" or "false" *) |
121 | Pgipbool (* booleans: "true" or "false" *) |
139 | Pgipint of int option * int option (* ranged integers, should be XSD canonical *) |
122 | Pgipint of int option * int option (* ranged integers, should be XSD canonical *) |
140 | Pgipnat (* naturals: non-negative integers (convenience) *) |
123 | Pgipnat (* naturals: non-negative integers (convenience) *) |
141 | Pgipreal (* floating-point numbers *) |
124 | Pgipreal (* floating-point numbers *) |