5014

1 
(* Title: Pure/seq.ML


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


31 
val succeed: 'a > 'a seq


32 
val fail: 'a > 'b seq


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


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


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


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


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


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


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


40 
end;


41 


42 
structure Seq: SEQ =


43 
struct


44 


45 


46 
(** lazy sequences **)


47 


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


49 


50 
(*the abstraction for making a sequence*)


51 
val make = Seq;


52 


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


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


55 


56 


57 
(*the empty sequence*)


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


59 


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


61 
evaluation of xq need not be delayed, otherwise use


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


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


64 


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


66 


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


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


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


70 


71 


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


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


74 
fun chop (n, xq) =


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


76 
else


77 
(case pull xq of


78 
None => ([], xq)


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


80 


81 
(*conversion from sequence to list*)


82 
fun list_of xq =


83 
(case pull xq of


84 
None => []


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


86 


87 
(*conversion from list to sequence*)


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


89 


90 


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


92 
fun map f xq =


93 
make (fn () =>


94 
(case pull xq of


95 
None => None


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


97 


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


99 
fun mapp f xq yq =


100 
let


101 
fun copy s =


102 
make (fn () =>


103 
(case pull s of


104 
None => pull yq


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


106 
in copy xq end;


107 


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


109 
fun append (xq, yq) =


110 
let


111 
fun copy s =


112 
make (fn () =>


113 
(case pull s of


114 
None => pull yq


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


116 
in copy xq end;


117 


118 
(*filter sequence by predicate*)


119 
fun filter pred xq =


120 
let


121 
fun copy s =


122 
make (fn () =>


123 
(case pull s of


124 
None => None


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


126 
in copy xq end;


127 


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


129 
fun flat xqq =


130 
make (fn () =>


131 
(case pull xqq of


132 
None => None


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


134 


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


136 
fun interleave (xq, yq) =


137 
make (fn () =>


138 
(case pull xq of


139 
None => pull yq


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


141 


142 


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


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


145 
fun print prelem count seq =


146 
let


147 
fun pr (k, xq) =


148 
if k > count then ()


149 
else


150 
(case pull xq of


151 
None => ()


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


153 
in pr (1, seq) end;


154 


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


156 
fun it_right f (xq, yq) =


157 
let


158 
fun its s =


159 
make (fn () =>


160 
(case pull s of


161 
None => pull yq


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


163 
in its xq end;


164 


165 


166 


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


168 


169 
fun succeed x = single x;


170 
fun fail _ = empty;


171 


172 


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


174 


175 
fun ORELSE (f, g) x =


176 
(case pull (f x) of


177 
None => g x


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


179 


180 
fun APPEND (f, g) x =


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


182 


183 


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


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


186 


187 


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


189 


190 
fun REPEAT f =


191 
let


192 
fun rep qs x =


193 
(case pull (f x) of


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


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


196 
and repq [] = None


197 
 repq (q :: qs) =


198 
(case pull q of


199 
None => repq qs


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


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


202 


203 


204 
end;
