# HG changeset patch # User wenzelm # Date 1150139945 -7200 # Node ID 8e1cee9e03dc337cc9b97500f1f32148569b3d4c # Parent 227a01b8db8090efbfb584b37c07660848284c38 tuned interfaces; diff -r 227a01b8db80 -r 8e1cee9e03dc src/Pure/General/seq.ML --- a/src/Pure/General/seq.ML Mon Jun 12 21:19:04 2006 +0200 +++ b/src/Pure/General/seq.ML Mon Jun 12 21:19:05 2006 +0200 @@ -19,10 +19,10 @@ val try: ('a -> 'b) -> 'a -> 'b seq val hd: 'a seq -> 'a val tl: 'a seq -> 'a seq - val chop: int * 'a seq -> 'a list * 'a seq + val chop: int -> 'a seq -> 'a list * 'a seq val list_of: 'a seq -> 'a list val of_list: 'a list -> 'a seq - val append: 'a seq * 'a seq -> 'a seq + val append: 'a seq -> 'a seq -> 'a seq val mapp: ('a -> 'b) -> 'a seq -> 'b seq -> 'b seq val interleave: 'a seq * 'a seq -> 'a seq val filter: ('a -> bool) -> 'a seq -> 'a seq @@ -88,12 +88,12 @@ (*the list of the first n elements, paired with rest of sequence; if length of list is less than n, then sequence had less than n elements*) -fun chop (n, xq) = +fun chop n xq = if n <= 0 then ([], xq) else (case pull xq of NONE => ([], xq) - | SOME (x, xq') => apfst (Library.cons x) (chop (n - 1, xq'))); + | SOME (x, xq') => apfst (Library.cons x) (chop (n - 1) xq')); (*conversion from sequence to list*) fun list_of xq = @@ -106,7 +106,7 @@ (*sequence append: put the elements of xq in front of those of yq*) -fun append (xq, yq) = +fun append xq yq = let fun copy s = make (fn () => @@ -147,7 +147,7 @@ make (fn () => (case pull xqq of NONE => NONE - | SOME (xq, xqq') => pull (append (xq, flat xqq')))); + | SOME (xq, xqq') => pull (append xq (flat xqq')))); (*map the function f over the sequence, making a new sequence*) fun map f xq = @@ -193,7 +193,7 @@ (case pull (commute xqs) of NONE => NONE | SOME (xs, xsq) => - SOME (x :: xs, append (map (Library.cons x) xsq, commute (xq' :: xqs)))))); + SOME (x :: xs, append (map (Library.cons x) xsq) (commute (xq' :: xqs)))))); fun map_list f = commute o List.map f; @@ -212,7 +212,7 @@ | some => make (fn () => some)); fun op APPEND (f, g) x = - append (f x, make (fn () => pull (g x))); + append (f x) (make (fn () => pull (g x))); fun EVERY fs = foldr THEN succeed fs; fun FIRST fs = foldr ORELSE fail fs;