1 (* Title: HOL/Tools/Nitpick/nitpick_util.ML
2 Author: Jasmin Blanchette, TU Muenchen
3 Copyright 2008, 2009, 2010
5 General-purpose functions used by the Nitpick modules.
8 signature NITPICK_UTIL =
10 type styp = string * typ
11 datatype polarity = Pos | Neg | Neut
13 exception ARG of string * string
14 exception BAD of string * string
15 exception TOO_SMALL of string * string
16 exception TOO_LARGE of string * string
17 exception NOT_SUPPORTED of string
18 exception SAME of unit
20 val nitpick_prefix : string
21 val curry3 : ('a * 'b * 'c -> 'd) -> 'a -> 'b -> 'c -> 'd
22 val pairf : ('a -> 'b) -> ('a -> 'c) -> 'a -> 'b * 'c
23 val pair_from_fun : (bool -> 'a) -> 'a * 'a
24 val fun_from_pair : 'a * 'a -> bool -> 'a
25 val int_from_bool : bool -> int
26 val nat_minus : int -> int -> int
27 val reasonable_power : int -> int -> int
28 val exact_log : int -> int -> int
29 val exact_root : int -> int -> int
30 val offset_list : int list -> int list
31 val index_seq : int -> int -> int list
32 val filter_indices : int list -> 'a list -> 'a list
33 val filter_out_indices : int list -> 'a list -> 'a list
34 val fold1 : ('a -> 'a -> 'a) -> 'a list -> 'a
35 val replicate_list : int -> 'a list -> 'a list
36 val n_fold_cartesian_product : 'a list list -> 'a list list
37 val all_distinct_unordered_pairs_of : ''a list -> (''a * ''a) list
38 val nth_combination : (int * int) list -> int -> int list
39 val all_combinations : (int * int) list -> int list list
40 val all_permutations : 'a list -> 'a list list
41 val batch_list : int -> 'a list -> 'a list list
42 val chunk_list_unevenly : int list -> 'a list -> 'a list list
43 val map3 : ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
45 ('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
49 val plural_s : int -> string
50 val plural_s_for_list : 'a list -> string
51 val serial_commas : string -> string list -> string list
52 val timestamp : unit -> string
53 val parse_bool_option : bool -> string -> string -> bool option
54 val parse_time_option : string -> string -> Time.time option
55 val flip_polarity : polarity -> polarity
60 val nat_subscript : int -> string
61 val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b
62 val DETERM_TIMEOUT : Time.time option -> tactic -> tactic
63 val setmp_show_all_types : ('a -> 'b) -> 'a -> 'b
65 val pstrs : string -> Pretty.T list
66 val unyxml : string -> string
67 val maybe_quote : string -> string
68 val hashw : word * word -> word
69 val hashw_string : string * word -> word
72 structure Nitpick_Util : NITPICK_UTIL =
75 type styp = string * typ
77 datatype polarity = Pos | Neg | Neut
79 exception ARG of string * string
80 exception BAD of string * string
81 exception TOO_SMALL of string * string
82 exception TOO_LARGE of string * string
83 exception NOT_SUPPORTED of string
84 exception SAME of unit
86 val nitpick_prefix = "Nitpick."
88 fun curry3 f = fn x => fn y => fn z => f (x, y, z)
90 fun pairf f g x = (f x, g x)
92 fun pair_from_fun f = (f false, f true)
93 fun fun_from_pair (f, t) b = if b then t else f
95 fun int_from_bool b = if b then 1 else 0
96 fun nat_minus i j = if i > j then i - j else 0
98 val max_exponent = 16384
100 fun reasonable_power _ 0 = 1
101 | reasonable_power a 1 = a
102 | reasonable_power 0 _ = 0
103 | reasonable_power 1 _ = 1
104 | reasonable_power a b =
106 raise ARG ("Nitpick_Util.reasonable_power",
107 "negative exponent (" ^ signed_string_of_int b ^ ")")
108 else if b > max_exponent then
109 raise TOO_LARGE ("Nitpick_Util.reasonable_power",
110 "too large exponent (" ^ signed_string_of_int b ^ ")")
112 let val c = reasonable_power a (b div 2) in
113 c * c * reasonable_power a (b mod 2)
118 val r = Math.ln (Real.fromInt n) / Math.ln (Real.fromInt m) |> Real.round
120 if reasonable_power m r = n then
123 raise ARG ("Nitpick_Util.exact_log",
124 commas (map signed_string_of_int [m, n]))
128 let val r = Math.pow (Real.fromInt n, 1.0 / (Real.fromInt m)) |> Real.round in
129 if reasonable_power r m = n then
132 raise ARG ("Nitpick_Util.exact_root",
133 commas (map signed_string_of_int [m, n]))
136 fun fold1 f = foldl1 (uncurry f)
138 fun replicate_list 0 _ = []
139 | replicate_list n xs = xs @ replicate_list (n - 1) xs
141 fun offset_list ns = rev (tl (fold (fn x => fn xs => (x + hd xs) :: xs) ns [0]))
142 fun index_seq j0 n = if j0 < 0 then j0 downto j0 - n + 1 else j0 upto j0 + n - 1
144 fun filter_indices js xs =
147 | aux i (j :: js) (x :: xs) =
148 if i = j then x :: aux (i + 1) js xs else aux (i + 1) (j :: js) xs
149 | aux _ _ _ = raise ARG ("Nitpick_Util.filter_indices",
150 "indices unordered or out of range")
152 fun filter_out_indices js xs =
155 | aux i (j :: js) (x :: xs) =
156 if i = j then aux (i + 1) js xs else x :: aux (i + 1) (j :: js) xs
157 | aux _ _ _ = raise ARG ("Nitpick_Util.filter_out_indices",
158 "indices unordered or out of range")
161 fun cartesian_product [] _ = []
162 | cartesian_product (x :: xs) yss =
163 map (cons x) yss @ cartesian_product xs yss
164 fun n_fold_cartesian_product xss = fold_rev cartesian_product xss [[]]
165 fun all_distinct_unordered_pairs_of [] = []
166 | all_distinct_unordered_pairs_of (x :: xs) =
167 map (pair x) xs @ all_distinct_unordered_pairs_of xs
169 val nth_combination =
171 fun aux [] n = ([], n)
172 | aux ((k, j0) :: xs) n =
173 let val (js, n) = aux xs n in ((n mod k) + j0 :: js, n div k) end
176 val all_combinations = n_fold_cartesian_product o map (uncurry index_seq o swap)
178 fun all_permutations [] = [[]]
179 | all_permutations xs =
180 maps (fn j => map (cons (nth xs j)) (all_permutations (nth_drop j xs)))
181 (index_seq 0 (length xs))
183 fun batch_list _ [] = []
185 if length xs <= k then [xs]
186 else List.take (xs, k) :: batch_list k (List.drop (xs, k))
188 fun chunk_list_unevenly _ [] = []
189 | chunk_list_unevenly [] ys = map single ys
190 | chunk_list_unevenly (k :: ks) ys =
191 let val (ys1, ys2) = chop k ys in ys1 :: chunk_list_unevenly ks ys2 end
193 fun map3 _ [] [] [] = []
194 | map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs
195 | map3 _ _ _ _ = raise UnequalLengths
197 fun double_lookup eq ps key =
198 case AList.lookup (fn (SOME x, SOME y) => eq (x, y) | _ => false) ps
201 | NONE => ps |> find_first (is_none o fst) |> Option.map snd
202 fun triple_lookup _ [(NONE, z)] _ = SOME z
203 | triple_lookup eq ps key =
204 case AList.lookup (op =) ps (SOME key) of
206 | NONE => double_lookup eq ps key
208 fun is_substring_of needle stack =
209 not (Substring.isEmpty (snd (Substring.position needle
210 (Substring.full stack))))
212 val plural_s = Sledgehammer_Util.plural_s
213 fun plural_s_for_list xs = plural_s (length xs)
215 val serial_commas = Sledgehammer_Util.serial_commas
217 val timestamp = Sledgehammer_Util.timestamp
218 val parse_bool_option = Sledgehammer_Util.parse_bool_option
219 val parse_time_option = Sledgehammer_Util.parse_time_option
221 fun flip_polarity Pos = Neg
222 | flip_polarity Neg = Pos
223 | flip_polarity Neut = Neut
225 val prop_T = @{typ prop}
226 val bool_T = @{typ bool}
227 val nat_T = @{typ nat}
228 val int_T = @{typ int}
230 val subscript = implode o map (prefix "\<^isub>") o explode
231 fun nat_subscript n =
232 (* cheap trick to ensure proper alphanumeric ordering for one- and two-digit
234 if n <= 9 then "\<^bsub>" ^ signed_string_of_int n ^ "\<^esub>"
235 else subscript (string_of_int n)
237 fun time_limit NONE = I
238 | time_limit (SOME delay) = TimeLimit.timeLimit delay
240 fun DETERM_TIMEOUT delay tac st =
241 Seq.of_list (the_list (time_limit delay (fn () => SINGLE tac st) ()))
243 fun setmp_show_all_types f =
244 setmp_CRITICAL show_all_types
245 (! show_types orelse ! show_sorts orelse ! show_all_types) f
249 val pstrs = Pretty.breaks o map Pretty.str o space_explode " "
251 val unyxml = Sledgehammer_Util.unyxml
252 val maybe_quote = Sledgehammer_Util.maybe_quote
254 (* This hash function is recommended in Compilers: Principles, Techniques, and
255 Tools, by Aho, Sethi, and Ullman. The "hashpjw" function, which they
256 particularly recommend, triggers a bug in versions of Poly/ML up to 4.2.0. *)
257 fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w))
258 fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w)
259 fun hashw_string (s:string, w) = CharVector.foldl hashw_char w s