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


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

5558

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

5014

41 
end;


42 


43 
structure Seq: SEQ =


44 
struct


45 


46 


47 
(** lazy sequences **)


48 


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


50 


51 
(*the abstraction for making a sequence*)


52 
val make = Seq;


53 


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


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


56 


57 


58 
(*the empty sequence*)


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


60 


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


62 
evaluation of xq need not be delayed, otherwise use


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


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


65 


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


67 


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


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


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


71 


72 


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


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


75 
fun chop (n, xq) =


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


77 
else


78 
(case pull xq of


79 
None => ([], xq)


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


81 


82 
(*conversion from sequence to list*)


83 
fun list_of xq =


84 
(case pull xq of


85 
None => []


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


87 


88 
(*conversion from list to sequence*)


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


90 


91 


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


93 
fun map f xq =


94 
make (fn () =>


95 
(case pull xq of


96 
None => None


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


98 


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


100 
fun mapp f xq yq =


101 
let


102 
fun copy s =


103 
make (fn () =>


104 
(case pull s of


105 
None => pull yq


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


107 
in copy xq end;


108 


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


110 
fun append (xq, yq) =


111 
let


112 
fun copy s =


113 
make (fn () =>


114 
(case pull s of


115 
None => pull yq


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


117 
in copy xq end;


118 


119 
(*filter sequence by predicate*)


120 
fun filter pred xq =


121 
let


122 
fun copy s =


123 
make (fn () =>


124 
(case pull s of


125 
None => None


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


127 
in copy xq end;


128 


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


130 
fun flat xqq =


131 
make (fn () =>


132 
(case pull xqq of


133 
None => None


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


135 


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


137 
fun interleave (xq, yq) =


138 
make (fn () =>


139 
(case pull xq of


140 
None => pull yq


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


142 


143 


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


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


146 
fun print prelem count seq =


147 
let


148 
fun pr (k, xq) =


149 
if k > count then ()


150 
else


151 
(case pull xq of


152 
None => ()


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


154 
in pr (1, seq) end;


155 


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


157 
fun it_right f (xq, yq) =


158 
let


159 
fun its s =


160 
make (fn () =>


161 
(case pull s of


162 
None => pull yq


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


164 
in its xq end;


165 


166 


167 


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


169 


170 
fun succeed x = single x;


171 
fun fail _ = empty;


172 


173 

5864

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

5014

175 

5864

176 
fun op ORELSE (f, g) x =

5014

177 
(case pull (f x) of


178 
None => g x


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


180 

5864

181 
fun op APPEND (f, g) x =

5014

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


183 


184 


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


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


187 


188 


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


190 


191 
fun REPEAT f =


192 
let


193 
fun rep qs x =


194 
(case pull (f x) of


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


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


197 
and repq [] = None


198 
 repq (q :: qs) =


199 
(case pull q of


200 
None => repq qs


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


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


203 

5558

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


205 

5014

206 


207 
end;
