author  paulson 
Tue, 22 Jul 1997 11:14:18 +0200  
changeset 3538  ed9de44032e0 
parent 1501  bb7f99a0a6f0 
permissions  rwrr 
1460  1 
(* Title: sequence 
0  2 
ID: $Id$ 
1460  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1988 University of Cambridge 
720
e6cf828a0c67
Pure/sequence: added comment explaining that memoing sequences were found
lcp
parents:
669
diff
changeset

5 

e6cf828a0c67
Pure/sequence: added comment explaining that memoing sequences were found
lcp
parents:
669
diff
changeset

6 
Unbounded sequences implemented by closures. 
0  7 

720
e6cf828a0c67
Pure/sequence: added comment explaining that memoing sequences were found
lcp
parents:
669
diff
changeset

8 
RECOMPUTES if sequence is reinspected. 
0  9 

720
e6cf828a0c67
Pure/sequence: added comment explaining that memoing sequences were found
lcp
parents:
669
diff
changeset

10 
Memoing, using polymorphic refs, was found to be slower! (More GCs) 
0  11 
*) 
12 

13 

14 
signature SEQUENCE = 

15 
sig 

16 
type 'a seq 

1460  17 
val append : 'a seq * 'a seq > 'a seq 
18 
val chop : int * 'a seq > 'a list * 'a seq 

19 
val cons : 'a * 'a seq > 'a seq 

20 
val filters : ('a > bool) > 'a seq > 'a seq 

21 
val flats : 'a seq seq > 'a seq 

22 
val hd : 'a seq > 'a 

669  23 
val interleave: 'a seq * 'a seq > 'a seq 
1460  24 
val its_right : ('a * 'b seq > 'b seq) > 'a seq * 'b seq > 'b seq 
25 
val list_of_s : 'a seq > 'a list 

26 
val mapp : ('a > 'b) > 'a seq > 'b seq > 'b seq 

27 
val maps : ('a > 'b) > 'a seq > 'b seq 

28 
val null : 'a seq 

29 
val prints : (int > 'a > unit) > int > 'a seq > unit 

30 
val pull : 'a seq > ('a * 'a seq) option 

31 
val s_of_list : 'a list > 'a seq 

32 
val seqof : (unit > ('a * 'a seq) option) > 'a seq 

33 
val single : 'a > 'a seq 

34 
val tl : 'a seq > 'a seq 

0  35 
end; 
36 

37 

1501  38 
structure Sequence : SEQUENCE = 
0  39 
struct 
40 

41 
datatype 'a seq = Seq of unit > ('a * 'a seq)option; 

42 

43 
(*Return next sequence element as None or Some(x,str) *) 

44 
fun pull(Seq f) = f(); 

45 

669  46 
(*Head and tail. Beware of calling the sequence function twice!!*) 
47 
fun hd s = #1 (the (pull s)) 

48 
and tl s = #2 (the (pull s)); 

49 

0  50 
(*the abstraction for making a sequence*) 
51 
val seqof = Seq; 

52 

53 
(*prefix an element to the sequence 

54 
use cons(x,s) only if evaluation of s need not be delayed, 

55 
otherwise use seqof(fn()=> Some(x,s)) *) 

56 
fun cons all = Seq(fn()=>Some all); 

57 

58 
(*the empty sequence*) 

59 
val null = Seq(fn()=>None); 

60 

61 
fun single(x) = cons (x, null); 

62 

63 
(*The list of the first n elements, paired with rest of sequence. 

64 
If length of list is less than n, then sequence had less than n elements.*) 

65 
fun chop (n:int, s: 'a seq): 'a list * 'a seq = 

66 
if n<=0 then ([],s) 

67 
else case pull(s) of 

68 
None => ([],s) 

69 
 Some(x,s') => let val (xs,s'') = chop (n1,s') 

1460  70 
in (x::xs, s'') end; 
0  71 

72 
(*conversion from sequence to list*) 

73 
fun list_of_s (s: 'a seq) : 'a list = case pull(s) of 

74 
None => [] 

75 
 Some(x,s') => x :: list_of_s s'; 

76 

77 

78 
(*conversion from list to sequence*) 

79 
fun s_of_list [] = null 

80 
 s_of_list (x::l) = cons (x, s_of_list l); 

81 

82 

83 
(*functional to print a sequence, up to "count" elements 

84 
the function prelem should print the element number and also the element*) 

85 
fun prints (prelem: int > 'a > unit) count (s: 'a seq) : unit = 

86 
let fun pr (k,s) = 

1460  87 
if k>count then () 
88 
else case pull(s) of 

89 
None => () 

90 
 Some(x,s') => (prelem k x; prs"\n"; pr (k+1, s')) 

0  91 
in pr(1,s) end; 
92 

93 
(*Map the function f over the sequence, making a new sequence*) 

94 
fun maps f xq = seqof (fn()=> case pull(xq) of 

95 
None => None 

96 
 Some(x,yq) => Some(f x, maps f yq)); 

97 

98 
(*Sequence append: put the elements of xq in front of those of yq*) 

99 
fun append (xq,yq) = 

100 
let fun copy xq = seqof (fn()=> 

1460  101 
case pull xq of 
102 
None => pull yq 

103 
 Some(x,xq') => Some (x, copy xq')) 

0  104 
in copy xq end; 
105 

106 
(*Interleave elements of xq with those of yq  fairer than append*) 

107 
fun interleave (xq,yq) = seqof (fn()=> 

108 
case pull(xq) of 

109 
None => pull yq 

1460  110 
 Some(x,xq') => Some (x, interleave(yq, xq'))); 
0  111 

112 
(*map over a sequence xq, append the sequence yq*) 

113 
fun mapp f xq yq = 

114 
let fun copy s = seqof (fn()=> 

115 
case pull(s) of 

1460  116 
None => pull(yq) 
0  117 
 Some(x,xq') => Some(f x, copy xq')) 
118 
in copy xq end; 

119 

120 
(*Flatten a sequence of sequences to a single sequence. *) 

121 
fun flats ss = seqof (fn()=> case pull(ss) of 

122 
None => None 

123 
 Some(s,ss') => pull(append(s, flats ss'))); 

124 

125 
(*accumulating a function over a sequence; this is lazy*) 

126 
fun its_right (f: 'a * 'b seq > 'b seq) (s: 'a seq, bstr: 'b seq) : 'b seq = 

127 
let fun its s = seqof (fn()=> 

128 
case pull(s) of 

1460  129 
None => pull bstr 
130 
 Some(a,s') => pull(f(a, its s'))) 

0  131 
in its s end; 
132 

133 
fun filters pred xq = 

134 
let fun copy s = seqof (fn()=> 

135 
case pull(s) of 

1460  136 
None => None 
0  137 
 Some(x,xq') => if pred x then Some(x, copy xq') 
1460  138 
else pull (copy xq') ) 
0  139 
in copy xq end 
140 

141 
end; 