--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/seq.ML Fri Nov 21 15:27:43 1997 +0100
@@ -0,0 +1,155 @@
+(* Title: Pure/seq.ML
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+
+Unbounded sequences implemented by closures. RECOMPUTES if sequence
+is re-inspected. Memoing, using polymorphic refs, was found to be
+slower! (More GCs)
+*)
+
+signature SEQ =
+sig
+ type 'a seq
+ val make: (unit -> ('a * 'a seq) option) -> 'a seq
+ val pull: 'a seq -> ('a * 'a seq) option
+ val empty: 'a seq
+ val cons: 'a * 'a seq -> 'a seq
+ val single: 'a -> 'a seq
+ val hd: 'a seq -> 'a
+ val tl: 'a seq -> 'a seq
+ val chop: int * 'a seq -> 'a list * 'a seq
+ val list_of: 'a seq -> 'a list
+ val of_list: 'a list -> 'a seq
+ val map: ('a -> 'b) -> 'a seq -> 'b seq
+ val mapp: ('a -> 'b) -> 'a seq -> 'b seq -> 'b seq
+ val append: 'a seq * 'a seq -> 'a seq
+ val filter: ('a -> bool) -> 'a seq -> 'a seq
+ val flat: 'a seq seq -> 'a seq
+ val interleave: 'a seq * 'a seq -> 'a seq
+ val print: (int -> 'a -> unit) -> int -> 'a seq -> unit
+ val it_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq
+end;
+
+structure Seq: SEQ =
+struct
+
+
+datatype 'a seq = Seq of unit -> ('a * 'a seq) option;
+
+(*the abstraction for making a sequence*)
+val make = Seq;
+
+(*return next sequence element as None or Some (x, xq)*)
+fun pull (Seq f) = f ();
+
+
+(*the empty sequence*)
+val empty = make (fn () => None);
+
+(*prefix an element to the sequence -- use cons (x, xq) only if
+ evaluation of xq need not be delayed, otherwise use
+ make (fn () => Some (x, xq))*)
+fun cons x_xq = make (fn () => Some x_xq);
+
+fun single x = cons (x, empty);
+
+(*head and tail -- beware of calling the sequence function twice!!*)
+fun hd xq = #1 (the (pull xq))
+and tl xq = #2 (the (pull xq));
+
+
+(*the list of the first n elements, paired with rest of sequence;
+ if length of list is less than n, then sequence had less than n elements*)
+fun chop (n, xq) =
+ if n <= 0 then ([], xq)
+ else
+ (case pull xq of
+ None => ([], xq)
+ | Some (x, xq') => apfst (Library.cons x) (chop (n - 1, xq')));
+
+(*conversion from sequence to list*)
+fun list_of xq =
+ (case pull xq of
+ None => []
+ | Some (x, xq') => x :: list_of xq');
+
+(*conversion from list to sequence*)
+fun of_list xs = foldr cons (xs, empty);
+
+
+(*map the function f over the sequence, making a new sequence*)
+fun map f xq =
+ make (fn () =>
+ (case pull xq of
+ None => None
+ | Some (x, xq') => Some (f x, map f xq')));
+
+(*map over a sequence xq, append the sequence yq*)
+fun mapp f xq yq =
+ let
+ fun copy s =
+ make (fn () =>
+ (case pull s of
+ None => pull yq
+ | Some (x, s') => Some (f x, copy s')))
+ in copy xq end;
+
+(*sequence append: put the elements of xq in front of those of yq*)
+fun append (xq, yq) =
+ let
+ fun copy s =
+ make (fn () =>
+ (case pull s of
+ None => pull yq
+ | Some (x, s') => Some (x, copy s')))
+ in copy xq end;
+
+(*filter sequence by predicate*)
+fun filter pred xq =
+ let
+ fun copy s =
+ make (fn () =>
+ (case pull s of
+ None => None
+ | Some (x, s') => if pred x then Some (x, copy s') else pull (copy s')));
+ in copy xq end;
+
+(*flatten a sequence of sequences to a single sequence*)
+fun flat xqq =
+ make (fn () =>
+ (case pull xqq of
+ None => None
+ | Some (xq, xqq') => pull (append (xq, flat xqq'))));
+
+(*interleave elements of xq with those of yq -- fairer than append*)
+fun interleave (xq, yq) =
+ make (fn () =>
+ (case pull xq of
+ None => pull yq
+ | Some (x, xq') => Some (x, interleave (yq, xq'))));
+
+
+(*functional to print a sequence, up to "count" elements;
+ the function prelem should print the element number and also the element*)
+fun print prelem count seq =
+ let
+ fun pr (k, xq) =
+ if k > count then ()
+ else
+ (case pull xq of
+ None => ()
+ | Some (x, xq') => (prelem k x; writeln ""; pr (k + 1, xq')))
+ in pr (1, seq) end;
+
+(*accumulating a function over a sequence; this is lazy*)
+fun it_right f (xq, yq) =
+ let
+ fun its s =
+ make (fn () =>
+ (case pull s of
+ None => pull yq
+ | Some (a, s') => pull (f (a, its s'))))
+ in its xq end;
+
+
+end;