63806
|
1 |
(* Title: Pure/General/value.ML
|
|
2 |
Author: Makarius
|
|
3 |
|
|
4 |
Plain values, represented as string.
|
|
5 |
*)
|
|
6 |
|
|
7 |
signature VALUE =
|
|
8 |
sig
|
|
9 |
val parse_bool: string -> bool
|
|
10 |
val print_bool: bool -> string
|
|
11 |
val parse_nat: string -> int
|
|
12 |
val parse_int: string -> int
|
|
13 |
val print_int: int -> string
|
|
14 |
val parse_real: string -> real
|
|
15 |
val print_real: real -> string
|
|
16 |
end;
|
|
17 |
|
|
18 |
structure Value: VALUE =
|
|
19 |
struct
|
|
20 |
|
|
21 |
fun parse_bool "true" = true
|
|
22 |
| parse_bool "false" = false
|
|
23 |
| parse_bool s = raise Fail ("Bad boolean " ^ quote s);
|
|
24 |
|
|
25 |
val print_bool = Bool.toString;
|
|
26 |
|
|
27 |
|
|
28 |
fun parse_nat s =
|
|
29 |
let val i = Int.fromString s in
|
|
30 |
if is_none i orelse the i < 0
|
|
31 |
then raise Fail ("Bad natural number " ^ quote s)
|
|
32 |
else the i
|
|
33 |
end;
|
|
34 |
|
|
35 |
fun parse_int s =
|
|
36 |
let val i = Int.fromString s in
|
|
37 |
if is_none i orelse String.isPrefix "~" s
|
|
38 |
then raise Fail ("Bad integer " ^ quote s)
|
|
39 |
else the i
|
|
40 |
end;
|
|
41 |
|
|
42 |
val print_int = signed_string_of_int;
|
|
43 |
|
|
44 |
|
|
45 |
fun parse_real s =
|
|
46 |
(case Real.fromString s of
|
|
47 |
SOME x => x
|
|
48 |
| NONE => raise Fail ("Bad real " ^ quote s));
|
|
49 |
|
|
50 |
fun print_real x =
|
|
51 |
let val s = signed_string_of_real x in
|
|
52 |
(case space_explode "." s of
|
|
53 |
[a, b] => if forall_string (fn c => c = "0") b then a else s
|
|
54 |
| _ => s)
|
|
55 |
end;
|
|
56 |
|
|
57 |
end;
|