author | blanchet |
Fri, 16 Apr 2010 14:48:34 +0200 | |
changeset 36169 | 27b1cc58715e |
parent 36142 | f5e15e9aae10 |
child 36170 | 0cdb76723c88 |
permissions | -rw-r--r-- |
36062 | 1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_util.ML |
35963 | 2 |
Author: Jasmin Blanchette, TU Muenchen |
3 |
||
4 |
General-purpose functions used by the Sledgehammer modules. |
|
5 |
*) |
|
6 |
||
7 |
signature SLEDGEHAMMER_UTIL = |
|
8 |
sig |
|
36142
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36062
diff
changeset
|
9 |
val plural_s : int -> string |
35963 | 10 |
val serial_commas : string -> string list -> string list |
36169
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36142
diff
changeset
|
11 |
val replace_all : string -> string -> string -> string |
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36142
diff
changeset
|
12 |
val remove_all : string -> string -> string |
35963 | 13 |
val parse_bool_option : bool -> string -> string -> bool option |
14 |
val parse_time_option : string -> string -> Time.time option |
|
36062 | 15 |
val hashw : word * word -> word |
16 |
val hashw_char : Char.char * word -> word |
|
17 |
val hashw_string : string * word -> word |
|
35963 | 18 |
end; |
19 |
||
20 |
structure Sledgehammer_Util : SLEDGEHAMMER_UTIL = |
|
21 |
struct |
|
22 |
||
36142
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36062
diff
changeset
|
23 |
fun plural_s n = if n = 1 then "" else "s" |
36062 | 24 |
|
35963 | 25 |
fun serial_commas _ [] = ["??"] |
26 |
| serial_commas _ [s] = [s] |
|
27 |
| serial_commas conj [s1, s2] = [s1, conj, s2] |
|
28 |
| serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3] |
|
29 |
| serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss |
|
30 |
||
36169
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36142
diff
changeset
|
31 |
fun replace_all bef aft = |
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36142
diff
changeset
|
32 |
let |
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36142
diff
changeset
|
33 |
fun aux seen "" = String.implode (rev seen) |
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36142
diff
changeset
|
34 |
| aux seen s = |
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36142
diff
changeset
|
35 |
if String.isPrefix bef s then |
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36142
diff
changeset
|
36 |
aux seen "" ^ aft ^ aux [] (unprefix bef s) |
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36142
diff
changeset
|
37 |
else |
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36142
diff
changeset
|
38 |
aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE)) |
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36142
diff
changeset
|
39 |
in aux [] end |
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36142
diff
changeset
|
40 |
|
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36142
diff
changeset
|
41 |
fun remove_all bef = replace_all bef "" |
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36142
diff
changeset
|
42 |
|
35963 | 43 |
fun parse_bool_option option name s = |
44 |
(case s of |
|
45 |
"smart" => if option then NONE else raise Option |
|
46 |
| "false" => SOME false |
|
47 |
| "true" => SOME true |
|
48 |
| "" => SOME true |
|
49 |
| _ => raise Option) |
|
50 |
handle Option.Option => |
|
51 |
let val ss = map quote ((option ? cons "smart") ["true", "false"]) in |
|
52 |
error ("Parameter " ^ quote name ^ " must be assigned " ^ |
|
53 |
space_implode " " (serial_commas "or" ss) ^ ".") |
|
54 |
end |
|
55 |
||
56 |
fun parse_time_option _ "none" = NONE |
|
57 |
| parse_time_option name s = |
|
58 |
let |
|
59 |
val msecs = |
|
60 |
case space_explode " " s of |
|
61 |
[s1, "min"] => 60000 * the (Int.fromString s1) |
|
62 |
| [s1, "s"] => 1000 * the (Int.fromString s1) |
|
63 |
| [s1, "ms"] => the (Int.fromString s1) |
|
64 |
| _ => 0 |
|
65 |
in |
|
66 |
if msecs <= 0 then |
|
67 |
error ("Parameter " ^ quote name ^ " must be assigned a positive time \ |
|
68 |
\value (e.g., \"60 s\", \"200 ms\") or \"none\".") |
|
69 |
else |
|
70 |
SOME (Time.fromMilliseconds msecs) |
|
71 |
end |
|
72 |
||
36142
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36062
diff
changeset
|
73 |
(* This hash function is recommended in Compilers: Principles, Techniques, and |
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36062
diff
changeset
|
74 |
Tools, by Aho, Sethi and Ullman. The hashpjw function, which they |
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36062
diff
changeset
|
75 |
particularly recommend, triggers a bug in versions of Poly/ML up to 4.2.0. *) |
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36062
diff
changeset
|
76 |
fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w)) |
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36062
diff
changeset
|
77 |
fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w) |
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36062
diff
changeset
|
78 |
fun hashw_string (s:string, w) = CharVector.foldl hashw_char w s |
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36062
diff
changeset
|
79 |
|
35963 | 80 |
end; |