Add first batch of totality checking tests

tests/Main.idr

@@ -32,7 +32,8 @@ idrisTests
        "interface005",
        "import001", "import002",
        "lazy001",
-       "record001", "record002"]
+       "record001", "record002",
+       "total001", "total002", "total003"]
 
 chdir : String -> IO Bool
 chdir dir 

tests/idris2/total001/Total.idr

@@ -0,0 +1,17 @@
+data Vect : Nat -> Type -> Type where
+     Nil : Vect Z a
+     (::) : a -> Vect k a -> Vect (S k) a
+
+data Fin : Nat -> Type where
+     FZ : Fin (S k)
+     FS : Fin k -> Fin (S k)
+
+lookup : Fin n -> Vect n a -> a
+lookup FZ (x :: xs) = x
+lookup (FS k) (x :: xs) = lookup k xs
+
+lookup' : Fin n -> Vect n a -> a
+lookup' (FS k) (x :: xs) = lookup' k xs
+
+lookup'' : Fin n -> Vect n a -> a
+lookup'' n xs = lookup' n xs

tests/idris2/total001/expected

@@ -0,0 +1,7 @@
+1/1: Building Total (Total.idr)
+Welcome to Idris 2 version 0.0. Enjoy yourself!
+Main> Main.lookup: All cases covered
+Main> Main.lookup':
+lookup' FZ _
+Main> Main.lookup'': Calls non covering function Main.lookup'
+Main> Bye for now!

tests/idris2/total001/input

@@ -0,0 +1,4 @@
+:missing lookup
+:missing lookup'
+:missing lookup''
+:q

tests/idris2/total001/run

@@ -0,0 +1,3 @@
+$1 Total.idr < input
+
+rm -rf build

tests/idris2/total002/Total.idr

@@ -0,0 +1,13 @@
+data Fin : Nat -> Type where
+     FZ : Fin (S k)
+     FS : Fin k -> Fin (S k)
+
+noFinZ : Fin Z -> Void
+noFinZ FZ impossible
+noFinZ (FS k) impossible
+
+noFinZ' : Fin Z -> Void
+noFinZ' x impossible
+
+noEmpty : Void -> Fin Z
+noEmpty t impossible

tests/idris2/total002/expected

@@ -0,0 +1,6 @@
+1/1: Building Total (Total.idr)
+Welcome to Idris 2 version 0.0. Enjoy yourself!
+Main> Main.noFinZ: All cases covered
+Main> Main.noFinZ': All cases covered
+Main> Main.noEmpty: All cases covered
+Main> Bye for now!

tests/idris2/total002/input

@@ -0,0 +1,4 @@
+:missing noFinZ
+:missing noFinZ'
+:missing noEmpty
+:q

tests/idris2/total002/run

@@ -0,0 +1,3 @@
+$1 Total.idr < input
+
+rm -rf build

tests/idris2/total003/Total.idr

@@ -0,0 +1,25 @@
+onlyOne : Int -> Int
+onlyOne 1 = 2
+
+covered : Int -> Int
+covered 1 = 2
+covered 2 = 3
+covered _ = 94
+
+data IntNat : Integer -> Nat -> Type where
+     IsZero : IntNat 0 Z
+     IsSuc : IntNat 1 (S k)
+
+-- Only identified as covering if 'x' has multiplicity 0 because then it
+-- doesn't show up in the case tree!
+matchInt : (0 x : Integer) -> (n : Nat) -> IntNat x n -> String
+matchInt 0 Z IsZero = "Zero"
+matchInt 1 (S k) IsSuc = "Non Zero"
+
+-- Should be identified as covering but isn't yet since the checker requires
+-- a catch all case. This does at least test that the declared 'impossible'
+-- case really is impossible; we can update it when the checker improves!
+matchInt' : (x : Integer) -> (n : Nat) -> IntNat x n -> String
+matchInt' 0 Z IsZero = "Zero"
+matchInt' 1 (S k) IsSuc = "Non Zero"
+matchInt' 0 (S k) x impossible

tests/idris2/total003/expected

@@ -0,0 +1,10 @@
+1/1: Building Total (Total.idr)
+Welcome to Idris 2 version 0.0. Enjoy yourself!
+Main> Main.onlyOne:
+onlyOne _
+Main> Main.covered: All cases covered
+Main> Main.matchInt: All cases covered
+Main> Main.matchInt':
+matchInt' _ _ IsZero
+matchInt' _ _ IsSuc
+Main> Bye for now!

tests/idris2/total003/input

@@ -0,0 +1,5 @@
+:missing onlyOne
+:missing covered
+:missing matchInt
+:missing matchInt'
+:q

tests/idris2/total003/run

@@ -0,0 +1,3 @@
+$1 Total.idr < input
+
+rm -rf build