added map_transpose
authorhaftmann
Mon Aug 10 12:24:47 2009 +0200 (2009-08-10)
changeset 323524839a704939a
parent 32351 96f9e6402403
child 32353 0ac26087464b
added map_transpose
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Mon Aug 10 10:25:00 2009 +0200
     1.2 +++ b/src/Pure/library.ML	Mon Aug 10 12:24:47 2009 +0200
     1.3 @@ -109,6 +109,7 @@
     1.4    val split_list: ('a * 'b) list -> 'a list * 'b list
     1.5    val map_product: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
     1.6    val fold_product: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
     1.7 +  val map_transpose: ('a list -> 'b) -> 'a list list -> 'b list
     1.8    val separate: 'a -> 'a list -> 'a list
     1.9    val surround: 'a -> 'a list -> 'a list
    1.10    val replicate: int -> 'a -> 'a list
    1.11 @@ -929,6 +930,17 @@
    1.12    in dups end;
    1.13  
    1.14  
    1.15 +(* matrices *)
    1.16 +
    1.17 +fun map_transpose f xss =
    1.18 +  let
    1.19 +    val n = case distinct (op =) (map length xss)
    1.20 +     of [] => 0
    1.21 +      | [n] => n
    1.22 +      | _ => raise UnequalLengths;
    1.23 +  in map (fn m => f (map (fn xs => nth xs m) xss)) (0 upto n - 1) end;
    1.24 +
    1.25 +
    1.26  
    1.27  (** lists as multisets **)
    1.28