author | wenzelm |
Mon, 13 May 2013 22:49:00 +0200 | |
changeset 51973 | e116eb9e5e17 |
parent 51972 | 39052352427d |
child 51985 | f6c04bf0123d |
permissions | -rw-r--r-- |
21637 | 1 |
(* Title: Pure/ProofGeneral/pgip_types.ML |
2 |
Author: David Aspinall |
|
3 |
||
21940 | 4 |
PGIP abstraction: types and conversions. |
21637 | 5 |
*) |
6 |
||
7 |
signature PGIPTYPES = |
|
8 |
sig |
|
9 |
(* Types and values (used for preferences and dialogs) *) |
|
10 |
||
40292 | 11 |
datatype pgiptype = |
12 |
Pgipnull | Pgipbool | Pgipint of int option * int option | Pgipnat | Pgipreal |
|
13 |
| Pgipstring | Pgipconst of string | Pgipchoice of pgipdtype list |
|
21637 | 14 |
|
15 |
and pgipdtype = Pgipdtype of string option * pgiptype (* type with opt. description *) |
|
16 |
||
17 |
exception PGIP of string |
|
21867 | 18 |
|
21637 | 19 |
(* Values as XML strings *) |
28020 | 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 *) |
|
40292 | 23 |
val read_pgipreal : string -> real (* raises PGIP *) |
28020 | 24 |
val read_pgipstring : string -> string (* raises PGIP *) |
40292 | 25 |
val real_to_pgstring : real -> string |
28020 | 26 |
val int_to_pgstring : int -> string |
21637 | 27 |
val bool_to_pgstring : bool -> string |
28 |
val string_to_pgstring : string -> string |
|
29 |
||
30 |
(* PGIP datatypes *) |
|
31 |
val pgiptype_to_xml : pgiptype -> XML.tree |
|
32 |
||
33 |
(* XML utils, only for PGIP code *) |
|
28020 | 34 |
val attr : string -> string -> XML.attributes |
21637 | 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 |
|
41 |
||
51973 | 42 |
structure PgipTypes : PGIPTYPES = |
21637 | 43 |
struct |
51973 | 44 |
|
21637 | 45 |
exception PGIP of string |
46 |
||
21867 | 47 |
(** XML utils **) |
48 |
||
28017 | 49 |
fun get_attr_opt attr attrs = Properties.get attrs attr |
21637 | 50 |
|
51 |
fun get_attr attr attrs = |
|
52 |
(case get_attr_opt attr attrs of |
|
53 |
SOME value => value |
|
21973
e7c9b0d3ce82
Quote arguments in PGIP exceptions. Tune comment.
aspinall
parents:
21944
diff
changeset
|
54 |
| NONE => raise PGIP ("Missing attribute: " ^ quote attr)) |
21637 | 55 |
|
56 |
fun get_attr_dflt attr dflt attrs = the_default dflt (get_attr_opt attr attrs) |
|
57 |
||
58 |
fun attr x y = [(x,y)] : XML.attributes |
|
59 |
||
60 |
fun opt_attr_map f attr_name opt_val = |
|
61 |
case opt_val of NONE => [] | SOME v => [(attr_name,f v)] |
|
62 |
(* or, if you've got function-itis: |
|
63 |
the_default [] (Option.map (single o (pair attr_name) o f) opt_val) |
|
64 |
*) |
|
65 |
||
21902 | 66 |
fun opt_attr attr_name = opt_attr_map I attr_name |
21637 | 67 |
|
21867 | 68 |
|
21637 | 69 |
(** Types and values **) |
70 |
||
71 |
(* readers and writers for values represented in XML strings *) |
|
72 |
||
73 |
fun read_pgipbool s = |
|
74 |
(case s of |
|
28020 | 75 |
"false" => false |
21637 | 76 |
| "true" => true |
21973
e7c9b0d3ce82
Quote arguments in PGIP exceptions. Tune comment.
aspinall
parents:
21944
diff
changeset
|
77 |
| _ => raise PGIP ("Invalid boolean value: " ^ quote s)) |
21637 | 78 |
|
79 |
local |
|
24133
75063f96618f
added int type constraints to accomodate hacked SML/NJ;
wenzelm
parents:
23753
diff
changeset
|
80 |
fun int_in_range (NONE,NONE) (_: int) = true |
21637 | 81 |
| int_in_range (SOME min,NONE) i = min<= i |
82 |
| int_in_range (NONE,SOME max) i = i<=max |
|
83 |
| int_in_range (SOME min,SOME max) i = min<= i andalso i<=max |
|
84 |
in |
|
85 |
fun read_pgipint range s = |
|
22009
b0c966b30066
approximate Syntax.read_int/nat by Int.fromString -- avoids dependency on Syntax module;
wenzelm
parents:
22003
diff
changeset
|
86 |
(case Int.fromString s of |
28020 | 87 |
SOME i => if int_in_range range i then i |
88 |
else raise PGIP ("Out of range integer value: " ^ quote s) |
|
21973
e7c9b0d3ce82
Quote arguments in PGIP exceptions. Tune comment.
aspinall
parents:
21944
diff
changeset
|
89 |
| NONE => raise PGIP ("Invalid integer value: " ^ quote s)) |
21637 | 90 |
end; |
91 |
||
92 |
fun read_pgipnat s = |
|
22009
b0c966b30066
approximate Syntax.read_int/nat by Int.fromString -- avoids dependency on Syntax module;
wenzelm
parents:
22003
diff
changeset
|
93 |
(case Int.fromString s of |
28020 | 94 |
SOME i => if i >= 0 then i |
22009
b0c966b30066
approximate Syntax.read_int/nat by Int.fromString -- avoids dependency on Syntax module;
wenzelm
parents:
22003
diff
changeset
|
95 |
else raise PGIP ("Invalid natural number: " ^ quote s) |
21973
e7c9b0d3ce82
Quote arguments in PGIP exceptions. Tune comment.
aspinall
parents:
21944
diff
changeset
|
96 |
| NONE => raise PGIP ("Invalid natural number: " ^ quote s)) |
21637 | 97 |
|
40292 | 98 |
fun read_pgipreal s = |
99 |
(case Real.fromString s of |
|
100 |
SOME x => x |
|
101 |
| NONE => raise PGIP ("Invalid floating-point number: " ^ quote s)) |
|
102 |
||
21637 | 103 |
(* NB: we can maybe do without xml decode/encode here. *) |
104 |
fun read_pgipstring s = (* non-empty strings, XML escapes decoded *) |
|
105 |
(case XML.parse_string s of |
|
28020 | 106 |
SOME s => s |
21973
e7c9b0d3ce82
Quote arguments in PGIP exceptions. Tune comment.
aspinall
parents:
21944
diff
changeset
|
107 |
| NONE => raise PGIP ("Expected a non-empty string: " ^ quote s)) |
28397
389c5e494605
handle _ should be avoided (spurious Interrupt will spoil the game);
wenzelm
parents:
28020
diff
changeset
|
108 |
handle _ => raise PGIP ("Invalid XML string syntax: " ^ quote s) (* FIXME avoid handle _ *) |
21637 | 109 |
|
21944 | 110 |
val int_to_pgstring = signed_string_of_int |
21637 | 111 |
|
41516
3a70387b5e01
smart_string_of_real: print integer values without fractional part;
wenzelm
parents:
40292
diff
changeset
|
112 |
val real_to_pgstring = smart_string_of_real; |
3a70387b5e01
smart_string_of_real: print integer values without fractional part;
wenzelm
parents:
40292
diff
changeset
|
113 |
|
40292 | 114 |
|
21637 | 115 |
fun string_to_pgstring s = XML.text s |
116 |
||
117 |
fun bool_to_pgstring b = if b then "true" else "false" |
|
118 |
||
119 |
||
120 |
(* PGIP datatypes. |
|
121 |
||
122 |
This is a reflection of the type structure of PGIP configuration, |
|
123 |
which is meant for setting up user dialogs and preference settings. |
|
124 |
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 |
|
126 |
Datatypes. |
|
127 |
||
128 |
The prover needs to interpret the strings representing the typed |
|
129 |
values, at least for the types it expects from the dialogs it |
|
130 |
configures. Here we go further and construct a type-safe |
|
131 |
encapsulation of these values, which would be useful for more |
|
132 |
advanced cases (e.g. generating and processing forms). |
|
133 |
*) |
|
134 |
||
135 |
||
136 |
datatype pgiptype = |
|
28020 | 137 |
Pgipnull (* unit type: unique element is empty string *) |
138 |
| Pgipbool (* booleans: "true" or "false" *) |
|
21637 | 139 |
| Pgipint of int option * int option (* ranged integers, should be XSD canonical *) |
28020 | 140 |
| Pgipnat (* naturals: non-negative integers (convenience) *) |
40292 | 141 |
| Pgipreal (* floating-point numbers *) |
28020 | 142 |
| Pgipstring (* non-empty strings *) |
143 |
| Pgipconst of string (* singleton type *) |
|
144 |
| Pgipchoice of pgipdtype list (* union type *) |
|
21637 | 145 |
|
146 |
(* Compared with the PGIP schema, we push descriptions of types inside choices. *) |
|
147 |
||
148 |
and pgipdtype = Pgipdtype of string option * pgiptype |
|
149 |
||
40292 | 150 |
datatype pgipuval = |
151 |
Pgvalnull | Pgvalbool of bool | Pgvalint of int | Pgvalnat of int | Pgvalreal of real |
|
152 |
| Pgvalstring of string | Pgvalconst of string |
|
21637 | 153 |
|
28020 | 154 |
type pgipval = pgiptype * pgipuval (* type-safe values *) |
21637 | 155 |
|
156 |
fun pgipdtype_to_xml (desco,ty) = |
|
157 |
let |
|
28020 | 158 |
val desc_attr = opt_attr "descr" desco |
21637 | 159 |
|
28020 | 160 |
val elt = case ty of |
161 |
Pgipnull => "pgipnull" |
|
162 |
| Pgipbool => "pgipbool" |
|
163 |
| Pgipint _ => "pgipint" |
|
164 |
| Pgipnat => "pgipint" |
|
41733
775da08dae1b
clarified comment -- ancienct PG 3.7.x is still in use;
wenzelm
parents:
41516
diff
changeset
|
165 |
| Pgipreal => "pgipint" (*sic!*) (*required for PG 4.0 and 3.7.x*) |
28020 | 166 |
| Pgipstring => "pgipstring" |
167 |
| Pgipconst _ => "pgipconst" |
|
168 |
| Pgipchoice _ => "pgipchoice" |
|
21637 | 169 |
|
28020 | 170 |
fun range_attr r v = attr r (int_to_pgstring v) |
21637 | 171 |
|
28020 | 172 |
val attrs = case ty of |
173 |
Pgipint (SOME min,SOME max) => (range_attr "min" min)@(range_attr "max" max) |
|
174 |
| Pgipint (SOME min,NONE) => (range_attr "min" min) |
|
175 |
| Pgipint (NONE,SOME max) => (range_attr "max" max) |
|
176 |
| Pgipnat => (range_attr "min" 0) |
|
177 |
| Pgipconst nm => attr "name" nm |
|
178 |
| _ => [] |
|
21637 | 179 |
|
28020 | 180 |
fun destpgipdtype (Pgipdtype x) = x |
21637 | 181 |
|
28020 | 182 |
val typargs = case ty of |
183 |
Pgipchoice ds => map destpgipdtype ds |
|
184 |
| _ => [] |
|
21637 | 185 |
in |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
29606
diff
changeset
|
186 |
XML.Elem ((elt, desc_attr @ attrs), map pgipdtype_to_xml typargs) |
21637 | 187 |
end |
188 |
||
21940 | 189 |
val pgiptype_to_xml = pgipdtype_to_xml o pair NONE |
21637 | 190 |
|
191 |
end |
|
192 |