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