src/Pure/library.ML
changeset 18514 0cec730b3942
parent 18461 9125d278fdc8
child 18549 5308a6ea3b96
     1.1 --- a/src/Pure/library.ML	Fri Dec 23 20:02:30 2005 +0100
     1.2 +++ b/src/Pure/library.ML	Tue Dec 27 15:24:23 2005 +0100
     1.3 @@ -98,7 +98,6 @@
     1.4    val fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
     1.5    val fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
     1.6    val fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
     1.7 -  val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b
     1.8    val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
     1.9    val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
    1.10    val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list
    1.11 @@ -109,6 +108,8 @@
    1.12    val nth_update: int * 'a -> 'a list -> 'a list
    1.13    val nth_map: int -> ('a -> 'a) -> 'a list -> 'a list
    1.14    val nth_list: 'a list list -> int -> 'a list
    1.15 +  val map_index: (int * 'a -> 'b) -> 'a list -> 'b list
    1.16 +  val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b
    1.17    val split_last: 'a list -> 'a list * 'a
    1.18    val find_index: ('a -> bool) -> 'a list -> int
    1.19    val find_index_eq: ''a -> ''a list -> int
    1.20 @@ -510,7 +511,7 @@
    1.21  
    1.22  fun fold_index f =
    1.23    let
    1.24 -    fun fold_aux _  [] y = y
    1.25 +    fun fold_aux _ [] y = y
    1.26        | fold_aux i (x :: xs) y = fold_aux (i+1) xs (f (i, x) y);
    1.27    in fold_aux 0 end;
    1.28  
    1.29 @@ -561,6 +562,12 @@
    1.30    | nth_map n f (x :: xs) = x :: nth_map (n - 1) f xs
    1.31    | nth_map _ _ [] = raise Subscript;
    1.32  
    1.33 +fun map_index f =
    1.34 +  let
    1.35 +    fun mapp _ [] = []
    1.36 +      | mapp i (x :: xs) = f (i, x) :: mapp (i+1) xs
    1.37 +  in mapp 0 end;
    1.38 +
    1.39  val last_elem = List.last;
    1.40  
    1.41  (*rear decomposition*)