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