Merge pull request #383 from edwinb/coverwhere

Pay attention to nested names in coverage check

src/TTImp/Impossible.idr

@@ -158,8 +158,8 @@ mutual
 export
 getImpossibleTerm : {vars : _} ->
                     {auto c : Ref Ctxt Defs} ->
-                    Env Term vars -> RawImp -> Core ClosedTerm
-getImpossibleTerm env tm
+                    Env Term vars -> NestedNames vars -> RawImp -> Core ClosedTerm
+getImpossibleTerm env nest tm
     = do q <- newRef QVar (the Int 0)
          mkTerm (applyEnv tm) Nothing [] []
   where
@@ -175,9 +175,17 @@ getImpossibleTerm env tm
           then addEnv fc env
           else Implicit fc False :: addEnv fc env
 
-    -- Need to apply the function to the surrounding environment
+    expandNest : RawImp -> RawImp
+    expandNest (IVar fc n)
+        = case lookup n (names nest) of
+               Just (Just n', _, _) => IVar fc n'
+               _ => IVar fc n
+    expandNest tm = tm
+
+    -- Need to apply the function to the surrounding environment, and update
+    -- the name to the proper one from the nested names map
     applyEnv : RawImp -> RawImp
     applyEnv (IApp fc fn arg) = IApp fc (applyEnv fn) arg
     applyEnv (IImplicitApp fc fn n arg)
         = IImplicitApp fc (applyEnv fn) n arg
-    applyEnv tm = apply tm (addEnv (getFC tm) env)
+    applyEnv tm = apply (expandNest tm) (addEnv (getFC tm) env)

src/TTImp/ProcessDef.idr

@@ -795,10 +795,11 @@ processDef opts nest env fc n_in cs_in
 
     getClause : Either RawImp Clause -> Core (Maybe Clause)
     getClause (Left rawlhs)
-        = catch (do lhsp <- getImpossibleTerm env rawlhs
+        = catch (do lhsp <- getImpossibleTerm env nest rawlhs
                     log 3 $ "Generated impossible LHS: " ++ show lhsp
                     pure $ Just $ MkClause [] lhsp (Erased (getFC rawlhs) True))
-                (\e => pure Nothing)
+                (\e => do log 5 $ "Error in getClause " ++ show e
+                          pure Nothing)
     getClause (Right c) = pure (Just c)
 
     checkCoverage : Int -> ClosedTerm -> RigCount ->

tests/Main.idr

@@ -97,7 +97,7 @@ idrisTests
        "reg001", "reg002", "reg003", "reg004", "reg005", "reg006", "reg007",
        "reg008", "reg009", "reg010", "reg011", "reg012", "reg013", "reg014",
        "reg015", "reg016", "reg017", "reg018", "reg019", "reg020", "reg021",
-       "reg022", "reg023", "reg024", "reg025", "reg026",
+       "reg022", "reg023", "reg024", "reg025", "reg026", "reg027",
        -- Totality checking
        "total001", "total002", "total003", "total004", "total005",
        "total006", "total007", "total008",

tests/idris2/reg027/expected

@@ -0,0 +1 @@
+1/1: Building pwhere (pwhere.idr)

tests/idris2/reg027/pwhere.idr

@@ -0,0 +1,13 @@
+module Main
+
+import Data.So
+
+total
+lem1 : So x -> So (not x) -> Void
+lem1 Oh Oh impossible
+
+foo : Nat -> Int
+foo z = 94
+  where
+    lem2 : So x -> So (not x) -> Void
+    lem2 Oh Oh impossible

tests/idris2/reg027/run

@@ -0,0 +1,3 @@
+$1 --check pwhere.idr
+
+rm -rf build