|
1 (* Title: HOL/Sledgehammer/sledgehammer_util.ML |
|
2 Author: Jasmin Blanchette, TU Muenchen |
|
3 |
|
4 General-purpose functions used by the Sledgehammer modules. |
|
5 *) |
|
6 |
|
7 signature SLEDGEHAMMER_UTIL = |
|
8 sig |
|
9 val serial_commas : string -> string list -> string list |
|
10 val parse_bool_option : bool -> string -> string -> bool option |
|
11 val parse_time_option : string -> string -> Time.time option |
|
12 end; |
|
13 |
|
14 structure Sledgehammer_Util : SLEDGEHAMMER_UTIL = |
|
15 struct |
|
16 |
|
17 fun serial_commas _ [] = ["??"] |
|
18 | serial_commas _ [s] = [s] |
|
19 | serial_commas conj [s1, s2] = [s1, conj, s2] |
|
20 | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3] |
|
21 | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss |
|
22 |
|
23 fun parse_bool_option option name s = |
|
24 (case s of |
|
25 "smart" => if option then NONE else raise Option |
|
26 | "false" => SOME false |
|
27 | "true" => SOME true |
|
28 | "" => SOME true |
|
29 | _ => raise Option) |
|
30 handle Option.Option => |
|
31 let val ss = map quote ((option ? cons "smart") ["true", "false"]) in |
|
32 error ("Parameter " ^ quote name ^ " must be assigned " ^ |
|
33 space_implode " " (serial_commas "or" ss) ^ ".") |
|
34 end |
|
35 |
|
36 fun parse_time_option _ "none" = NONE |
|
37 | parse_time_option name s = |
|
38 let |
|
39 val msecs = |
|
40 case space_explode " " s of |
|
41 [s1, "min"] => 60000 * the (Int.fromString s1) |
|
42 | [s1, "s"] => 1000 * the (Int.fromString s1) |
|
43 | [s1, "ms"] => the (Int.fromString s1) |
|
44 | _ => 0 |
|
45 in |
|
46 if msecs <= 0 then |
|
47 error ("Parameter " ^ quote name ^ " must be assigned a positive time \ |
|
48 \value (e.g., \"60 s\", \"200 ms\") or \"none\".") |
|
49 else |
|
50 SOME (Time.fromMilliseconds msecs) |
|
51 end |
|
52 |
|
53 end; |