@@ -0,0 +1,73 @@
4+plus : Nat -> Nat -> Nat
6+plus (S x) y = S (plus x y)
9+data Vect : Nat -> Type -> Type where
11+ (::) : a -> Vect k a -> Vect (S k) a
15+append : Vect n a -> Vect m a -> Vect (n + m) a
17+append (x :: xs) ys = x :: append xs ys
20+zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
22+zipWith f (x :: xs) (y :: ys) = f x y :: zipWith f xs ys
24+create_empties : Vect m (Vect 0 elem)
25+create_empties {m = Z} = []
26+create_empties {m = (S k)} = [] :: create_empties
28+transpose_helper : (row : Vect m elem) -> (rest_trans : Vect m (Vect k elem)) ->
29+ Vect m (Vect (S k) elem)
30+transpose_helper [] [] = []
31+transpose_helper (rowval :: xs) (restrow :: ys) = (rowval :: restrow) :: transpose_helper xs ys
33+transpose_vec : Vect n (Vect m elem) -> Vect m (Vect n elem)
34+transpose_vec [] = create_empties
35+transpose_vec (row :: rest) = let rest_trans = transpose_vec rest in
36+ transpose_helper row rest_trans
45+------- A main program to read dimensions, generate and tranpose a vector
47+instance Functor (Vect m) where
49+ map m (x :: xs) = m x :: map m xs
51+instance Show a => Show (Vect m a) where
52+ show x = show (toList x)
54+ toList : Vect m a -> List a
56+ toList (y :: xs) = y :: toList xs
58+countTo : (m : Nat) -> Vect m Int
60+countTo (S k) = 0 :: map (+1) (countTo k)
62+mkVect : (n, m : Nat) -> Vect n (Vect m Int)
64+mkVect (S k) m = countTo m :: map (map (+ cast m)) (mkVect k m)
67+main = do putStr "Rows: "
72+ putStrLn "Transposed:"
73+ printLn (transpose_vec (mkVect r c))