Merge pull request #1818 from GaloisInc/dm/issue1798

add source spans to exhaustivity warnings

CHANGES.md

@@ -46,6 +46,10 @@
 
 ## New features
 
+* Improved warning messages for non-exhaustive guards.
+  Warnings are now ordered by source location.
+  ([#1798](https://github.com/GaloisInc/cryptol/issues/1798))
+
 * Improved error messages mentioning module parameters
   ([#1560](https://github.com/GaloisInc/cryptol/issues/1560))
 

src/Cryptol/Parser/AST.hs

@@ -881,7 +881,12 @@ instance HasLoc (TySyn name) where
 instance HasLoc (PropSyn name) where
   getLoc (PropSyn x _ _ _) = getLoc x
 
-
+instance HasLoc (PropGuardCase name) where
+  getLoc n
+    | null locs = Nothing
+    | otherwise = Just (rCombs locs)
+    where
+    locs = catMaybes (getLoc (pgcExpr n) : map getLoc (pgcProps n))
 
 --------------------------------------------------------------------------------
 

src/Cryptol/TypeCheck/Error.hs

@@ -25,6 +25,11 @@ import Cryptol.TypeCheck.FFI.Error
 import Cryptol.ModuleSystem.Name(Name)
 import Cryptol.Utils.RecordMap
 
+-- | Clean up error messages by:
+---  * only reporting one error (most severe) for any given source location
+--   * sorting errors by source location (they are accumulated in
+--     reverse order by 'recordError')
+--   * dropping any errors that are subsumed by another
 cleanupErrors :: [(Range,Error)] -> [(Range,Error)]
 cleanupErrors = dropErrorsFromSameLoc
               . sortBy (compare `on` (cmpR . fst))    -- order errors
@@ -56,6 +61,17 @@ cleanupErrors = dropErrorsFromSameLoc
          in dropSubsumed (err : filter keep survived) (filter keep rest)
       [] -> survived
 
+-- | Clean up warning messages by sorting them by source location
+--   (they are accumulated in reverse order by 'recordWarning').
+cleanupWarnings :: [(Range,Warning)] -> [(Range,Warning)]
+cleanupWarnings = 
+  sortBy (compare `on` (cmpR . fst))    -- order warnings
+  where
+    cmpR r  = ( source r    -- First by file
+              , from r      -- Then starting position
+              , to r        -- Finally end position
+              )
+
 -- | Should the first error suppress the next one.
 subsumes :: (Range,Error) -> (Range,Error) -> Bool
 subsumes (_,NotForAll _ _ x _) (_,NotForAll _ _ y _) = x == y

src/Cryptol/TypeCheck/Infer.hs

@@ -1227,7 +1227,7 @@ checkSigB b (Forall as asmps0 t0, validSchema) =
                , foldr ETAbs (foldr EProofAbs e2 asmps) as
                )
 
-        P.DPropGuards cases0 -> do
+        P.DPropGuards cases0 -> inRangeMb (getLoc cases0) $ do
           asmps1 <- applySubstPreds asmps0
           t1     <- applySubst t0
           cases1 <- mapM (checkPropGuardCase asmps1) cases0

src/Cryptol/TypeCheck/Monad.hs

@@ -51,7 +51,7 @@ import           Cryptol.TypeCheck.Unify(doMGU, runResult, UnificationError(..)
                                         , Path, rootPath)
 import           Cryptol.TypeCheck.InferTypes
 import           Cryptol.TypeCheck.Error( Warning(..),Error(..)
-                                        , cleanupErrors, computeFreeVarNames
+                                        , cleanupErrors, computeFreeVarNames, cleanupWarnings
                                         )
 import qualified Cryptol.TypeCheck.SimpleSolver as Simple
 import qualified Cryptol.TypeCheck.Solver.SMT as SMT
@@ -184,10 +184,13 @@ runInferM info m0 =
               errs -> inferFailed warns [(r,apSubst theSu e) | (r,e) <- errs]
 
   where
-  inferOk ws a b c  = pure (InferOK (computeFreeVarNames ws []) ws a b c)
+  inferOk ws a b c  = 
+    let ws1 = cleanupWarnings ws
+    in pure (InferOK (computeFreeVarNames ws1 []) ws1 a b c)
   inferFailed ws es =
     let es1 = cleanupErrors es
-    in pure (InferFailed (computeFreeVarNames ws es1) ws es1)
+        ws1 = cleanupWarnings ws
+    in pure (InferFailed (computeFreeVarNames ws1 es1) ws1 es1)
 
 
   rw = RW { iErrors     = []

tests/constraint-guards/constant.icry.stdout

@@ -5,7 +5,7 @@ Loading module Main
     Unused name: n
 [warning] at constant.cry:14:10--14:15
     Unused name: n
-[warning] at constant.cry:28:1--28:10:
+[warning] at constant.cry:28:13--28:18:
   Could not prove that the constraint guards used in defining Main::idTypeNum were exhaustive.
 property isZero_correct Using exhaustive testing.
 Testing... Passed 1 tests.

tests/constraint-guards/nestMod.icry.stdout

@@ -1,9 +1,9 @@
 Loading module Cryptol
 Loading module Cryptol
 Loading module Main
-[warning] at nestMod.cry:8:5--8:13:
-  Assuming  n to have a numeric type
 [warning] at nestMod.cry:4:7--4:15:
   Assuming  n to have a numeric type
+[warning] at nestMod.cry:8:5--8:13:
+  Assuming  n to have a numeric type
 True
 False

tests/issues/issue1798.cry

@@ -0,0 +1,8 @@
+exhaustive1 : {w} [2 ^^ (2 ^^ w)] -> [2 ^^ (2 ^^ w)]
+exhaustive1 x
+  | (2 ^^ (2 ^^ w)) < 2 => x
+  | (2 ^^ (2 ^^ w)) == 2 => ~ x
+
+exhaustive2 : {w} [2 ^^ w] -> [2 ^^ w]
+exhaustive2 x
+  | (2 ^^ w) == 1 => ~ x

tests/issues/issue1798.icry

@@ -0,0 +1 @@
+:l issue1798.cry

tests/issues/issue1798.icry.stdout

@@ -0,0 +1,7 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+[warning] at issue1798.cry:3:5--4:25:
+  Could not prove that the constraint guards used in defining Main::exhaustive1 were exhaustive.
+[warning] at issue1798.cry:8:5--8:18:
+  Could not prove that the constraint guards used in defining Main::exhaustive2 were exhaustive.