| author | wenzelm | 
| Mon, 16 Nov 1998 11:11:58 +0100 | |
| changeset 5888 | d8e51792ca85 | 
| 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 *)  |