{-
data Nat = Z | S Nat
plus : Nat -> Nat -> Nat
plus Z y = y
plus (S x) y = S (plus x y)
-}
data Vect : Nat -> Type -> Type where
Nil : Vect Z a
(::) : a -> Vect k a -> Vect (S k) a
%name Vect xs, ys, zs
append : Vect n a -> Vect m a -> Vect (n + m) a
append [] ys = ys
append (x :: xs) ys = x :: append xs ys
zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
zipWith f [] ys = []
zipWith f (x :: xs) (y :: ys) = f x y :: zipWith f xs ys
create_empties : Vect m (Vect 0 elem)
create_empties {m = Z} = []
create_empties {m = (S k)} = [] :: create_empties
transpose_helper : (row : Vect m elem) -> (rest_trans : Vect m (Vect k elem)) ->
Vect m (Vect (S k) elem)
transpose_helper [] [] = []
transpose_helper (rowval :: xs) (restrow :: ys) = (rowval :: restrow) :: transpose_helper xs ys
transpose_vec : Vect n (Vect m elem) -> Vect m (Vect n elem)
transpose_vec [] = create_empties
transpose_vec (row :: rest) = let rest_trans = transpose_vec rest in
transpose_helper row rest_trans
------- A main program to read dimensions, generate and tranpose a vector
implementation Functor (Vect m) where
map m [] = []
map m (x :: xs) = m x :: map m xs
implementation Show a => Show (Vect m a) where
show x = show (toList x)
where
toList : Vect m a -> List a
toList [] = []
toList (y :: xs) = y :: toList xs
countTo : (m : Nat) -> Vect m Int
countTo Z = []
countTo (S k) = 0 :: map (+1) (countTo k)
mkVect : (n, m : Nat) -> Vect n (Vect m Int)
mkVect Z m = []
mkVect (S k) m = countTo m :: map (map (+ cast m)) (mkVect k m)
main : IO ()
main = do putStr "Rows: "
let r : Nat = 5
putStr "Columns: "
let c : Nat = 6
printLn (mkVect r c)
putStrLn "Transposed:"
printLn (transpose_vec (mkVect r c))