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 hash_string : string -> int |
10 val hash_string : string -> int |
11 val hash_term : term -> int |
|
12 val chunk_list : int -> 'a list -> 'a list list |
11 val chunk_list : int -> 'a list -> 'a list list |
13 val stringN_of_int : int -> int -> string |
12 val stringN_of_int : int -> int -> string |
14 val strip_spaces : bool -> (char -> bool) -> string -> string |
13 val strip_spaces : bool -> (char -> bool) -> string -> string |
15 val strip_spaces_except_between_idents : string -> string |
14 val strip_spaces_except_between_idents : string -> string |
16 val elide_string : int -> string -> string |
15 val elide_string : int -> string -> string |
61 Tools" by Aho, Sethi, and Ullman. The "hashpjw" function, which they |
60 Tools" by Aho, Sethi, and Ullman. The "hashpjw" function, which they |
62 particularly recommend, triggers a bug in versions of Poly/ML up to 4.2.0. *) |
61 particularly recommend, triggers a bug in versions of Poly/ML up to 4.2.0. *) |
63 fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w)) |
62 fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w)) |
64 fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w) |
63 fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w) |
65 fun hashw_string (s : string, w) = CharVector.foldl hashw_char w s |
64 fun hashw_string (s : string, w) = CharVector.foldl hashw_char w s |
66 fun hashw_term (t1 $ t2) = hashw (hashw_term t1, hashw_term t2) |
|
67 | hashw_term (Const (s, _)) = hashw_string (s, 0w0) |
|
68 | hashw_term (Free (s, _)) = hashw_string (s, 0w0) |
|
69 | hashw_term _ = 0w0 |
|
70 |
|
71 fun hash_string s = Word.toInt (hashw_string (s, 0w0)) |
65 fun hash_string s = Word.toInt (hashw_string (s, 0w0)) |
72 val hash_term = Word.toInt o hashw_term |
|
73 |
66 |
74 fun chunk_list _ [] = [] |
67 fun chunk_list _ [] = [] |
75 | chunk_list k xs = |
68 | chunk_list k xs = |
76 let val (xs1, xs2) = chop k xs in xs1 :: chunk_list k xs2 end |
69 let val (xs1, xs2) = chop k xs in xs1 :: chunk_list k xs2 end |
77 |
70 |