tuned interfaces;
authorwenzelm
Mon Jun 12 21:19:05 2006 +0200 (2006-06-12)
changeset 198658e1cee9e03dc
parent 19864 227a01b8db80
child 19866 d47f32a4964a
tuned interfaces;
src/Pure/General/seq.ML
     1.1 --- a/src/Pure/General/seq.ML	Mon Jun 12 21:19:04 2006 +0200
     1.2 +++ b/src/Pure/General/seq.ML	Mon Jun 12 21:19:05 2006 +0200
     1.3 @@ -19,10 +19,10 @@
     1.4    val try: ('a -> 'b) -> 'a -> 'b seq
     1.5    val hd: 'a seq -> 'a
     1.6    val tl: 'a seq -> 'a seq
     1.7 -  val chop: int * 'a seq -> 'a list * 'a seq
     1.8 +  val chop: int -> 'a seq -> 'a list * 'a seq
     1.9    val list_of: 'a seq -> 'a list
    1.10    val of_list: 'a list -> 'a seq
    1.11 -  val append: 'a seq * 'a seq -> 'a seq
    1.12 +  val append: 'a seq -> 'a seq -> 'a seq
    1.13    val mapp: ('a -> 'b) -> 'a seq -> 'b seq -> 'b seq
    1.14    val interleave: 'a seq * 'a seq -> 'a seq
    1.15    val filter: ('a -> bool) -> 'a seq -> 'a seq
    1.16 @@ -88,12 +88,12 @@
    1.17  
    1.18  (*the list of the first n elements, paired with rest of sequence;
    1.19    if length of list is less than n, then sequence had less than n elements*)
    1.20 -fun chop (n, xq) =
    1.21 +fun chop n xq =
    1.22    if n <= 0 then ([], xq)
    1.23    else
    1.24      (case pull xq of
    1.25        NONE => ([], xq)
    1.26 -    | SOME (x, xq') => apfst (Library.cons x) (chop (n - 1, xq')));
    1.27 +    | SOME (x, xq') => apfst (Library.cons x) (chop (n - 1) xq'));
    1.28  
    1.29  (*conversion from sequence to list*)
    1.30  fun list_of xq =
    1.31 @@ -106,7 +106,7 @@
    1.32  
    1.33  
    1.34  (*sequence append:  put the elements of xq in front of those of yq*)
    1.35 -fun append (xq, yq) =
    1.36 +fun append xq yq =
    1.37    let
    1.38      fun copy s =
    1.39        make (fn () =>
    1.40 @@ -147,7 +147,7 @@
    1.41    make (fn () =>
    1.42      (case pull xqq of
    1.43        NONE => NONE
    1.44 -    | SOME (xq, xqq') => pull (append (xq, flat xqq'))));
    1.45 +    | SOME (xq, xqq') => pull (append xq (flat xqq'))));
    1.46  
    1.47  (*map the function f over the sequence, making a new sequence*)
    1.48  fun map f xq =
    1.49 @@ -193,7 +193,7 @@
    1.50              (case pull (commute xqs) of
    1.51                NONE => NONE
    1.52              | SOME (xs, xsq) =>
    1.53 -                SOME (x :: xs, append (map (Library.cons x) xsq, commute (xq' :: xqs))))));
    1.54 +                SOME (x :: xs, append (map (Library.cons x) xsq) (commute (xq' :: xqs))))));
    1.55  
    1.56  fun map_list f = commute o List.map f;
    1.57  
    1.58 @@ -212,7 +212,7 @@
    1.59    | some => make (fn () => some));
    1.60  
    1.61  fun op APPEND (f, g) x =
    1.62 -  append (f x, make (fn () => pull (g x)));
    1.63 +  append (f x) (make (fn () => pull (g x)));
    1.64  
    1.65  fun EVERY fs = foldr THEN succeed fs;
    1.66  fun FIRST fs = foldr ORELSE fail fs;