author | blanchet |
Mon, 07 Jan 2013 19:15:01 +0100 | |
changeset 50758 | 26936f4ae087 |
parent 45778 | df6e210fb44c |
child 72004 | 913162a47d9f |
permissions | -rw-r--r-- |
39348 | 1 |
(* ========================================================================= *) |
2 |
(* ML UTILITY FUNCTIONS *) |
|
39502 | 3 |
(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *) |
39348 | 4 |
(* ========================================================================= *) |
5 |
||
6 |
structure Useful :> Useful = |
|
7 |
struct |
|
8 |
||
9 |
(* ------------------------------------------------------------------------- *) |
|
10 |
(* Exceptions. *) |
|
11 |
(* ------------------------------------------------------------------------- *) |
|
12 |
||
13 |
exception Error of string; |
|
14 |
||
15 |
exception Bug of string; |
|
16 |
||
17 |
fun errorToStringOption err = |
|
18 |
case err of |
|
19 |
Error message => SOME ("Error: " ^ message) |
|
20 |
| _ => NONE; |
|
21 |
||
22 |
(*mlton |
|
23 |
val () = MLton.Exn.addExnMessager errorToStringOption; |
|
24 |
*) |
|
25 |
||
26 |
fun errorToString err = |
|
27 |
case errorToStringOption err of |
|
28 |
SOME s => "\n" ^ s ^ "\n" |
|
29 |
| NONE => raise Bug "errorToString: not an Error exception"; |
|
30 |
||
31 |
fun bugToStringOption err = |
|
32 |
case err of |
|
33 |
Bug message => SOME ("Bug: " ^ message) |
|
34 |
| _ => NONE; |
|
35 |
||
36 |
(*mlton |
|
37 |
val () = MLton.Exn.addExnMessager bugToStringOption; |
|
38 |
*) |
|
39 |
||
40 |
fun bugToString err = |
|
41 |
case bugToStringOption err of |
|
42 |
SOME s => "\n" ^ s ^ "\n" |
|
43 |
| NONE => raise Bug "bugToString: not a Bug exception"; |
|
44 |
||
45 |
fun total f x = SOME (f x) handle Error _ => NONE; |
|
46 |
||
47 |
fun can f = Option.isSome o total f; |
|
48 |
||
49 |
(* ------------------------------------------------------------------------- *) |
|
50 |
(* Tracing. *) |
|
51 |
(* ------------------------------------------------------------------------- *) |
|
52 |
||
42102 | 53 |
local |
54 |
val traceOut = TextIO.stdOut; |
|
55 |
||
56 |
fun tracePrintFn mesg = |
|
57 |
let |
|
58 |
val () = TextIO.output (traceOut,mesg) |
|
59 |
||
60 |
val () = TextIO.flushOut traceOut |
|
61 |
in |
|
62 |
() |
|
63 |
end; |
|
64 |
in |
|
65 |
val tracePrint = ref tracePrintFn; |
|
66 |
end; |
|
39348 | 67 |
|
68 |
fun trace mesg = !tracePrint mesg; |
|
69 |
||
70 |
(* ------------------------------------------------------------------------- *) |
|
71 |
(* Combinators. *) |
|
72 |
(* ------------------------------------------------------------------------- *) |
|
73 |
||
74 |
fun C f x y = f y x; |
|
75 |
||
76 |
fun I x = x; |
|
77 |
||
78 |
fun K x y = x; |
|
79 |
||
80 |
fun S f g x = f x (g x); |
|
81 |
||
82 |
fun W f x = f x x; |
|
83 |
||
84 |
fun funpow 0 _ x = x |
|
85 |
| funpow n f x = funpow (n - 1) f (f x); |
|
86 |
||
87 |
fun exp m = |
|
88 |
let |
|
89 |
fun f _ 0 z = z |
|
90 |
| f x y z = f (m (x,x)) (y div 2) (if y mod 2 = 0 then z else m (z,x)) |
|
91 |
in |
|
92 |
f |
|
93 |
end; |
|
94 |
||
95 |
(* ------------------------------------------------------------------------- *) |
|
96 |
(* Pairs. *) |
|
97 |
(* ------------------------------------------------------------------------- *) |
|
98 |
||
99 |
fun fst (x,_) = x; |
|
100 |
||
101 |
fun snd (_,y) = y; |
|
102 |
||
103 |
fun pair x y = (x,y); |
|
104 |
||
105 |
fun swap (x,y) = (y,x); |
|
106 |
||
107 |
fun curry f x y = f (x,y); |
|
108 |
||
109 |
fun uncurry f (x,y) = f x y; |
|
110 |
||
111 |
val op## = fn (f,g) => fn (x,y) => (f x, g y); |
|
112 |
||
113 |
(* ------------------------------------------------------------------------- *) |
|
114 |
(* State transformers. *) |
|
115 |
(* ------------------------------------------------------------------------- *) |
|
116 |
||
117 |
val unit : 'a -> 's -> 'a * 's = pair; |
|
118 |
||
119 |
fun bind f (g : 'a -> 's -> 'b * 's) = uncurry g o f; |
|
120 |
||
121 |
fun mmap f (m : 's -> 'a * 's) = bind m (unit o f); |
|
122 |
||
123 |
fun mjoin (f : 's -> ('s -> 'a * 's) * 's) = bind f I; |
|
124 |
||
125 |
fun mwhile c b = let fun f a = if c a then bind (b a) f else unit a in f end; |
|
126 |
||
127 |
(* ------------------------------------------------------------------------- *) |
|
128 |
(* Equality. *) |
|
129 |
(* ------------------------------------------------------------------------- *) |
|
130 |
||
131 |
val equal = fn x => fn y => x = y; |
|
132 |
||
133 |
val notEqual = fn x => fn y => x <> y; |
|
134 |
||
135 |
fun listEqual xEq = |
|
136 |
let |
|
137 |
fun xsEq [] [] = true |
|
138 |
| xsEq (x1 :: xs1) (x2 :: xs2) = xEq x1 x2 andalso xsEq xs1 xs2 |
|
139 |
| xsEq _ _ = false |
|
140 |
in |
|
141 |
xsEq |
|
142 |
end; |
|
143 |
||
144 |
(* ------------------------------------------------------------------------- *) |
|
145 |
(* Comparisons. *) |
|
146 |
(* ------------------------------------------------------------------------- *) |
|
147 |
||
148 |
fun mapCompare f cmp (a,b) = cmp (f a, f b); |
|
149 |
||
150 |
fun revCompare cmp x_y = |
|
151 |
case cmp x_y of LESS => GREATER | EQUAL => EQUAL | GREATER => LESS; |
|
152 |
||
153 |
fun prodCompare xCmp yCmp ((x1,y1),(x2,y2)) = |
|
154 |
case xCmp (x1,x2) of |
|
155 |
LESS => LESS |
|
156 |
| EQUAL => yCmp (y1,y2) |
|
157 |
| GREATER => GREATER; |
|
158 |
||
159 |
fun lexCompare cmp = |
|
160 |
let |
|
161 |
fun lex ([],[]) = EQUAL |
|
162 |
| lex ([], _ :: _) = LESS |
|
163 |
| lex (_ :: _, []) = GREATER |
|
164 |
| lex (x :: xs, y :: ys) = |
|
165 |
case cmp (x,y) of |
|
166 |
LESS => LESS |
|
167 |
| EQUAL => lex (xs,ys) |
|
168 |
| GREATER => GREATER |
|
169 |
in |
|
170 |
lex |
|
171 |
end; |
|
172 |
||
173 |
fun optionCompare _ (NONE,NONE) = EQUAL |
|
174 |
| optionCompare _ (NONE,_) = LESS |
|
175 |
| optionCompare _ (_,NONE) = GREATER |
|
176 |
| optionCompare cmp (SOME x, SOME y) = cmp (x,y); |
|
177 |
||
178 |
fun boolCompare (false,true) = LESS |
|
179 |
| boolCompare (true,false) = GREATER |
|
180 |
| boolCompare _ = EQUAL; |
|
181 |
||
182 |
(* ------------------------------------------------------------------------- *) |
|
183 |
(* Lists. *) |
|
184 |
(* ------------------------------------------------------------------------- *) |
|
185 |
||
186 |
fun cons x y = x :: y; |
|
187 |
||
188 |
fun hdTl l = (hd l, tl l); |
|
189 |
||
190 |
fun append xs ys = xs @ ys; |
|
191 |
||
192 |
fun singleton a = [a]; |
|
193 |
||
194 |
fun first f [] = NONE |
|
195 |
| first f (x :: xs) = (case f x of NONE => first f xs | s => s); |
|
196 |
||
197 |
fun maps (_ : 'a -> 's -> 'b * 's) [] = unit [] |
|
198 |
| maps f (x :: xs) = |
|
199 |
bind (f x) (fn y => bind (maps f xs) (fn ys => unit (y :: ys))); |
|
200 |
||
201 |
fun mapsPartial (_ : 'a -> 's -> 'b option * 's) [] = unit [] |
|
202 |
| mapsPartial f (x :: xs) = |
|
203 |
bind |
|
204 |
(f x) |
|
205 |
(fn yo => |
|
206 |
bind |
|
207 |
(mapsPartial f xs) |
|
208 |
(fn ys => unit (case yo of NONE => ys | SOME y => y :: ys))); |
|
209 |
||
210 |
fun zipWith f = |
|
211 |
let |
|
212 |
fun z l [] [] = l |
|
213 |
| z l (x :: xs) (y :: ys) = z (f x y :: l) xs ys |
|
214 |
| z _ _ _ = raise Error "zipWith: lists different lengths"; |
|
215 |
in |
|
45778 | 216 |
fn xs => fn ys => List.rev (z [] xs ys) |
39348 | 217 |
end; |
218 |
||
219 |
fun zip xs ys = zipWith pair xs ys; |
|
220 |
||
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
221 |
local |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
222 |
fun inc ((x,y),(xs,ys)) = (x :: xs, y :: ys); |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
223 |
in |
45778 | 224 |
fun unzip ab = List.foldl inc ([],[]) (List.rev ab); |
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
225 |
end; |
39348 | 226 |
|
227 |
fun cartwith f = |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
228 |
let |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
229 |
fun aux _ res _ [] = res |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
230 |
| aux xsCopy res [] (y :: yt) = aux xsCopy res xsCopy yt |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
231 |
| aux xsCopy res (x :: xt) (ys as y :: _) = |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
232 |
aux xsCopy (f x y :: res) xt ys |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
233 |
in |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
234 |
fn xs => fn ys => |
45778 | 235 |
let val xs' = List.rev xs in aux xs' [] xs' (List.rev ys) end |
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
236 |
end; |
39348 | 237 |
|
238 |
fun cart xs ys = cartwith pair xs ys; |
|
239 |
||
240 |
fun takeWhile p = |
|
241 |
let |
|
45778 | 242 |
fun f acc [] = List.rev acc |
243 |
| f acc (x :: xs) = if p x then f (x :: acc) xs else List.rev acc |
|
39348 | 244 |
in |
245 |
f [] |
|
246 |
end; |
|
247 |
||
248 |
fun dropWhile p = |
|
249 |
let |
|
250 |
fun f [] = [] |
|
251 |
| f (l as x :: xs) = if p x then f xs else l |
|
252 |
in |
|
253 |
f |
|
254 |
end; |
|
255 |
||
256 |
fun divideWhile p = |
|
257 |
let |
|
45778 | 258 |
fun f acc [] = (List.rev acc, []) |
259 |
| f acc (l as x :: xs) = if p x then f (x :: acc) xs else (List.rev acc, l) |
|
39348 | 260 |
in |
261 |
f [] |
|
262 |
end; |
|
263 |
||
264 |
fun groups f = |
|
265 |
let |
|
266 |
fun group acc row x l = |
|
267 |
case l of |
|
268 |
[] => |
|
269 |
let |
|
45778 | 270 |
val acc = if List.null row then acc else List.rev row :: acc |
39348 | 271 |
in |
45778 | 272 |
List.rev acc |
39348 | 273 |
end |
274 |
| h :: t => |
|
275 |
let |
|
276 |
val (eor,x) = f (h,x) |
|
277 |
in |
|
45778 | 278 |
if eor then group (List.rev row :: acc) [h] x t |
39348 | 279 |
else group acc (h :: row) x t |
280 |
end |
|
281 |
in |
|
282 |
group [] [] |
|
283 |
end; |
|
284 |
||
285 |
fun groupsBy eq = |
|
286 |
let |
|
287 |
fun f (x_y as (x,_)) = (not (eq x_y), x) |
|
288 |
in |
|
289 |
fn [] => [] |
|
290 |
| h :: t => |
|
291 |
case groups f h t of |
|
292 |
[] => [[h]] |
|
293 |
| hs :: ts => (h :: hs) :: ts |
|
294 |
end; |
|
295 |
||
296 |
local |
|
297 |
fun fstEq ((x,_),(y,_)) = x = y; |
|
298 |
||
42102 | 299 |
fun collapse l = (fst (hd l), List.map snd l); |
39348 | 300 |
in |
42102 | 301 |
fun groupsByFst l = List.map collapse (groupsBy fstEq l); |
39348 | 302 |
end; |
303 |
||
304 |
fun groupsOf n = |
|
305 |
let |
|
306 |
fun f (_,i) = if i = 1 then (true,n) else (false, i - 1) |
|
307 |
in |
|
308 |
groups f (n + 1) |
|
309 |
end; |
|
310 |
||
311 |
fun index p = |
|
312 |
let |
|
313 |
fun idx _ [] = NONE |
|
314 |
| idx n (x :: xs) = if p x then SOME n else idx (n + 1) xs |
|
315 |
in |
|
316 |
idx 0 |
|
317 |
end; |
|
318 |
||
319 |
fun enumerate l = fst (maps (fn x => fn m => ((m, x), m + 1)) l 0); |
|
320 |
||
321 |
local |
|
322 |
fun revDiv acc l 0 = (acc,l) |
|
323 |
| revDiv _ [] _ = raise Subscript |
|
324 |
| revDiv acc (h :: t) n = revDiv (h :: acc) t (n - 1); |
|
325 |
in |
|
326 |
fun revDivide l = revDiv [] l; |
|
327 |
end; |
|
328 |
||
45778 | 329 |
fun divide l n = let val (a,b) = revDivide l n in (List.rev a, b) end; |
39348 | 330 |
|
331 |
fun updateNth (n,x) l = |
|
332 |
let |
|
333 |
val (a,b) = revDivide l n |
|
334 |
in |
|
335 |
case b of [] => raise Subscript | _ :: t => List.revAppend (a, x :: t) |
|
336 |
end; |
|
337 |
||
338 |
fun deleteNth n l = |
|
339 |
let |
|
340 |
val (a,b) = revDivide l n |
|
341 |
in |
|
342 |
case b of [] => raise Subscript | _ :: t => List.revAppend (a,t) |
|
343 |
end; |
|
344 |
||
345 |
(* ------------------------------------------------------------------------- *) |
|
346 |
(* Sets implemented with lists. *) |
|
347 |
(* ------------------------------------------------------------------------- *) |
|
348 |
||
349 |
fun mem x = List.exists (equal x); |
|
350 |
||
351 |
fun insert x s = if mem x s then s else x :: s; |
|
352 |
||
353 |
fun delete x s = List.filter (not o equal x) s; |
|
354 |
||
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
355 |
local |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
356 |
fun inc (v,x) = if mem v x then x else v :: x; |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
357 |
in |
45778 | 358 |
fun setify s = List.rev (List.foldl inc [] s); |
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
359 |
end; |
39348 | 360 |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
361 |
fun union s t = |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
362 |
let |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
363 |
fun inc (v,x) = if mem v t then x else v :: x |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
364 |
in |
45778 | 365 |
List.foldl inc t (List.rev s) |
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
366 |
end; |
39348 | 367 |
|
368 |
fun intersect s t = |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
369 |
let |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
370 |
fun inc (v,x) = if mem v t then v :: x else x |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
371 |
in |
45778 | 372 |
List.foldl inc [] (List.rev s) |
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
373 |
end; |
39348 | 374 |
|
375 |
fun difference s t = |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
376 |
let |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
377 |
fun inc (v,x) = if mem v t then x else v :: x |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
378 |
in |
45778 | 379 |
List.foldl inc [] (List.rev s) |
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
380 |
end; |
39348 | 381 |
|
382 |
fun subset s t = List.all (fn x => mem x t) s; |
|
383 |
||
384 |
fun distinct [] = true |
|
385 |
| distinct (x :: rest) = not (mem x rest) andalso distinct rest; |
|
386 |
||
387 |
(* ------------------------------------------------------------------------- *) |
|
388 |
(* Sorting and searching. *) |
|
389 |
(* ------------------------------------------------------------------------- *) |
|
390 |
||
391 |
(* Finding the minimum and maximum element of a list, wrt some order. *) |
|
392 |
||
393 |
fun minimum cmp = |
|
394 |
let |
|
395 |
fun min (l,m,r) _ [] = (m, List.revAppend (l,r)) |
|
396 |
| min (best as (_,m,_)) l (x :: r) = |
|
397 |
min (case cmp (x,m) of LESS => (l,x,r) | _ => best) (x :: l) r |
|
398 |
in |
|
399 |
fn [] => raise Empty |
|
400 |
| h :: t => min ([],h,t) [h] t |
|
401 |
end; |
|
402 |
||
403 |
fun maximum cmp = minimum (revCompare cmp); |
|
404 |
||
405 |
(* Merge (for the following merge-sort, but generally useful too). *) |
|
406 |
||
407 |
fun merge cmp = |
|
408 |
let |
|
409 |
fun mrg acc [] ys = List.revAppend (acc,ys) |
|
410 |
| mrg acc xs [] = List.revAppend (acc,xs) |
|
411 |
| mrg acc (xs as x :: xt) (ys as y :: yt) = |
|
412 |
(case cmp (x,y) of |
|
413 |
GREATER => mrg (y :: acc) xs yt |
|
414 |
| _ => mrg (x :: acc) xt ys) |
|
415 |
in |
|
416 |
mrg [] |
|
417 |
end; |
|
418 |
||
419 |
(* Merge sort (stable). *) |
|
420 |
||
421 |
fun sort cmp = |
|
422 |
let |
|
45778 | 423 |
fun findRuns acc r rs [] = List.rev (List.rev (r :: rs) :: acc) |
39348 | 424 |
| findRuns acc r rs (x :: xs) = |
425 |
case cmp (r,x) of |
|
45778 | 426 |
GREATER => findRuns (List.rev (r :: rs) :: acc) x [] xs |
39348 | 427 |
| _ => findRuns acc x (r :: rs) xs |
428 |
||
45778 | 429 |
fun mergeAdj acc [] = List.rev acc |
39348 | 430 |
| mergeAdj acc (xs as [_]) = List.revAppend (acc,xs) |
431 |
| mergeAdj acc (x :: y :: xs) = mergeAdj (merge cmp x y :: acc) xs |
|
432 |
||
433 |
fun mergePairs [xs] = xs |
|
434 |
| mergePairs l = mergePairs (mergeAdj [] l) |
|
435 |
in |
|
436 |
fn [] => [] |
|
437 |
| l as [_] => l |
|
438 |
| h :: t => mergePairs (findRuns [] h [] t) |
|
439 |
end; |
|
440 |
||
441 |
fun sortMap _ _ [] = [] |
|
442 |
| sortMap _ _ (l as [_]) = l |
|
443 |
| sortMap f cmp xs = |
|
444 |
let |
|
445 |
fun ncmp ((m,_),(n,_)) = cmp (m,n) |
|
42102 | 446 |
val nxs = List.map (fn x => (f x, x)) xs |
39348 | 447 |
val nys = sort ncmp nxs |
448 |
in |
|
42102 | 449 |
List.map snd nys |
39348 | 450 |
end; |
451 |
||
452 |
(* ------------------------------------------------------------------------- *) |
|
453 |
(* Integers. *) |
|
454 |
(* ------------------------------------------------------------------------- *) |
|
455 |
||
456 |
fun interval m 0 = [] |
|
457 |
| interval m len = m :: interval (m + 1) (len - 1); |
|
458 |
||
459 |
fun divides _ 0 = true |
|
460 |
| divides 0 _ = false |
|
461 |
| divides a b = b mod (Int.abs a) = 0; |
|
462 |
||
463 |
local |
|
464 |
fun hcf 0 n = n |
|
465 |
| hcf 1 _ = 1 |
|
466 |
| hcf m n = hcf (n mod m) m; |
|
467 |
in |
|
468 |
fun gcd m n = |
|
469 |
let |
|
470 |
val m = Int.abs m |
|
471 |
and n = Int.abs n |
|
472 |
in |
|
473 |
if m < n then hcf m n else hcf n m |
|
474 |
end; |
|
475 |
end; |
|
476 |
||
477 |
local |
|
39501
aaa7078fff55
updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents:
39445
diff
changeset
|
478 |
fun calcPrimes mode ps i n = |
aaa7078fff55
updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents:
39445
diff
changeset
|
479 |
if n = 0 then ps |
aaa7078fff55
updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents:
39445
diff
changeset
|
480 |
else if List.exists (fn p => divides p i) ps then |
aaa7078fff55
updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents:
39445
diff
changeset
|
481 |
let |
aaa7078fff55
updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents:
39445
diff
changeset
|
482 |
val i = i + 1 |
aaa7078fff55
updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents:
39445
diff
changeset
|
483 |
and n = if mode then n else n - 1 |
aaa7078fff55
updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents:
39445
diff
changeset
|
484 |
in |
aaa7078fff55
updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents:
39445
diff
changeset
|
485 |
calcPrimes mode ps i n |
aaa7078fff55
updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents:
39445
diff
changeset
|
486 |
end |
39348 | 487 |
else |
488 |
let |
|
489 |
val ps = ps @ [i] |
|
39501
aaa7078fff55
updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents:
39445
diff
changeset
|
490 |
and i = i + 1 |
39348 | 491 |
and n = n - 1 |
492 |
in |
|
39501
aaa7078fff55
updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents:
39445
diff
changeset
|
493 |
calcPrimes mode ps i n |
39348 | 494 |
end; |
495 |
in |
|
39501
aaa7078fff55
updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents:
39445
diff
changeset
|
496 |
fun primes n = |
aaa7078fff55
updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents:
39445
diff
changeset
|
497 |
if n <= 0 then [] |
aaa7078fff55
updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents:
39445
diff
changeset
|
498 |
else calcPrimes true [2] 3 (n - 1); |
39348 | 499 |
|
39501
aaa7078fff55
updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents:
39445
diff
changeset
|
500 |
fun primesUpTo n = |
aaa7078fff55
updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents:
39445
diff
changeset
|
501 |
if n < 2 then [] |
aaa7078fff55
updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents:
39445
diff
changeset
|
502 |
else calcPrimes false [2] 3 (n - 2); |
39348 | 503 |
end; |
504 |
||
505 |
(* ------------------------------------------------------------------------- *) |
|
506 |
(* Strings. *) |
|
507 |
(* ------------------------------------------------------------------------- *) |
|
508 |
||
509 |
local |
|
510 |
fun len l = (length l, l) |
|
511 |
||
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
512 |
val upper = len (String.explode "ABCDEFGHIJKLMNOPQRSTUVWXYZ"); |
39348 | 513 |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
514 |
val lower = len (String.explode "abcdefghijklmnopqrstuvwxyz"); |
39348 | 515 |
|
516 |
fun rotate (n,l) c k = |
|
517 |
List.nth (l, (k + Option.valOf (index (equal c) l)) mod n); |
|
518 |
in |
|
519 |
fun rot k c = |
|
520 |
if Char.isLower c then rotate lower c k |
|
521 |
else if Char.isUpper c then rotate upper c k |
|
522 |
else c; |
|
523 |
end; |
|
524 |
||
525 |
fun charToInt #"0" = SOME 0 |
|
526 |
| charToInt #"1" = SOME 1 |
|
527 |
| charToInt #"2" = SOME 2 |
|
528 |
| charToInt #"3" = SOME 3 |
|
529 |
| charToInt #"4" = SOME 4 |
|
530 |
| charToInt #"5" = SOME 5 |
|
531 |
| charToInt #"6" = SOME 6 |
|
532 |
| charToInt #"7" = SOME 7 |
|
533 |
| charToInt #"8" = SOME 8 |
|
534 |
| charToInt #"9" = SOME 9 |
|
535 |
| charToInt _ = NONE; |
|
536 |
||
537 |
fun charFromInt 0 = SOME #"0" |
|
538 |
| charFromInt 1 = SOME #"1" |
|
539 |
| charFromInt 2 = SOME #"2" |
|
540 |
| charFromInt 3 = SOME #"3" |
|
541 |
| charFromInt 4 = SOME #"4" |
|
542 |
| charFromInt 5 = SOME #"5" |
|
543 |
| charFromInt 6 = SOME #"6" |
|
544 |
| charFromInt 7 = SOME #"7" |
|
545 |
| charFromInt 8 = SOME #"8" |
|
546 |
| charFromInt 9 = SOME #"9" |
|
547 |
| charFromInt _ = NONE; |
|
548 |
||
549 |
fun nChars x = |
|
550 |
let |
|
551 |
fun dup 0 l = l | dup n l = dup (n - 1) (x :: l) |
|
552 |
in |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
553 |
fn n => String.implode (dup n []) |
39348 | 554 |
end; |
555 |
||
556 |
fun chomp s = |
|
557 |
let |
|
558 |
val n = size s |
|
559 |
in |
|
560 |
if n = 0 orelse String.sub (s, n - 1) <> #"\n" then s |
|
561 |
else String.substring (s, 0, n - 1) |
|
562 |
end; |
|
563 |
||
564 |
local |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
565 |
fun chop l = |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
566 |
case l of |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
567 |
[] => [] |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
568 |
| h :: t => if Char.isSpace h then chop t else l; |
39348 | 569 |
in |
45778 | 570 |
val trim = String.implode o chop o List.rev o chop o List.rev o String.explode; |
39348 | 571 |
end; |
572 |
||
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
573 |
val join = String.concatWith; |
39348 | 574 |
|
575 |
local |
|
576 |
fun match [] l = SOME l |
|
577 |
| match _ [] = NONE |
|
578 |
| match (x :: xs) (y :: ys) = if x = y then match xs ys else NONE; |
|
579 |
||
580 |
fun stringify acc [] = acc |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
581 |
| stringify acc (h :: t) = stringify (String.implode h :: acc) t; |
39348 | 582 |
in |
583 |
fun split sep = |
|
584 |
let |
|
585 |
val pat = String.explode sep |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
586 |
|
45778 | 587 |
fun div1 prev recent [] = stringify [] (List.rev recent :: prev) |
39348 | 588 |
| div1 prev recent (l as h :: t) = |
589 |
case match pat l of |
|
590 |
NONE => div1 prev (h :: recent) t |
|
45778 | 591 |
| SOME rest => div1 (List.rev recent :: prev) [] rest |
39348 | 592 |
in |
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
593 |
fn s => div1 [] [] (String.explode s) |
39348 | 594 |
end; |
595 |
end; |
|
596 |
||
597 |
fun capitalize s = |
|
598 |
if s = "" then s |
|
599 |
else str (Char.toUpper (String.sub (s,0))) ^ String.extract (s,1,NONE); |
|
600 |
||
601 |
fun mkPrefix p s = p ^ s; |
|
602 |
||
603 |
fun destPrefix p = |
|
604 |
let |
|
605 |
fun check s = |
|
606 |
if String.isPrefix p s then () |
|
607 |
else raise Error "destPrefix" |
|
608 |
||
609 |
val sizeP = size p |
|
610 |
in |
|
611 |
fn s => |
|
612 |
let |
|
613 |
val () = check s |
|
614 |
in |
|
615 |
String.extract (s,sizeP,NONE) |
|
616 |
end |
|
617 |
end; |
|
618 |
||
619 |
fun isPrefix p = can (destPrefix p); |
|
620 |
||
621 |
fun stripPrefix pred s = |
|
622 |
Substring.string (Substring.dropl pred (Substring.full s)); |
|
623 |
||
624 |
fun mkSuffix p s = s ^ p; |
|
625 |
||
626 |
fun destSuffix p = |
|
627 |
let |
|
628 |
fun check s = |
|
629 |
if String.isSuffix p s then () |
|
630 |
else raise Error "destSuffix" |
|
631 |
||
632 |
val sizeP = size p |
|
633 |
in |
|
634 |
fn s => |
|
635 |
let |
|
636 |
val () = check s |
|
637 |
||
638 |
val sizeS = size s |
|
639 |
in |
|
640 |
String.substring (s, 0, sizeS - sizeP) |
|
641 |
end |
|
642 |
end; |
|
643 |
||
644 |
fun isSuffix p = can (destSuffix p); |
|
645 |
||
646 |
fun stripSuffix pred s = |
|
647 |
Substring.string (Substring.dropr pred (Substring.full s)); |
|
648 |
||
649 |
(* ------------------------------------------------------------------------- *) |
|
650 |
(* Tables. *) |
|
651 |
(* ------------------------------------------------------------------------- *) |
|
652 |
||
653 |
type columnAlignment = {leftAlign : bool, padChar : char} |
|
654 |
||
655 |
fun alignColumn {leftAlign,padChar} column = |
|
656 |
let |
|
42102 | 657 |
val (n,_) = maximum Int.compare (List.map size column) |
39348 | 658 |
|
659 |
fun pad entry row = |
|
660 |
let |
|
661 |
val padding = nChars padChar (n - size entry) |
|
662 |
in |
|
663 |
if leftAlign then entry ^ padding ^ row |
|
664 |
else padding ^ entry ^ row |
|
665 |
end |
|
666 |
in |
|
667 |
zipWith pad column |
|
668 |
end; |
|
669 |
||
670 |
local |
|
671 |
fun alignTab aligns rows = |
|
672 |
case aligns of |
|
42102 | 673 |
[] => List.map (K "") rows |
674 |
| [{leftAlign = true, padChar = #" "}] => List.map hd rows |
|
39348 | 675 |
| align :: aligns => |
42102 | 676 |
let |
677 |
val col = List.map hd rows |
|
678 |
and cols = alignTab aligns (List.map tl rows) |
|
679 |
in |
|
680 |
alignColumn align col cols |
|
681 |
end; |
|
39348 | 682 |
in |
683 |
fun alignTable aligns rows = |
|
42102 | 684 |
if List.null rows then [] else alignTab aligns rows; |
39348 | 685 |
end; |
686 |
||
687 |
(* ------------------------------------------------------------------------- *) |
|
688 |
(* Reals. *) |
|
689 |
(* ------------------------------------------------------------------------- *) |
|
690 |
||
691 |
val realToString = Real.toString; |
|
692 |
||
693 |
fun percentToString x = Int.toString (Real.round (100.0 * x)) ^ "%"; |
|
694 |
||
695 |
fun pos r = Real.max (r,0.0); |
|
696 |
||
697 |
local |
|
698 |
val invLn2 = 1.0 / Math.ln 2.0; |
|
699 |
in |
|
700 |
fun log2 x = invLn2 * Math.ln x; |
|
701 |
end; |
|
702 |
||
703 |
(* ------------------------------------------------------------------------- *) |
|
704 |
(* Sums. *) |
|
705 |
(* ------------------------------------------------------------------------- *) |
|
706 |
||
707 |
datatype ('a,'b) sum = Left of 'a | Right of 'b |
|
708 |
||
709 |
fun destLeft (Left l) = l |
|
710 |
| destLeft _ = raise Error "destLeft"; |
|
711 |
||
712 |
fun isLeft (Left _) = true |
|
713 |
| isLeft (Right _) = false; |
|
714 |
||
715 |
fun destRight (Right r) = r |
|
716 |
| destRight _ = raise Error "destRight"; |
|
717 |
||
718 |
fun isRight (Left _) = false |
|
719 |
| isRight (Right _) = true; |
|
720 |
||
721 |
(* ------------------------------------------------------------------------- *) |
|
722 |
(* Useful impure features. *) |
|
723 |
(* ------------------------------------------------------------------------- *) |
|
724 |
||
725 |
local |
|
726 |
val generator = ref 0 |
|
39501
aaa7078fff55
updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents:
39445
diff
changeset
|
727 |
|
aaa7078fff55
updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents:
39445
diff
changeset
|
728 |
fun newIntThunk () = |
39348 | 729 |
let |
730 |
val n = !generator |
|
39501
aaa7078fff55
updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents:
39445
diff
changeset
|
731 |
|
39348 | 732 |
val () = generator := n + 1 |
733 |
in |
|
734 |
n |
|
39501
aaa7078fff55
updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents:
39445
diff
changeset
|
735 |
end; |
39348 | 736 |
|
39501
aaa7078fff55
updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents:
39445
diff
changeset
|
737 |
fun newIntsThunk k () = |
39348 | 738 |
let |
739 |
val n = !generator |
|
39501
aaa7078fff55
updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents:
39445
diff
changeset
|
740 |
|
39348 | 741 |
val () = generator := n + k |
742 |
in |
|
743 |
interval n k |
|
39501
aaa7078fff55
updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents:
39445
diff
changeset
|
744 |
end; |
aaa7078fff55
updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents:
39445
diff
changeset
|
745 |
in |
aaa7078fff55
updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents:
39445
diff
changeset
|
746 |
fun newInt () = Portable.critical newIntThunk (); |
aaa7078fff55
updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents:
39445
diff
changeset
|
747 |
|
aaa7078fff55
updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents:
39445
diff
changeset
|
748 |
fun newInts k = |
aaa7078fff55
updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents:
39445
diff
changeset
|
749 |
if k <= 0 then [] |
aaa7078fff55
updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents:
39445
diff
changeset
|
750 |
else Portable.critical (newIntsThunk k) (); |
39348 | 751 |
end; |
752 |
||
753 |
fun withRef (r,new) f x = |
|
754 |
let |
|
755 |
val old = !r |
|
756 |
val () = r := new |
|
757 |
val y = f x handle e => (r := old; raise e) |
|
758 |
val () = r := old |
|
759 |
in |
|
760 |
y |
|
761 |
end; |
|
762 |
||
763 |
fun cloneArray a = |
|
764 |
let |
|
765 |
fun index i = Array.sub (a,i) |
|
766 |
in |
|
767 |
Array.tabulate (Array.length a, index) |
|
768 |
end; |
|
769 |
||
770 |
(* ------------------------------------------------------------------------- *) |
|
771 |
(* Environment. *) |
|
772 |
(* ------------------------------------------------------------------------- *) |
|
773 |
||
774 |
fun host () = Option.getOpt (OS.Process.getEnv "HOSTNAME", "unknown"); |
|
775 |
||
776 |
fun time () = Date.fmt "%H:%M:%S" (Date.fromTimeLocal (Time.now ())); |
|
777 |
||
778 |
fun date () = Date.fmt "%d/%m/%Y" (Date.fromTimeLocal (Time.now ())); |
|
779 |
||
780 |
fun readDirectory {directory = dir} = |
|
781 |
let |
|
782 |
val dirStrm = OS.FileSys.openDir dir |
|
783 |
||
784 |
fun readAll acc = |
|
785 |
case OS.FileSys.readDir dirStrm of |
|
786 |
NONE => acc |
|
787 |
| SOME file => |
|
788 |
let |
|
789 |
val filename = OS.Path.joinDirFile {dir = dir, file = file} |
|
790 |
||
791 |
val acc = {filename = filename} :: acc |
|
792 |
in |
|
793 |
readAll acc |
|
794 |
end |
|
795 |
||
796 |
val filenames = readAll [] |
|
797 |
||
798 |
val () = OS.FileSys.closeDir dirStrm |
|
799 |
in |
|
45778 | 800 |
List.rev filenames |
39348 | 801 |
end; |
802 |
||
803 |
fun readTextFile {filename} = |
|
804 |
let |
|
805 |
open TextIO |
|
806 |
||
807 |
val h = openIn filename |
|
808 |
||
809 |
val contents = inputAll h |
|
810 |
||
811 |
val () = closeIn h |
|
812 |
in |
|
813 |
contents |
|
814 |
end; |
|
815 |
||
816 |
fun writeTextFile {contents,filename} = |
|
817 |
let |
|
818 |
open TextIO |
|
819 |
val h = openOut filename |
|
820 |
val () = output (h,contents) |
|
821 |
val () = closeOut h |
|
822 |
in |
|
823 |
() |
|
824 |
end; |
|
825 |
||
826 |
(* ------------------------------------------------------------------------- *) |
|
827 |
(* Profiling and error reporting. *) |
|
828 |
(* ------------------------------------------------------------------------- *) |
|
829 |
||
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
830 |
fun chat s = TextIO.output (TextIO.stdOut, s ^ "\n"); |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
831 |
|
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
832 |
fun chide s = TextIO.output (TextIO.stdErr, s ^ "\n"); |
39348 | 833 |
|
834 |
local |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39414
diff
changeset
|
835 |
fun err x s = chide (x ^ ": " ^ s); |
39348 | 836 |
in |
837 |
fun try f x = f x |
|
838 |
handle e as Error _ => (err "try" (errorToString e); raise e) |
|
839 |
| e as Bug _ => (err "try" (bugToString e); raise e) |
|
840 |
| e => (err "try" "strange exception raised"; raise e); |
|
841 |
||
842 |
val warn = err "WARNING"; |
|
843 |
||
844 |
fun die s = (err "\nFATAL ERROR" s; OS.Process.exit OS.Process.failure); |
|
845 |
end; |
|
846 |
||
847 |
fun timed f a = |
|
848 |
let |
|
849 |
val tmr = Timer.startCPUTimer () |
|
850 |
val res = f a |
|
851 |
val {usr,sys,...} = Timer.checkCPUTimer tmr |
|
852 |
in |
|
853 |
(Time.toReal usr + Time.toReal sys, res) |
|
854 |
end; |
|
855 |
||
856 |
local |
|
857 |
val MIN = 1.0; |
|
858 |
||
859 |
fun several n t f a = |
|
860 |
let |
|
861 |
val (t',res) = timed f a |
|
862 |
val t = t + t' |
|
863 |
val n = n + 1 |
|
864 |
in |
|
865 |
if t > MIN then (t / Real.fromInt n, res) else several n t f a |
|
866 |
end; |
|
867 |
in |
|
868 |
fun timedMany f a = several 0 0.0 f a |
|
869 |
end; |
|
870 |
||
871 |
val executionTime = |
|
872 |
let |
|
873 |
val startTime = Time.toReal (Time.now ()) |
|
874 |
in |
|
875 |
fn () => Time.toReal (Time.now ()) - startTime |
|
876 |
end; |
|
877 |
||
878 |
end |