blanchet@36062
|
1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_util.ML
|
blanchet@35961
|
2 |
Author: Jasmin Blanchette, TU Muenchen
|
blanchet@35961
|
3 |
|
blanchet@35961
|
4 |
General-purpose functions used by the Sledgehammer modules.
|
blanchet@35961
|
5 |
*)
|
blanchet@35961
|
6 |
|
blanchet@35961
|
7 |
signature SLEDGEHAMMER_UTIL =
|
blanchet@35961
|
8 |
sig
|
blanchet@35961
|
9 |
val serial_commas : string -> string list -> string list
|
blanchet@35961
|
10 |
val parse_bool_option : bool -> string -> string -> bool option
|
blanchet@35961
|
11 |
val parse_time_option : string -> string -> Time.time option
|
blanchet@36062
|
12 |
val hashw : word * word -> word
|
blanchet@36062
|
13 |
val hashw_char : Char.char * word -> word
|
blanchet@36062
|
14 |
val hashw_string : string * word -> word
|
blanchet@35961
|
15 |
end;
|
blanchet@35961
|
16 |
|
blanchet@35961
|
17 |
structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
|
blanchet@35961
|
18 |
struct
|
blanchet@35961
|
19 |
|
blanchet@36062
|
20 |
(* This hash function is recommended in Compilers: Principles, Techniques, and
|
blanchet@36062
|
21 |
Tools, by Aho, Sethi and Ullman. The hashpjw function, which they
|
blanchet@36062
|
22 |
particularly recommend, triggers a bug in versions of Poly/ML up to 4.2.0. *)
|
blanchet@36062
|
23 |
fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w))
|
blanchet@36062
|
24 |
fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w)
|
blanchet@36062
|
25 |
fun hashw_string (s:string, w) = CharVector.foldl hashw_char w s
|
blanchet@36062
|
26 |
|
blanchet@35961
|
27 |
fun serial_commas _ [] = ["??"]
|
blanchet@35961
|
28 |
| serial_commas _ [s] = [s]
|
blanchet@35961
|
29 |
| serial_commas conj [s1, s2] = [s1, conj, s2]
|
blanchet@35961
|
30 |
| serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
|
blanchet@35961
|
31 |
| serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
|
blanchet@35961
|
32 |
|
blanchet@35961
|
33 |
fun parse_bool_option option name s =
|
blanchet@35961
|
34 |
(case s of
|
blanchet@35961
|
35 |
"smart" => if option then NONE else raise Option
|
blanchet@35961
|
36 |
| "false" => SOME false
|
blanchet@35961
|
37 |
| "true" => SOME true
|
blanchet@35961
|
38 |
| "" => SOME true
|
blanchet@35961
|
39 |
| _ => raise Option)
|
blanchet@35961
|
40 |
handle Option.Option =>
|
blanchet@35961
|
41 |
let val ss = map quote ((option ? cons "smart") ["true", "false"]) in
|
blanchet@35961
|
42 |
error ("Parameter " ^ quote name ^ " must be assigned " ^
|
blanchet@35961
|
43 |
space_implode " " (serial_commas "or" ss) ^ ".")
|
blanchet@35961
|
44 |
end
|
blanchet@35961
|
45 |
|
blanchet@35961
|
46 |
fun parse_time_option _ "none" = NONE
|
blanchet@35961
|
47 |
| parse_time_option name s =
|
blanchet@35961
|
48 |
let
|
blanchet@35961
|
49 |
val msecs =
|
blanchet@35961
|
50 |
case space_explode " " s of
|
blanchet@35961
|
51 |
[s1, "min"] => 60000 * the (Int.fromString s1)
|
blanchet@35961
|
52 |
| [s1, "s"] => 1000 * the (Int.fromString s1)
|
blanchet@35961
|
53 |
| [s1, "ms"] => the (Int.fromString s1)
|
blanchet@35961
|
54 |
| _ => 0
|
blanchet@35961
|
55 |
in
|
blanchet@35961
|
56 |
if msecs <= 0 then
|
blanchet@35961
|
57 |
error ("Parameter " ^ quote name ^ " must be assigned a positive time \
|
blanchet@35961
|
58 |
\value (e.g., \"60 s\", \"200 ms\") or \"none\".")
|
blanchet@35961
|
59 |
else
|
blanchet@35961
|
60 |
SOME (Time.fromMilliseconds msecs)
|
blanchet@35961
|
61 |
end
|
blanchet@35961
|
62 |
|
blanchet@35961
|
63 |
end;
|