wenzelm@6118: (*  Title:      Pure/General/seq.ML
wenzelm@5014:     ID:         $Id$
wenzelm@5014:     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
wenzelm@5014: 
wenzelm@5014: Unbounded sequences implemented by closures.  RECOMPUTES if sequence
wenzelm@5014: is re-inspected.  Memoing, using polymorphic refs, was found to be
wenzelm@5014: slower!  (More GCs)
wenzelm@5014: *)
wenzelm@5014: 
wenzelm@5014: signature SEQ =
wenzelm@5014: sig
wenzelm@5014:   type 'a seq
wenzelm@5014:   val make: (unit -> ('a * 'a seq) option) -> 'a seq
wenzelm@5014:   val pull: 'a seq -> ('a * 'a seq) option
wenzelm@5014:   val empty: 'a seq
wenzelm@5014:   val cons: 'a * 'a seq -> 'a seq
wenzelm@5014:   val single: 'a -> 'a seq
wenzelm@5014:   val hd: 'a seq -> 'a
wenzelm@5014:   val tl: 'a seq -> 'a seq
wenzelm@5014:   val chop: int * 'a seq -> 'a list * 'a seq
wenzelm@5014:   val list_of: 'a seq -> 'a list
wenzelm@5014:   val of_list: 'a list -> 'a seq
wenzelm@5014:   val map: ('a -> 'b) -> 'a seq -> 'b seq
wenzelm@5014:   val mapp: ('a -> 'b) -> 'a seq -> 'b seq -> 'b seq
wenzelm@5014:   val append: 'a seq * 'a seq -> 'a seq
wenzelm@5014:   val filter: ('a -> bool) -> 'a seq -> 'a seq
wenzelm@5014:   val flat: 'a seq seq -> 'a seq
wenzelm@5014:   val interleave: 'a seq * 'a seq -> 'a seq
wenzelm@5014:   val print: (int -> 'a -> unit) -> int -> 'a seq -> unit
wenzelm@5014:   val it_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq
wenzelm@6927:   val commute: 'a seq list -> 'a list seq
wenzelm@5014:   val succeed: 'a -> 'a seq
wenzelm@5014:   val fail: 'a -> 'b seq
wenzelm@5014:   val THEN: ('a -> 'b seq) * ('b -> 'c seq) -> 'a -> 'c seq
wenzelm@5014:   val ORELSE: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq
wenzelm@5014:   val APPEND: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq
wenzelm@5014:   val EVERY: ('a -> 'a seq) list -> 'a -> 'a seq
wenzelm@5014:   val FIRST: ('a -> 'b seq) list -> 'a -> 'b seq
wenzelm@5014:   val TRY: ('a -> 'a seq) -> 'a -> 'a seq
wenzelm@5014:   val REPEAT: ('a -> 'a seq) -> 'a -> 'a seq
wenzelm@5558:   val REPEAT1: ('a -> 'a seq) -> 'a -> 'a seq
wenzelm@8535:   val INTERVAL: (int -> 'a -> 'a seq) -> int -> int -> 'a -> 'a seq
wenzelm@5014: end;
wenzelm@5014: 
wenzelm@5014: structure Seq: SEQ =
wenzelm@5014: struct
wenzelm@5014: 
wenzelm@5014: 
wenzelm@5014: (** lazy sequences **)
wenzelm@5014: 
wenzelm@5014: datatype 'a seq = Seq of unit -> ('a * 'a seq) option;
wenzelm@5014: 
wenzelm@5014: (*the abstraction for making a sequence*)
wenzelm@5014: val make = Seq;
wenzelm@5014: 
wenzelm@5014: (*return next sequence element as None or Some (x, xq)*)
wenzelm@5014: fun pull (Seq f) = f ();
wenzelm@5014: 
wenzelm@5014: 
wenzelm@5014: (*the empty sequence*)
wenzelm@5014: val empty = Seq (fn () => None);
wenzelm@5014: 
wenzelm@5014: (*prefix an element to the sequence -- use cons (x, xq) only if
wenzelm@5014:   evaluation of xq need not be delayed, otherwise use
wenzelm@5014:   make (fn () => Some (x, xq))*)
wenzelm@5014: fun cons x_xq = make (fn () => Some x_xq);
wenzelm@5014: 
wenzelm@5014: fun single x = cons (x, empty);
wenzelm@5014: 
wenzelm@5014: (*head and tail -- beware of calling the sequence function twice!!*)
wenzelm@5014: fun hd xq = #1 (the (pull xq))
wenzelm@5014: and tl xq = #2 (the (pull xq));
wenzelm@5014: 
wenzelm@5014: 
wenzelm@5014: (*the list of the first n elements, paired with rest of sequence;
wenzelm@5014:   if length of list is less than n, then sequence had less than n elements*)
wenzelm@5014: fun chop (n, xq) =
wenzelm@5014:   if n <= 0 then ([], xq)
wenzelm@5014:   else
wenzelm@5014:     (case pull xq of
wenzelm@5014:       None => ([], xq)
wenzelm@5014:     | Some (x, xq') => apfst (Library.cons x) (chop (n - 1, xq')));
wenzelm@5014: 
wenzelm@5014: (*conversion from sequence to list*)
wenzelm@5014: fun list_of xq =
wenzelm@5014:   (case pull xq of
wenzelm@5014:     None => []
wenzelm@5014:   | Some (x, xq') => x :: list_of xq');
wenzelm@5014: 
wenzelm@5014: (*conversion from list to sequence*)
wenzelm@5014: fun of_list xs = foldr cons (xs, empty);
wenzelm@5014: 
wenzelm@5014: 
wenzelm@5014: (*map the function f over the sequence, making a new sequence*)
wenzelm@5014: fun map f xq =
wenzelm@5014:   make (fn () =>
wenzelm@5014:     (case pull xq of
wenzelm@5014:       None => None
wenzelm@5014:     | Some (x, xq') => Some (f x, map f xq')));
wenzelm@5014: 
wenzelm@5014: (*map over a sequence xq, append the sequence yq*)
wenzelm@5014: fun mapp f xq yq =
wenzelm@5014:   let
wenzelm@5014:     fun copy s =
wenzelm@5014:       make (fn () =>
wenzelm@5014:         (case pull s of
wenzelm@5014:           None => pull yq
wenzelm@5014:         | Some (x, s') => Some (f x, copy s')))
wenzelm@5014:   in copy xq end;
wenzelm@5014: 
wenzelm@5014: (*sequence append:  put the elements of xq in front of those of yq*)
wenzelm@5014: fun append (xq, yq) =
wenzelm@5014:   let
wenzelm@5014:     fun copy s =
wenzelm@5014:       make (fn () =>
wenzelm@5014:         (case pull s of
wenzelm@5014:           None => pull yq
wenzelm@5014:         | Some (x, s') => Some (x, copy s')))
wenzelm@5014:   in copy xq end;
wenzelm@5014: 
wenzelm@5014: (*filter sequence by predicate*)
wenzelm@5014: fun filter pred xq =
wenzelm@5014:   let
wenzelm@5014:     fun copy s =
wenzelm@5014:       make (fn () =>
wenzelm@5014:         (case pull s of
wenzelm@5014:           None => None
wenzelm@5014:         | Some (x, s') => if pred x then Some (x, copy s') else pull (copy s')));
wenzelm@5014:   in copy xq end;
wenzelm@5014: 
wenzelm@5014: (*flatten a sequence of sequences to a single sequence*)
wenzelm@5014: fun flat xqq =
wenzelm@5014:   make (fn () =>
wenzelm@5014:     (case pull xqq of
wenzelm@5014:       None => None
wenzelm@5014:     | Some (xq, xqq') => pull (append (xq, flat xqq'))));
wenzelm@5014: 
wenzelm@5014: (*interleave elements of xq with those of yq -- fairer than append*)
wenzelm@5014: fun interleave (xq, yq) =
wenzelm@5014:   make (fn () =>
wenzelm@5014:     (case pull xq of
wenzelm@5014:       None => pull yq
wenzelm@5014:     | Some (x, xq') => Some (x, interleave (yq, xq'))));
wenzelm@5014: 
wenzelm@5014: 
wenzelm@5014: (*functional to print a sequence, up to "count" elements;
wenzelm@5014:   the function prelem should print the element number and also the element*)
wenzelm@5014: fun print prelem count seq =
wenzelm@5014:   let
wenzelm@5014:     fun pr (k, xq) =
wenzelm@5014:       if k > count then ()
wenzelm@5014:       else
wenzelm@5014:         (case pull xq of
wenzelm@5014:           None => ()
wenzelm@5014:         | Some (x, xq') => (prelem k x; writeln ""; pr (k + 1, xq')))
wenzelm@5014:   in pr (1, seq) end;
wenzelm@5014: 
wenzelm@5014: (*accumulating a function over a sequence; this is lazy*)
wenzelm@5014: fun it_right f (xq, yq) =
wenzelm@5014:   let
wenzelm@5014:     fun its s =
wenzelm@5014:       make (fn () =>
wenzelm@5014:         (case pull s of
wenzelm@5014:           None => pull yq
wenzelm@5014:         | Some (a, s') => pull (f (a, its s'))))
wenzelm@5014:   in its xq end;
wenzelm@5014: 
wenzelm@6927: (*turn a list of sequences into a sequence of lists*)
wenzelm@6927: fun commute [] = single []
wenzelm@6927:   | commute (xq :: xqs) =
wenzelm@6927:       make (fn () =>
wenzelm@6927:         (case pull xq of
wenzelm@6927:           None => None
wenzelm@6927:         | Some (x, xq') =>
wenzelm@6927:             (case pull (commute xqs) of
wenzelm@6927:               None => None
wenzelm@6927:             | Some (xs, xsq) =>
wenzelm@6927:                 Some (x :: xs, append (map (Library.cons x) xsq, commute (xq' :: xqs))))));
wenzelm@6927: 
wenzelm@5014: 
wenzelm@5014: 
wenzelm@5014: (** sequence functions **)      (*some code duplicated from Pure/tctical.ML*)
wenzelm@5014: 
wenzelm@5014: fun succeed x = single x;
wenzelm@5014: fun fail _ = empty;
wenzelm@5014: 
wenzelm@5014: 
wenzelm@5864: fun op THEN (f, g) x = flat (map g (f x));
wenzelm@5014: 
wenzelm@5864: fun op ORELSE (f, g) x =
wenzelm@5014:   (case pull (f x) of
wenzelm@5014:     None => g x
wenzelm@5014:   | some => make (fn () => some));
wenzelm@5014: 
wenzelm@5864: fun op APPEND (f, g) x =
wenzelm@5014:   append (f x, make (fn () => pull (g x)));
wenzelm@5014: 
wenzelm@5014: 
wenzelm@5014: fun EVERY fs = foldr THEN (fs, succeed);
wenzelm@5014: fun FIRST fs = foldr ORELSE (fs, fail);
wenzelm@5014: 
wenzelm@5014: 
wenzelm@5014: fun TRY f = ORELSE (f, succeed);
wenzelm@5014: 
wenzelm@5014: fun REPEAT f =
wenzelm@5014:   let
wenzelm@5014:     fun rep qs x =
wenzelm@5014:       (case pull (f x) of
wenzelm@5014:         None => Some (x, make (fn () => repq qs))
wenzelm@5014:       | Some (x', q) => rep (q :: qs) x')
wenzelm@5014:     and repq [] = None
wenzelm@5014:       | repq (q :: qs) =
wenzelm@5014:           (case pull q of
wenzelm@5014:             None => repq qs
wenzelm@5014:           | Some (x, q) => rep (q :: qs) x);
wenzelm@5014:   in fn x => make (fn () => rep [] x) end;
wenzelm@5014: 
wenzelm@5558: fun REPEAT1 f = THEN (f, REPEAT f);
wenzelm@5558: 
wenzelm@5014: 
wenzelm@8535: fun INTERVAL f i j x =
wenzelm@8535:   if i > j then single x
wenzelm@8535:   else op THEN (f j, INTERVAL f i (j - 1)) x;
wenzelm@8535: 
wenzelm@8535: 
wenzelm@5014: end;