author | paulson |
Fri, 17 Oct 1997 11:00:50 +0200 | |
changeset 3913 | 96e28b16861c |
parent 3391 | 5e45dd3b64e9 |
child 9867 | bf8300fa4238 |
permissions | -rw-r--r-- |
3302 | 1 |
(* Title: TFL/utils |
2 |
ID: $Id$ |
|
3 |
Author: Konrad Slind, Cambridge University Computer Laboratory |
|
4 |
Copyright 1997 University of Cambridge |
|
2112 | 5 |
|
3302 | 6 |
Basic utilities |
7 |
*) |
|
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
8 |
|
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
9 |
structure Utils = |
2112 | 10 |
struct |
11 |
||
12 |
(* Standard exception for TFL. *) |
|
13 |
exception ERR of {module:string,func:string, mesg:string}; |
|
14 |
fun UTILS_ERR{func,mesg} = ERR{module = "Utils",func=func,mesg=mesg}; |
|
15 |
||
16 |
||
17 |
(* Simple combinators *) |
|
18 |
||
19 |
fun C f x y = f y x |
|
20 |
||
21 |
fun itlist f L base_value = |
|
22 |
let fun it [] = base_value |
|
23 |
| it (a::rst) = f a (it rst) |
|
24 |
in it L |
|
25 |
end; |
|
26 |
||
27 |
fun rev_itlist f = |
|
28 |
let fun rev_it [] base = base |
|
29 |
| rev_it (a::rst) base = rev_it rst (f a base) |
|
30 |
in rev_it |
|
31 |
end; |
|
32 |
||
33 |
fun end_itlist f = |
|
34 |
let fun endit [] = raise UTILS_ERR{func="end_itlist", mesg="list too short"} |
|
35 |
| endit alist = |
|
36 |
let val (base::ralist) = rev alist |
|
37 |
in itlist f (rev ralist) base |
|
38 |
end |
|
39 |
in endit |
|
40 |
end; |
|
41 |
||
42 |
fun itlist2 f L1 L2 base_value = |
|
43 |
let fun it ([],[]) = base_value |
|
44 |
| it ((a::rst1),(b::rst2)) = f a b (it (rst1,rst2)) |
|
45 |
| it _ = raise UTILS_ERR{func="itlist2",mesg="different length lists"} |
|
46 |
in it (L1,L2) |
|
47 |
end; |
|
48 |
||
49 |
fun pluck p = |
|
50 |
let fun remv ([],_) = raise UTILS_ERR{func="pluck",mesg = "item not found"} |
|
51 |
| remv (h::t, A) = if p h then (h, rev A @ t) else remv (t,h::A) |
|
52 |
in fn L => remv(L,[]) |
|
53 |
end; |
|
54 |
||
55 |
fun take f = |
|
56 |
let fun grab(0,L) = [] |
|
57 |
| grab(n, x::rst) = f x::grab(n-1,rst) |
|
58 |
in grab |
|
59 |
end; |
|
60 |
||
61 |
fun zip3 [][][] = [] |
|
62 |
| zip3 (x::l1) (y::l2) (z::l3) = (x,y,z)::zip3 l1 l2 l3 |
|
63 |
| zip3 _ _ _ = raise UTILS_ERR{func="zip3",mesg="different lengths"}; |
|
64 |
||
65 |
||
66 |
fun can f x = (f x ; true) handle _ => false; |
|
67 |
fun holds P x = P x handle _ => false; |
|
68 |
||
69 |
||
70 |
fun sort R = |
|
71 |
let fun part (m, []) = ([],[]) |
|
72 |
| part (m, h::rst) = |
|
73 |
let val (l1,l2) = part (m,rst) |
|
74 |
in if (R h m) then (h::l1, l2) |
|
75 |
else (l1, h::l2) end |
|
76 |
fun qsort [] = [] |
|
77 |
| qsort (h::rst) = |
|
78 |
let val (l1,l2) = part(h,rst) |
|
79 |
in qsort l1@ [h] @qsort l2 |
|
80 |
end |
|
81 |
in qsort |
|
82 |
end; |
|
83 |
||
84 |
||
85 |
||
86 |
end; (* Utils *) |