6118

1 
(* Title: Pure/General/seq.ML

5014

2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory

12851

4 
Author: Markus Wenzel, TU Munich

5014

5 


6 
Unbounded sequences implemented by closures. RECOMPUTES if sequence


7 
is reinspected. Memoing, using polymorphic refs, was found to be


8 
slower! (More GCs)


9 
*)


10 


11 
signature SEQ =


12 
sig


13 
type 'a seq


14 
val make: (unit > ('a * 'a seq) option) > 'a seq


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


16 
val empty: 'a seq


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


18 
val single: 'a > 'a seq

11721

19 
val try: ('a > 'b) > 'a > 'b seq

5014

20 
val hd: 'a seq > 'a


21 
val tl: 'a seq > 'a seq


22 
val chop: int * 'a seq > 'a list * 'a seq


23 
val list_of: 'a seq > 'a list


24 
val of_list: 'a list > 'a seq


25 
val map: ('a > 'b) > 'a seq > 'b seq


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


27 
val append: 'a seq * 'a seq > 'a seq


28 
val filter: ('a > bool) > 'a seq > 'a seq


29 
val flat: 'a seq seq > 'a seq


30 
val interleave: 'a seq * 'a seq > 'a seq


31 
val print: (int > 'a > unit) > int > 'a seq > unit


32 
val it_right : ('a * 'b seq > 'b seq) > 'a seq * 'b seq > 'b seq

6927

33 
val commute: 'a seq list > 'a list seq

5014

34 
val succeed: 'a > 'a seq


35 
val fail: 'a > 'b seq


36 
val THEN: ('a > 'b seq) * ('b > 'c seq) > 'a > 'c seq


37 
val ORELSE: ('a > 'b seq) * ('a > 'b seq) > 'a > 'b seq


38 
val APPEND: ('a > 'b seq) * ('a > 'b seq) > 'a > 'b seq


39 
val EVERY: ('a > 'a seq) list > 'a > 'a seq


40 
val FIRST: ('a > 'b seq) list > 'a > 'b seq


41 
val TRY: ('a > 'a seq) > 'a > 'a seq


42 
val REPEAT: ('a > 'a seq) > 'a > 'a seq

5558

43 
val REPEAT1: ('a > 'a seq) > 'a > 'a seq

8535

44 
val INTERVAL: (int > 'a > 'a seq) > int > int > 'a > 'a seq

12851

45 
val DETERM: ('a > 'b seq) > 'a > 'b seq

5014

46 
end;


47 


48 
structure Seq: SEQ =


49 
struct


50 


51 


52 
(** lazy sequences **)


53 


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


55 


56 
(*the abstraction for making a sequence*)


57 
val make = Seq;


58 

15531

59 
(*return next sequence element as NONE or SOME (x, xq)*)

5014

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


61 


62 


63 
(*the empty sequence*)

15531

64 
val empty = Seq (fn () => NONE);

5014

65 


66 
(*prefix an element to the sequence  use cons (x, xq) only if


67 
evaluation of xq need not be delayed, otherwise use

15531

68 
make (fn () => SOME (x, xq))*)


69 
fun cons x_xq = make (fn () => SOME x_xq);

5014

70 


71 
fun single x = cons (x, empty);


72 


73 
(*head and tail  beware of calling the sequence function twice!!*)


74 
fun hd xq = #1 (the (pull xq))


75 
and tl xq = #2 (the (pull xq));


76 

11721

77 
(*partial function as procedure*)


78 
fun try f x =


79 
(case Library.try f x of

15531

80 
SOME y => single y


81 
 NONE => empty);

11721

82 

5014

83 


84 
(*the list of the first n elements, paired with rest of sequence;


85 
if length of list is less than n, then sequence had less than n elements*)


86 
fun chop (n, xq) =


87 
if n <= 0 then ([], xq)


88 
else


89 
(case pull xq of

15531

90 
NONE => ([], xq)


91 
 SOME (x, xq') => apfst (Library.cons x) (chop (n  1, xq')));

5014

92 


93 
(*conversion from sequence to list*)


94 
fun list_of xq =


95 
(case pull xq of

15531

96 
NONE => []


97 
 SOME (x, xq') => x :: list_of xq');

5014

98 


99 
(*conversion from list to sequence*)


100 
fun of_list xs = foldr cons (xs, empty);


101 


102 


103 
(*map the function f over the sequence, making a new sequence*)


104 
fun map f xq =


105 
make (fn () =>


106 
(case pull xq of

15531

107 
NONE => NONE


108 
 SOME (x, xq') => SOME (f x, map f xq')));

5014

109 


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


111 
fun mapp f xq yq =


112 
let


113 
fun copy s =


114 
make (fn () =>


115 
(case pull s of

15531

116 
NONE => pull yq


117 
 SOME (x, s') => SOME (f x, copy s')))

5014

118 
in copy xq end;


119 


120 
(*sequence append: put the elements of xq in front of those of yq*)


121 
fun append (xq, yq) =


122 
let


123 
fun copy s =


124 
make (fn () =>


125 
(case pull s of

15531

126 
NONE => pull yq


127 
 SOME (x, s') => SOME (x, copy s')))

5014

128 
in copy xq end;


129 


130 
(*filter sequence by predicate*)


131 
fun filter pred xq =


132 
let


133 
fun copy s =


134 
make (fn () =>


135 
(case pull s of

15531

136 
NONE => NONE


137 
 SOME (x, s') => if pred x then SOME (x, copy s') else pull (copy s')));

5014

138 
in copy xq end;


139 


140 
(*flatten a sequence of sequences to a single sequence*)


141 
fun flat xqq =


142 
make (fn () =>


143 
(case pull xqq of

15531

144 
NONE => NONE


145 
 SOME (xq, xqq') => pull (append (xq, flat xqq'))));

5014

146 


147 
(*interleave elements of xq with those of yq  fairer than append*)


148 
fun interleave (xq, yq) =


149 
make (fn () =>


150 
(case pull xq of

15531

151 
NONE => pull yq


152 
 SOME (x, xq') => SOME (x, interleave (yq, xq'))));

5014

153 


154 


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


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


157 
fun print prelem count seq =


158 
let


159 
fun pr (k, xq) =


160 
if k > count then ()


161 
else


162 
(case pull xq of

15531

163 
NONE => ()


164 
 SOME (x, xq') => (prelem k x; writeln ""; pr (k + 1, xq')))

5014

165 
in pr (1, seq) end;


166 


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


168 
fun it_right f (xq, yq) =


169 
let


170 
fun its s =


171 
make (fn () =>


172 
(case pull s of

15531

173 
NONE => pull yq


174 
 SOME (a, s') => pull (f (a, its s'))))

5014

175 
in its xq end;


176 

6927

177 
(*turn a list of sequences into a sequence of lists*)


178 
fun commute [] = single []


179 
 commute (xq :: xqs) =


180 
make (fn () =>


181 
(case pull xq of

15531

182 
NONE => NONE


183 
 SOME (x, xq') =>

6927

184 
(case pull (commute xqs) of

15531

185 
NONE => NONE


186 
 SOME (xs, xsq) =>


187 
SOME (x :: xs, append (map (Library.cons x) xsq, commute (xq' :: xqs))))));

6927

188 

5014

189 


190 

12851

191 
(** sequence functions **) (*some code copied from Pure/tctical.ML*)

5014

192 


193 
fun succeed x = single x;


194 
fun fail _ = empty;


195 

5864

196 
fun op THEN (f, g) x = flat (map g (f x));

5014

197 

5864

198 
fun op ORELSE (f, g) x =

5014

199 
(case pull (f x) of

15531

200 
NONE => g x

5014

201 
 some => make (fn () => some));


202 

5864

203 
fun op APPEND (f, g) x =

5014

204 
append (f x, make (fn () => pull (g x)));


205 


206 
fun EVERY fs = foldr THEN (fs, succeed);


207 
fun FIRST fs = foldr ORELSE (fs, fail);


208 


209 
fun TRY f = ORELSE (f, succeed);


210 


211 
fun REPEAT f =


212 
let


213 
fun rep qs x =


214 
(case pull (f x) of

15531

215 
NONE => SOME (x, make (fn () => repq qs))


216 
 SOME (x', q) => rep (q :: qs) x')


217 
and repq [] = NONE

5014

218 
 repq (q :: qs) =


219 
(case pull q of

15531

220 
NONE => repq qs


221 
 SOME (x, q) => rep (q :: qs) x);

5014

222 
in fn x => make (fn () => rep [] x) end;


223 

5558

224 
fun REPEAT1 f = THEN (f, REPEAT f);


225 

8535

226 
fun INTERVAL f i j x =


227 
if i > j then single x


228 
else op THEN (f j, INTERVAL f i (j  1)) x;


229 

12851

230 
fun DETERM f x =


231 
(case pull (f x) of

15531

232 
NONE => empty


233 
 SOME (x', _) => cons (x', empty));

8535

234 

5014

235 
end;
