Merge pull request #1067 from GaloisInc/issue1044

Relax the check that all values are consumed

src/Cryptol/Symbolic/SBV.hs

@@ -422,7 +422,7 @@ processResults ProverCommand{..} ts results =
     -- to always be the first value in the model assignment list.
     let Right (_, (safetyCV : cvs)) = SBV.getModelAssignment result
         safety = SBV.cvToBool safetyCV
-        (vs, []) = parseValues ts cvs
+        (vs, _) = parseValues ts cvs
         mdl = computeModel prims ts vs
     return (safety, mdl)
 

src/Cryptol/TypeCheck/Depends.hs

@@ -15,7 +15,7 @@ import qualified Cryptol.Parser.AST as P
 import           Cryptol.Parser.Position(Range, Located(..), thing)
 import           Cryptol.Parser.Names (namesB, tnamesT, tnamesC,
                                       boundNamesSet, boundNames)
-import           Cryptol.TypeCheck.Monad( InferM, recordError, getTVars )
+import           Cryptol.TypeCheck.Monad( InferM, getTVars )
 import           Cryptol.TypeCheck.Error(Error(..))
 import           Cryptol.Utils.Panic(panic)
 import           Cryptol.Utils.RecordMap(recordElements)
@@ -29,6 +29,7 @@ import           Data.Map (Map)
 import qualified Data.Map as Map
 import qualified Data.Set as Set
 import           Data.Text (Text)
+import           MonadLib (ExceptionT, runExceptionT, raise)
 
 data TyDecl =
     TS (P.TySyn Name) (Maybe Text)          -- ^ Type synonym
@@ -49,13 +50,13 @@ setDocString x d =
 
 -- | Check for duplicate and recursive type synonyms.
 -- Returns the type-synonyms in dependency order.
-orderTyDecls :: [TyDecl] -> InferM [TyDecl]
+orderTyDecls :: [TyDecl] -> InferM (Either Error [TyDecl])
 orderTyDecls ts =
   do vs <- getTVars
      ds <- combine $ map (toMap vs) ts
      let ordered = mkScc [ (t,[x],deps)
                               | (x,(t,deps)) <- Map.toList (Map.map thing ds) ]
-     concat `fmap` mapM check ordered
+     runExceptionT (concat `fmap` mapM check ordered)
 
   where
   toMap vs ty@(PT p _) =
@@ -113,17 +114,12 @@ orderTyDecls ts =
   getN (AT x _) = thing (P.ptName x)
   getN (PT x _) = thing (P.primTName x)
 
+  check :: SCC TyDecl -> ExceptionT Error InferM [TyDecl]
   check (AcyclicSCC x) = return [x]
 
   -- We don't support any recursion, for now.
   -- We could support recursion between newtypes, or newtypes and tysysn.
-  check (CyclicSCC xs) =
-    do recordError (RecursiveTypeDecls (map getN xs))
-       return [] -- XXX: This is likely to cause fake errors for missing
-                 -- type synonyms. We could avoid this by, for example, checking
-                 -- for recursive synonym errors, when looking up tycons.
-
-
+  check (CyclicSCC xs) = raise (RecursiveTypeDecls (map getN xs))
 
 -- | Associate type signatures with bindings and order bindings by dependency.
 orderBinds :: [P.Bind Name] -> [SCC (P.Bind Name)]

src/Cryptol/TypeCheck/Infer.hs

@@ -946,8 +946,10 @@ checkSigB b (Forall as asmps0 t0, validSchema) = case thing (P.bDef b) of
         }
 
 inferDs :: FromDecl d => [d] -> ([DeclGroup] -> InferM a) -> InferM a
-inferDs ds continue = checkTyDecls =<< orderTyDecls (mapMaybe toTyDecl ds)
+inferDs ds continue = either onErr checkTyDecls =<< orderTyDecls (mapMaybe toTyDecl ds)
   where
+  onErr err = recordError err >> continue []
+
   isTopLevel = isTopDecl (head ds)
 
   checkTyDecls (AT t mbD : ts) =

tests/issues/issue1040.cry

@@ -0,0 +1,6 @@
+module binarytree where
+
+newtype Tree = { inTree : Tree }
+
+build : Tree
+build = Tree { inTree = undefined }

tests/issues/issue1040.icry

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

tests/issues/issue1040.icry.stdout

@@ -0,0 +1,7 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module binarytree
+
+[error] at issue1040.cry:1:1--6:36:
+  Recursive type declarations:
+    `binarytree::Tree`

tests/issues/issue1044.icry

@@ -0,0 +1,5 @@
+:set prover=sbv-z3
+:safe \(x:Z 7) -> x * (recip x) == 1
+
+:set prover=w4-z3
+:safe \(x:Z 7) -> x * (recip x) == 1

tests/issues/issue1044.icry.stdout

@@ -0,0 +1,17 @@
+Loading module Cryptol
+Counterexample
+(\(x : Z 7) -> x * (recip x) == 1) 0 ~> ERROR
+division by 0
+-- Backtrace --
+Cryptol::recip called at issue1044.icry:2:24--2:29
+(Cryptol::*) called at issue1044.icry:2:19--2:37
+(Cryptol::==) called at issue1044.icry:2:19--2:37
+<interactive>::it called at issue1044.icry:2:7--2:37
+Counterexample
+(\(x : Z 7) -> x * (recip x) == 1) 0 ~> ERROR
+division by 0
+-- Backtrace --
+Cryptol::recip called at issue1044.icry:5:24--5:29
+(Cryptol::*) called at issue1044.icry:5:19--5:37
+(Cryptol::==) called at issue1044.icry:5:19--5:37
+<interactive>::it called at issue1044.icry:5:7--5:37