src/Pure/seq.ML
author nipkow
Fri Nov 28 07:35:10 1997 +0100 (1997-11-28)
changeset 4318 9b672ea2dfe7
parent 4279 835ea07170a6
child 4992 c63a93b8577c
permissions -rw-r--r--
Fixed the definition of `termord': is now antisymmetric.
     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 re-inspected.  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 end;
    32 
    33 structure Seq: SEQ =
    34 struct
    35 
    36 
    37 datatype 'a seq = Seq of unit -> ('a * 'a seq) option;
    38 
    39 (*the abstraction for making a sequence*)
    40 val make = Seq;
    41 
    42 (*return next sequence element as None or Some (x, xq)*)
    43 fun pull (Seq f) = f ();
    44 
    45 
    46 (*the empty sequence*)
    47 val empty = Seq (fn () => None);
    48 
    49 (*prefix an element to the sequence -- use cons (x, xq) only if
    50   evaluation of xq need not be delayed, otherwise use
    51   make (fn () => Some (x, xq))*)
    52 fun cons x_xq = make (fn () => Some x_xq);
    53 
    54 fun single x = cons (x, empty);
    55 
    56 (*head and tail -- beware of calling the sequence function twice!!*)
    57 fun hd xq = #1 (the (pull xq))
    58 and tl xq = #2 (the (pull xq));
    59 
    60 
    61 (*the list of the first n elements, paired with rest of sequence;
    62   if length of list is less than n, then sequence had less than n elements*)
    63 fun chop (n, xq) =
    64   if n <= 0 then ([], xq)
    65   else
    66     (case pull xq of
    67       None => ([], xq)
    68     | Some (x, xq') => apfst (Library.cons x) (chop (n - 1, xq')));
    69 
    70 (*conversion from sequence to list*)
    71 fun list_of xq =
    72   (case pull xq of
    73     None => []
    74   | Some (x, xq') => x :: list_of xq');
    75 
    76 (*conversion from list to sequence*)
    77 fun of_list xs = foldr cons (xs, empty);
    78 
    79 
    80 (*map the function f over the sequence, making a new sequence*)
    81 fun map f xq =
    82   make (fn () =>
    83     (case pull xq of
    84       None => None
    85     | Some (x, xq') => Some (f x, map f xq')));
    86 
    87 (*map over a sequence xq, append the sequence yq*)
    88 fun mapp f xq yq =
    89   let
    90     fun copy s =
    91       make (fn () =>
    92         (case pull s of
    93           None => pull yq
    94         | Some (x, s') => Some (f x, copy s')))
    95   in copy xq end;
    96 
    97 (*sequence append:  put the elements of xq in front of those of yq*)
    98 fun append (xq, yq) =
    99   let
   100     fun copy s =
   101       make (fn () =>
   102         (case pull s of
   103           None => pull yq
   104         | Some (x, s') => Some (x, copy s')))
   105   in copy xq end;
   106 
   107 (*filter sequence by predicate*)
   108 fun filter pred xq =
   109   let
   110     fun copy s =
   111       make (fn () =>
   112         (case pull s of
   113           None => None
   114         | Some (x, s') => if pred x then Some (x, copy s') else pull (copy s')));
   115   in copy xq end;
   116 
   117 (*flatten a sequence of sequences to a single sequence*)
   118 fun flat xqq =
   119   make (fn () =>
   120     (case pull xqq of
   121       None => None
   122     | Some (xq, xqq') => pull (append (xq, flat xqq'))));
   123 
   124 (*interleave elements of xq with those of yq -- fairer than append*)
   125 fun interleave (xq, yq) =
   126   make (fn () =>
   127     (case pull xq of
   128       None => pull yq
   129     | Some (x, xq') => Some (x, interleave (yq, xq'))));
   130 
   131 
   132 (*functional to print a sequence, up to "count" elements;
   133   the function prelem should print the element number and also the element*)
   134 fun print prelem count seq =
   135   let
   136     fun pr (k, xq) =
   137       if k > count then ()
   138       else
   139         (case pull xq of
   140           None => ()
   141         | Some (x, xq') => (prelem k x; writeln ""; pr (k + 1, xq')))
   142   in pr (1, seq) end;
   143 
   144 (*accumulating a function over a sequence; this is lazy*)
   145 fun it_right f (xq, yq) =
   146   let
   147     fun its s =
   148       make (fn () =>
   149         (case pull s of
   150           None => pull yq
   151         | Some (a, s') => pull (f (a, its s'))))
   152   in its xq end;
   153 
   154 
   155 end;