Make :dumptests check whether type is testable before starting.

Instead of panicking, :dumptests will now print the message
"The expression is not of a testable type" when used with an
inappropriately-typed expression. Also, Integer return values
are now supported.

Fixes #615.

src/Cryptol/REPL/Command.hs

@@ -316,7 +316,11 @@ dumpTestsCmd outFile str =
      ppopts <- getPPValOpts
      testNum <- getKnownUser "tests" :: REPL Int
      g <- io newTFGen
-     tests <- io $ TestR.returnTests g evo ty val testNum
+     gens <-
+       case TestR.dumpableType ty of
+         Nothing -> raise (TypeNotTestable ty)
+         Just gens -> return gens
+     tests <- io $ TestR.returnTests g evo gens val testNum
      out <- forM tests $
             \(args, x) ->
               do argOut <- mapM (rEval . E.ppValue ppopts) args

src/Cryptol/Testing/Random.hs

@@ -9,17 +9,17 @@
 -- This module generates random values for Cryptol types.
 
 {-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 module Cryptol.Testing.Random where
 
 import Cryptol.Eval.Monad     (ready,runEval,EvalOpts)
 import Cryptol.Eval.Value     (BV(..),Value,GenValue(..),SeqMap(..), WordValue(..), BitWord(..))
 import qualified Cryptol.Testing.Concrete as Conc
-import Cryptol.TypeCheck.AST  (Type(..),TCon(..),TC(..),tNoUser)
+import Cryptol.TypeCheck.AST  (Type(..), TCon(..), TC(..), tNoUser, tIsFun)
 import Cryptol.TypeCheck.SimpType(tRebuild')
 
 import Cryptol.Utils.Ident    (Ident)
 import Cryptol.Utils.Panic    (panic)
-import Cryptol.Utils.PP       (pp)
 
 import Control.Monad          (forM,join)
 import Data.List              (unfoldr, genericTake, genericIndex)
@@ -63,28 +63,20 @@ returnOneTest evOpts fun argGens sz g0 =
      return (args, result, g1)
    where
      go (VFun f) (v : vs) = join (go <$> (f (ready v)) <*> pure vs)
-     go (VFun _) [] = panic "Not enough arguments to function while generating tests" []
-     go v@(VBit _) [] = return v
-     go v@(VSeq _ _) [] = return v
-     go v@(VWord _ _) [] = return v
-     go v@(VRecord _) [] = return v
-     go v@(VTuple _) [] = return v
-     go _ _ = panic "Cryptol.Testing.Random" ["Unsupported return value for testing"]
+     go (VFun _) [] = panic "Cryptol.Testing.Random" ["Not enough arguments to function while generating tests"]
+     go _ (_ : _) = panic "Cryptol.Testing.Random" ["Too many arguments to function while generating tests"]
+     go v [] = return v
 
 
 -- | Return a collection of random tests.
 returnTests :: RandomGen g
          => g -- ^ The random generator state
          -> EvalOpts -- ^ How to evaluate things
-         -> Type -- ^ The type of the function for which tests are to be generated
+         -> [Gen g Bool BV Integer] -- ^ Generators for the function arguments
          -> Value -- ^ The function itself
          -> Int -- ^ How many tests?
          -> IO [([Value], Value)] -- ^ A list of pairs of random arguments and computed outputs
-returnTests g evo ty fun num =
-    case argGens ty of
-      Nothing -> panic "Cryptol.Testing.Random" ["Can't generate test inputs for type", show (pp ty)]
-      Just args ->
-        do go args g 0
+returnTests g evo gens fun num = go gens g 0
   where
     go args g0 n
       | n >= num = return []
@@ -94,12 +86,19 @@ returnTests g evo ty fun num =
            more <- go args g1 (n + 1)
            return ((inputs, output) : more)
 
-    argGens t =
-      case tNoUser t of
-        TCon (TC TCFun) [t1, t2] ->
-          (:) <$> randomValue t1 <*> argGens t2
-        _ -> pure []
-
+{- | Given a (function) type, compute generators for the function's
+arguments. This is like @testableType@, but allows the result to be
+any finite type instead of just @Bit@. -}
+dumpableType :: forall g. RandomGen g => Type -> Maybe [Gen g Bool BV Integer]
+dumpableType ty =
+  case tIsFun ty of
+    Just (t1, t2) ->
+      do g  <- randomValue t1
+         as <- testableType t2
+         return (g : as)
+    Nothing ->
+      do (_ :: Gen g Bool BV Integer) <- randomValue ty
+         return []
 
 {- | Given a (function) type, compute generators for
 the function's arguments. Currently we do not support polymorphic functions.