Calculate missing cases via coverage checker

src/Core/CaseTree.idr

@@ -1,6 +1,7 @@
 module Core.CaseTree
 
 import Core.TT
+import Data.NameMap
 
 %default covering
 
@@ -112,6 +113,36 @@ export
 Weaken CaseTree where
   weakenNs ns t = insertCaseNames {outer = []} ns t 
 
+getNames : ({vs : _} -> NameMap () -> Term vs -> NameMap ()) ->
+           CaseTree vars -> NameMap ()
+getNames add sc = getSet empty sc
+  where
+    mutual
+      getAltSet : NameMap () -> CaseAlt vs -> NameMap ()
+      getAltSet ns (ConCase n t args sc) = getSet (insert n () ns) sc
+      getAltSet ns (DelayCase t a sc) = getSet ns sc
+      getAltSet ns (ConstCase i sc) = getSet ns sc
+      getAltSet ns (DefaultCase sc) = getSet ns sc
+
+      getAltSets : NameMap () -> List (CaseAlt vs) -> NameMap ()
+      getAltSets ns [] = ns
+      getAltSets ns (a :: as) 
+          = assert_total $ getAltSets (getAltSet ns a) as
+
+      getSet : NameMap () -> CaseTree vs -> NameMap ()
+      getSet ns (Case _ x ty xs) = getAltSets ns xs
+      getSet ns (STerm tm) = add ns tm
+      getSet ns (Unmatched msg) = ns
+      getSet ns Impossible = ns
+
+export
+getRefs : CaseTree vars -> NameMap ()
+getRefs = getNames addRefs
+
+export
+getMetas : CaseTree vars -> NameMap ()
+getMetas = getNames addMetas
+
 export
 mkPat' : List Pat -> ClosedTerm -> ClosedTerm -> Pat
 mkPat' args orig (Ref fc Bound n) = PLoc fc n

src/TTImp/Elab/Check.idr

@@ -502,6 +502,9 @@ convert fc elabinfo env x y
                             -- resolving any more constraints
                             catch (solveConstraints umode Normal)
                                   (\err => pure ())
+                            -- We need to normalise the known holes before
+                            -- throwing because they may no longer be known
+                            -- by the time we look at the error
                             throw (WhenUnifying fc env 
                                       !(normaliseHoles defs env xtm)
                                       !(normaliseHoles defs env ytm) err))

src/TTImp/Parser.idr

@@ -698,6 +698,9 @@ command
          l <- intLit
          n <- name
          pure (GenerateDef (fromInteger l) n)
+  <|> do symbol ":"; exactIdent "missing"
+         n <- name
+         pure (Missing n)
   <|> do symbol ":"; exactIdent "di"
          n <- name
          pure (DebugInfo n)

src/TTImp/ProcessDef.idr

@@ -16,8 +16,11 @@ import TTImp.BindImplicits
 import TTImp.Elab
 import TTImp.Elab.Check
 import TTImp.TTImp
+import TTImp.Unelab
 import TTImp.Utils
 
+import Data.NameMap
+
 mutual
   mismatchNF : Defs -> NF vars -> NF vars -> Core Bool
   mismatchNF defs (NTCon _ _ xt _ xargs) (NTCon _ _ yt _ yargs) 
@@ -494,7 +497,7 @@ processDef : {auto c : Ref Ctxt Defs} ->
              {auto u : Ref UST UState} ->
              List ElabOpt -> NestedNames vars -> Env Term vars -> FC ->
              Name -> List ImpClause -> Core ()
-processDef {vars} opts nest env fc n_in cs_in
+processDef opts nest env fc n_in cs_in
     = do n <- inCurrentNS n_in
          defs <- get Ctxt
          Just gdef <- lookupCtxtExact n (gamma defs)
@@ -518,6 +521,62 @@ processDef {vars} opts nest env fc n_in cs_in
                  | Nothing => throw (InternalError "WAT")
         
          log 5 $ "Case tree for " ++ show n ++ ": " ++ show tree_ct
-         addDef n (record { definition = PMDef cargs tree_ct tree_rt pats } gdef)
-         pure ()
-         
+         addDef n (record { definition = PMDef cargs tree_ct tree_rt pats,
+                            refersTo = getRefs tree_ct } gdef)
+
+         cov <- checkCoverage nidx mult cs tree_ct
+         setCovering fc n cov
+  where
+    simplePat : Term vars -> Bool
+    simplePat (Local _ _ _ _) = True
+    simplePat (Erased _) = True
+    simplePat _ = False
+
+    -- Is the clause returned from 'checkClause' a catch all clause, i.e.
+    -- one where all the arguments are variables? If so, no need to do the
+    -- (potentially expensive) coverage check
+    catchAll : Maybe (Clause, Clause) -> Bool
+    catchAll Nothing = False
+    catchAll (Just (MkClause env lhs _, _))
+       = all simplePat (map snd (getArgs lhs))
+   
+    -- Return 'Nothing' if the clause is impossible, otherwise return the
+    -- original
+    checkImpossible : Int -> RigCount -> ClosedTerm -> 
+                      Core (Maybe ClosedTerm)
+    checkImpossible n mult tm
+        = do itm <- unelabNoPatvars [] tm
+             handleUnify
+               (do ctxt <- get Ctxt
+                   log 3 $ "Checking for impossibility: " ++ show itm
+                   ok <- checkClause mult False n [] (MkNested []) []
+                                     (ImpossibleClause fc itm)
+                   put Ctxt ctxt
+                   maybe (pure Nothing) (\chktm => pure (Just tm)) ok)
+               (\err => case err of
+                             WhenUnifying _ env l r err
+                               => do defs <- get Ctxt
+                                     if !(impossibleOK defs !(nf defs env l) 
+                                                            !(nf defs env r))
+                                        then pure Nothing
+                                        else pure (Just tm)
+                             _ => pure (Just tm))
+
+    checkCoverage : Int -> RigCount -> List (Maybe (Clause, Clause)) ->
+                    CaseTree vs -> Core Covering
+    checkCoverage n mult cs ctree
+        = do missCase <- if any catchAll cs
+                            then do log 3 $ "Catch all case in " ++ show n
+                                    pure []
+                            else getMissing fc (Resolved n) ctree
+             log 3 ("Initially missing in " ++ show n ++ ":\n" ++ 
+                               showSep "\n" (map show missCase))
+             missImp <- traverse (checkImpossible n mult) missCase
+             let miss = mapMaybe id missImp
+             if isNil miss
+                then do [] <- getNonCoveringRefs fc (Resolved n)
+                           | ns => pure (NonCoveringCall ns)
+                        pure IsCovering
+                else pure (MissingCases miss)
+
+    

src/TTImp/TTImp.idr

@@ -300,6 +300,7 @@ data ImpREPL : Type where
      ProofSearch : Name -> ImpREPL
      ExprSearch : Name -> ImpREPL
      GenerateDef : Int -> Name -> ImpREPL
+     Missing : Name -> ImpREPL
      DebugInfo : Name -> ImpREPL
      Quit : ImpREPL
 

src/Yaffle/REPL.idr

@@ -95,6 +95,25 @@ process (GenerateDef line name)
               Just _ => coreLift $ putStrLn "Already defined"
               Nothing => coreLift $ putStrLn $ "Can't find declaration for " ++ show name
          pure True
+process (Missing n_in) 
+    = do defs <- get Ctxt
+         case !(lookupCtxtName n_in (gamma defs)) of
+              [] => throw (UndefinedName emptyFC n_in)
+              ts => do traverse_ (\fn => 
+                          do tot <- getTotality emptyFC fn
+                             the (Core ()) $ case isCovering tot of
+                                  MissingCases cs => 
+                                     coreLift (putStrLn (show fn ++ ":\n" ++
+                                                 showSep "\n" (map show cs)))
+                                  NonCoveringCall ns =>
+                                     coreLift (putStrLn 
+                                         (show fn ++ ": Calls non covering function" 
+                                           ++ case ns of
+                                                   [fn] => " " ++ show fn
+                                                   _ => "s: " ++ showSep ", " (map show ns)))
+                                  _ => coreLift $ putStrLn (show fn ++ ": All cases covered")) 
+                        (map fst ts)
+                       pure True
 process (DebugInfo n)
     = do defs <- get Ctxt
          traverse showInfo !(lookupDefName n (gamma defs))

tests/Main.idr

@@ -8,7 +8,7 @@ ttimpTests : List String
 ttimpTests 
     = ["basic001", "basic002", "basic003", "basic004", "basic005",
        "basic006",
-       "coverage001",
+       "coverage001", "coverage002",
        "dot001",
        "eta001", "eta002",
        "lazy001",

tests/ttimp/coverage002/Vect.yaff

@@ -0,0 +1,33 @@
+data Bool : Type where
+     False : Bool
+     True : Bool
+
+not : Bool -> Bool
+not False = True
+not True = False
+
+data Nat : Type where
+     Z : Nat
+     S : Nat -> Nat
+
+plus : Nat -> Nat -> Nat
+plus Z y = y
+plus (S k) y = S (plus k y)
+
+data Vect : ? -> Type -> Type where
+     Nil : Vect Z a
+     Cons : 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 (Cons x xs) = x
+lookup (FS k) (Cons x xs) = lookup k xs
+
+lookup' : Fin n -> Vect n a -> a
+lookup' (FS k) (Cons x xs) = lookup' k xs
+
+lookup'' : Fin n -> Vect n a -> a
+lookup'' n xs = lookup' n xs

tests/ttimp/coverage002/expected

@@ -0,0 +1,7 @@
+Processing as TTImp
+Written TTC
+Yaffle> Main.lookup: All cases covered
+Yaffle> Main.lookup':
+($resolved132 {arg:0} {arg:1} (Main.FZ {m:0}) {arg:3})
+Yaffle> Main.lookup'': Calls non covering function $resolved132
+Yaffle> Bye for now!

tests/ttimp/coverage002/input

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

tests/ttimp/coverage002/run

@@ -0,0 +1,3 @@
+$1 Vect.yaff < input
+
+rm -rf build