equal
deleted
inserted
replaced
7 signature SLEDGEHAMMER_UTIL = |
7 signature SLEDGEHAMMER_UTIL = |
8 sig |
8 sig |
9 val sledgehammerN : string |
9 val sledgehammerN : string |
10 val log2 : real -> real |
10 val log2 : real -> real |
11 val app_hd : ('a -> 'a) -> 'a list -> 'a list |
11 val app_hd : ('a -> 'a) -> 'a list -> 'a list |
|
12 val n_fold_cartesian_product : 'a list list -> 'a list list |
12 val plural_s : int -> string |
13 val plural_s : int -> string |
13 val serial_commas : string -> string list -> string list |
14 val serial_commas : string -> string list -> string list |
14 val simplify_spaces : string -> string |
15 val simplify_spaces : string -> string |
15 val with_cleanup : ('a -> unit) -> ('a -> 'b) -> 'a -> 'b |
16 val with_cleanup : ('a -> unit) -> ('a -> 'b) -> 'a -> 'b |
16 val infinite_timeout : Time.time |
17 val infinite_timeout : Time.time |
45 val log10_2 = Math.log10 2.0 |
46 val log10_2 = Math.log10 2.0 |
46 |
47 |
47 fun log2 n = Math.log10 n / log10_2 |
48 fun log2 n = Math.log10 n / log10_2 |
48 |
49 |
49 fun app_hd f (x :: xs) = f x :: xs |
50 fun app_hd f (x :: xs) = f x :: xs |
|
51 |
|
52 fun cartesian_product [] _ = [] |
|
53 | cartesian_product (x :: xs) yss = |
|
54 map (cons x) yss @ cartesian_product xs yss |
|
55 |
|
56 fun n_fold_cartesian_product xss = fold_rev cartesian_product xss [[]] |
50 |
57 |
51 fun plural_s n = if n = 1 then "" else "s" |
58 fun plural_s n = if n = 1 then "" else "s" |
52 |
59 |
53 val serial_commas = Try.serial_commas |
60 val serial_commas = Try.serial_commas |
54 val simplify_spaces = strip_spaces false (K true) |
61 val simplify_spaces = strip_spaces false (K true) |