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.

src/TTImp/ProcessDef.idr

@@ -581,8 +581,8 @@ calcRefs rt at fn
 mkRunTime : {auto c : Ref Ctxt Defs} ->
             {auto m : Ref MD Metadata} ->
             {auto u : Ref UST UState} ->
-            Name -> Core ()
-mkRunTime n
+            FC -> Covering -> Name -> Core ()
+mkRunTime fc cov n
     = do log 5 $ "Making run time definition for " ++ show !(toFullNames n)
          defs <- get Ctxt
          Just gdef <- lookupCtxtExact n (gamma defs)
@@ -597,15 +597,40 @@ mkRunTime n
            pats' <- traverse (toErased (location gdef) (getSpec (flags gdef)))
                              pats
 
-           (rargs ** tree_rt) <- getPMDef (location gdef) RunTime n ty
-                                          (map (toClause (location gdef)) pats')
+           let clauses_init = map (toClause (location gdef)) pats'
+           let clauses = case cov of
+                              MissingCases _ => addErrorCase clauses_init
+                              _ => clauses_init
+
+           (rargs ** tree_rt) <- getPMDef (location gdef) RunTime n ty clauses
            log 5 $ "Runtime tree for " ++ show (fullname gdef) ++ ": " ++ show tree_rt
+
            let Just Refl = nameListEq cargs rargs
                    | Nothing => throw (InternalError "WAT")
            addDef n (record { definition = PMDef r rargs tree_ct tree_rt pats
                             } gdef)
            pure ()
   where
+    mkCrash : {vars : _} -> String -> Term vars
+    mkCrash msg
+       = apply fc (Ref fc Func (NS ["Builtin"] (UN "idris_crash")))
+               [Erased fc False, PrimVal fc (Str msg)]
+
+    matchAny : Term vars -> Term vars
+    matchAny (App fc f a) = App fc (matchAny f) (Erased fc False)
+    matchAny tm = tm
+
+    makeErrorClause : {vars : _} -> Env Term vars -> Term vars -> Clause
+    makeErrorClause env lhs
+        = MkClause env (matchAny lhs)
+             (mkCrash ("Unhandled input for " ++ show n ++ " at " ++ show fc))
+
+    addErrorCase : List Clause -> List Clause
+    addErrorCase [] = []
+    addErrorCase [MkClause env lhs rhs]
+        = MkClause env lhs rhs :: makeErrorClause env lhs :: []
+    addErrorCase (x :: xs) = x :: addErrorCase xs
+
     getSpec : List DefFlag -> Maybe (List (Name, Nat))
     getSpec [] = Nothing
     getSpec (PartialEval n :: _) = Just n
@@ -629,10 +654,10 @@ mkRunTime n
 compileRunTime : {auto c : Ref Ctxt Defs} ->
                  {auto m : Ref MD Metadata} ->
                  {auto u : Ref UST UState} ->
-                 Name -> Core ()
-compileRunTime atotal
+                 FC -> Covering -> Name -> Core ()
+compileRunTime fc cov atotal
     = do defs <- get Ctxt
-         traverse_ mkRunTime (toCompileCase defs)
+         traverse_ (mkRunTime fc cov) (toCompileCase defs)
          traverse (calcRefs True atotal) (toCompileCase defs)
 
          defs <- get Ctxt
@@ -702,10 +727,9 @@ processDef opts nest env fc n_in cs_in
          put MD md
 
          -- If we're not in a case tree, compile all the outstanding case
-         -- trees. TODO: Take into account coverage, and add error cases
-         -- if we're not covering.
+         -- trees.
          when (not (elem InCase opts)) $
-           compileRunTime atotal
+           compileRunTime fc cov atotal
 
   where
     simplePat : forall vars . Term vars -> Bool

tests/Main.idr

@@ -102,6 +102,7 @@ chezTests
    = ["chez001", "chez002", "chez003", "chez004", "chez005", "chez006",
       "chez007", "chez008", "chez009", "chez010", "chez011", "chez012",
       "chez013", "chez014", "chez015", "chez016", "chez017", "chez018",
+      "chez019",
       "reg001"]
 
 ideModeTests : List String

tests/chez/chez019/expected

@@ -0,0 +1,6 @@
+ERROR: Unhandled input for Main.foo at partial.idr:2:1--4:1
+2
+ERROR: Unhandled input for Main.lookup' at partial.idr:17:1--19:1
+ERROR: Unhandled input for Main.lookup' at partial.idr:17:1--19:1
+1/1: Building partial (partial.idr)
+Main> Main> Main> Main> Main> Bye for now!

tests/chez/chez019/input

@@ -0,0 +1,5 @@
+:exec main
+:exec printLn $ lookup (FS FZ) [1,2,3,4]
+:exec printLn $ lookup' (FS FZ) [1,2,3,4]
+:exec printLn $ lookup'' (FS FZ) [1,2,3,4]
+:q

tests/chez/chez019/partial.idr

@@ -0,0 +1,24 @@
+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)

tests/chez/chez019/run

@@ -0,0 +1,3 @@
+$1 --no-banner partial.idr < input
+
+rm -rf build testout.txt