git.iko.soy/Idris-dev
on ebbae35 help sign in
Idris-dev/test/basic015/basic015.idr
73 lines 1.9 kB history raw
1{-
2data Nat = Z | S Nat
4plus : Nat -> Nat -> Nat
5plus Z y = y
6plus (S x) y = S (plus x y)
7-}
9data Vect : Nat -> Type -> Type where
10 Nil : Vect Z a
11 (::) : a -> Vect k a -> Vect (S k) a
13%name Vect xs, ys, zs
15append : Vect n a -> Vect m a -> Vect (n + m) a
16append [] ys = ys
17append (x :: xs) ys = x :: append xs ys
20zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
21zipWith f [] ys = []
22zipWith f (x :: xs) (y :: ys) = f x y :: zipWith f xs ys
24create_empties : Vect m (Vect 0 elem)
25create_empties {m = Z} = []
26create_empties {m = (S k)} = [] :: create_empties
28transpose_helper : (row : Vect m elem) -> (rest_trans : Vect m (Vect k elem)) ->
29 Vect m (Vect (S k) elem)
30transpose_helper [] [] = []
31transpose_helper (rowval :: xs) (restrow :: ys) = (rowval :: restrow) :: transpose_helper xs ys
33transpose_vec : Vect n (Vect m elem) -> Vect m (Vect n elem)
34transpose_vec [] = create_empties
35transpose_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
47instance Functor (Vect m) where
48 map m [] = []
49 map m (x :: xs) = m x :: map m xs
51instance 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
58countTo : (m : Nat) -> Vect m Int
59countTo Z = []
60countTo (S k) = 0 :: map (+1) (countTo k)
62mkVect : (n, m : Nat) -> Vect n (Vect m Int)
63mkVect Z m = []
64mkVect (S k) m = countTo m :: map (map (+ cast m)) (mkVect k m)
66main : IO ()
67main = 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))