d30a1ea · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Add Prelude.Vect.transpose

d30a1eaMelvar Chen12 years ago

libs/prelude/Prelude/Vect.idr+6

@@ -451,6 +451,12 @@ range : Vect n (Fin n)

451range {n=Z} = []

452range {n=S _} = fZ :: map fS range

453

454+||| Transpose a Vect of Vects, turning rows into columns and vice versa.

455+|||

456+||| As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`.

457+transpose : Vect m (Vect n a) -> Vect n (Vect m a)

458+transpose [] = replicate _ []

459+transpose (x :: xs) = zipWith (::) x (transpose xs)

454

460

455--------------------------------------------------------------------------------

461--------------------------------------------------------------------------------

456-- Properties

462-- Properties

test/reg014/reg014.idr+6−6

@@ -3,10 +3,10 @@ module reg014

3Matrix : Type -> Nat -> Nat -> Type

4Matrix a n m = Vect n (Vect m a)

6−transpose : Matrix a (S n) (S m) -> Matrix a (S m) (S n)

6+mytranspose : Matrix a (S n) (S m) -> Matrix a (S m) (S n)

7−transpose ((x:: []) :: []) = [[x]]

7+mytranspose ((x:: []) :: []) = [[x]]

8−transpose [x :: y :: xs] = [x] :: (transpose [y :: xs])

8+mytranspose [x :: y :: xs] = [x] :: (mytranspose [y :: xs])

9−transpose (x :: y :: xs)

9+mytranspose (x :: y :: xs)

10− = let tx = transpose [x] in

10+ = let tx = mytranspose [x] in

11− let ux = transpose (y :: xs) in zipWith (++) tx ux

11+ let ux = mytranspose (y :: xs) in zipWith (++) tx ux