@@ -0,0 +1,73 @@
1+{-
2+data Nat = Z | S Nat
3+
4+plus : Nat -> Nat -> Nat
5+plus Z y = y
6+plus (S x) y = S (plus x y)
7+-}
8+
9+data Vect : Nat -> Type -> Type where
10+ Nil : Vect Z a
11+ (::) : a -> Vect k a -> Vect (S k) a
12+
13+%name Vect xs, ys, zs
14+
15+append : Vect n a -> Vect m a -> Vect (n + m) a
16+append [] ys = ys
17+append (x :: xs) ys = x :: append xs ys
18+
19+
20+zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
21+zipWith f [] ys = []
22+zipWith f (x :: xs) (y :: ys) = f x y :: zipWith f xs ys
23+
24+create_empties : Vect m (Vect 0 elem)
25+create_empties {m = Z} = []
26+create_empties {m = (S k)} = [] :: create_empties
27+
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
32+
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
37+
38+
39+
40+
41+
42+
43+
44+
45+------- A main program to read dimensions, generate and tranpose a vector
46+
47+instance Functor (Vect m) where
48+ map m [] = []
49+ map m (x :: xs) = m x :: map m xs
50+
51+instance Show a => Show (Vect m a) where
52+ show x = show (toList x)
53+ where
54+ toList : Vect m a -> List a
55+ toList [] = []
56+ toList (y :: xs) = y :: toList xs
57+
58+countTo : (m : Nat) -> Vect m Int
59+countTo Z = []
60+countTo (S k) = 0 :: map (+1) (countTo k)
61+
62+mkVect : (n, m : Nat) -> Vect n (Vect m Int)
63+mkVect Z m = []
64+mkVect (S k) m = countTo m :: map (map (+ cast m)) (mkVect k m)
65+
66+main : IO ()
67+main = do putStr "Rows: "
68+ let r : Nat = 5
69+ putStr "Columns: "
70+ let c : Nat = 6
71+ printLn (mkVect r c)
72+ putStrLn "Transposed:"
73+ printLn (transpose_vec (mkVect r c))