47 (''a * ''a -> bool) -> (''a option * 'b) list -> ''a -> 'b option |
47 (''a * ''a -> bool) -> (''a option * 'b) list -> ''a -> 'b option |
48 val is_substring_of : string -> string -> bool |
48 val is_substring_of : string -> string -> bool |
49 val plural_s : int -> string |
49 val plural_s : int -> string |
50 val plural_s_for_list : 'a list -> string |
50 val plural_s_for_list : 'a list -> string |
51 val serial_commas : string -> string list -> string list |
51 val serial_commas : string -> string list -> string list |
|
52 val pretty_serial_commas : string -> Pretty.T list -> Pretty.T list |
52 val parse_bool_option : bool -> string -> string -> bool option |
53 val parse_bool_option : bool -> string -> string -> bool option |
53 val parse_time_option : string -> string -> Time.time option |
54 val parse_time_option : string -> string -> Time.time option |
54 val flip_polarity : polarity -> polarity |
55 val flip_polarity : polarity -> polarity |
55 val prop_T : typ |
56 val prop_T : typ |
56 val bool_T : typ |
57 val bool_T : typ |
70 val DETERM_TIMEOUT : Time.time option -> tactic -> tactic |
71 val DETERM_TIMEOUT : Time.time option -> tactic -> tactic |
71 val setmp_show_all_types : ('a -> 'b) -> 'a -> 'b |
72 val setmp_show_all_types : ('a -> 'b) -> 'a -> 'b |
72 val indent_size : int |
73 val indent_size : int |
73 val pstrs : string -> Pretty.T list |
74 val pstrs : string -> Pretty.T list |
74 val unyxml : string -> string |
75 val unyxml : string -> string |
75 val maybe_quote : string -> string |
76 val pretty_maybe_quote : Pretty.T -> Pretty.T |
76 val hashw : word * word -> word |
77 val hashw : word * word -> word |
77 val hashw_string : string * word -> word |
78 val hashw_string : string * word -> word |
78 end; |
79 end; |
79 |
80 |
80 structure Nitpick_Util : NITPICK_UTIL = |
81 structure Nitpick_Util : NITPICK_UTIL = |
220 val plural_s = Sledgehammer_Util.plural_s |
221 val plural_s = Sledgehammer_Util.plural_s |
221 fun plural_s_for_list xs = plural_s (length xs) |
222 fun plural_s_for_list xs = plural_s (length xs) |
222 |
223 |
223 val serial_commas = Sledgehammer_Util.serial_commas |
224 val serial_commas = Sledgehammer_Util.serial_commas |
224 |
225 |
|
226 fun pretty_serial_commas _ [] = [] |
|
227 | pretty_serial_commas _ [p] = [p] |
|
228 | pretty_serial_commas conj [p1, p2] = |
|
229 [p1, Pretty.brk 1, Pretty.str conj, Pretty.brk 1, p2] |
|
230 | pretty_serial_commas conj [p1, p2, p3] = |
|
231 [p1, Pretty.str ",", Pretty.brk 1, p2, Pretty.str ",", Pretty.brk 1, |
|
232 Pretty.str conj, Pretty.brk 1, p3] |
|
233 | pretty_serial_commas conj (p :: ps) = |
|
234 p :: Pretty.str "," :: Pretty.brk 1 :: pretty_serial_commas conj ps |
|
235 |
225 val parse_bool_option = Sledgehammer_Util.parse_bool_option |
236 val parse_bool_option = Sledgehammer_Util.parse_bool_option |
226 val parse_time_option = Sledgehammer_Util.parse_time_option |
237 val parse_time_option = Sledgehammer_Util.parse_time_option |
227 |
238 |
228 fun flip_polarity Pos = Neg |
239 fun flip_polarity Pos = Neg |
229 | flip_polarity Neg = Pos |
240 | flip_polarity Neg = Pos |
260 fun DETERM_TIMEOUT delay tac st = |
271 fun DETERM_TIMEOUT delay tac st = |
261 Seq.of_list (the_list (time_limit delay (fn () => SINGLE tac st) ())) |
272 Seq.of_list (the_list (time_limit delay (fn () => SINGLE tac st) ())) |
262 |
273 |
263 fun setmp_show_all_types f = |
274 fun setmp_show_all_types f = |
264 setmp_CRITICAL show_all_types |
275 setmp_CRITICAL show_all_types |
265 (! show_types orelse ! show_sorts orelse ! show_all_types) f |
276 (!show_types orelse !show_sorts orelse !show_all_types) f |
266 |
277 |
267 val indent_size = 2 |
278 val indent_size = 2 |
268 |
279 |
269 val pstrs = Pretty.breaks o map Pretty.str o space_explode " " |
280 val pstrs = Pretty.breaks o map Pretty.str o space_explode " " |
270 |
281 |
271 val unyxml = Sledgehammer_Util.unyxml |
282 val unyxml = Sledgehammer_Util.unyxml |
|
283 |
272 val maybe_quote = Sledgehammer_Util.maybe_quote |
284 val maybe_quote = Sledgehammer_Util.maybe_quote |
|
285 fun pretty_maybe_quote pretty = |
|
286 let val s = Pretty.str_of pretty in |
|
287 if maybe_quote s = s then pretty else Pretty.enum "" "\"" "\"" [pretty] |
|
288 end |
273 |
289 |
274 (* This hash function is recommended in Compilers: Principles, Techniques, and |
290 (* This hash function is recommended in Compilers: Principles, Techniques, and |
275 Tools, by Aho, Sethi, and Ullman. The "hashpjw" function, which they |
291 Tools, by Aho, Sethi, and Ullman. The "hashpjw" function, which they |
276 particularly recommend, triggers a bug in versions of Poly/ML up to 4.2.0. *) |
292 particularly recommend, triggers a bug in versions of Poly/ML up to 4.2.0. *) |
277 fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w)) |
293 fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w)) |