src/Pure/General/seq.ML
author skalberg
Fri Mar 04 15:07:34 2005 +0100 (2005-03-04)
changeset 15574 b1d1b5bfc464
parent 15570 8d8c70b41bab
child 16002 e0557c452138
permissions -rw-r--r--
Removed practically all references to Library.foldr.
     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 
     6 Unbounded sequences implemented by closures.  RECOMPUTES if sequence
     7 is re-inspected.  Memoing, using polymorphic refs, was found to be
     8 slower!  (More GCs)
     9 *)
    10 
    11 signature SEQ =
    12 sig
    13   type 'a seq
    14   val make: (unit -> ('a * 'a seq) option) -> 'a seq
    15   val pull: 'a seq -> ('a * 'a seq) option
    16   val empty: 'a seq
    17   val cons: 'a * 'a seq -> 'a seq
    18   val single: 'a -> 'a seq
    19   val try: ('a -> 'b) -> 'a -> 'b 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   val DETERM: ('a -> 'b seq) -> 'a -> 'b seq
    46 end;
    47 
    48 structure Seq: SEQ =
    49 struct
    50 
    51 
    52 (** lazy sequences **)
    53 
    54 datatype 'a seq = Seq of unit -> ('a * 'a seq) option;
    55 
    56 (*the abstraction for making a sequence*)
    57 val make = Seq;
    58 
    59 (*return next sequence element as NONE or SOME (x, xq)*)
    60 fun pull (Seq f) = f ();
    61 
    62 
    63 (*the empty sequence*)
    64 val empty = Seq (fn () => NONE);
    65 
    66 (*prefix an element to the sequence -- use cons (x, xq) only if
    67   evaluation of xq need not be delayed, otherwise use
    68   make (fn () => SOME (x, xq))*)
    69 fun cons x_xq = make (fn () => SOME x_xq);
    70 
    71 fun single x = cons (x, empty);
    72 
    73 (*head and tail -- beware of calling the sequence function twice!!*)
    74 fun hd xq = #1 (valOf (pull xq))
    75 and tl xq = #2 (valOf (pull xq));
    76 
    77 (*partial function as procedure*)
    78 fun try f x =
    79   (case Library.try f x of
    80     SOME y => single y
    81   | NONE => empty);
    82 
    83 
    84 (*the list of the first n elements, paired with rest of sequence;
    85   if length of list is less than n, then sequence had less than n elements*)
    86 fun chop (n, xq) =
    87   if n <= 0 then ([], xq)
    88   else
    89     (case pull xq of
    90       NONE => ([], xq)
    91     | SOME (x, xq') => apfst (Library.cons x) (chop (n - 1, xq')));
    92 
    93 (*conversion from sequence to list*)
    94 fun list_of xq =
    95   (case pull xq of
    96     NONE => []
    97   | SOME (x, xq') => x :: list_of xq');
    98 
    99 (*conversion from list to sequence*)
   100 fun of_list xs = foldr cons empty xs;
   101 
   102 
   103 (*map the function f over the sequence, making a new sequence*)
   104 fun map f xq =
   105   make (fn () =>
   106     (case pull xq of
   107       NONE => NONE
   108     | SOME (x, xq') => SOME (f x, map f xq')));
   109 
   110 (*map over a sequence xq, append the sequence yq*)
   111 fun mapp f xq yq =
   112   let
   113     fun copy s =
   114       make (fn () =>
   115         (case pull s of
   116           NONE => pull yq
   117         | SOME (x, s') => SOME (f x, copy s')))
   118   in copy xq end;
   119 
   120 (*sequence append:  put the elements of xq in front of those of yq*)
   121 fun append (xq, yq) =
   122   let
   123     fun copy s =
   124       make (fn () =>
   125         (case pull s of
   126           NONE => pull yq
   127         | SOME (x, s') => SOME (x, copy s')))
   128   in copy xq end;
   129 
   130 (*filter sequence by predicate*)
   131 fun filter pred xq =
   132   let
   133     fun copy s =
   134       make (fn () =>
   135         (case pull s of
   136           NONE => NONE
   137         | SOME (x, s') => if pred x then SOME (x, copy s') else pull (copy s')));
   138   in copy xq end;
   139 
   140 (*flatten a sequence of sequences to a single sequence*)
   141 fun flat xqq =
   142   make (fn () =>
   143     (case pull xqq of
   144       NONE => NONE
   145     | SOME (xq, xqq') => pull (append (xq, flat xqq'))));
   146 
   147 (*interleave elements of xq with those of yq -- fairer than append*)
   148 fun interleave (xq, yq) =
   149   make (fn () =>
   150     (case pull xq of
   151       NONE => pull yq
   152     | SOME (x, xq') => SOME (x, interleave (yq, xq'))));
   153 
   154 
   155 (*functional to print a sequence, up to "count" elements;
   156   the function prelem should print the element number and also the element*)
   157 fun print prelem count seq =
   158   let
   159     fun pr (k, xq) =
   160       if k > count then ()
   161       else
   162         (case pull xq of
   163           NONE => ()
   164         | SOME (x, xq') => (prelem k x; writeln ""; pr (k + 1, xq')))
   165   in pr (1, seq) end;
   166 
   167 (*accumulating a function over a sequence; this is lazy*)
   168 fun it_right f (xq, yq) =
   169   let
   170     fun its s =
   171       make (fn () =>
   172         (case pull s of
   173           NONE => pull yq
   174         | SOME (a, s') => pull (f (a, its s'))))
   175   in its xq end;
   176 
   177 (*turn a list of sequences into a sequence of lists*)
   178 fun commute [] = single []
   179   | commute (xq :: xqs) =
   180       make (fn () =>
   181         (case pull xq of
   182           NONE => NONE
   183         | SOME (x, xq') =>
   184             (case pull (commute xqs) of
   185               NONE => NONE
   186             | SOME (xs, xsq) =>
   187                 SOME (x :: xs, append (map (Library.cons x) xsq, commute (xq' :: xqs))))));
   188 
   189 
   190 
   191 (** sequence functions **)      (*some code copied from Pure/tctical.ML*)
   192 
   193 fun succeed x = single x;
   194 fun fail _ = empty;
   195 
   196 fun op THEN (f, g) x = flat (map g (f x));
   197 
   198 fun op ORELSE (f, g) x =
   199   (case pull (f x) of
   200     NONE => g x
   201   | some => make (fn () => some));
   202 
   203 fun op APPEND (f, g) x =
   204   append (f x, make (fn () => pull (g x)));
   205 
   206 fun EVERY fs = foldr THEN succeed fs;
   207 fun FIRST fs = foldr ORELSE fail fs;
   208 
   209 fun TRY f = ORELSE (f, succeed);
   210 
   211 fun REPEAT f =
   212   let
   213     fun rep qs x =
   214       (case pull (f x) of
   215         NONE => SOME (x, make (fn () => repq qs))
   216       | SOME (x', q) => rep (q :: qs) x')
   217     and repq [] = NONE
   218       | repq (q :: qs) =
   219           (case pull q of
   220             NONE => repq qs
   221           | SOME (x, q) => rep (q :: qs) x);
   222   in fn x => make (fn () => rep [] x) end;
   223 
   224 fun REPEAT1 f = THEN (f, REPEAT f);
   225 
   226 fun INTERVAL f i j x =
   227   if i > j then single x
   228   else op THEN (f j, INTERVAL f i (j - 1)) x;
   229 
   230 fun DETERM f x =
   231   (case pull (f x) of
   232     NONE => empty
   233   | SOME (x', _) => cons (x', empty));
   234 
   235 end;