blanchet@33192
|
1 |
(* Title: HOL/Nitpick/Tools/nitpick_util.ML
|
blanchet@33192
|
2 |
Author: Jasmin Blanchette, TU Muenchen
|
blanchet@33192
|
3 |
Copyright 2008, 2009
|
blanchet@33192
|
4 |
|
blanchet@33192
|
5 |
General-purpose functions used by the Nitpick modules.
|
blanchet@33192
|
6 |
*)
|
blanchet@33192
|
7 |
|
blanchet@33192
|
8 |
infix 6 nat_minus
|
blanchet@33192
|
9 |
infix 7 pairf
|
blanchet@33192
|
10 |
|
blanchet@33192
|
11 |
signature BASIC_NITPICK_UTIL =
|
blanchet@33192
|
12 |
sig
|
blanchet@33192
|
13 |
type styp = string * typ
|
blanchet@33192
|
14 |
end;
|
blanchet@33192
|
15 |
|
blanchet@33192
|
16 |
signature NITPICK_UTIL =
|
blanchet@33192
|
17 |
sig
|
blanchet@33192
|
18 |
include BASIC_NITPICK_UTIL
|
blanchet@33192
|
19 |
|
blanchet@33192
|
20 |
datatype polarity = Pos | Neg | Neut
|
blanchet@33192
|
21 |
|
blanchet@33192
|
22 |
exception ARG of string * string
|
blanchet@33192
|
23 |
exception BAD of string * string
|
blanchet@33192
|
24 |
exception LIMIT of string * string
|
blanchet@33192
|
25 |
exception NOT_SUPPORTED of string
|
blanchet@33192
|
26 |
exception SAME of unit
|
blanchet@33192
|
27 |
|
blanchet@33192
|
28 |
val nitpick_prefix : string
|
blanchet@33192
|
29 |
val curry3 : ('a * 'b * 'c -> 'd) -> 'a -> 'b -> 'c -> 'd
|
blanchet@33192
|
30 |
val pairf : ('a -> 'b) * ('a -> 'c) -> 'a -> 'b * 'c
|
blanchet@33192
|
31 |
val int_for_bool : bool -> int
|
blanchet@33192
|
32 |
val nat_minus : int * int -> int
|
blanchet@33192
|
33 |
val reasonable_power : int -> int -> int
|
blanchet@33192
|
34 |
val exact_log : int -> int -> int
|
blanchet@33192
|
35 |
val exact_root : int -> int -> int
|
blanchet@33192
|
36 |
val offset_list : int list -> int list
|
blanchet@33192
|
37 |
val index_seq : int -> int -> int list
|
blanchet@33192
|
38 |
val filter_indices : int list -> 'a list -> 'a list
|
blanchet@33192
|
39 |
val filter_out_indices : int list -> 'a list -> 'a list
|
blanchet@33192
|
40 |
val fold1 : ('a -> 'a -> 'a) -> 'a list -> 'a
|
blanchet@33192
|
41 |
val replicate_list : int -> 'a list -> 'a list
|
blanchet@33192
|
42 |
val n_fold_cartesian_product : 'a list list -> 'a list list
|
blanchet@33192
|
43 |
val all_distinct_unordered_pairs_of : ''a list -> (''a * ''a) list
|
blanchet@33192
|
44 |
val nth_combination : (int * int) list -> int -> int list
|
blanchet@33192
|
45 |
val all_combinations : (int * int) list -> int list list
|
blanchet@33192
|
46 |
val all_permutations : 'a list -> 'a list list
|
blanchet@33192
|
47 |
val batch_list : int -> 'a list -> 'a list list
|
blanchet@33192
|
48 |
val chunk_list_unevenly : int list -> 'a list -> 'a list list
|
blanchet@33192
|
49 |
val map3 : ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
|
blanchet@33192
|
50 |
val double_lookup :
|
blanchet@33192
|
51 |
('a * 'a -> bool) -> ('a option * 'b) list -> 'a -> 'b option
|
blanchet@33192
|
52 |
val triple_lookup :
|
blanchet@33192
|
53 |
(''a * ''a -> bool) -> (''a option * 'b) list -> ''a -> 'b option
|
blanchet@33192
|
54 |
val is_substring_of : string -> string -> bool
|
blanchet@33192
|
55 |
val serial_commas : string -> string list -> string list
|
blanchet@33192
|
56 |
val plural_s : int -> string
|
blanchet@33192
|
57 |
val plural_s_for_list : 'a list -> string
|
blanchet@33192
|
58 |
val flip_polarity : polarity -> polarity
|
blanchet@33192
|
59 |
val prop_T : typ
|
blanchet@33192
|
60 |
val bool_T : typ
|
blanchet@33192
|
61 |
val nat_T : typ
|
blanchet@33192
|
62 |
val int_T : typ
|
blanchet@33192
|
63 |
val subscript : string -> string
|
blanchet@33192
|
64 |
val nat_subscript : int -> string
|
blanchet@33192
|
65 |
val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b
|
blanchet@33192
|
66 |
val silence : ('a -> 'b) -> 'a -> 'b
|
blanchet@33192
|
67 |
val DETERM_TIMEOUT : Time.time option -> tactic -> tactic
|
blanchet@33192
|
68 |
val setmp_show_all_types : ('a -> 'b) -> 'a -> 'b
|
blanchet@33192
|
69 |
val indent_size : int
|
blanchet@33192
|
70 |
val pstrs : string -> Pretty.T list
|
blanchet@33192
|
71 |
val plain_string_from_yxml : string -> string
|
blanchet@33192
|
72 |
val maybe_quote : string -> string
|
blanchet@33192
|
73 |
end
|
blanchet@33192
|
74 |
|
blanchet@33224
|
75 |
structure Nitpick_Util : NITPICK_UTIL =
|
blanchet@33192
|
76 |
struct
|
blanchet@33192
|
77 |
|
blanchet@33192
|
78 |
type styp = string * typ
|
blanchet@33192
|
79 |
|
blanchet@33192
|
80 |
datatype polarity = Pos | Neg | Neut
|
blanchet@33192
|
81 |
|
blanchet@33192
|
82 |
exception ARG of string * string
|
blanchet@33192
|
83 |
exception BAD of string * string
|
blanchet@33192
|
84 |
exception LIMIT of string * string
|
blanchet@33192
|
85 |
exception NOT_SUPPORTED of string
|
blanchet@33192
|
86 |
exception SAME of unit
|
blanchet@33192
|
87 |
|
blanchet@33192
|
88 |
val nitpick_prefix = "Nitpick."
|
blanchet@33192
|
89 |
|
blanchet@33192
|
90 |
(* ('a * 'b * 'c -> 'd) -> 'a -> 'b -> 'c -> 'd *)
|
blanchet@33192
|
91 |
fun curry3 f = fn x => fn y => fn z => f (x, y, z)
|
blanchet@33192
|
92 |
|
blanchet@33192
|
93 |
(* ('a -> 'b) * ('a -> 'c) -> 'a -> 'b * 'c *)
|
blanchet@33192
|
94 |
fun (f pairf g) = fn x => (f x, g x)
|
blanchet@33192
|
95 |
|
blanchet@33192
|
96 |
(* bool -> int *)
|
blanchet@33192
|
97 |
fun int_for_bool b = if b then 1 else 0
|
blanchet@33192
|
98 |
(* int * int -> int *)
|
blanchet@33192
|
99 |
fun (i nat_minus j) = if i > j then i - j else 0
|
blanchet@33192
|
100 |
|
blanchet@33192
|
101 |
val max_exponent = 16384
|
blanchet@33192
|
102 |
|
blanchet@33192
|
103 |
(* int -> int -> int *)
|
blanchet@33192
|
104 |
fun reasonable_power a 0 = 1
|
blanchet@33192
|
105 |
| reasonable_power a 1 = a
|
blanchet@33192
|
106 |
| reasonable_power 0 _ = 0
|
blanchet@33192
|
107 |
| reasonable_power 1 _ = 1
|
blanchet@33192
|
108 |
| reasonable_power a b =
|
blanchet@33192
|
109 |
if b < 0 orelse b > max_exponent then
|
blanchet@33224
|
110 |
raise LIMIT ("Nitpick_Util.reasonable_power",
|
blanchet@33192
|
111 |
"too large exponent (" ^ signed_string_of_int b ^ ")")
|
blanchet@33192
|
112 |
else
|
blanchet@33192
|
113 |
let
|
blanchet@33192
|
114 |
val c = reasonable_power a (b div 2) in
|
blanchet@33192
|
115 |
c * c * reasonable_power a (b mod 2)
|
blanchet@33192
|
116 |
end
|
blanchet@33192
|
117 |
|
blanchet@33192
|
118 |
(* int -> int -> int *)
|
blanchet@33192
|
119 |
fun exact_log m n =
|
blanchet@33192
|
120 |
let
|
blanchet@33192
|
121 |
val r = Math.ln (Real.fromInt n) / Math.ln (Real.fromInt m) |> Real.round
|
blanchet@33192
|
122 |
in
|
blanchet@33192
|
123 |
if reasonable_power m r = n then
|
blanchet@33192
|
124 |
r
|
blanchet@33192
|
125 |
else
|
blanchet@33224
|
126 |
raise ARG ("Nitpick_Util.exact_log",
|
blanchet@33192
|
127 |
commas (map signed_string_of_int [m, n]))
|
blanchet@33192
|
128 |
end
|
blanchet@33192
|
129 |
|
blanchet@33192
|
130 |
(* int -> int -> int *)
|
blanchet@33192
|
131 |
fun exact_root m n =
|
blanchet@33192
|
132 |
let val r = Math.pow (Real.fromInt n, 1.0 / (Real.fromInt m)) |> Real.round in
|
blanchet@33192
|
133 |
if reasonable_power r m = n then
|
blanchet@33192
|
134 |
r
|
blanchet@33192
|
135 |
else
|
blanchet@33224
|
136 |
raise ARG ("Nitpick_Util.exact_root",
|
blanchet@33192
|
137 |
commas (map signed_string_of_int [m, n]))
|
blanchet@33192
|
138 |
end
|
blanchet@33192
|
139 |
|
blanchet@33192
|
140 |
(* ('a -> 'a -> 'a) -> 'a list -> 'a *)
|
blanchet@33192
|
141 |
fun fold1 f = foldl1 (uncurry f)
|
blanchet@33192
|
142 |
|
blanchet@33192
|
143 |
(* int -> 'a list -> 'a list *)
|
blanchet@33192
|
144 |
fun replicate_list 0 _ = []
|
blanchet@33192
|
145 |
| replicate_list n xs = xs @ replicate_list (n - 1) xs
|
blanchet@33192
|
146 |
|
blanchet@33192
|
147 |
(* int list -> int list *)
|
blanchet@33192
|
148 |
fun offset_list ns = rev (tl (fold (fn x => fn xs => (x + hd xs) :: xs) ns [0]))
|
blanchet@33192
|
149 |
(* int -> int -> int list *)
|
blanchet@33192
|
150 |
fun index_seq j0 n = if j0 < 0 then j0 downto j0 - n + 1 else j0 upto j0 + n - 1
|
blanchet@33192
|
151 |
|
blanchet@33192
|
152 |
(* int list -> 'a list -> 'a list *)
|
blanchet@33192
|
153 |
fun filter_indices js xs =
|
blanchet@33192
|
154 |
let
|
blanchet@33192
|
155 |
(* int -> int list -> 'a list -> 'a list *)
|
blanchet@33192
|
156 |
fun aux _ [] _ = []
|
blanchet@33192
|
157 |
| aux i (j :: js) (x :: xs) =
|
blanchet@33192
|
158 |
if i = j then x :: aux (i + 1) js xs else aux (i + 1) (j :: js) xs
|
blanchet@33224
|
159 |
| aux _ _ _ = raise ARG ("Nitpick_Util.filter_indices",
|
blanchet@33192
|
160 |
"indices unordered or out of range")
|
blanchet@33192
|
161 |
in aux 0 js xs end
|
blanchet@33192
|
162 |
fun filter_out_indices js xs =
|
blanchet@33192
|
163 |
let
|
blanchet@33192
|
164 |
(* int -> int list -> 'a list -> 'a list *)
|
blanchet@33192
|
165 |
fun aux _ [] xs = xs
|
blanchet@33192
|
166 |
| aux i (j :: js) (x :: xs) =
|
blanchet@33192
|
167 |
if i = j then aux (i + 1) js xs else x :: aux (i + 1) (j :: js) xs
|
blanchet@33224
|
168 |
| aux _ _ _ = raise ARG ("Nitpick_Util.filter_out_indices",
|
blanchet@33192
|
169 |
"indices unordered or out of range")
|
blanchet@33192
|
170 |
in aux 0 js xs end
|
blanchet@33192
|
171 |
|
blanchet@33192
|
172 |
(* 'a list -> 'a list list -> 'a list list *)
|
blanchet@33192
|
173 |
fun cartesian_product [] _ = []
|
blanchet@33192
|
174 |
| cartesian_product (x :: xs) yss =
|
blanchet@33192
|
175 |
map (cons x) yss @ cartesian_product xs yss
|
blanchet@33192
|
176 |
(* 'a list list -> 'a list list *)
|
blanchet@33192
|
177 |
fun n_fold_cartesian_product xss = fold_rev cartesian_product xss [[]]
|
blanchet@33192
|
178 |
(* ''a list -> (''a * ''a) list *)
|
blanchet@33192
|
179 |
fun all_distinct_unordered_pairs_of [] = []
|
blanchet@33192
|
180 |
| all_distinct_unordered_pairs_of (x :: xs) =
|
blanchet@33192
|
181 |
map (pair x) xs @ all_distinct_unordered_pairs_of xs
|
blanchet@33192
|
182 |
|
blanchet@33192
|
183 |
(* (int * int) list -> int -> int list *)
|
blanchet@33192
|
184 |
val nth_combination =
|
blanchet@33192
|
185 |
let
|
blanchet@33192
|
186 |
(* (int * int) list -> int -> int list * int *)
|
blanchet@33192
|
187 |
fun aux [] n = ([], n)
|
blanchet@33192
|
188 |
| aux ((k, j0) :: xs) n =
|
blanchet@33192
|
189 |
let val (js, n) = aux xs n in ((n mod k) + j0 :: js, n div k) end
|
blanchet@33192
|
190 |
in fst oo aux end
|
blanchet@33192
|
191 |
|
blanchet@33192
|
192 |
(* (int * int) list -> int list list *)
|
blanchet@33192
|
193 |
val all_combinations = n_fold_cartesian_product o map (uncurry index_seq o swap)
|
blanchet@33192
|
194 |
|
blanchet@33192
|
195 |
(* 'a list -> 'a list list *)
|
blanchet@33192
|
196 |
fun all_permutations [] = [[]]
|
blanchet@33192
|
197 |
| all_permutations xs =
|
blanchet@33192
|
198 |
maps (fn j => map (cons (nth xs j)) (all_permutations (nth_drop j xs)))
|
blanchet@33192
|
199 |
(index_seq 0 (length xs))
|
blanchet@33192
|
200 |
|
blanchet@33192
|
201 |
(* int -> 'a list -> 'a list list *)
|
blanchet@33192
|
202 |
fun batch_list _ [] = []
|
blanchet@33192
|
203 |
| batch_list k xs =
|
blanchet@33192
|
204 |
if length xs <= k then [xs]
|
blanchet@33192
|
205 |
else List.take (xs, k) :: batch_list k (List.drop (xs, k))
|
blanchet@33192
|
206 |
|
blanchet@33192
|
207 |
(* int list -> 'a list -> 'a list list *)
|
blanchet@33192
|
208 |
fun chunk_list_unevenly _ [] = []
|
blanchet@33192
|
209 |
| chunk_list_unevenly [] ys = map single ys
|
blanchet@33192
|
210 |
| chunk_list_unevenly (k :: ks) ys =
|
blanchet@33192
|
211 |
let val (ys1, ys2) = chop k ys in ys1 :: chunk_list_unevenly ks ys2 end
|
blanchet@33192
|
212 |
|
blanchet@33192
|
213 |
(* ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list *)
|
blanchet@33192
|
214 |
fun map3 _ [] [] [] = []
|
blanchet@33192
|
215 |
| map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs
|
blanchet@33192
|
216 |
| map3 _ _ _ _ = raise UnequalLengths
|
blanchet@33192
|
217 |
|
blanchet@33192
|
218 |
(* ('a * 'a -> bool) -> ('a option * 'b) list -> 'a -> 'b option *)
|
blanchet@33192
|
219 |
fun double_lookup eq ps key =
|
blanchet@33192
|
220 |
case AList.lookup (fn (SOME x, SOME y) => eq (x, y) | _ => false) ps
|
blanchet@33192
|
221 |
(SOME key) of
|
blanchet@33192
|
222 |
SOME z => SOME z
|
blanchet@33192
|
223 |
| NONE => ps |> find_first (is_none o fst) |> Option.map snd
|
blanchet@33192
|
224 |
(* (''a * ''a -> bool) -> (''a option * 'b) list -> ''a -> 'b option *)
|
blanchet@33192
|
225 |
fun triple_lookup eq ps key =
|
blanchet@33192
|
226 |
case AList.lookup (op =) ps (SOME key) of
|
blanchet@33192
|
227 |
SOME z => SOME z
|
blanchet@33192
|
228 |
| NONE => double_lookup eq ps key
|
blanchet@33192
|
229 |
|
blanchet@33192
|
230 |
(* string -> string -> bool *)
|
blanchet@33192
|
231 |
fun is_substring_of needle stack =
|
blanchet@33192
|
232 |
not (Substring.isEmpty (snd (Substring.position needle
|
blanchet@33192
|
233 |
(Substring.full stack))))
|
blanchet@33192
|
234 |
|
blanchet@33192
|
235 |
(* string -> string list -> string list *)
|
blanchet@33192
|
236 |
fun serial_commas _ [] = ["??"]
|
blanchet@33192
|
237 |
| serial_commas _ [s] = [s]
|
blanchet@33192
|
238 |
| serial_commas conj [s1, s2] = [s1, conj, s2]
|
blanchet@33192
|
239 |
| serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
|
blanchet@33192
|
240 |
| serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
|
blanchet@33192
|
241 |
|
blanchet@33192
|
242 |
(* int -> string *)
|
blanchet@33192
|
243 |
fun plural_s n = if n = 1 then "" else "s"
|
blanchet@33192
|
244 |
(* 'a list -> string *)
|
blanchet@33192
|
245 |
fun plural_s_for_list xs = plural_s (length xs)
|
blanchet@33192
|
246 |
|
blanchet@33192
|
247 |
(* polarity -> polarity *)
|
blanchet@33192
|
248 |
fun flip_polarity Pos = Neg
|
blanchet@33192
|
249 |
| flip_polarity Neg = Pos
|
blanchet@33192
|
250 |
| flip_polarity Neut = Neut
|
blanchet@33192
|
251 |
|
blanchet@33192
|
252 |
val prop_T = @{typ prop}
|
blanchet@33192
|
253 |
val bool_T = @{typ bool}
|
blanchet@33192
|
254 |
val nat_T = @{typ nat}
|
blanchet@33192
|
255 |
val int_T = @{typ int}
|
blanchet@33192
|
256 |
|
blanchet@33192
|
257 |
(* string -> string *)
|
blanchet@33192
|
258 |
val subscript = implode o map (prefix "\<^isub>") o explode
|
blanchet@33192
|
259 |
(* int -> string *)
|
blanchet@33192
|
260 |
val nat_subscript = subscript o signed_string_of_int
|
blanchet@33192
|
261 |
|
blanchet@33192
|
262 |
(* Time.time option -> ('a -> 'b) -> 'a -> 'b *)
|
blanchet@33192
|
263 |
fun time_limit NONE f = f
|
blanchet@33192
|
264 |
| time_limit (SOME delay) f = TimeLimit.timeLimit delay f
|
blanchet@33192
|
265 |
|
blanchet@33192
|
266 |
(* (string -> unit) Unsynchronized.ref -> ('a -> 'b) -> 'a -> 'b *)
|
blanchet@33192
|
267 |
fun silence_one out_fn = setmp_CRITICAL out_fn (K ())
|
blanchet@33192
|
268 |
|
blanchet@33192
|
269 |
(* ('a -> 'b) -> 'a -> 'b *)
|
blanchet@33192
|
270 |
fun silence f =
|
blanchet@33192
|
271 |
fold silence_one
|
blanchet@33192
|
272 |
[Output.writeln_fn, Output.priority_fn, Output.tracing_fn,
|
blanchet@33192
|
273 |
Output.warning_fn, Output.error_fn, Output.debug_fn] f
|
blanchet@33192
|
274 |
|
blanchet@33192
|
275 |
(* Time.time option -> tactic -> tactic *)
|
blanchet@33192
|
276 |
fun DETERM_TIMEOUT delay tac st =
|
blanchet@33192
|
277 |
Seq.of_list (the_list (time_limit delay (fn () => SINGLE tac st) ()))
|
blanchet@33192
|
278 |
|
blanchet@33192
|
279 |
(* ('a -> 'b) -> 'a -> 'b *)
|
blanchet@33192
|
280 |
fun setmp_show_all_types f =
|
blanchet@33192
|
281 |
setmp_CRITICAL show_all_types
|
blanchet@33192
|
282 |
(! show_types orelse ! show_sorts orelse ! show_all_types) f
|
blanchet@33192
|
283 |
|
blanchet@33192
|
284 |
val indent_size = 2
|
blanchet@33192
|
285 |
|
blanchet@33192
|
286 |
(* string -> Pretty.T list *)
|
blanchet@33192
|
287 |
val pstrs = Pretty.breaks o map Pretty.str o space_explode " "
|
blanchet@33192
|
288 |
|
blanchet@33192
|
289 |
(* XML.tree -> string *)
|
blanchet@33192
|
290 |
fun plain_string_from_xml_tree t =
|
blanchet@33192
|
291 |
Buffer.empty |> XML.add_content t |> Buffer.content
|
blanchet@33192
|
292 |
(* string -> string *)
|
blanchet@33192
|
293 |
val plain_string_from_yxml = plain_string_from_xml_tree o YXML.parse
|
blanchet@33192
|
294 |
|
blanchet@33192
|
295 |
(* string -> bool *)
|
blanchet@33192
|
296 |
val is_long_identifier = forall Syntax.is_identifier o space_explode "."
|
blanchet@33192
|
297 |
(* string -> string *)
|
blanchet@33192
|
298 |
fun maybe_quote y =
|
blanchet@33192
|
299 |
let val s = plain_string_from_yxml y in
|
blanchet@33192
|
300 |
y |> (not (is_long_identifier (perhaps (try (unprefix "'")) s))
|
blanchet@33192
|
301 |
orelse OuterKeyword.is_keyword s) ? quote
|
blanchet@33192
|
302 |
end
|
blanchet@33192
|
303 |
|
blanchet@33192
|
304 |
end;
|
blanchet@33192
|
305 |
|
blanchet@33224
|
306 |
structure Basic_Nitpick_Util : BASIC_NITPICK_UTIL = Nitpick_Util;
|
blanchet@33224
|
307 |
open Basic_Nitpick_Util;
|