read chapter 3

chapter3/PatternMatching.idr

@@ -13,3 +13,33 @@ invert False = True
 describeList : Show a => List a -> String
 describeList [] = "Empty"
 describeList (x :: xs) = "Non-empty (" ++ show x ++ "), tail = " ++ show xs
+
+showList : Show a => List a -> String
+showList [] = "[]"
+showList (x :: xs) = "[" ++ show x ++ showListInner xs
+  where
+    showListInner : Show a => List a -> String
+    showListInner [] = "]"
+    showListInner (x :: xs) = ", " ++ show x ++ showListInner xs
+
+allLengthsNoMap : List String -> List Nat
+allLengthsNoMap [] = []
+allLengthsNoMap (word :: words) = length word :: allLengthsNoMap words
+
+xor : Bool -> Bool -> Bool
+xor False y = y
+xor True y = not y
+
+isEven2 : Nat -> Bool
+isEven2 Z = True
+isEven2 (S k) = not (isEven2 k)
+
+mutual
+  isEven : Nat -> Bool
+  isEven Z = True
+  isEven (S k) = isOdd k
+  isOdd : Nat -> Bool
+  isOdd Z = False
+  isOdd (S k) = isEven k
+
+  

chapter3/Vectors.idr

@@ -0,0 +1,54 @@
+module Vectors
+
+import Data.Vect
+
+fourInts : Vect 4 Int
+fourInts = [0, 1, 2, 3]
+
+sixInts : Vect 6 Int
+sixInts = [1, 2, 3, 4, 5, 6]
+
+tenInts : Vect 10 Int
+tenInts = fourInts ++ sixInts
+
+nInts : (n : Nat) -> Vect n Int
+nInts Z = []
+nInts (S k) = 1 :: nInts k
+
+-- Word length
+
+
+allLengths : Vect len String -> Vect len Nat
+allLengths [] = []
+allLengths (word :: words) = length word :: allLengths words
+
+insert : Ord elem => (x : elem) -> (xsSorted : Vect len elem) -> Vect (S len) elem
+insert x [] = [x]
+insert x (y :: xs) = case x < y of
+                          False => y :: insert x xs
+                          True => x :: y :: xs
+
+-- insertion sort
+insSort :Ord elem => Vect n elem -> Vect n elem
+insSort [] = []
+insSort (x :: xs) = let xsSorted = insSort xs in
+                        insert x xsSorted
+
+
+-- Exercises
+my_length : List a -> Nat
+my_length [] = 0
+my_length (_ :: xs) = S (my_length xs)
+
+my_reverse : List a -> List a
+my_reverse [] = []
+my_reverse (x :: xs) = (my_reverse xs) ++ [x]
+
+
+my_map : (a -> b) -> List a -> List b
+my_map _ [] = []
+my_map f (x :: xs) = (f x) :: my_map f xs
+
+my_vect_map : (a -> b) -> Vect n a -> Vect n b
+my_vect_map _ [] = []
+my_vect_map f (x :: xs) = (f x) :: my_vect_map f xs