Make :check work for tests involving type Integer.

src/Cryptol/REPL/Command.hs

@@ -316,7 +316,7 @@ qcCmd qcMode str =
      (val,ty) <- replEvalExpr expr
      EnvNum testNum  <- getUser "tests"
      case testableType ty of
-       Just (sz,tys,vss) | qcMode == QCExhaust || sz <= toInteger testNum -> do
+       Just (Just sz,tys,vss) | qcMode == QCExhaust || sz <= toInteger testNum -> do
             rPutStrLn "Using exhaustive testing."
             let f _ [] = panic "Cryptol.REPL.Command"
                                     ["Exhaustive testing ran out of test cases"]
@@ -328,7 +328,7 @@ qcCmd qcMode str =
                     testFn = f
                   , testProp = str
                   , testTotal = sz
-                  , testPossible = sz
+                  , testPossible = Just sz
                   , testRptProgress = ppProgress
                   , testClrProgress = delProgress
                   , testRptFailure = ppFailure tys expr
@@ -363,7 +363,9 @@ qcCmd qcMode str =
                 g <- io newTFGen
                 report <- runTests testSpec g
                 when (isPass (reportResult report)) $
-                  rPutStrLn $ coverageString testNum sz
+                  case sz of
+                    Nothing -> return ()
+                    Just n -> rPutStrLn $ coverageString testNum n
                 return [report]
        Nothing -> return []
 

src/Cryptol/Testing/Concrete.hs

@@ -9,7 +9,7 @@
 {-# LANGUAGE RecordWildCards #-}
 module Cryptol.Testing.Concrete where
 
-import Control.Monad (join)
+import Control.Monad (join, liftM2)
 
 import Cryptol.Eval.Monad
 import Cryptol.Eval.Value
@@ -63,14 +63,14 @@ runOneTest evOpts v0 vs0 = run `X.catch` handle
 {- | Given a (function) type, compute all possible inputs for it.
 We also return the types of the arguments and
 the total number of test (i.e., the length of the outer list. -}
-testableType :: Type -> Maybe (Integer, [Type], [[Value]])
+testableType :: Type -> Maybe (Maybe Integer, [Type], [[Value]])
 testableType ty =
   case tNoUser ty of
     TCon (TC TCFun) [t1,t2] ->
-      do sz        <- typeSize t1
+      do let sz = typeSize t1
          (tot,ts,vss) <- testableType t2
-         return (sz * tot, t1:ts, [ v : vs | v <- typeValues t1, vs <- vss ])
-    TCon (TC TCBit) [] -> return (1, [], [[]])
+         return (liftM2 (*) sz tot, t1:ts, [ v : vs | v <- typeValues t1, vs <- vss ])
+    TCon (TC TCBit) [] -> return (Just 1, [], [[]])
     _ -> Nothing
 
 {- | Given a fully-evaluated type, try to compute the number of values in it.
@@ -144,7 +144,7 @@ data TestSpec m s = TestSpec {
     testFn :: Integer -> s -> m (TestResult, s)
   , testProp :: String -- ^ The property as entered by the user
   , testTotal :: Integer
-  , testPossible :: Integer
+  , testPossible :: Maybe Integer -- ^ Nothing indicates infinity
   , testRptProgress :: Integer -> Integer -> m ()
   , testClrProgress :: m ()
   , testRptFailure :: TestResult -> m ()
@@ -155,7 +155,7 @@ data TestReport = TestReport {
     reportResult :: TestResult
   , reportProp :: String -- ^ The property as entered by the user
   , reportTestsRun :: Integer
-  , reportTestsPossible :: Integer
+  , reportTestsPossible :: Maybe Integer
   }
 
 runTests :: Monad m => TestSpec m s -> s -> m TestReport

src/Cryptol/Testing/Random.hs

@@ -70,6 +70,8 @@ randomValue ty =
       case (tc, map (tRebuild' False) ts) of
         (TC TCBit, [])                        -> Just randomBit
 
+        (TC TCInteger, [])                    -> Just randomInteger
+
         (TC TCSeq, [TCon (TC TCInf) [], el])  ->
           do mk <- randomValue el
              return (randomStream mk)
@@ -99,6 +101,12 @@ randomBit _ g =
   let (b,g1) = random g
   in (VBit (bitLit b), g1)
 
+-- | Generate a random integer value.
+randomInteger :: (BitWord b w i, RandomGen g) => Gen g b w i
+randomInteger _ g =
+  let (x, g1) = random g
+  in (VInteger (integerLit x), g1)
+
 -- | Generate a random word of the given length (i.e., a value of type @[w]@)
 -- The size parameter is assumed to vary between 1 and 100, and we use
 -- it to generate smaller numbers first.