--- a/src/Pure/sequence.ML Fri Nov 21 15:41:27 1997 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,141 +0,0 @@
-(* Title: sequence
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1988 University of Cambridge
-
-Unbounded sequences implemented by closures.
-
-RECOMPUTES if sequence is re-inspected.
-
-Memoing, using polymorphic refs, was found to be slower! (More GCs)
-*)
-
-
-signature SEQUENCE =
- sig
- type 'a seq
- val append : 'a seq * 'a seq -> 'a seq
- val chop : int * 'a seq -> 'a list * 'a seq
- val cons : 'a * 'a seq -> 'a seq
- val filters : ('a -> bool) -> 'a seq -> 'a seq
- val flats : 'a seq seq -> 'a seq
- val hd : 'a seq -> 'a
- val interleave: 'a seq * 'a seq -> 'a seq
- val its_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq
- val list_of_s : 'a seq -> 'a list
- val mapp : ('a -> 'b) -> 'a seq -> 'b seq -> 'b seq
- val maps : ('a -> 'b) -> 'a seq -> 'b seq
- val null : 'a seq
- val prints : (int -> 'a -> unit) -> int -> 'a seq -> unit
- val pull : 'a seq -> ('a * 'a seq) option
- val s_of_list : 'a list -> 'a seq
- val seqof : (unit -> ('a * 'a seq) option) -> 'a seq
- val single : 'a -> 'a seq
- val tl : 'a seq -> 'a seq
- end;
-
-
-structure Sequence : SEQUENCE =
-struct
-
-datatype 'a seq = Seq of unit -> ('a * 'a seq)option;
-
-(*Return next sequence element as None or Some(x,str) *)
-fun pull(Seq f) = f();
-
-(*Head and tail. Beware of calling the sequence function twice!!*)
-fun hd s = #1 (the (pull s))
-and tl s = #2 (the (pull s));
-
-(*the abstraction for making a sequence*)
-val seqof = Seq;
-
-(*prefix an element to the sequence
- use cons(x,s) only if evaluation of s need not be delayed,
- otherwise use seqof(fn()=> Some(x,s)) *)
-fun cons all = Seq(fn()=>Some all);
-
-(*the empty sequence*)
-val null = Seq(fn()=>None);
-
-fun single(x) = cons (x, null);
-
-(*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:int, s: 'a seq): 'a list * 'a seq =
- if n<=0 then ([],s)
- else case pull(s) of
- None => ([],s)
- | Some(x,s') => let val (xs,s'') = chop (n-1,s')
- in (x::xs, s'') end;
-
-(*conversion from sequence to list*)
-fun list_of_s (s: 'a seq) : 'a list = case pull(s) of
- None => []
- | Some(x,s') => x :: list_of_s s';
-
-
-(*conversion from list to sequence*)
-fun s_of_list [] = null
- | s_of_list (x::l) = cons (x, s_of_list l);
-
-
-(*functional to print a sequence, up to "count" elements
- the function prelem should print the element number and also the element*)
-fun prints (prelem: int -> 'a -> unit) count (s: 'a seq) : unit =
- let fun pr (k,s) =
- if k>count then ()
- else case pull(s) of
- None => ()
- | Some(x,s') => (prelem k x; prs"\n"; pr (k+1, s'))
- in pr(1,s) end;
-
-(*Map the function f over the sequence, making a new sequence*)
-fun maps f xq = seqof (fn()=> case pull(xq) of
- None => None
- | Some(x,yq) => Some(f x, maps f yq));
-
-(*Sequence append: put the elements of xq in front of those of yq*)
-fun append (xq,yq) =
- let fun copy xq = seqof (fn()=>
- case pull xq of
- None => pull yq
- | Some(x,xq') => Some (x, copy xq'))
- in copy xq end;
-
-(*Interleave elements of xq with those of yq -- fairer than append*)
-fun interleave (xq,yq) = seqof (fn()=>
- case pull(xq) of
- None => pull yq
- | Some(x,xq') => Some (x, interleave(yq, xq')));
-
-(*map over a sequence xq, append the sequence yq*)
-fun mapp f xq yq =
- let fun copy s = seqof (fn()=>
- case pull(s) of
- None => pull(yq)
- | Some(x,xq') => Some(f x, copy xq'))
- in copy xq end;
-
-(*Flatten a sequence of sequences to a single sequence. *)
-fun flats ss = seqof (fn()=> case pull(ss) of
- None => None
- | Some(s,ss') => pull(append(s, flats ss')));
-
-(*accumulating a function over a sequence; this is lazy*)
-fun its_right (f: 'a * 'b seq -> 'b seq) (s: 'a seq, bstr: 'b seq) : 'b seq =
- let fun its s = seqof (fn()=>
- case pull(s) of
- None => pull bstr
- | Some(a,s') => pull(f(a, its s')))
- in its s end;
-
-fun filters pred xq =
- let fun copy s = seqof (fn()=>
- case pull(s) of
- None => None
- | Some(x,xq') => if pred x then Some(x, copy xq')
- else pull (copy xq') )
- in copy xq end
-
-end;