removed splitAt (superceded by chop);
authorwenzelm
Wed Apr 26 22:38:11 2006 +0200 (2006-04-26)
changeset 1947470223ad97843
parent 19473 d87a8838afa4
child 19475 8aa2b380614a
removed splitAt (superceded by chop);
removed if_none (superceded by the_default);
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Wed Apr 26 22:38:05 2006 +0200
     1.2 +++ b/src/Pure/library.ML	Wed Apr 26 22:38:11 2006 +0200
     1.3 @@ -48,7 +48,6 @@
     1.4    val these: 'a list option -> 'a list
     1.5    val the_default: 'a -> 'a option -> 'a
     1.6    val the_list: 'a option -> 'a list
     1.7 -  val if_none: 'a option -> 'a -> 'a
     1.8    val is_some: 'a option -> bool
     1.9    val is_none: 'a option -> bool
    1.10    val perhaps: ('a -> 'a option) -> 'a -> 'a
    1.11 @@ -116,11 +115,11 @@
    1.12    val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
    1.13    val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
    1.14    val flat: 'a list list -> 'a list
    1.15 +  val maps: ('a -> 'b list) -> 'a list -> 'b list
    1.16    val unflat: 'a list list -> 'b list -> 'b list list
    1.17    val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list
    1.18    val fold_burrow: ('a list -> 'c -> 'b list * 'd) -> 'a list list -> 'c -> 'b list list * 'd
    1.19    val chop: int -> 'a list -> 'a list * 'a list
    1.20 -  val splitAt: int * 'a list -> 'a list * 'a list
    1.21    val dropwhile: ('a -> bool) -> 'a list -> 'a list
    1.22    val nth: 'a list -> int -> 'a
    1.23    val nth_update: int * 'a -> 'a list -> 'a list
    1.24 @@ -352,10 +351,6 @@
    1.25  fun the_list (SOME x) = [x]
    1.26    | the_list _ = []
    1.27  
    1.28 -(*strict!*)
    1.29 -fun if_none NONE y = y
    1.30 -  | if_none (SOME x) _ = x;
    1.31 -
    1.32  fun is_some (SOME _) = true
    1.33    | is_some NONE = false;
    1.34  
    1.35 @@ -372,6 +367,7 @@
    1.36    | merge_opt _ (x, NONE) = x
    1.37    | merge_opt eq (SOME x, SOME y) = if eq (x, y) then SOME y else raise Option;
    1.38  
    1.39 +
    1.40  (* exceptions *)
    1.41  
    1.42  val do_transform_failure = ref true;
    1.43 @@ -587,8 +583,6 @@
    1.44    | chop _ [] = ([], [])
    1.45    | chop n (x :: xs) = chop (n - 1) xs |>> cons x;
    1.46  
    1.47 -fun splitAt (n, xs) = chop n xs;
    1.48 -
    1.49  (*take the first n elements from a list*)
    1.50  fun take (n, []) = []
    1.51    | take (n, x :: xs) =
    1.52 @@ -610,9 +604,9 @@
    1.53  
    1.54  (*update nth element*)
    1.55  fun nth_update (n, x) xs =
    1.56 -    (case splitAt (n, xs) of
    1.57 -      (_, []) => raise Subscript
    1.58 -    | (prfx, _ :: sffx') => prfx @ (x :: sffx'))
    1.59 +  (case chop n xs of
    1.60 +    (_, []) => raise Subscript
    1.61 +  | (prfx, _ :: sffx') => prfx @ (x :: sffx'));
    1.62  
    1.63  fun nth_map 0 f (x :: xs) = f x :: xs
    1.64    | nth_map n f (x :: xs) = x :: nth_map (n - 1) f xs
    1.65 @@ -666,6 +660,8 @@
    1.66  
    1.67  val flat = List.concat;
    1.68  
    1.69 +fun maps f = flat o map f;
    1.70 +
    1.71  fun unflat (xs :: xss) ys =
    1.72        let val (ps, qs) = chop (length xs) ys
    1.73        in ps :: unflat xss qs end
    1.74 @@ -1095,7 +1091,7 @@
    1.75  fun fold_bal f [x] = x
    1.76    | fold_bal f [] = raise Balance
    1.77    | fold_bal f xs =
    1.78 -      let val (ps,qs) = splitAt(length xs div 2, xs)
    1.79 +      let val (ps, qs) = chop (length xs div 2) xs
    1.80        in  f (fold_bal f ps, fold_bal f qs)  end;
    1.81  
    1.82  (*construct something of the form f(...g(...(x)...)) for balanced access*)