src/Pure/General/seq.ML
author wenzelm
Tue Sep 13 22:19:31 2005 +0200 (2005-09-13)
changeset 17347 fb3d42ef61ed
parent 16534 95460b6eb712
child 19475 8aa2b380614a
permissions -rw-r--r--
added maps, map_list, lift, lifts;
     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 lift: ('a -> 'b -> 'c) -> 'a seq -> 'b -> 'c seq
    33   val lifts: ('a -> 'b -> 'c seq) -> 'a seq -> 'b -> 'c seq
    34   val print: (int -> 'a -> unit) -> int -> 'a seq -> unit
    35   val it_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq
    36   val commute: 'a seq list -> 'a list seq
    37   val map_list: ('a -> 'b seq) -> 'a list -> 'b list 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 Library.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 (Library.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 = foldr cons empty xs;
   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 
   160 fun lift f xq y = map (fn x => f x y) xq;
   161 fun lifts f xq y = maps (fn x => f x y) xq;
   162 
   163 (*print a sequence, up to "count" elements*)
   164 fun print print_elem count =
   165   let
   166     fun prnt k xq =
   167       if k > count then ()
   168       else
   169         (case pull xq of
   170           NONE => ()
   171         | SOME (x, xq') => (print_elem k x; writeln ""; prnt (k + 1) xq'));
   172   in prnt 1 end;
   173 
   174 (*accumulating a function over a sequence; this is lazy*)
   175 fun it_right f (xq, yq) =
   176   let
   177     fun its s =
   178       make (fn () =>
   179         (case pull s of
   180           NONE => pull yq
   181         | SOME (a, s') => pull (f (a, its s'))))
   182   in its xq end;
   183 
   184 (*turn a list of sequences into a sequence of lists*)
   185 fun commute [] = single []
   186   | commute (xq :: xqs) =
   187       make (fn () =>
   188         (case pull xq of
   189           NONE => NONE
   190         | SOME (x, xq') =>
   191             (case pull (commute xqs) of
   192               NONE => NONE
   193             | SOME (xs, xsq) =>
   194                 SOME (x :: xs, append (map (Library.cons x) xsq, commute (xq' :: xqs))))));
   195 
   196 fun map_list f = commute o List.map f;
   197 
   198 
   199 
   200 (** sequence functions **)      (*some code copied from Pure/tctical.ML*)
   201 
   202 fun succeed x = single x;
   203 fun fail _ = empty;
   204 
   205 fun op THEN (f, g) x = flat (map g (f x));
   206 
   207 fun op ORELSE (f, g) x =
   208   (case pull (f x) of
   209     NONE => g x
   210   | some => make (fn () => some));
   211 
   212 fun op APPEND (f, g) x =
   213   append (f x, make (fn () => pull (g x)));
   214 
   215 fun EVERY fs = foldr THEN succeed fs;
   216 fun FIRST fs = foldr ORELSE fail fs;
   217 
   218 fun TRY f = ORELSE (f, succeed);
   219 
   220 fun REPEAT f =
   221   let
   222     fun rep qs x =
   223       (case pull (f x) of
   224         NONE => SOME (x, make (fn () => repq qs))
   225       | SOME (x', q) => rep (q :: qs) x')
   226     and repq [] = NONE
   227       | repq (q :: qs) =
   228           (case pull q of
   229             NONE => repq qs
   230           | SOME (x, q) => rep (q :: qs) x);
   231   in fn x => make (fn () => rep [] x) end;
   232 
   233 fun REPEAT1 f = THEN (f, REPEAT f);
   234 
   235 fun INTERVAL f i j x =
   236   if i > j then single x
   237   else op THEN (f j, INTERVAL f i (j - 1)) x;
   238 
   239 fun DETERM f x =
   240   (case pull (f x) of
   241     NONE => empty
   242   | SOME (x', _) => cons (x', empty));
   243 
   244 end;