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