Coverage checker looks at 'impossible' clauses

These can give valuable information, but since they're not well typed,
we have to rebuild as close an approximation as we can before passing it
to the case tree compiler. We can do this in a type-directed way, but
ignoring whether any of the arguments are convertible, and not trying to
solve any of the implicits. If this fails, it doesn't use the impossible
case, otherwise it uses it to find the missing cases in the resulting
case tree.

idris2.ipkg

@@ -100,6 +100,7 @@ modules =
     TTImp.Elab.Rewrite,
     TTImp.Elab.Term,
     TTImp.Elab.Utils,
+    TTImp.Impossible,
     TTImp.Interactive.CaseSplit,
     TTImp.Interactive.ExprSearch,
     TTImp.Interactive.GenerateDef,

src/TTImp/Impossible.idr

@@ -0,0 +1,159 @@
+module TTImp.Impossible
+
+import Core.Context
+import Core.Env
+import Core.Normalise
+import Core.TT
+import Core.Value
+
+import TTImp.TTImp
+
+-- This file contains support for building a guess at the term on the LHS of an 
+-- 'impossible' case, in order to help build a tree of covered cases for
+-- coverage checking. Since the LHS by definition won't be well typed, we are
+-- only guessing! But we can still do some type-directed disambiguation of
+-- names.
+-- Constants (fromInteger/fromString etc) won't be supported, because in general
+-- they involve resoling interfaces - they'll just become unmatchable patterns.
+
+match : {auto c : Ref Ctxt Defs} ->
+        NF [] -> (Name, Int, ClosedTerm) -> Core Bool
+match nty (n, i, rty)
+    = do defs <- get Ctxt
+         rtynf <- nf defs [] rty
+         sameRet nty rtynf
+  where
+    sameRet : NF [] -> NF [] -> Core Bool
+    sameRet _ (NApp _ _ _) = pure True
+    sameRet _ (NErased _ _) = pure True
+    sameRet (NApp _ _ _) _ = pure True
+    sameRet (NErased _ _) _ = pure True
+    sameRet (NTCon _ n _ _ _) (NTCon _ n' _ _ _) = pure (n == n')
+    sameRet (NPrimVal _ c) (NPrimVal _ c') = pure (c == c')
+    sameRet (NType _) (NType _) = pure True
+    sameRet nf (NBind fc _ (Pi _ _ _) sc)
+        = do defs <- get Ctxt
+             sc' <- sc defs (toClosure defaultOpts [] (Erased fc False))
+             sameRet nf sc'
+    sameRet _ _ = pure False
+
+dropNoMatch : {auto c : Ref Ctxt Defs} ->
+              Maybe (NF []) -> List (Name, Int, ClosedTerm) ->
+              Core (List (Name, Int, ClosedTerm))
+dropNoMatch _ [t] = pure [t]
+dropNoMatch Nothing ts = pure ts
+dropNoMatch (Just nty) ts
+    = -- if the return type of a thing in ts doesn't match nty, drop it
+      filterM (match nty) ts
+
+nextVar : {auto q : Ref QVar Int} ->
+          FC -> Core (Term [])
+nextVar fc
+    = do i <- get QVar
+         put QVar (i + 1)
+         pure (Ref fc Bound (MN "imp" i))
+
+mutual
+  processArgs : {auto c : Ref Ctxt Defs} ->
+                {auto q : Ref QVar Int} ->
+                Term [] -> NF [] ->
+                (expargs : List RawImp) -> (impargs : List (Maybe Name, RawImp)) ->
+                Core ClosedTerm
+  processArgs fn (NBind fc x (Pi r Explicit ty) sc) (e :: exp) imp
+     = do e' <- mkTerm e (Just ty) [] []
+          defs <- get Ctxt
+          processArgs (App fc fn e') !(sc defs (toClosure defaultOpts [] e'))
+                      exp imp
+  processArgs fn (NBind fc x (Pi r Implicit ty) sc) exp imp
+     = do defs <- get Ctxt
+          case useImp [] imp of
+            Nothing => do e' <- nextVar fc
+                          processArgs (App fc fn e')
+                                      !(sc defs (toClosure defaultOpts [] e'))
+                                      exp imp
+            Just (e, impargs') =>
+               do e' <- mkTerm e (Just ty) [] []
+                  processArgs (App fc fn e') !(sc defs (toClosure defaultOpts [] e'))
+                              exp impargs'
+    where
+      useImp : List (Maybe Name, RawImp) -> List (Maybe Name, RawImp) ->
+               Maybe (RawImp, List (Maybe Name, RawImp))
+      useImp acc [] = Nothing
+      useImp acc ((Just x', xtm) :: rest)
+          = if x == x'
+               then Just (xtm, reverse acc ++ rest)
+               else useImp ((Just x', xtm) :: acc) rest
+      useImp acc (ximp :: rest)
+          = useImp (ximp :: acc) rest
+  processArgs fn (NBind fc x (Pi r AutoImplicit ty) sc) exp imp
+     = do defs <- get Ctxt
+          case useAutoImp [] imp of
+            Nothing => do e' <- nextVar fc
+                          processArgs (App fc fn e')
+                                      !(sc defs (toClosure defaultOpts [] e'))
+                                      exp imp
+            Just (e, impargs') =>
+               do e' <- mkTerm e (Just ty) [] []
+                  processArgs (App fc fn e') !(sc defs (toClosure defaultOpts [] e'))
+                              exp impargs'
+    where
+      useAutoImp : List (Maybe Name, RawImp) -> List (Maybe Name, RawImp) ->
+                   Maybe (RawImp, List (Maybe Name, RawImp))
+      useAutoImp acc [] = Nothing
+      useAutoImp acc ((Nothing, xtm) :: rest)
+          = Just (xtm, reverse acc ++ rest)
+      useAutoImp acc ((Just x', xtm) :: rest)
+          = if x == x'
+               then Just (xtm, reverse acc ++ rest)
+               else useAutoImp ((Just x', xtm) :: acc) rest
+      useAutoImp acc (ximp :: rest)
+          = useAutoImp (ximp :: acc) rest
+  processArgs fn ty [] [] = pure fn
+  processArgs fn ty exp imp
+     = throw (GenericMsg (getLoc fn) 
+                ("Badly formed impossible clause "
+                     ++ show (fn, exp, imp)))
+
+  buildApp : {auto c : Ref Ctxt Defs} ->
+             {auto q : Ref QVar Int} ->
+             FC -> Name -> Maybe (NF []) ->
+             (expargs : List RawImp) -> (impargs : List (Maybe Name, RawImp)) ->
+             Core ClosedTerm
+  buildApp fc n mty exp imp
+      = do defs <- get Ctxt
+           fi <- fromIntegerName
+           si <- fromStringName
+           ci <- fromCharName
+           when (Just n `elem` [fi, si,ci]) $
+               throw (InternalError "Can't deal with constants here yet")
+
+           tys <- lookupTyName n (gamma defs)
+           [(n', _, ty)] <- dropNoMatch mty tys
+              | [] => throw (UndefinedName fc n)
+              | ts => throw (AmbiguousName fc (map fst ts))
+           tynf <- nf defs [] ty
+           processArgs (Ref fc Func n') tynf exp imp
+
+  mkTerm : {auto c : Ref Ctxt Defs} -> 
+           {auto q : Ref QVar Int} ->
+           RawImp -> Maybe (NF []) ->
+           (expargs : List RawImp) -> (impargs : List (Maybe Name, RawImp)) ->
+           Core ClosedTerm
+  mkTerm (IVar fc n) mty exp imp
+     = buildApp fc n mty exp imp
+  mkTerm (IApp fc fn arg) mty exp imp
+     = mkTerm fn mty (arg :: exp) imp
+  mkTerm (IImplicitApp fc fn nm arg) mty exp imp
+     = mkTerm fn mty exp ((nm, arg) :: imp)
+  mkTerm (IPrimVal fc c) _ _ _ = pure (PrimVal fc c)
+  mkTerm tm _ _ _ = nextVar (getFC tm)
+
+-- Given an LHS that is declared 'impossible', build a term to match from,
+-- so that when we build the case tree for checking coverage, we take into
+-- account the impossible clauses
+export
+getImpossibleTerm : {auto c : Ref Ctxt Defs} ->
+                    RawImp -> Core ClosedTerm
+getImpossibleTerm tm
+    = do q <- newRef QVar (the Int 0)
+         mkTerm tm Nothing [] []

src/TTImp/ProcessDef.idr

@@ -17,6 +17,7 @@ import Core.UnifyState
 import TTImp.BindImplicits
 import TTImp.Elab
 import TTImp.Elab.Check
+import TTImp.Impossible
 import TTImp.TTImp
 import TTImp.Unelab
 import TTImp.Utils
@@ -319,11 +320,6 @@ applyEnv env withname
                   \fc, nt => applyTo fc
                          (Ref fc nt (Resolved n')) env))
 
-getImpossibleTerm : {vars : _} ->
-                    {auto c : Ref Ctxt Defs} ->
-                    RawImp -> Core (Term vars)
-getImpossibleTerm tm = pure (Erased (getFC tm) False)
-
 -- Check a pattern clause, returning the component of the 'Case' expression it
 -- represents, or Nothing if it's an impossible clause
 export
@@ -333,7 +329,7 @@ checkClause : {vars : _} ->
               {auto u : Ref UST UState} ->
               (mult : RigCount) -> (hashit : Bool) ->
               Int -> List ElabOpt -> NestedNames vars -> Env Term vars ->
-              ImpClause -> Core (Either (Term vars) Clause)
+              ImpClause -> Core (Either RawImp Clause)
 checkClause mult hashit n opts nest env (ImpossibleClause fc lhs)
     = do lhs_raw <- lhsInCurrentNS nest lhs
          handleUnify
@@ -350,16 +346,14 @@ checkClause mult hashit n opts nest env (ImpossibleClause fc lhs)
                defs <- get Ctxt
                lhs <- normaliseHoles defs env lhstm
                if !(hasEmptyPat defs env lhs)
-                  then do lhs_p <- getImpossibleTerm lhs_raw
+                  then pure (Left lhs_raw)
-                          pure (Left lhs_p)
                   else throw (ValidCase fc env (Left lhs)))
            (\err =>
               case err of
                    ValidCase _ _ _ => throw err
                    _ => do defs <- get Ctxt
                            if !(impossibleErrOK defs err)
-                              then do lhs_p <- getImpossibleTerm lhs_raw
+                              then pure (Left lhs_raw)
-                                      pure (Left lhs_p)
                               else throw (ValidCase fc env (Right err)))
 checkClause {vars} mult hashit n opts nest env (PatClause fc lhs_in rhs)
     = do (_, (vars'  ** (sub', env', nest', lhstm', lhsty'))) <-
@@ -681,11 +675,21 @@ processDef opts nest env fc n_in cs_in
                                         else pure (Just tm)
                              _ => pure (Just tm))
 
+    getClause : {auto c : Ref Ctxt Defs} ->
+                Either RawImp Clause -> Core (Maybe Clause)
+    getClause (Left rawlhs)
+        = catch (do lhsp <- getImpossibleTerm rawlhs
+                    log 3 $ "Generated impossible LHS: " ++ show lhsp
+                    pure $ Just $ MkClause [] lhsp (Erased (getFC rawlhs) True))
+                (\e => pure Nothing)
+    getClause (Right c) = pure (Just c)
+
     checkCoverage : Int -> ClosedTerm -> RigCount ->
-                    List (Either (Term vs) Clause) ->
+                    List (Either RawImp Clause) ->
                     Core Covering
     checkCoverage n ty mult cs
-        = do let covcs = rights cs -- TODO: Make stand in LHS for impossible clauses
+        = do covcs' <- traverse getClause cs -- Make stand in LHS for impossible clauses
+             let covcs = mapMaybe id covcs'
              (_ ** ctree) <- getPMDef fc CompileTime (Resolved n) ty covcs
              missCase <- if any catchAll covcs
                             then do log 3 $ "Catch all case in " ++ show n

tests/Main.idr

@@ -33,6 +33,7 @@ idrisTests
        "basic031", "basic032", "basic033", "basic034", "basic035",
        -- Coverage checking
        "coverage001", "coverage002", "coverage003", "coverage004",
+       "coverage005",
        -- Error messages
        "error001", "error002", "error003", "error004", "error005",
        "error006", "error007", "error008", "error009", "error010",