--- a/src/Pure/library.ML Fri May 31 07:55:40 2013 +0200
+++ b/src/Pure/library.ML Fri May 31 09:30:32 2013 +0200
@@ -82,6 +82,7 @@
val map_index: (int * 'a -> 'b) -> 'a list -> 'b list
val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b
val map_range: (int -> 'a) -> int -> 'a list
+ val fold_range: (int -> 'a -> 'a) -> int -> 'a -> 'a
val split_last: 'a list -> 'a list * 'a
val find_first: ('a -> bool) -> 'a list -> 'a option
val find_index: ('a -> bool) -> 'a list -> int
@@ -430,21 +431,28 @@
fun map_index f =
let
- fun mapp (_: int) [] = []
- | mapp i (x :: xs) = f (i, x) :: mapp (i + 1) xs
- in mapp 0 end;
+ fun map_aux (_: int) [] = []
+ | map_aux i (x :: xs) = f (i, x) :: map_aux (i + 1) xs
+ in map_aux 0 end;
fun fold_index f =
let
fun fold_aux (_: int) [] y = y
- | fold_aux i (x :: xs) y = fold_aux (i + 1) xs (f (i, x) y);
+ | fold_aux i (x :: xs) y = fold_aux (i + 1) xs (f (i, x) y)
in fold_aux 0 end;
fun map_range f i =
let
- fun mapp (k: int) =
- if k < i then f k :: mapp (k + 1) else [];
- in mapp 0 end;
+ fun map_aux (k: int) =
+ if k < i then f k :: map_aux (k + 1) else []
+ in map_aux 0 end;
+
+fun fold_range f i =
+ let
+ fun fold_aux (k: int) y =
+ if k < i then fold_aux (k + 1) (f k y) else y
+ in fold_aux 0 end;
+
(*rear decomposition*)
fun split_last [] = raise List.Empty