diff --git a/chapter3/PatternMatching.idr b/chapter3/PatternMatching.idr index 11fe257..7dbeaaa 100644 --- a/chapter3/PatternMatching.idr +++ b/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 + + diff --git a/chapter3/Vectors.idr b/chapter3/Vectors.idr new file mode 100644 index 0000000..2290fc8 --- /dev/null +++ b/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