author  paulson 
Fri, 03 Nov 2000 10:23:24 +0100  
changeset 10368  f7e8abd8ea15 
parent 10015  8c16ec5ba62b 
permissions  rwrr 
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(n1,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; 