# HG changeset patch # User haftmann # Date 1135693463 -3600 # Node ID 0cec730b39426a0194ce56e30e7518b86f61bef8 # Parent 791b53bf40736e43f4d79c1d316c0bd024b7a79c added map_index diff -r 791b53bf4073 -r 0cec730b3942 src/Pure/library.ML --- a/src/Pure/library.ML Fri Dec 23 20:02:30 2005 +0100 +++ b/src/Pure/library.ML Tue Dec 27 15:24:23 2005 +0100 @@ -98,7 +98,6 @@ val fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b val fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b val fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b - val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list @@ -109,6 +108,8 @@ val nth_update: int * 'a -> 'a list -> 'a list val nth_map: int -> ('a -> 'a) -> 'a list -> 'a list val nth_list: 'a list list -> int -> 'a list + val map_index: (int * 'a -> 'b) -> 'a list -> 'b list + val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b val split_last: 'a list -> 'a list * 'a val find_index: ('a -> bool) -> 'a list -> int val find_index_eq: ''a -> ''a list -> int @@ -510,7 +511,7 @@ fun fold_index f = let - fun fold_aux _ [] y = y + fun fold_aux _ [] y = y | fold_aux i (x :: xs) y = fold_aux (i+1) xs (f (i, x) y); in fold_aux 0 end; @@ -561,6 +562,12 @@ | nth_map n f (x :: xs) = x :: nth_map (n - 1) f xs | nth_map _ _ [] = raise Subscript; +fun map_index f = + let + fun mapp _ [] = [] + | mapp i (x :: xs) = f (i, x) :: mapp (i+1) xs + in mapp 0 end; + val last_elem = List.last; (*rear decomposition*)