Add Chapter 8 tests

tests/Main.idr

@@ -48,7 +48,7 @@ idrisTests
 typeddTests : List String
 typeddTests
    = ["chapter01", "chapter02", "chapter03", "chapter04", "chapter05",
-      "chapter06", "chapter07"]
+      "chapter06", "chapter07", "chapter08"]
 
 chezTests : List String
 chezTests

tests/typedd-book/chapter08/AppendVec.idr

@@ -0,0 +1,12 @@
+import Data.Nat
+import Data.Vect
+
+append_nil : Vect m elem -> Vect (plus m 0) elem
+append_nil {m} xs = rewrite plusZeroRightNeutral m in xs
+
+append_xs : Vect (S (m + k)) elem -> Vect (plus m (S k)) elem
+append_xs {m} {k} xs = rewrite sym (plusSuccRightSucc m k) in xs
+
+append : Vect n elem -> Vect m elem -> Vect (m + n) elem
+append [] ys = append_nil ys
+append (x :: xs) ys = append_xs (x :: append xs ys)

tests/typedd-book/chapter08/CheckEqDec.idr

@@ -0,0 +1,17 @@
+
+zeroNotSuc : (0 = S k) -> Void
+zeroNotSuc Refl impossible
+
+sucNotZero : (S k = 0) -> Void
+sucNotZero Refl impossible
+
+noRec : (contra : (k = j) -> Void) -> (S k = S j) -> Void
+noRec contra Refl = contra Refl
+
+checkEqNat : (num1 : Nat) -> (num2 : Nat) -> Dec (num1 = num2)
+checkEqNat Z Z = Yes Refl
+checkEqNat Z (S k) = No zeroNotSuc
+checkEqNat (S k) Z = No sucNotZero
+checkEqNat (S k) (S j) = case checkEqNat k j of
+                              Yes prf => Yes (cong S prf)
+                              No contra => No (noRec contra)

tests/typedd-book/chapter08/CheckEqMaybe.idr

@@ -0,0 +1,7 @@
+checkEqNat : (num1 : Nat) -> (num2 : Nat) -> Maybe (num1 = num2)
+checkEqNat Z Z = Just Refl
+checkEqNat Z (S k) = Nothing
+checkEqNat (S k) Z = Nothing
+checkEqNat (S k) (S j) = case checkEqNat k j of
+                              Nothing => Nothing
+                              Just prf => Just (cong S prf)

tests/typedd-book/chapter08/EqNat.idr

@@ -0,0 +1,15 @@
+data EqNat : Nat -> Nat -> Type where
+     Same : (x : Nat) -> EqNat x x
+
+sameS : (k : Nat) -> (j : Nat) -> (eq : EqNat k j) -> EqNat (S k) (S j)
+sameS k k (Same k) = Same (S k)
+
+checkEqNat : (num1 : Nat) -> (num2 : Nat) -> Maybe (EqNat num1 num2)
+checkEqNat Z Z = Just (Same Z)
+checkEqNat Z (S k) = Nothing
+checkEqNat (S k) Z = Nothing
+checkEqNat (S k) (S j) = case checkEqNat k j of
+                              Nothing => Nothing
+                              Just eq => Just (sameS _ _ eq)
+
+

tests/typedd-book/chapter08/ExactLength.idr

@@ -0,0 +1,25 @@
+data Vect : Nat -> Type -> Type where
+     Nil  : Vect Z a
+     (::) : a -> Vect k a -> Vect (S k) a
+
+%name Vect xs, ys, zs
+
+data EqNat : Nat -> Nat -> Type where
+     Same : (x : Nat) -> EqNat x x
+
+sameS : (k : Nat) -> (j : Nat) -> (eq : EqNat k j) -> EqNat (S k) (S j)
+sameS k k (Same k) = Same (S k)
+
+checkEqNat : (num1 : Nat) -> (num2 : Nat) -> Maybe (EqNat num1 num2)
+checkEqNat Z Z = Just (Same Z)
+checkEqNat Z (S k) = Nothing
+checkEqNat (S k) Z = Nothing
+checkEqNat (S k) (S j) = case checkEqNat k j of
+                              Nothing => Nothing
+                              Just eq => Just (sameS _ _ eq)
+
+exactLength : {m : _} -> 
+              (len : Nat) -> (input : Vect m a) -> Maybe (Vect len a)
+exactLength {m} len input = case checkEqNat m len of
+                                 Nothing => Nothing
+                                 Just (Same len) => Just input

tests/typedd-book/chapter08/ExactLengthDec.idr

@@ -0,0 +1,13 @@
+import Decidable.Equality
+
+data Vect : Nat -> Type -> Type where
+     Nil  : Vect Z a
+     (::) : a -> Vect k a -> Vect (S k) a
+
+%name Vect xs, ys, zs
+
+exactLength : {m : _} ->
+              (len : Nat) -> (input : Vect m a) -> Maybe (Vect len a)
+exactLength {m} len input = case decEq m len of
+                                 Yes Refl => Just input
+                                 No contra => Nothing

tests/typedd-book/chapter08/ReverseVec.idr

@@ -0,0 +1,15 @@
+import Data.Nat
+import Data.Vect
+
+myReverse1 : Vect n a -> Vect n a
+myReverse1 [] = []
+myReverse1 {n = S k} (x :: xs)
+        = let result = myReverse1 xs ++ [x] in
+              rewrite plusCommutative 1 k in result
+
+myReverse : Vect n a -> Vect n a
+myReverse [] = []
+myReverse (x :: xs) = reverseProof (myReverse xs ++ [x])
+  where
+    reverseProof : Vect (k + 1) a -> Vect (S k) a
+    reverseProof {k} result = rewrite plusCommutative 1 k in result

tests/typedd-book/chapter08/TCVects.idr

@@ -0,0 +1,7 @@
+import Data.Vect
+
+test1 : Vect 4 Int
+test1 = [1, 2, 3, 4]
+
+test2: Vect (2 + 2) Int
+test2 = ?test2_rhs

tests/typedd-book/chapter08/Void.idr

@@ -0,0 +1,14 @@
+twoPlusTwoNotFive : 2 + 2 = 5 -> Void
+twoPlusTwoNotFive Refl impossible
+
+valueNotSuc : (x : Nat) -> x = S x -> Void
+valueNotSuc _ Refl impossible
+
+loop : Void
+loop = loop
+
+nohead : Void
+nohead = getHead []
+  where
+    getHead : List Void -> Void
+    getHead (x :: xs) = x

tests/typedd-book/chapter08/expected

@@ -0,0 +1,9 @@
+1/1: Building AppendVec (AppendVec.idr)
+1/1: Building CheckEqDec (CheckEqDec.idr)
+1/1: Building CheckEqMaybe (CheckEqMaybe.idr)
+1/1: Building EqNat (EqNat.idr)
+1/1: Building ExactLength (ExactLength.idr)
+1/1: Building ExactLengthDec (ExactLengthDec.idr)
+1/1: Building ReverseVec (ReverseVec.idr)
+1/1: Building TCVects (TCVects.idr)
+1/1: Building Void (Void.idr)

tests/typedd-book/chapter08/run

@@ -0,0 +1,11 @@
+$1 AppendVec.idr --check
+$1 CheckEqDec.idr --check
+$1 CheckEqMaybe.idr --check
+$1 EqNat.idr --check
+$1 ExactLength.idr --check
+$1 ExactLengthDec.idr --check
+$1 ReverseVec.idr --check
+$1 TCVects.idr --check
+$1 Void.idr --check
+
+rm -rf build