src/Pure/General/seq.ML
changeset 17347 fb3d42ef61ed
parent 16534 95460b6eb712
child 19475 8aa2b380614a
     1.1 --- a/src/Pure/General/seq.ML	Tue Sep 13 22:19:30 2005 +0200
     1.2 +++ b/src/Pure/General/seq.ML	Tue Sep 13 22:19:31 2005 +0200
     1.3 @@ -22,15 +22,19 @@
     1.4    val chop: int * 'a seq -> 'a list * 'a seq
     1.5    val list_of: 'a seq -> 'a list
     1.6    val of_list: 'a list -> 'a seq
     1.7 -  val map: ('a -> 'b) -> 'a seq -> 'b seq
     1.8 +  val append: 'a seq * 'a seq -> 'a seq
     1.9    val mapp: ('a -> 'b) -> 'a seq -> 'b seq -> 'b seq
    1.10 -  val append: 'a seq * 'a seq -> 'a seq
    1.11 +  val interleave: 'a seq * 'a seq -> 'a seq
    1.12    val filter: ('a -> bool) -> 'a seq -> 'a seq
    1.13    val flat: 'a seq seq -> 'a seq
    1.14 -  val interleave: 'a seq * 'a seq -> 'a seq
    1.15 +  val map: ('a -> 'b) -> 'a seq -> 'b seq
    1.16 +  val maps: ('a -> 'b seq) -> 'a seq -> 'b seq
    1.17 +  val lift: ('a -> 'b -> 'c) -> 'a seq -> 'b -> 'c seq
    1.18 +  val lifts: ('a -> 'b -> 'c seq) -> 'a seq -> 'b -> 'c seq
    1.19    val print: (int -> 'a -> unit) -> int -> 'a seq -> unit
    1.20    val it_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq
    1.21    val commute: 'a seq list -> 'a list seq
    1.22 +  val map_list: ('a -> 'b seq) -> 'a list -> 'b list seq
    1.23    val succeed: 'a -> 'a seq
    1.24    val fail: 'a -> 'b seq
    1.25    val THEN: ('a -> 'b seq) * ('b -> 'c seq) -> 'a -> 'c seq
    1.26 @@ -100,12 +104,15 @@
    1.27  fun of_list xs = foldr cons empty xs;
    1.28  
    1.29  
    1.30 -(*map the function f over the sequence, making a new sequence*)
    1.31 -fun map f xq =
    1.32 -  make (fn () =>
    1.33 -    (case pull xq of
    1.34 -      NONE => NONE
    1.35 -    | SOME (x, xq') => SOME (f x, map f xq')));
    1.36 +(*sequence append:  put the elements of xq in front of those of yq*)
    1.37 +fun append (xq, yq) =
    1.38 +  let
    1.39 +    fun copy s =
    1.40 +      make (fn () =>
    1.41 +        (case pull s of
    1.42 +          NONE => pull yq
    1.43 +        | SOME (x, s') => SOME (x, copy s')))
    1.44 +  in copy xq end;
    1.45  
    1.46  (*map over a sequence xq, append the sequence yq*)
    1.47  fun mapp f xq yq =
    1.48 @@ -117,15 +124,12 @@
    1.49          | SOME (x, s') => SOME (f x, copy s')))
    1.50    in copy xq end;
    1.51  
    1.52 -(*sequence append:  put the elements of xq in front of those of yq*)
    1.53 -fun append (xq, yq) =
    1.54 -  let
    1.55 -    fun copy s =
    1.56 -      make (fn () =>
    1.57 -        (case pull s of
    1.58 -          NONE => pull yq
    1.59 -        | SOME (x, s') => SOME (x, copy s')))
    1.60 -  in copy xq end;
    1.61 +(*interleave elements of xq with those of yq -- fairer than append*)
    1.62 +fun interleave (xq, yq) =
    1.63 +  make (fn () =>
    1.64 +    (case pull xq of
    1.65 +      NONE => pull yq
    1.66 +    | SOME (x, xq') => SOME (x, interleave (yq, xq'))));
    1.67  
    1.68  (*filter sequence by predicate*)
    1.69  fun filter pred xq =
    1.70 @@ -144,12 +148,17 @@
    1.71        NONE => NONE
    1.72      | SOME (xq, xqq') => pull (append (xq, flat xqq'))));
    1.73  
    1.74 -(*interleave elements of xq with those of yq -- fairer than append*)
    1.75 -fun interleave (xq, yq) =
    1.76 +(*map the function f over the sequence, making a new sequence*)
    1.77 +fun map f xq =
    1.78    make (fn () =>
    1.79      (case pull xq of
    1.80 -      NONE => pull yq
    1.81 -    | SOME (x, xq') => SOME (x, interleave (yq, xq'))));
    1.82 +      NONE => NONE
    1.83 +    | SOME (x, xq') => SOME (f x, map f xq')));
    1.84 +
    1.85 +fun maps f = flat o map f;
    1.86 +
    1.87 +fun lift f xq y = map (fn x => f x y) xq;
    1.88 +fun lifts f xq y = maps (fn x => f x y) xq;
    1.89  
    1.90  (*print a sequence, up to "count" elements*)
    1.91  fun print print_elem count =
    1.92 @@ -184,6 +193,8 @@
    1.93              | SOME (xs, xsq) =>
    1.94                  SOME (x :: xs, append (map (Library.cons x) xsq, commute (xq' :: xqs))))));
    1.95  
    1.96 +fun map_list f = commute o List.map f;
    1.97 +
    1.98  
    1.99  
   1.100  (** sequence functions **)      (*some code copied from Pure/tctical.ML*)