author | slotosch |
Sun, 25 May 1997 16:57:19 +0200 | |
changeset 3325 | 4e4ee8a101be |
parent 3302 | 404fe31fd8d2 |
child 3330 | ab7161e593c8 |
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 |
local |
|
17 |
fun info_string s {module,func,mesg} = |
|
18 |
(s^" at "^module^"."^func^":\n"^mesg^"\n") |
|
19 |
in |
|
20 |
val ERR_string = info_string "Exception raised" |
|
21 |
val MESG_string = info_string "Message" |
|
22 |
end; |
|
23 |
||
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
24 |
fun Raise (e as ERR sss) = (TextIO.output(TextIO.stdOut, ERR_string sss); |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
25 |
raise e) |
2112 | 26 |
| Raise e = raise e; |
27 |
||
28 |
||
29 |
(* Simple combinators *) |
|
30 |
||
31 |
fun C f x y = f y x |
|
32 |
||
33 |
val concat = curry (op ^) |
|
34 |
fun quote s = "\""^s^"\""; |
|
35 |
||
36 |
fun itlist f L base_value = |
|
37 |
let fun it [] = base_value |
|
38 |
| it (a::rst) = f a (it rst) |
|
39 |
in it L |
|
40 |
end; |
|
41 |
||
42 |
fun rev_itlist f = |
|
43 |
let fun rev_it [] base = base |
|
44 |
| rev_it (a::rst) base = rev_it rst (f a base) |
|
45 |
in rev_it |
|
46 |
end; |
|
47 |
||
48 |
fun end_itlist f = |
|
49 |
let fun endit [] = raise UTILS_ERR{func="end_itlist", mesg="list too short"} |
|
50 |
| endit alist = |
|
51 |
let val (base::ralist) = rev alist |
|
52 |
in itlist f (rev ralist) base |
|
53 |
end |
|
54 |
in endit |
|
55 |
end; |
|
56 |
||
57 |
fun itlist2 f L1 L2 base_value = |
|
58 |
let fun it ([],[]) = base_value |
|
59 |
| it ((a::rst1),(b::rst2)) = f a b (it (rst1,rst2)) |
|
60 |
| it _ = raise UTILS_ERR{func="itlist2",mesg="different length lists"} |
|
61 |
in it (L1,L2) |
|
62 |
end; |
|
63 |
||
64 |
fun mapfilter f alist = itlist (fn i=>fn L=> (f i::L) handle _ => L) alist []; |
|
65 |
||
66 |
fun pluck p = |
|
67 |
let fun remv ([],_) = raise UTILS_ERR{func="pluck",mesg = "item not found"} |
|
68 |
| remv (h::t, A) = if p h then (h, rev A @ t) else remv (t,h::A) |
|
69 |
in fn L => remv(L,[]) |
|
70 |
end; |
|
71 |
||
72 |
fun front_back [] = raise UTILS_ERR{func="front_back",mesg="empty list"} |
|
73 |
| front_back [x] = ([],x) |
|
74 |
| front_back (h::t) = |
|
75 |
let val (L,b) = front_back t |
|
76 |
in (h::L,b) |
|
77 |
end; |
|
78 |
||
79 |
fun take f = |
|
80 |
let fun grab(0,L) = [] |
|
81 |
| grab(n, x::rst) = f x::grab(n-1,rst) |
|
82 |
in grab |
|
83 |
end; |
|
84 |
||
85 |
fun zip3 [][][] = [] |
|
86 |
| zip3 (x::l1) (y::l2) (z::l3) = (x,y,z)::zip3 l1 l2 l3 |
|
87 |
| zip3 _ _ _ = raise UTILS_ERR{func="zip3",mesg="different lengths"}; |
|
88 |
||
89 |
||
90 |
fun can f x = (f x ; true) handle _ => false; |
|
91 |
fun holds P x = P x handle _ => false; |
|
92 |
||
93 |
||
94 |
(* Set ops *) |
|
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
95 |
nonfix mem; (* Gag Barf Choke *) |
2112 | 96 |
fun mem eq_func i = |
97 |
let val eqi = eq_func i |
|
98 |
fun mm [] = false |
|
99 |
| mm (a::rst) = eqi a orelse mm rst |
|
100 |
in mm |
|
101 |
end; |
|
102 |
||
103 |
fun mk_set eq_func = |
|
104 |
let val mem = mem eq_func |
|
105 |
fun mk [] = [] |
|
106 |
| mk (a::rst) = if (mem a rst) then mk rst else a::(mk rst) |
|
107 |
in mk |
|
108 |
end; |
|
109 |
||
110 |
(* All the elements in the first set that are not also in the second set. *) |
|
111 |
fun set_diff eq_func S1 S2 = filter (fn x => not (mem eq_func x S2)) S1 |
|
112 |
||
113 |
||
114 |
fun sort R = |
|
115 |
let fun part (m, []) = ([],[]) |
|
116 |
| part (m, h::rst) = |
|
117 |
let val (l1,l2) = part (m,rst) |
|
118 |
in if (R h m) then (h::l1, l2) |
|
119 |
else (l1, h::l2) end |
|
120 |
fun qsort [] = [] |
|
121 |
| qsort (h::rst) = |
|
122 |
let val (l1,l2) = part(h,rst) |
|
123 |
in qsort l1@ [h] @qsort l2 |
|
124 |
end |
|
125 |
in qsort |
|
126 |
end; |
|
127 |
||
128 |
||
129 |
||
130 |
end; (* Utils *) |