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