1 (* Title: HOL/Tools/TFL/utils.ML |
|
2 Author: Konrad Slind, Cambridge University Computer Laboratory |
|
3 |
|
4 Basic utilities. |
|
5 *) |
|
6 |
|
7 signature UTILS = |
|
8 sig |
|
9 exception ERR of {module: string, func: string, mesg: string} |
|
10 val end_itlist: ('a -> 'a -> 'a) -> 'a list -> 'a |
|
11 val itlist2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c |
|
12 val pluck: ('a -> bool) -> 'a list -> 'a * 'a list |
|
13 val zip3: 'a list -> 'b list -> 'c list -> ('a*'b*'c) list |
|
14 val take: ('a -> 'b) -> int * 'a list -> 'b list |
|
15 end; |
|
16 |
|
17 structure Utils: UTILS = |
|
18 struct |
|
19 |
|
20 (*standard exception for TFL*) |
|
21 exception ERR of {module: string, func: string, mesg: string}; |
|
22 |
|
23 fun UTILS_ERR func mesg = ERR {module = "Utils", func = func, mesg = mesg}; |
|
24 |
|
25 |
|
26 fun end_itlist f [] = raise (UTILS_ERR "end_itlist" "list too short") |
|
27 | end_itlist f [x] = x |
|
28 | end_itlist f (x :: xs) = f x (end_itlist f xs); |
|
29 |
|
30 fun itlist2 f L1 L2 base_value = |
|
31 let fun it ([],[]) = base_value |
|
32 | it ((a::rst1),(b::rst2)) = f a b (it (rst1,rst2)) |
|
33 | it _ = raise UTILS_ERR "itlist2" "different length lists" |
|
34 in it (L1,L2) |
|
35 end; |
|
36 |
|
37 fun pluck p = |
|
38 let fun remv ([],_) = raise UTILS_ERR "pluck" "item not found" |
|
39 | remv (h::t, A) = if p h then (h, rev A @ t) else remv (t,h::A) |
|
40 in fn L => remv(L,[]) |
|
41 end; |
|
42 |
|
43 fun take f = |
|
44 let fun grab(0,L) = [] |
|
45 | grab(n, x::rst) = f x::grab(n-1,rst) |
|
46 in grab |
|
47 end; |
|
48 |
|
49 fun zip3 [][][] = [] |
|
50 | zip3 (x::l1) (y::l2) (z::l3) = (x,y,z)::zip3 l1 l2 l3 |
|
51 | zip3 _ _ _ = raise UTILS_ERR "zip3" "different lengths"; |
|
52 |
|
53 |
|
54 end; |
|