6118

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

5014

2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 


5 
Unbounded sequences implemented by closures. RECOMPUTES if sequence


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


7 
slower! (More GCs)


8 
*)


9 


10 
signature SEQ =


11 
sig


12 
type 'a seq


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


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


15 
val empty: 'a seq


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


17 
val single: 'a > 'a seq


18 
val hd: 'a seq > 'a


19 
val tl: 'a seq > 'a seq


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


21 
val list_of: 'a seq > 'a list


22 
val of_list: 'a list > 'a seq


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


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


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


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


27 
val flat: 'a seq seq > 'a seq


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


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


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

6927

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

5014

32 
val succeed: 'a > 'a seq


33 
val fail: 'a > 'b seq


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


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


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


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


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


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


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

5558

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

5014

42 
end;


43 


44 
structure Seq: SEQ =


45 
struct


46 


47 


48 
(** lazy sequences **)


49 


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


51 


52 
(*the abstraction for making a sequence*)


53 
val make = Seq;


54 


55 
(*return next sequence element as None or Some (x, xq)*)


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


57 


58 


59 
(*the empty sequence*)


60 
val empty = Seq (fn () => None);


61 


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


63 
evaluation of xq need not be delayed, otherwise use


64 
make (fn () => Some (x, xq))*)


65 
fun cons x_xq = make (fn () => Some x_xq);


66 


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


68 


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


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


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


72 


73 


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


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


76 
fun chop (n, xq) =


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


78 
else


79 
(case pull xq of


80 
None => ([], xq)


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


82 


83 
(*conversion from sequence to list*)


84 
fun list_of xq =


85 
(case pull xq of


86 
None => []


87 
 Some (x, xq') => x :: list_of xq');


88 


89 
(*conversion from list to sequence*)


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


91 


92 


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


94 
fun map f xq =


95 
make (fn () =>


96 
(case pull xq of


97 
None => None


98 
 Some (x, xq') => Some (f x, map f xq')));


99 


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


101 
fun mapp f xq yq =


102 
let


103 
fun copy s =


104 
make (fn () =>


105 
(case pull s of


106 
None => pull yq


107 
 Some (x, s') => Some (f x, copy s')))


108 
in copy xq end;


109 


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


111 
fun append (xq, yq) =


112 
let


113 
fun copy s =


114 
make (fn () =>


115 
(case pull s of


116 
None => pull yq


117 
 Some (x, s') => Some (x, copy s')))


118 
in copy xq end;


119 


120 
(*filter sequence by predicate*)


121 
fun filter pred xq =


122 
let


123 
fun copy s =


124 
make (fn () =>


125 
(case pull s of


126 
None => None


127 
 Some (x, s') => if pred x then Some (x, copy s') else pull (copy s')));


128 
in copy xq end;


129 


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


131 
fun flat xqq =


132 
make (fn () =>


133 
(case pull xqq of


134 
None => None


135 
 Some (xq, xqq') => pull (append (xq, flat xqq'))));


136 


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


138 
fun interleave (xq, yq) =


139 
make (fn () =>


140 
(case pull xq of


141 
None => pull yq


142 
 Some (x, xq') => Some (x, interleave (yq, xq'))));


143 


144 


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


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


147 
fun print prelem count seq =


148 
let


149 
fun pr (k, xq) =


150 
if k > count then ()


151 
else


152 
(case pull xq of


153 
None => ()


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


155 
in pr (1, seq) end;


156 


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


158 
fun it_right f (xq, yq) =


159 
let


160 
fun its s =


161 
make (fn () =>


162 
(case pull s of


163 
None => pull yq


164 
 Some (a, s') => pull (f (a, its s'))))


165 
in its xq end;


166 

6927

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


168 
fun commute [] = single []


169 
 commute (xq :: xqs) =


170 
make (fn () =>


171 
(case pull xq of


172 
None => None


173 
 Some (x, xq') =>


174 
(case pull (commute xqs) of


175 
None => None


176 
 Some (xs, xsq) =>


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


178 

5014

179 


180 


181 
(** sequence functions **) (*some code duplicated from Pure/tctical.ML*)


182 


183 
fun succeed x = single x;


184 
fun fail _ = empty;


185 


186 

5864

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

5014

188 

5864

189 
fun op ORELSE (f, g) x =

5014

190 
(case pull (f x) of


191 
None => g x


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


193 

5864

194 
fun op APPEND (f, g) x =

5014

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


196 


197 


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


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


200 


201 


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


203 


204 
fun REPEAT f =


205 
let


206 
fun rep qs x =


207 
(case pull (f x) of


208 
None => Some (x, make (fn () => repq qs))


209 
 Some (x', q) => rep (q :: qs) x')


210 
and repq [] = None


211 
 repq (q :: qs) =


212 
(case pull q of


213 
None => repq qs


214 
 Some (x, q) => rep (q :: qs) x);


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


216 

5558

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


218 

5014

219 


220 
end;
