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