5 *) |
5 *) |
6 |
6 |
7 signature ATP_UTIL = |
7 signature ATP_UTIL = |
8 sig |
8 sig |
9 val timestamp : unit -> string |
9 val timestamp : unit -> string |
10 val hashw : word * word -> word |
10 val hash_string : string -> int |
11 val hashw_string : string * word -> word |
11 val hash_term : term -> int |
12 val strip_spaces : bool -> (char -> bool) -> string -> string |
12 val strip_spaces : bool -> (char -> bool) -> string -> string |
13 val nat_subscript : int -> string |
13 val nat_subscript : int -> string |
14 val unyxml : string -> string |
14 val unyxml : string -> string |
15 val maybe_quote : string -> string |
15 val maybe_quote : string -> string |
16 val string_from_ext_time : bool * Time.time -> string |
16 val string_from_ext_time : bool * Time.time -> string |
40 Tools" by Aho, Sethi, and Ullman. The "hashpjw" function, which they |
40 Tools" by Aho, Sethi, and Ullman. The "hashpjw" function, which they |
41 particularly recommend, triggers a bug in versions of Poly/ML up to 4.2.0. *) |
41 particularly recommend, triggers a bug in versions of Poly/ML up to 4.2.0. *) |
42 fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w)) |
42 fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w)) |
43 fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w) |
43 fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w) |
44 fun hashw_string (s : string, w) = CharVector.foldl hashw_char w s |
44 fun hashw_string (s : string, w) = CharVector.foldl hashw_char w s |
|
45 fun hashw_term (t1 $ t2) = hashw (hashw_term t1, hashw_term t2) |
|
46 | hashw_term (Const (s, _)) = hashw_string (s, 0w0) |
|
47 | hashw_term (Free (s, _)) = hashw_string (s, 0w0) |
|
48 | hashw_term _ = 0w0 |
|
49 |
|
50 fun hash_string s = Word.toInt (hashw_string (s, 0w0)) |
|
51 val hash_term = Word.toInt o hashw_term |
45 |
52 |
46 fun strip_c_style_comment _ [] = [] |
53 fun strip_c_style_comment _ [] = [] |
47 | strip_c_style_comment is_evil (#"*" :: #"/" :: cs) = |
54 | strip_c_style_comment is_evil (#"*" :: #"/" :: cs) = |
48 strip_spaces_in_list true is_evil cs |
55 strip_spaces_in_list true is_evil cs |
49 | strip_c_style_comment is_evil (_ :: cs) = strip_c_style_comment is_evil cs |
56 | strip_c_style_comment is_evil (_ :: cs) = strip_c_style_comment is_evil cs |