author  paulson 
Thu, 01 Oct 1998 18:30:05 +0200  
changeset 5601  b6456ccd9e3e 
parent 3391  5e45dd3b64e9 
child 9867  bf8300fa4238 
permissions  rwrr 
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(n1,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 *) 