# HG changeset patch # User wenzelm # Date 1146083891 -7200 # Node ID 70223ad978430f5522badcc3ad5fa8e5d85a4834 # Parent d87a8838afa4117372f1b12f286f44b3536bc892 removed splitAt (superceded by chop); removed if_none (superceded by the_default); diff -r d87a8838afa4 -r 70223ad97843 src/Pure/library.ML --- a/src/Pure/library.ML Wed Apr 26 22:38:05 2006 +0200 +++ b/src/Pure/library.ML Wed Apr 26 22:38:11 2006 +0200 @@ -48,7 +48,6 @@ val these: 'a list option -> 'a list val the_default: 'a -> 'a option -> 'a val the_list: 'a option -> 'a list - val if_none: 'a option -> 'a -> 'a val is_some: 'a option -> bool val is_none: 'a option -> bool val perhaps: ('a -> 'a option) -> 'a -> 'a @@ -116,11 +115,11 @@ val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list val flat: 'a list list -> 'a list + val maps: ('a -> 'b list) -> 'a list -> 'b list val unflat: 'a list list -> 'b list -> 'b list list val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list val fold_burrow: ('a list -> 'c -> 'b list * 'd) -> 'a list list -> 'c -> 'b list list * 'd val chop: int -> 'a list -> 'a list * 'a list - val splitAt: int * 'a list -> 'a list * 'a list val dropwhile: ('a -> bool) -> 'a list -> 'a list val nth: 'a list -> int -> 'a val nth_update: int * 'a -> 'a list -> 'a list @@ -352,10 +351,6 @@ fun the_list (SOME x) = [x] | the_list _ = [] -(*strict!*) -fun if_none NONE y = y - | if_none (SOME x) _ = x; - fun is_some (SOME _) = true | is_some NONE = false; @@ -372,6 +367,7 @@ | merge_opt _ (x, NONE) = x | merge_opt eq (SOME x, SOME y) = if eq (x, y) then SOME y else raise Option; + (* exceptions *) val do_transform_failure = ref true; @@ -587,8 +583,6 @@ | chop _ [] = ([], []) | chop n (x :: xs) = chop (n - 1) xs |>> cons x; -fun splitAt (n, xs) = chop n xs; - (*take the first n elements from a list*) fun take (n, []) = [] | take (n, x :: xs) = @@ -610,9 +604,9 @@ (*update nth element*) fun nth_update (n, x) xs = - (case splitAt (n, xs) of - (_, []) => raise Subscript - | (prfx, _ :: sffx') => prfx @ (x :: sffx')) + (case chop n xs of + (_, []) => raise Subscript + | (prfx, _ :: sffx') => prfx @ (x :: sffx')); fun nth_map 0 f (x :: xs) = f x :: xs | nth_map n f (x :: xs) = x :: nth_map (n - 1) f xs @@ -666,6 +660,8 @@ val flat = List.concat; +fun maps f = flat o map f; + fun unflat (xs :: xss) ys = let val (ps, qs) = chop (length xs) ys in ps :: unflat xss qs end @@ -1095,7 +1091,7 @@ fun fold_bal f [x] = x | fold_bal f [] = raise Balance | fold_bal f xs = - let val (ps,qs) = splitAt(length xs div 2, xs) + let val (ps, qs) = chop (length xs div 2) xs in f (fold_bal f ps, fold_bal f qs) end; (*construct something of the form f(...g(...(x)...)) for balanced access*)