Idris2/tests/chez/chez019/partial.idr

%default partial

foo : Maybe a -> a
foo (Just x) = x

data Vect : ? -> 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

main : IO ()
main = do let x = foo Nothing
          printLn (the Int x)
All functions now need to be covering by default This has caught a couple of things in the Idris 2 code base itself. Some tests needed partial annotations too. 2020-05-24 21:58:20 +03:00			`%default partial`

Add runtime error for unhandled cases Should have done this ages ago, it was much easier than I expected... this adds an explicit error clause before running the pattern match compiler for runtime case trees, but only if the coverage checker finds there are missing cases. 2020-05-21 12:53:24 +03:00			`foo : Maybe a -> a`
			`foo (Just x) = x`

			`data Vect : ? -> 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`

			`main : IO ()`
			`main = do let x = foo Nothing`
			`printLn (the Int x)`