src/Pure/General/seq.ML
author wenzelm
Wed Jun 10 11:52:59 1998 +0200 (1998-06-10)
changeset 5014 32e6cab5e7d4
child 5558 64a8495201d1
permissions -rw-r--r--
moved seq.ML to General/seq.ML;
     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   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
    40 end;
    41 
    42 structure Seq: SEQ =
    43 struct
    44 
    45 
    46 (** lazy sequences **)
    47 
    48 datatype 'a seq = Seq of unit -> ('a * 'a seq) option;
    49 
    50 (*the abstraction for making a sequence*)
    51 val make = Seq;
    52 
    53 (*return next sequence element as None or Some (x, xq)*)
    54 fun pull (Seq f) = f ();
    55 
    56 
    57 (*the empty sequence*)
    58 val empty = Seq (fn () => None);
    59 
    60 (*prefix an element to the sequence -- use cons (x, xq) only if
    61   evaluation of xq need not be delayed, otherwise use
    62   make (fn () => Some (x, xq))*)
    63 fun cons x_xq = make (fn () => Some x_xq);
    64 
    65 fun single x = cons (x, empty);
    66 
    67 (*head and tail -- beware of calling the sequence function twice!!*)
    68 fun hd xq = #1 (the (pull xq))
    69 and tl xq = #2 (the (pull xq));
    70 
    71 
    72 (*the list of the first n elements, paired with rest of sequence;
    73   if length of list is less than n, then sequence had less than n elements*)
    74 fun chop (n, xq) =
    75   if n <= 0 then ([], xq)
    76   else
    77     (case pull xq of
    78       None => ([], xq)
    79     | Some (x, xq') => apfst (Library.cons x) (chop (n - 1, xq')));
    80 
    81 (*conversion from sequence to list*)
    82 fun list_of xq =
    83   (case pull xq of
    84     None => []
    85   | Some (x, xq') => x :: list_of xq');
    86 
    87 (*conversion from list to sequence*)
    88 fun of_list xs = foldr cons (xs, empty);
    89 
    90 
    91 (*map the function f over the sequence, making a new sequence*)
    92 fun map f xq =
    93   make (fn () =>
    94     (case pull xq of
    95       None => None
    96     | Some (x, xq') => Some (f x, map f xq')));
    97 
    98 (*map over a sequence xq, append the sequence yq*)
    99 fun mapp f xq yq =
   100   let
   101     fun copy s =
   102       make (fn () =>
   103         (case pull s of
   104           None => pull yq
   105         | Some (x, s') => Some (f x, copy s')))
   106   in copy xq end;
   107 
   108 (*sequence append:  put the elements of xq in front of those of yq*)
   109 fun append (xq, yq) =
   110   let
   111     fun copy s =
   112       make (fn () =>
   113         (case pull s of
   114           None => pull yq
   115         | Some (x, s') => Some (x, copy s')))
   116   in copy xq end;
   117 
   118 (*filter sequence by predicate*)
   119 fun filter pred xq =
   120   let
   121     fun copy s =
   122       make (fn () =>
   123         (case pull s of
   124           None => None
   125         | Some (x, s') => if pred x then Some (x, copy s') else pull (copy s')));
   126   in copy xq end;
   127 
   128 (*flatten a sequence of sequences to a single sequence*)
   129 fun flat xqq =
   130   make (fn () =>
   131     (case pull xqq of
   132       None => None
   133     | Some (xq, xqq') => pull (append (xq, flat xqq'))));
   134 
   135 (*interleave elements of xq with those of yq -- fairer than append*)
   136 fun interleave (xq, yq) =
   137   make (fn () =>
   138     (case pull xq of
   139       None => pull yq
   140     | Some (x, xq') => Some (x, interleave (yq, xq'))));
   141 
   142 
   143 (*functional to print a sequence, up to "count" elements;
   144   the function prelem should print the element number and also the element*)
   145 fun print prelem count seq =
   146   let
   147     fun pr (k, xq) =
   148       if k > count then ()
   149       else
   150         (case pull xq of
   151           None => ()
   152         | Some (x, xq') => (prelem k x; writeln ""; pr (k + 1, xq')))
   153   in pr (1, seq) end;
   154 
   155 (*accumulating a function over a sequence; this is lazy*)
   156 fun it_right f (xq, yq) =
   157   let
   158     fun its s =
   159       make (fn () =>
   160         (case pull s of
   161           None => pull yq
   162         | Some (a, s') => pull (f (a, its s'))))
   163   in its xq end;
   164 
   165 
   166 
   167 (** sequence functions **)      (*some code duplicated from Pure/tctical.ML*)
   168 
   169 fun succeed x = single x;
   170 fun fail _ = empty;
   171 
   172 
   173 fun THEN (f, g) x = flat (map g (f x));
   174 
   175 fun ORELSE (f, g) x =
   176   (case pull (f x) of
   177     None => g x
   178   | some => make (fn () => some));
   179 
   180 fun APPEND (f, g) x =
   181   append (f x, make (fn () => pull (g x)));
   182 
   183 
   184 fun EVERY fs = foldr THEN (fs, succeed);
   185 fun FIRST fs = foldr ORELSE (fs, fail);
   186 
   187 
   188 fun TRY f = ORELSE (f, succeed);
   189 
   190 fun REPEAT f =
   191   let
   192     fun rep qs x =
   193       (case pull (f x) of
   194         None => Some (x, make (fn () => repq qs))
   195       | Some (x', q) => rep (q :: qs) x')
   196     and repq [] = None
   197       | repq (q :: qs) =
   198           (case pull q of
   199             None => repq qs
   200           | Some (x, q) => rep (q :: qs) x);
   201   in fn x => make (fn () => rep [] x) end;
   202 
   203 
   204 end;