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