d30a1ea · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add Prelude.Vect.transpose

Test adjusted due to name clash.

commitd30a1eaa3f89fd14fcda08713831f8255d883831 authorMelvar Chen <Melvar.Chen@googlemail.com> dateFri 30 May 2014, 16:44 (12 years ago) parent8e2f681

2 files changed+12−6

unifiedsplit

libs/prelude/Prelude/Vect.idr+6

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

451451range {n=Z} = []

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

453453

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)

454460

455461--------------------------------------------------------------------------------

456462-- Properties

test/reg014/reg014.idr+6−6

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

33Matrix : Type -> Nat -> Nat -> Type

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

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

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

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

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

10− = let tx = transpose [x] in

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

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

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

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

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

10+ = let tx = mytranspose [x] in

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

1212