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