    -- |
    -- Module      :  Cryptol.Testing.Random
    -- Copyright   :  (c) 2013-2016 Galois, Inc.
    -- License     :  BSD3
    -- Maintainer  :  cryptol@galois.com
    -- Stability   :  provisional
    -- Portability :  portable
    --
    -- This module generates random values for Cryptol types.

    {-# LANGUAGE BangPatterns #-}
    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE MultiWayIf #-}
    {-# LANGUAGE RecordWildCards #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE Trustworthy #-}
    {-# LANGUAGE TypeFamilies #-}
    module Cryptol.Testing.Random
    ( Gen
    , randomValue
    , dumpableType
    , testableType
    , TestResult(..)
    , isPass
    , returnTests
    , returnTests'
    , exhaustiveTests
    , randomTests
    , randomTests'
    ) where

    import qualified Control.Exception as X
    import Control.Monad          (liftM2)
    import Control.Monad.IO.Class (MonadIO(..))
    import Data.Bits
    import Data.List              (unfoldr, genericTake, genericIndex, genericReplicate)
    import qualified Data.Sequence as Seq

    import System.Random.TF.Gen
    import System.Random.TF.Instances

    import Cryptol.Backend        (Backend(..), SRational(..))
    import Cryptol.Backend.FloatHelpers (floatFromBits)
    import Cryptol.Backend.Monad  (runEval,Eval,EvalErrorEx(..))
    import Cryptol.Backend.Concrete
    import Cryptol.Backend.SeqMap (indexSeqMap, finiteSeqMap)
    import Cryptol.Backend.WordValue (wordVal)

    import Cryptol.Eval.Type      (TValue(..))
    import Cryptol.Eval.Value     (GenValue(..), ppValue, defaultPPOpts, fromVFun)
    import Cryptol.TypeCheck.Solver.InfNat (widthInteger)
    import Cryptol.Utils.Ident    (Ident)
    import Cryptol.Utils.Panic    (panic)
    import Cryptol.Utils.RecordMap

    type Gen g x = Integer -> g -> (SEval x (GenValue x), g)

    type Value = GenValue Concrete

    {- | Apply a testable value to some randomly-generated arguments.
         Returns @Nothing@ if the function returned @True@, or
         @Just counterexample@ if it returned @False@.

        Please note that this function assumes that the generators match
        the supplied value, otherwise we'll panic.
     -}
    runOneTest :: RandomGen g
            => Value   -- ^ Function under test
            -> [Gen g Concrete] -- ^ Argument generators
            -> Integer -- ^ Size
            -> g
            -> IO (TestResult, g)
    runOneTest :: forall g.
    RandomGen g =>
    Value -> [Gen g Concrete] -> Integer -> g -> IO (TestResult, g)
    runOneTest Value
    fun [Gen g Concrete]
    argGens Integer
    sz g
    g0 = do
      let ([Eval Value]
    args, g
    g1) = ((Integer -> g -> (Eval Value, g))
     -> ([Eval Value], g) -> ([Eval Value], g))
    -> ([Eval Value], g)
    -> [Integer -> g -> (Eval Value, g)]
    -> ([Eval Value], g)
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (Integer -> g -> (Eval Value, g))
    -> ([Eval Value], g) -> ([Eval Value], g)
    mkArg ([], g
    g0) [Integer -> g -> (Eval Value, g)]
    [Gen g Concrete]
    argGens
          mkArg :: (Integer -> g -> (Eval Value, g))
    -> ([Eval Value], g) -> ([Eval Value], g)
    mkArg Integer -> g -> (Eval Value, g)
    argGen ([Eval Value]
    as, g
    g) = let (Eval Value
    a, g
    g') = Integer -> g -> (Eval Value, g)
    argGen Integer
    sz g
    g in (Eval Value
    aEval Value -> [Eval Value] -> [Eval Value]
    forall a. a -> [a] -> [a]
    :[Eval Value]
    as, g
    g')
      [Value]
    args' <- CallStack -> Eval [Value] -> IO [Value]
    forall a. CallStack -> Eval a -> IO a
    runEval CallStack
    forall a. Monoid a => a
    mempty ([Eval Value] -> Eval [Value]
    forall (t :: * -> *) (m :: * -> *) a.
    (Traversable t, Monad m) =>
    t (m a) -> m (t a)
    forall (m :: * -> *) a. Monad m => [m a] -> m [a]
    sequence [Eval Value]
    args)
      TestResult
    result <- Value -> [Value] -> IO TestResult
    evalTest Value
    fun [Value]
    args'
      (TestResult, g) -> IO (TestResult, g)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TestResult
    result, g
    g1)

    returnOneTest :: RandomGen g
               => Value    -- ^ Function to be used to calculate tests
               -> [Gen g Concrete] -- ^ Argument generators
               -> Integer -- ^ Size
               -> g -- ^ Initial random state
               -> IO ([Value], Value, g) -- ^ Arguments, result, and new random state
    returnOneTest :: forall g.
    RandomGen g =>
    Value -> [Gen g Concrete] -> Integer -> g -> IO ([Value], Value, g)
    returnOneTest Value
    fun [Gen g Concrete]
    argGens Integer
    sz g
    g0 =
      do let ([Eval Value]
    args, g
    g1) = ((Integer -> g -> (Eval Value, g))
     -> ([Eval Value], g) -> ([Eval Value], g))
    -> ([Eval Value], g)
    -> [Integer -> g -> (Eval Value, g)]
    -> ([Eval Value], g)
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (Integer -> g -> (Eval Value, g))
    -> ([Eval Value], g) -> ([Eval Value], g)
    mkArg ([], g
    g0) [Integer -> g -> (Eval Value, g)]
    [Gen g Concrete]
    argGens
             mkArg :: (Integer -> g -> (Eval Value, g))
    -> ([Eval Value], g) -> ([Eval Value], g)
    mkArg Integer -> g -> (Eval Value, g)
    argGen ([Eval Value]
    as, g
    g) = let (Eval Value
    a, g
    g') = Integer -> g -> (Eval Value, g)
    argGen Integer
    sz g
    g in (Eval Value
    aEval Value -> [Eval Value] -> [Eval Value]
    forall a. a -> [a] -> [a]
    :[Eval Value]
    as, g
    g')
         [Value]
    args' <- CallStack -> Eval [Value] -> IO [Value]
    forall a. CallStack -> Eval a -> IO a
    runEval CallStack
    forall a. Monoid a => a
    mempty ([Eval Value] -> Eval [Value]
    forall (t :: * -> *) (m :: * -> *) a.
    (Traversable t, Monad m) =>
    t (m a) -> m (t a)
    forall (m :: * -> *) a. Monad m => [m a] -> m [a]
    sequence [Eval Value]
    args)
         Value
    result <- CallStack -> Eval Value -> IO Value
    forall a. CallStack -> Eval a -> IO a
    runEval CallStack
    forall a. Monoid a => a
    mempty (Value -> [Value] -> Eval Value
    go Value
    fun [Value]
    args')
         ([Value], Value, g) -> IO ([Value], Value, g)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Value]
    args', Value
    result, g
    g1)
       where
         go :: Value -> [Value] -> Eval Value
    go f :: Value
    f@VFun{} (Value
    v : [Value]
    vs) =
           do Value
    f' <- Concrete -> Value -> SEval Concrete Value -> SEval Concrete Value
    forall sym.
    Backend sym =>
    sym
    -> GenValue sym
    -> SEval sym (GenValue sym)
    -> SEval sym (GenValue sym)
    fromVFun Concrete
    Concrete Value
    f (Value -> Eval Value
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Value
    v)
              Value -> [Value] -> Eval Value
    go Value
    f' [Value]
    vs
         go VFun{} [] = String -> [String] -> Eval Value
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "Cryptol.Testing.Random" [String
    "Not enough arguments to function while generating tests"]
         go Value
    _ (Value
    _ : [Value]
    _) = String -> [String] -> Eval Value
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "Cryptol.Testing.Random" [String
    "Too many arguments to function while generating tests"]
         go Value
    v [] = Value -> Eval Value
    forall a. a -> Eval a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Value
    v

    returnTests :: RandomGen g
             => g -- ^ The random generator state
             -> [Gen g Concrete] -- ^ 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
                                           --   as well as the new state of the RNG
    returnTests :: forall g.
    RandomGen g =>
    g -> [Gen g Concrete] -> Value -> Int -> IO [([Value], Value)]
    returnTests g
    g [Gen g Concrete]
    gens Value
    fun Int
    num = ([([Value], Value)], g) -> [([Value], Value)]
    forall a b. (a, b) -> a
    fst (([([Value], Value)], g) -> [([Value], Value)])
    -> IO ([([Value], Value)], g) -> IO [([Value], Value)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> g -> [Gen g Concrete] -> Value -> Int -> IO ([([Value], Value)], g)
    forall g.
    RandomGen g =>
    g -> [Gen g Concrete] -> Value -> Int -> IO ([([Value], Value)], g)
    returnTests' g
    g [Gen g Concrete]
    gens Value
    fun Int
    num

    -- | Return a collection of random tests.
    returnTests' :: RandomGen g
             => g -- ^ The random generator state
             -> [Gen g Concrete] -- ^ Generators for the function arguments
             -> Value -- ^ The function itself
             -> Int -- ^ How many tests?
             -> IO ([([Value], Value)], g) -- ^ A list of pairs of random arguments and computed outputs
                                           --   as well as the new state of the RNG
    returnTests' :: forall g.
    RandomGen g =>
    g -> [Gen g Concrete] -> Value -> Int -> IO ([([Value], Value)], g)
    returnTests' g
    g [Gen g Concrete]
    gens Value
    fun Int
    num = [Integer -> g -> (Eval Value, g)]
    -> g -> Int -> IO ([([Value], Value)], g)
    go [Integer -> g -> (Eval Value, g)]
    [Gen g Concrete]
    gens g
    g Int
    0
      where
        go :: [Integer -> g -> (Eval Value, g)]
    -> g -> Int -> IO ([([Value], Value)], g)
    go [Integer -> g -> (Eval Value, g)]
    args g
    g0 Int
    n
          | Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    num = ([([Value], Value)], g) -> IO ([([Value], Value)], g)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([], g
    g0)
          | Bool
    otherwise =
            do let sz :: Integer
    sz = Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger (Int -> Int -> Int
    forall a. Integral a => a -> a -> a
    div (Int
    100 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    * (Int
    1 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    n)) Int
    num)
               ([Value]
    inputs, Value
    output, g
    g1) <- Value -> [Gen g Concrete] -> Integer -> g -> IO ([Value], Value, g)
    forall g.
    RandomGen g =>
    Value -> [Gen g Concrete] -> Integer -> g -> IO ([Value], Value, g)
    returnOneTest Value
    fun [Integer -> g -> (Eval Value, g)]
    [Gen g Concrete]
    args Integer
    sz g
    g0
               ([([Value], Value)]
    more, g
    g2) <- [Integer -> g -> (Eval Value, g)]
    -> g -> Int -> IO ([([Value], Value)], g)
    go [Integer -> g -> (Eval Value, g)]
    args g
    g1 (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1)
               ([([Value], Value)], g) -> IO ([([Value], Value)], g)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (([Value]
    inputs, Value
    output) ([Value], Value) -> [([Value], Value)] -> [([Value], Value)]
    forall a. a -> [a] -> [a]
    : [([Value], Value)]
    more, g
    g2)

    {- | Given a (function) type, compute generators for the function's
    arguments. -}
    dumpableType :: forall g. RandomGen g => TValue -> Maybe [Gen g Concrete]
    dumpableType :: forall g. RandomGen g => TValue -> Maybe [Gen g Concrete]
    dumpableType (TVFun TValue
    t1 TValue
    t2) =
       do Integer -> g -> (Eval Value, g)
    g  <- Concrete -> TValue -> Maybe (Gen g Concrete)
    forall sym g.
    (Backend sym, RandomGen g) =>
    sym -> TValue -> Maybe (Gen g sym)
    randomValue Concrete
    Concrete TValue
    t1
          [Integer -> g -> (Eval Value, g)]
    as <- TValue -> Maybe [Gen g Concrete]
    forall g. RandomGen g => TValue -> Maybe [Gen g Concrete]
    dumpableType TValue
    t2
          [Integer -> g -> (Eval Value, g)]
    -> Maybe [Integer -> g -> (Eval Value, g)]
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Integer -> g -> (Eval Value, g)
    g (Integer -> g -> (Eval Value, g))
    -> [Integer -> g -> (Eval Value, g)]
    -> [Integer -> g -> (Eval Value, g)]
    forall a. a -> [a] -> [a]
    : [Integer -> g -> (Eval Value, g)]
    as)
    dumpableType TValue
    ty =
       do (Gen g Concrete
    _ :: Gen g Concrete) <- Concrete -> TValue -> Maybe (Gen g Concrete)
    forall sym g.
    (Backend sym, RandomGen g) =>
    sym -> TValue -> Maybe (Gen g sym)
    randomValue Concrete
    Concrete TValue
    ty
          [Integer -> g -> (Eval Value, g)]
    -> Maybe [Integer -> g -> (Eval Value, g)]
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []

    {-# SPECIALIZE randomValue ::
      RandomGen g => Concrete -> TValue -> Maybe (Gen g Concrete)
      #-}

    {- | A generator for values of the given type.  This fails if we are
    given a type that lacks a suitable random value generator. -}
    randomValue :: (Backend sym, RandomGen g) => sym -> TValue -> Maybe (Gen g sym)
    randomValue :: forall sym g.
    (Backend sym, RandomGen g) =>
    sym -> TValue -> Maybe (Gen g sym)
    randomValue sym
    sym TValue
    ty =
      case TValue
    ty of
        TValue
    TVBit         -> Gen g sym -> Maybe (Gen g sym)
    forall a. a -> Maybe a
    Just (sym -> Gen g sym
    forall sym g. (Backend sym, RandomGen g) => sym -> Gen g sym
    randomBit sym
    sym)
        TValue
    TVInteger     -> Gen g sym -> Maybe (Gen g sym)
    forall a. a -> Maybe a
    Just (sym -> Gen g sym
    forall sym g. (Backend sym, RandomGen g) => sym -> Gen g sym
    randomInteger sym
    sym)
        TValue
    TVRational    -> Gen g sym -> Maybe (Gen g sym)
    forall a. a -> Maybe a
    Just (sym -> Gen g sym
    forall sym g. (Backend sym, RandomGen g) => sym -> Gen g sym
    randomRational sym
    sym)
        TVIntMod Integer
    m    -> Gen g sym -> Maybe (Gen g sym)
    forall a. a -> Maybe a
    Just (sym -> Integer -> Gen g sym
    forall sym g.
    (Backend sym, RandomGen g) =>
    sym -> Integer -> Gen g sym
    randomIntMod sym
    sym Integer
    m)
        TVFloat Integer
    e Integer
    p   -> Gen g sym -> Maybe (Gen g sym)
    forall a. a -> Maybe a
    Just (sym -> Integer -> Integer -> Gen g sym
    forall sym g.
    (Backend sym, RandomGen g) =>
    sym -> Integer -> Integer -> Gen g sym
    randomFloat sym
    sym Integer
    e Integer
    p)
        TVSeq Integer
    n TValue
    TVBit -> Gen g sym -> Maybe (Gen g sym)
    forall a. a -> Maybe a
    Just (sym -> Integer -> Gen g sym
    forall sym g.
    (Backend sym, RandomGen g) =>
    sym -> Integer -> Gen g sym
    randomWord sym
    sym Integer
    n)
        TVSeq Integer
    n TValue
    el ->
             do Gen g sym
    mk <- sym -> TValue -> Maybe (Gen g sym)
    forall sym g.
    (Backend sym, RandomGen g) =>
    sym -> TValue -> Maybe (Gen g sym)
    randomValue sym
    sym TValue
    el
                Gen g sym -> Maybe (Gen g sym)
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Integer -> Gen g sym -> Gen g sym
    forall sym g.
    (Backend sym, RandomGen g) =>
    Integer -> Gen g sym -> Gen g sym
    randomSequence Integer
    n Gen g sym
    mk)
        TVStream TValue
    el  ->
             do Gen g sym
    mk <- sym -> TValue -> Maybe (Gen g sym)
    forall sym g.
    (Backend sym, RandomGen g) =>
    sym -> TValue -> Maybe (Gen g sym)
    randomValue sym
    sym TValue
    el
                Gen g sym -> Maybe (Gen g sym)
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Gen g sym -> Gen g sym
    forall sym g. (Backend sym, RandomGen g) => Gen g sym -> Gen g sym
    randomStream Gen g sym
    mk)
        TVTuple [TValue]
    els ->
             do [Gen g sym]
    mks <- (TValue -> Maybe (Gen g sym)) -> [TValue] -> Maybe [Gen g sym]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (sym -> TValue -> Maybe (Gen g sym)
    forall sym g.
    (Backend sym, RandomGen g) =>
    sym -> TValue -> Maybe (Gen g sym)
    randomValue sym
    sym) [TValue]
    els
                Gen g sym -> Maybe (Gen g sym)
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Gen g sym] -> Gen g sym
    forall sym g.
    (Backend sym, RandomGen g) =>
    [Gen g sym] -> Gen g sym
    randomTuple [Gen g sym]
    mks)
        TVRec RecordMap Ident TValue
    fs ->
             do RecordMap Ident (Gen g sym)
    gs <- (TValue -> Maybe (Gen g sym))
    -> RecordMap Ident TValue -> Maybe (RecordMap Ident (Gen g sym))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> RecordMap Ident a -> f (RecordMap Ident b)
    traverse (sym -> TValue -> Maybe (Gen g sym)
    forall sym g.
    (Backend sym, RandomGen g) =>
    sym -> TValue -> Maybe (Gen g sym)
    randomValue sym
    sym) RecordMap Ident TValue
    fs
                Gen g sym -> Maybe (Gen g sym)
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (RecordMap Ident (Gen g sym) -> Gen g sym
    forall sym g.
    (Backend sym, RandomGen g) =>
    RecordMap Ident (Gen g sym) -> Gen g sym
    randomRecord RecordMap Ident (Gen g sym)
    gs)
        TVNewtype Newtype
    _ [Either Nat' TValue]
    _ RecordMap Ident TValue
    fs ->
             do RecordMap Ident (Gen g sym)
    gs <- (TValue -> Maybe (Gen g sym))
    -> RecordMap Ident TValue -> Maybe (RecordMap Ident (Gen g sym))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> RecordMap Ident a -> f (RecordMap Ident b)
    traverse (sym -> TValue -> Maybe (Gen g sym)
    forall sym g.
    (Backend sym, RandomGen g) =>
    sym -> TValue -> Maybe (Gen g sym)
    randomValue sym
    sym) RecordMap Ident TValue
    fs
                Gen g sym -> Maybe (Gen g sym)
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (RecordMap Ident (Gen g sym) -> Gen g sym
    forall sym g.
    (Backend sym, RandomGen g) =>
    RecordMap Ident (Gen g sym) -> Gen g sym
    randomRecord RecordMap Ident (Gen g sym)
    gs)
        TVArray{} -> Maybe (Gen g sym)
    forall a. Maybe a
    Nothing
        TVFun{} -> Maybe (Gen g sym)
    forall a. Maybe a
    Nothing
        TVAbstract{} -> Maybe (Gen g sym)
    forall a. Maybe a
    Nothing

    {-# INLINE randomBit #-}

    -- | Generate a random bit value.
    randomBit :: (Backend sym, RandomGen g) => sym -> Gen g sym
    randomBit :: forall sym g. (Backend sym, RandomGen g) => sym -> Gen g sym
    randomBit sym
    sym Integer
    _ g
    g =
      let (Bool
    b,g
    g1) = g -> (Bool, g)
    forall g. RandomGen g => g -> (Bool, g)
    forall a g. (Random a, RandomGen g) => g -> (a, g)
    random g
    g
      in (GenValue sym -> SEval sym (GenValue sym)
    forall a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SBit sym -> GenValue sym
    forall sym. SBit sym -> GenValue sym
    VBit (sym -> Bool -> SBit sym
    forall sym. Backend sym => sym -> Bool -> SBit sym
    bitLit sym
    sym Bool
    b)), g
    g1)

    {-# INLINE randomSize #-}

    randomSize :: RandomGen g => Int -> Int -> g -> (Int, g)
    randomSize :: forall g. RandomGen g => Int -> Int -> g -> (Int, g)
    randomSize Int
    k Int
    n g
    g
      | Int
    p Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    1 = (Int
    n, g
    g')
      | Bool
    otherwise = Int -> Int -> g -> (Int, g)
    forall g. RandomGen g => Int -> Int -> g -> (Int, g)
    randomSize Int
    k (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1) g
    g'
      where (Int
    p, g
    g') = (Int, Int) -> g -> (Int, g)
    forall g. RandomGen g => (Int, Int) -> g -> (Int, g)
    forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
    randomR (Int
    1, Int
    k) g
    g

    {-# INLINE randomInteger #-}

    -- | Generate a random integer value. The size parameter is assumed to
    -- vary between 1 and 100, and we use it to generate smaller numbers
    -- first.
    randomInteger :: (Backend sym, RandomGen g) => sym -> Gen g sym
    randomInteger :: forall sym g. (Backend sym, RandomGen g) => sym -> Gen g sym
    randomInteger sym
    sym Integer
    w g
    g =
      let (Int
    n, g
    g1) = if Integer
    w Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    100 then (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    w, g
    g) else Int -> Int -> g -> (Int, g)
    forall g. RandomGen g => Int -> Int -> g -> (Int, g)
    randomSize Int
    8 Int
    100 g
    g
          (Integer
    i, g
    g2) = (Integer, Integer) -> g -> (Integer, g)
    forall g. RandomGen g => (Integer, Integer) -> g -> (Integer, g)
    forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
    randomR (- Integer
    256Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^Int
    n, Integer
    256Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^Int
    n) g
    g1
      in (SInteger sym -> GenValue sym
    forall sym. SInteger sym -> GenValue sym
    VInteger (SInteger sym -> GenValue sym)
    -> SEval sym (SInteger sym) -> SEval sym (GenValue sym)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> Integer -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> Integer -> SEval sym (SInteger sym)
    integerLit sym
    sym Integer
    i, g
    g2)

    {-# INLINE randomIntMod #-}

    randomIntMod :: (Backend sym, RandomGen g) => sym -> Integer -> Gen g sym
    randomIntMod :: forall sym g.
    (Backend sym, RandomGen g) =>
    sym -> Integer -> Gen g sym
    randomIntMod sym
    sym Integer
    modulus Integer
    _ g
    g =
      let (Integer
    i, g
    g') = (Integer, Integer) -> g -> (Integer, g)
    forall g. RandomGen g => (Integer, Integer) -> g -> (Integer, g)
    forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
    randomR (Integer
    0, Integer
    modulusInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1) g
    g
      in (SInteger sym -> GenValue sym
    forall sym. SInteger sym -> GenValue sym
    VInteger (SInteger sym -> GenValue sym)
    -> SEval sym (SInteger sym) -> SEval sym (GenValue sym)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> Integer -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> Integer -> SEval sym (SInteger sym)
    integerLit sym
    sym Integer
    i, g
    g')

    {-# INLINE randomRational #-}

    randomRational :: (Backend sym, RandomGen g) => sym -> Gen g sym
    randomRational :: forall sym g. (Backend sym, RandomGen g) => sym -> Gen g sym
    randomRational sym
    sym Integer
    w g
    g =
      let (Int
    sz, g
    g1) = if Integer
    w Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    100 then (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    w, g
    g) else Int -> Int -> g -> (Int, g)
    forall g. RandomGen g => Int -> Int -> g -> (Int, g)
    randomSize Int
    8 Int
    100 g
    g
          (Integer
    n, g
    g2) = (Integer, Integer) -> g -> (Integer, g)
    forall g. RandomGen g => (Integer, Integer) -> g -> (Integer, g)
    forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
    randomR (- Integer
    256Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^Int
    sz, Integer
    256Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^Int
    sz) g
    g1
          (Integer
    d, g
    g3) = (Integer, Integer) -> g -> (Integer, g)
    forall g. RandomGen g => (Integer, Integer) -> g -> (Integer, g)
    forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
    randomR ( Integer
    1, Integer
    256Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^Int
    sz) g
    g2
       in (do SInteger sym
    n' <- sym -> Integer -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> Integer -> SEval sym (SInteger sym)
    integerLit sym
    sym Integer
    n
              SInteger sym
    d' <- sym -> Integer -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> Integer -> SEval sym (SInteger sym)
    integerLit sym
    sym Integer
    d
              GenValue sym -> SEval sym (GenValue sym)
    forall a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SRational sym -> GenValue sym
    forall sym. SRational sym -> GenValue sym
    VRational (SInteger sym -> SInteger sym -> SRational sym
    forall sym. SInteger sym -> SInteger sym -> SRational sym
    SRational SInteger sym
    n' SInteger sym
    d'))
           , g
    g3)

    {-# INLINE randomWord #-}

    -- | 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.
    randomWord :: (Backend sym, RandomGen g) => sym -> Integer -> Gen g sym
    randomWord :: forall sym g.
    (Backend sym, RandomGen g) =>
    sym -> Integer -> Gen g sym
    randomWord sym
    sym Integer
    w Integer
    _sz g
    g =
       let (Integer
    val, g
    g1) = (Integer, Integer) -> g -> (Integer, g)
    forall g. RandomGen g => (Integer, Integer) -> g -> (Integer, g)
    forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
    randomR (Integer
    0,Integer
    2Integer -> Integer -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^Integer
    wInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1) g
    g
       in (Integer -> WordValue sym -> GenValue sym
    forall sym. Integer -> WordValue sym -> GenValue sym
    VWord Integer
    w (WordValue sym -> GenValue sym)
    -> (SWord sym -> WordValue sym) -> SWord sym -> GenValue sym
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SWord sym -> WordValue sym
    forall sym. SWord sym -> WordValue sym
    wordVal (SWord sym -> GenValue sym)
    -> SEval sym (SWord sym) -> SEval sym (GenValue sym)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> Integer -> Integer -> SEval sym (SWord sym)
    forall sym.
    Backend sym =>
    sym -> Integer -> Integer -> SEval sym (SWord sym)
    wordLit sym
    sym Integer
    w Integer
    val, g
    g1)

    {-# INLINE randomStream #-}

    -- | Generate a random infinite stream value.
    randomStream :: (Backend sym, RandomGen g) => Gen g sym -> Gen g sym
    randomStream :: forall sym g. (Backend sym, RandomGen g) => Gen g sym -> Gen g sym
    randomStream Gen g sym
    mkElem Integer
    sz g
    g =
      let (g
    g1,g
    g2) = g -> (g, g)
    forall g. RandomGen g => g -> (g, g)
    split g
    g
      in (GenValue sym -> SEval sym (GenValue sym)
    forall a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (GenValue sym -> SEval sym (GenValue sym))
    -> GenValue sym -> SEval sym (GenValue sym)
    forall a b. (a -> b) -> a -> b
    $ SeqMap sym (GenValue sym) -> GenValue sym
    forall sym. SeqMap sym (GenValue sym) -> GenValue sym
    VStream (SeqMap sym (GenValue sym) -> GenValue sym)
    -> SeqMap sym (GenValue sym) -> GenValue sym
    forall a b. (a -> b) -> a -> b
    $ (Integer -> SEval sym (GenValue sym)) -> SeqMap sym (GenValue sym)
    forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
    indexSeqMap ((Integer -> SEval sym (GenValue sym))
     -> SeqMap sym (GenValue sym))
    -> (Integer -> SEval sym (GenValue sym))
    -> SeqMap sym (GenValue sym)
    forall a b. (a -> b) -> a -> b
    $ [SEval sym (GenValue sym)] -> Integer -> SEval sym (GenValue sym)
    forall i a. Integral i => [a] -> i -> a
    genericIndex ((g -> Maybe (SEval sym (GenValue sym), g))
    -> g -> [SEval sym (GenValue sym)]
    forall b a. (b -> Maybe (a, b)) -> b -> [a]
    unfoldr ((SEval sym (GenValue sym), g)
    -> Maybe (SEval sym (GenValue sym), g)
    forall a. a -> Maybe a
    Just ((SEval sym (GenValue sym), g)
     -> Maybe (SEval sym (GenValue sym), g))
    -> (g -> (SEval sym (GenValue sym), g))
    -> g
    -> Maybe (SEval sym (GenValue sym), g)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Gen g sym
    mkElem Integer
    sz) g
    g1), g
    g2)

    {-# INLINE randomSequence #-}

    {- | Generate a random sequence.  This should be used for sequences
    other than bits.  For sequences of bits use "randomWord". -}
    randomSequence :: (Backend sym, RandomGen g) => Integer -> Gen g sym -> Gen g sym
    randomSequence :: forall sym g.
    (Backend sym, RandomGen g) =>
    Integer -> Gen g sym -> Gen g sym
    randomSequence Integer
    w Gen g sym
    mkElem Integer
    sz g
    g0 = do
      let (g
    g1,g
    g2) = g -> (g, g)
    forall g. RandomGen g => g -> (g, g)
    split g
    g0
      let f :: g -> Maybe (SEval sym (GenValue sym), g)
    f g
    g = let (SEval sym (GenValue sym)
    x,g
    g') = Gen g sym
    mkElem Integer
    sz g
    g
                 in SEval sym (GenValue sym)
    -> Maybe (SEval sym (GenValue sym), g)
    -> Maybe (SEval sym (GenValue sym), g)
    forall a b. a -> b -> b
    seq SEval sym (GenValue sym)
    x ((SEval sym (GenValue sym), g)
    -> Maybe (SEval sym (GenValue sym), g)
    forall a. a -> Maybe a
    Just (SEval sym (GenValue sym)
    x, g
    g'))
      let xs :: Seq (SEval sym (GenValue sym))
    xs = [SEval sym (GenValue sym)] -> Seq (SEval sym (GenValue sym))
    forall a. [a] -> Seq a
    Seq.fromList ([SEval sym (GenValue sym)] -> Seq (SEval sym (GenValue sym)))
    -> [SEval sym (GenValue sym)] -> Seq (SEval sym (GenValue sym))
    forall a b. (a -> b) -> a -> b
    $ Integer -> [SEval sym (GenValue sym)] -> [SEval sym (GenValue sym)]
    forall i a. Integral i => i -> [a] -> [a]
    genericTake Integer
    w ([SEval sym (GenValue sym)] -> [SEval sym (GenValue sym)])
    -> [SEval sym (GenValue sym)] -> [SEval sym (GenValue sym)]
    forall a b. (a -> b) -> a -> b
    $ (g -> Maybe (SEval sym (GenValue sym), g))
    -> g -> [SEval sym (GenValue sym)]
    forall b a. (b -> Maybe (a, b)) -> b -> [a]
    unfoldr g -> Maybe (SEval sym (GenValue sym), g)
    f g
    g1
      let v :: GenValue sym
    v  = Integer -> SeqMap sym (GenValue sym) -> GenValue sym
    forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
    VSeq Integer
    w (SeqMap sym (GenValue sym) -> GenValue sym)
    -> SeqMap sym (GenValue sym) -> GenValue sym
    forall a b. (a -> b) -> a -> b
    $ (Integer -> SEval sym (GenValue sym)) -> SeqMap sym (GenValue sym)
    forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
    indexSeqMap ((Integer -> SEval sym (GenValue sym))
     -> SeqMap sym (GenValue sym))
    -> (Integer -> SEval sym (GenValue sym))
    -> SeqMap sym (GenValue sym)
    forall a b. (a -> b) -> a -> b
    $ \Integer
    i -> Seq (SEval sym (GenValue sym)) -> Int -> SEval sym (GenValue sym)
    forall a. Seq a -> Int -> a
    Seq.index Seq (SEval sym (GenValue sym))
    xs (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    i)
      Seq (SEval sym (GenValue sym))
    -> (SEval sym (GenValue sym), g) -> (SEval sym (GenValue sym), g)
    forall a b. a -> b -> b
    seq Seq (SEval sym (GenValue sym))
    xs (GenValue sym -> SEval sym (GenValue sym)
    forall a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure GenValue sym
    v, g
    g2)

    {-# INLINE randomTuple #-}

    -- | Generate a random tuple value.
    randomTuple :: (Backend sym, RandomGen g) => [Gen g sym] -> Gen g sym
    randomTuple :: forall sym g.
    (Backend sym, RandomGen g) =>
    [Gen g sym] -> Gen g sym
    randomTuple [Gen g sym]
    gens Integer
    sz = [SEval sym (GenValue sym)]
    -> [Gen g sym] -> g -> (SEval sym (GenValue sym), g)
    go [] [Gen g sym]
    gens
      where
      go :: [SEval sym (GenValue sym)]
    -> [Gen g sym] -> g -> (SEval sym (GenValue sym), g)
    go [SEval sym (GenValue sym)]
    els [] g
    g = (GenValue sym -> SEval sym (GenValue sym)
    forall a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (GenValue sym -> SEval sym (GenValue sym))
    -> GenValue sym -> SEval sym (GenValue sym)
    forall a b. (a -> b) -> a -> b
    $ [SEval sym (GenValue sym)] -> GenValue sym
    forall sym. [SEval sym (GenValue sym)] -> GenValue sym
    VTuple ([SEval sym (GenValue sym)] -> [SEval sym (GenValue sym)]
    forall a. [a] -> [a]
    reverse [SEval sym (GenValue sym)]
    els), g
    g)
      go [SEval sym (GenValue sym)]
    els (Gen g sym
    mkElem : [Gen g sym]
    more) g
    g =
        let (SEval sym (GenValue sym)
    v, g
    g1) = Gen g sym
    mkElem Integer
    sz g
    g
        in SEval sym (GenValue sym)
    -> (SEval sym (GenValue sym), g) -> (SEval sym (GenValue sym), g)
    forall a b. a -> b -> b
    seq SEval sym (GenValue sym)
    v ([SEval sym (GenValue sym)]
    -> [Gen g sym] -> g -> (SEval sym (GenValue sym), g)
    go (SEval sym (GenValue sym)
    v SEval sym (GenValue sym)
    -> [SEval sym (GenValue sym)] -> [SEval sym (GenValue sym)]
    forall a. a -> [a] -> [a]
    : [SEval sym (GenValue sym)]
    els) [Gen g sym]
    more g
    g1)

    {-# INLINE randomRecord #-}

    -- | Generate a random record value.
    randomRecord :: (Backend sym, RandomGen g) => RecordMap Ident (Gen g sym) -> Gen g sym
    randomRecord :: forall sym g.
    (Backend sym, RandomGen g) =>
    RecordMap Ident (Gen g sym) -> Gen g sym
    randomRecord RecordMap Ident (Gen g sym)
    gens Integer
    sz g
    g0 =
      let (g
    g', RecordMap Ident (SEval sym (GenValue sym))
    m) = (g -> Gen g sym -> (g, SEval sym (GenValue sym)))
    -> g
    -> RecordMap Ident (Gen g sym)
    -> (g, RecordMap Ident (SEval sym (GenValue sym)))
    forall a b c k.
    (a -> b -> (a, c)) -> a -> RecordMap k b -> (a, RecordMap k c)
    recordMapAccum g -> Gen g sym -> (g, SEval sym (GenValue sym))
    mk g
    g0 RecordMap Ident (Gen g sym)
    gens in (GenValue sym -> SEval sym (GenValue sym)
    forall a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (GenValue sym -> SEval sym (GenValue sym))
    -> GenValue sym -> SEval sym (GenValue sym)
    forall a b. (a -> b) -> a -> b
    $ RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
    forall sym.
    RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
    VRecord RecordMap Ident (SEval sym (GenValue sym))
    m, g
    g')
      where
        mk :: g -> Gen g sym -> (g, SEval sym (GenValue sym))
    mk g
    g Gen g sym
    gen =
          let (SEval sym (GenValue sym)
    v, g
    g') = Gen g sym
    gen Integer
    sz g
    g
          in SEval sym (GenValue sym)
    -> (g, SEval sym (GenValue sym)) -> (g, SEval sym (GenValue sym))
    forall a b. a -> b -> b
    seq SEval sym (GenValue sym)
    v (g
    g', SEval sym (GenValue sym)
    v)

    randomFloat ::
      (Backend sym, RandomGen g) =>
      sym ->
      Integer {- ^ Exponent width -} ->
      Integer {- ^ Precision width -} ->
      Gen g sym
    randomFloat :: forall sym g.
    (Backend sym, RandomGen g) =>
    sym -> Integer -> Integer -> Gen g sym
    randomFloat sym
    sym Integer
    e Integer
    p Integer
    w g
    g0 =
        let sz :: Integer
    sz = Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    max Integer
    0 (Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    min Integer
    100 Integer
    w)
            ( Integer
    x, g
    g') = (Integer, Integer) -> g -> (Integer, g)
    forall g. RandomGen g => (Integer, Integer) -> g -> (Integer, g)
    forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
    randomR (Integer
    0, Integer
    10Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    *(Integer
    szInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +Integer
    1)) g
    g0
         in if | Integer
    x Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    2    -> (SFloat sym -> GenValue sym
    forall sym. SFloat sym -> GenValue sym
    VFloat (SFloat sym -> GenValue sym)
    -> SEval sym (SFloat sym) -> SEval sym (GenValue sym)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> Integer -> Integer -> SEval sym (SFloat sym)
    forall sym.
    Backend sym =>
    sym -> Integer -> Integer -> SEval sym (SFloat sym)
    fpNaN sym
    sym Integer
    e Integer
    p, g
    g')
               | Integer
    x Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    4    -> (SFloat sym -> GenValue sym
    forall sym. SFloat sym -> GenValue sym
    VFloat (SFloat sym -> GenValue sym)
    -> SEval sym (SFloat sym) -> SEval sym (GenValue sym)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> Integer -> Integer -> SEval sym (SFloat sym)
    forall sym.
    Backend sym =>
    sym -> Integer -> Integer -> SEval sym (SFloat sym)
    fpPosInf sym
    sym Integer
    e Integer
    p, g
    g')
               | Integer
    x Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    6    -> (SFloat sym -> GenValue sym
    forall sym. SFloat sym -> GenValue sym
    VFloat (SFloat sym -> GenValue sym)
    -> SEval sym (SFloat sym) -> SEval sym (GenValue sym)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (sym -> SFloat sym -> SEval sym (SFloat sym)
    forall sym.
    Backend sym =>
    sym -> SFloat sym -> SEval sym (SFloat sym)
    fpNeg sym
    sym (SFloat sym -> SEval sym (SFloat sym))
    -> SEval sym (SFloat sym) -> SEval sym (SFloat sym)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> Integer -> Integer -> SEval sym (SFloat sym)
    forall sym.
    Backend sym =>
    sym -> Integer -> Integer -> SEval sym (SFloat sym)
    fpPosInf sym
    sym Integer
    e Integer
    p), g
    g')
               | Integer
    x Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    8    -> (SFloat sym -> GenValue sym
    forall sym. SFloat sym -> GenValue sym
    VFloat (SFloat sym -> GenValue sym)
    -> SEval sym (SFloat sym) -> SEval sym (GenValue sym)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> Integer -> Integer -> Rational -> SEval sym (SFloat sym)
    forall sym.
    Backend sym =>
    sym -> Integer -> Integer -> Rational -> SEval sym (SFloat sym)
    fpLit sym
    sym Integer
    e Integer
    p Rational
    0, g
    g')
               | Integer
    x Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    10   -> (SFloat sym -> GenValue sym
    forall sym. SFloat sym -> GenValue sym
    VFloat (SFloat sym -> GenValue sym)
    -> SEval sym (SFloat sym) -> SEval sym (GenValue sym)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (sym -> SFloat sym -> SEval sym (SFloat sym)
    forall sym.
    Backend sym =>
    sym -> SFloat sym -> SEval sym (SFloat sym)
    fpNeg sym
    sym (SFloat sym -> SEval sym (SFloat sym))
    -> SEval sym (SFloat sym) -> SEval sym (SFloat sym)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> Integer -> Integer -> Rational -> SEval sym (SFloat sym)
    forall sym.
    Backend sym =>
    sym -> Integer -> Integer -> Rational -> SEval sym (SFloat sym)
    fpLit sym
    sym Integer
    e Integer
    p Rational
    0), g
    g')
               | Integer
    x Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    sz       -> g -> (SEval sym (GenValue sym), g)
    genSubnormal g
    g'  -- about 10% of the time
               | Integer
    x Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    4Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    *(Integer
    szInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +Integer
    1) -> g -> (SEval sym (GenValue sym), g)
    genBinary g
    g'     -- about 40%
               | Bool
    otherwise     -> Integer -> g -> (SEval sym (GenValue sym), g)
    genNormal (Integer -> Integer
    forall a. Integral a => a -> Integer
    toInteger Integer
    sz) g
    g'  -- remaining ~50%

      where
        emax :: Integer
    emax = Int -> Integer
    forall a. Bits a => Int -> a
    bit (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    e) Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1
        smax :: Integer
    smax = Int -> Integer
    forall a. Bits a => Int -> a
    bit (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    p) Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1

        -- generates floats uniformly chosen from among all bitpatterns
        genBinary :: g -> (SEval sym (GenValue sym), g)
    genBinary g
    g =
          let (Integer
    v, g
    g1) = (Integer, Integer) -> g -> (Integer, g)
    forall g. RandomGen g => (Integer, Integer) -> g -> (Integer, g)
    forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
    randomR (Integer
    0, Int -> Integer
    forall a. Bits a => Int -> a
    bit (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger (Integer
    eInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +Integer
    p)) Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1) g
    g
           in (SFloat sym -> GenValue sym
    forall sym. SFloat sym -> GenValue sym
    VFloat (SFloat sym -> GenValue sym)
    -> SEval sym (SFloat sym) -> SEval sym (GenValue sym)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (sym -> Integer -> Integer -> SWord sym -> SEval sym (SFloat sym)
    forall sym.
    Backend sym =>
    sym -> Integer -> Integer -> SWord sym -> SEval sym (SFloat sym)
    fpFromBits sym
    sym Integer
    e Integer
    p (SWord sym -> SEval sym (SFloat sym))
    -> SEval sym (SWord sym) -> SEval sym (SFloat sym)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> Integer -> Integer -> SEval sym (SWord sym)
    forall sym.
    Backend sym =>
    sym -> Integer -> Integer -> SEval sym (SWord sym)
    wordLit sym
    sym (Integer
    eInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +Integer
    p) Integer
    v), g
    g1)

        -- generates floats corresponding to subnormal values.  These are
        -- values with 0 biased exponent and nonzero mantissa.
        genSubnormal :: g -> (SEval sym (GenValue sym), g)
    genSubnormal g
    g =
          let (Bool
    sgn, g
    g1) = g -> (Bool, g)
    forall g. RandomGen g => g -> (Bool, g)
    forall a g. (Random a, RandomGen g) => g -> (a, g)
    random g
    g
              (Integer
    v, g
    g2)   = (Integer, Integer) -> g -> (Integer, g)
    forall g. RandomGen g => (Integer, Integer) -> g -> (Integer, g)
    forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
    randomR (Integer
    1, Int -> Integer
    forall a. Bits a => Int -> a
    bit (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    p) Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1) g
    g1
           in (SFloat sym -> GenValue sym
    forall sym. SFloat sym -> GenValue sym
    VFloat (SFloat sym -> GenValue sym)
    -> SEval sym (SFloat sym) -> SEval sym (GenValue sym)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((if Bool
    sgn then sym -> SFloat sym -> SEval sym (SFloat sym)
    forall sym.
    Backend sym =>
    sym -> SFloat sym -> SEval sym (SFloat sym)
    fpNeg sym
    sym else SFloat sym -> SEval sym (SFloat sym)
    forall a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure) (SFloat sym -> SEval sym (SFloat sym))
    -> SEval sym (SFloat sym) -> SEval sym (SFloat sym)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> Integer -> Integer -> SWord sym -> SEval sym (SFloat sym)
    forall sym.
    Backend sym =>
    sym -> Integer -> Integer -> SWord sym -> SEval sym (SFloat sym)
    fpFromBits sym
    sym Integer
    e Integer
    p (SWord sym -> SEval sym (SFloat sym))
    -> SEval sym (SWord sym) -> SEval sym (SFloat sym)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> Integer -> Integer -> SEval sym (SWord sym)
    forall sym.
    Backend sym =>
    sym -> Integer -> Integer -> SEval sym (SWord sym)
    wordLit sym
    sym (Integer
    eInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +Integer
    p) Integer
    v), g
    g2)

        -- generates floats where the exponent and mantissa are scaled by the size
        genNormal :: Integer -> g -> (SEval sym (GenValue sym), g)
    genNormal Integer
    sz g
    g =
          let (Bool
    sgn, g
    g1) = g -> (Bool, g)
    forall g. RandomGen g => g -> (Bool, g)
    forall a g. (Random a, RandomGen g) => g -> (a, g)
    random g
    g
              (Integer
    ex,  g
    g2) = (Integer, Integer) -> g -> (Integer, g)
    forall g. RandomGen g => (Integer, Integer) -> g -> (Integer, g)
    forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
    randomR ((Integer
    1Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    emax)Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    *Integer
    sz Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `div` Integer
    100, (Integer
    szInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    *Integer
    emax) Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `div` Integer
    100) g
    g1
              (Integer
    mag, g
    g3) = (Integer, Integer) -> g -> (Integer, g)
    forall g. RandomGen g => (Integer, Integer) -> g -> (Integer, g)
    forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
    randomR (Integer
    1, Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    max Integer
    1 ((Integer
    szInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    *Integer
    smax) Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `div` Integer
    100)) g
    g2
              r :: Rational
    r  = Integer -> Rational
    forall a. Num a => Integer -> a
    fromInteger Integer
    mag Rational -> Integer -> Rational
    forall a b. (Fractional a, Integral b) => a -> b -> a
    ^^ (Integer
    ex Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer -> Integer
    widthInteger Integer
    mag)
              r' :: Rational
    r' = if Bool
    sgn then Rational -> Rational
    forall a. Num a => a -> a
    negate Rational
    r else Rational
    r
           in (SFloat sym -> GenValue sym
    forall sym. SFloat sym -> GenValue sym
    VFloat (SFloat sym -> GenValue sym)
    -> SEval sym (SFloat sym) -> SEval sym (GenValue sym)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> Integer -> Integer -> Rational -> SEval sym (SFloat sym)
    forall sym.
    Backend sym =>
    sym -> Integer -> Integer -> Rational -> SEval sym (SFloat sym)
    fpLit sym
    sym Integer
    e Integer
    p Rational
    r', g
    g3)

    -- | A test result is either a pass, a failure due to evaluating to
    -- @False@, or a failure due to an exception raised during evaluation
    data TestResult
      = Pass
      | FailFalse [Value]
      | FailError EvalErrorEx [Value]

    isPass :: TestResult -> Bool
    isPass :: TestResult -> Bool
    isPass TestResult
    Pass = Bool
    True
    isPass TestResult
    _    = Bool
    False

    -- | Apply a testable value to some arguments.
    -- Note that this function assumes that the values come from a call to
    -- `testableType` (i.e., things are type-correct). We run in the IO
    -- monad in order to catch any @EvalError@s.
    evalTest :: Value -> [Value] -> IO TestResult
    evalTest :: Value -> [Value] -> IO TestResult
    evalTest Value
    v0 [Value]
    vs0 = IO TestResult
    run IO TestResult -> (EvalErrorEx -> IO TestResult) -> IO TestResult
    forall e a. Exception e => IO a -> (e -> IO a) -> IO a
    `X.catch` EvalErrorEx -> IO TestResult
    handle
      where
        run :: IO TestResult
    run = do
          Bool
    result <- CallStack -> Eval Bool -> IO Bool
    forall a. CallStack -> Eval a -> IO a
    runEval CallStack
    forall a. Monoid a => a
    mempty (Value -> [Value] -> Eval Bool
    go Value
    v0 [Value]
    vs0)
          if Bool
    result
            then TestResult -> IO TestResult
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return TestResult
    Pass
            else TestResult -> IO TestResult
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Value] -> TestResult
    FailFalse [Value]
    vs0)
        handle :: EvalErrorEx -> IO TestResult
    handle EvalErrorEx
    e = TestResult -> IO TestResult
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (EvalErrorEx -> [Value] -> TestResult
    FailError EvalErrorEx
    e [Value]
    vs0)

        go :: Value -> [Value] -> Eval Bool
        go :: Value -> [Value] -> Eval Bool
    go f :: Value
    f@VFun{} (Value
    v : [Value]
    vs) = do Value
    f' <- Concrete -> Value -> SEval Concrete Value -> SEval Concrete Value
    forall sym.
    Backend sym =>
    sym
    -> GenValue sym
    -> SEval sym (GenValue sym)
    -> SEval sym (GenValue sym)
    fromVFun Concrete
    Concrete Value
    f (Value -> Eval Value
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Value
    v)
                                  Value -> [Value] -> Eval Bool
    go Value
    f' [Value]
    vs
        go VFun{}   []       = String -> [String] -> Eval Bool
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "Not enough arguments while applying function"
                               []
        go (VBit SBit Concrete
    b) []       = Bool -> Eval Bool
    forall a. a -> Eval a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    SBit Concrete
    b
        go Value
    v [Value]
    vs              = do Doc
    vdoc    <- Concrete -> PPOpts -> Value -> SEval Concrete Doc
    forall sym.
    Backend sym =>
    sym -> PPOpts -> GenValue sym -> SEval sym Doc
    ppValue Concrete
    Concrete PPOpts
    defaultPPOpts Value
    v
                                  [Doc]
    vsdocs  <- (Value -> Eval Doc) -> [Value] -> Eval [Doc]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (Concrete -> PPOpts -> Value -> SEval Concrete Doc
    forall sym.
    Backend sym =>
    sym -> PPOpts -> GenValue sym -> SEval sym Doc
    ppValue Concrete
    Concrete PPOpts
    defaultPPOpts) [Value]
    vs
                                  String -> [String] -> Eval Bool
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "Type error while running test" ([String] -> Eval Bool) -> [String] -> Eval Bool
    forall a b. (a -> b) -> a -> b
    $
                                   [ String
    "Function:"
                                   , Doc -> String
    forall a. Show a => a -> String
    show Doc
    vdoc
                                   , String
    "Arguments:"
                                   ] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ (Doc -> String) -> [Doc] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map Doc -> String
    forall a. Show a => a -> String
    show [Doc]
    vsdocs

    {- | Given a (function) type, compute data necessary for
         random or exhaustive testing.

         The first returned component is a count of the number of
         possible input test vectors, if the input types are finite.
         The second component is a list of all the types of the function
         inputs.  The third component is a list of all input test vectors
         for exhaustive testing.  This will be empty unless the
         input types are finite.  The final argument is a list of generators
         for the inputs of the function.

         This function will return @Nothing@ if the input type does not
         eventually return @Bit@, or if we cannot compute a generator
         for one of the inputs.
    -}
    testableType :: RandomGen g =>
      TValue ->
      Maybe (Maybe Integer, [TValue], [[Value]], [Gen g Concrete])
    testableType :: forall g.
    RandomGen g =>
    TValue
    -> Maybe (Maybe Integer, [TValue], [[Value]], [Gen g Concrete])
    testableType (TVFun TValue
    t1 TValue
    t2) =
       do let sz :: Maybe Integer
    sz = TValue -> Maybe Integer
    typeSize TValue
    t1
          Integer -> g -> (Eval Value, g)
    g <- Concrete -> TValue -> Maybe (Gen g Concrete)
    forall sym g.
    (Backend sym, RandomGen g) =>
    sym -> TValue -> Maybe (Gen g sym)
    randomValue Concrete
    Concrete TValue
    t1
          (Maybe Integer
    tot,[TValue]
    ts,[[Value]]
    vss,[Integer -> g -> (Eval Value, g)]
    gs) <- TValue
    -> Maybe (Maybe Integer, [TValue], [[Value]], [Gen g Concrete])
    forall g.
    RandomGen g =>
    TValue
    -> Maybe (Maybe Integer, [TValue], [[Value]], [Gen g Concrete])
    testableType TValue
    t2
          let tot' :: Maybe Integer
    tot' = (Integer -> Integer -> Integer)
    -> Maybe Integer -> Maybe Integer -> Maybe Integer
    forall (m :: * -> *) a1 a2 r.
    Monad m =>
    (a1 -> a2 -> r) -> m a1 -> m a2 -> m r
    liftM2 Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    (*) Maybe Integer
    sz Maybe Integer
    tot
          let vss' :: [[Value]]
    vss' = [ Value
    v Value -> [Value] -> [Value]
    forall a. a -> [a] -> [a]
    : [Value]
    vs | Value
    v <- TValue -> [Value]
    typeValues TValue
    t1, [Value]
    vs <- [[Value]]
    vss ]
          (Maybe Integer, [TValue], [[Value]],
     [Integer -> g -> (Eval Value, g)])
    -> Maybe
         (Maybe Integer, [TValue], [[Value]],
          [Integer -> g -> (Eval Value, g)])
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Integer
    tot', TValue
    t1TValue -> [TValue] -> [TValue]
    forall a. a -> [a] -> [a]
    :[TValue]
    ts, [[Value]]
    vss', Integer -> g -> (Eval Value, g)
    g(Integer -> g -> (Eval Value, g))
    -> [Integer -> g -> (Eval Value, g)]
    -> [Integer -> g -> (Eval Value, g)]
    forall a. a -> [a] -> [a]
    :[Integer -> g -> (Eval Value, g)]
    gs)
    testableType TValue
    TVBit = (Maybe Integer, [TValue], [[Value]],
     [Integer -> g -> (Eval Value, g)])
    -> Maybe
         (Maybe Integer, [TValue], [[Value]],
          [Integer -> g -> (Eval Value, g)])
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just Integer
    1, [], [[]], [])
    testableType TValue
    _ = Maybe
      (Maybe Integer, [TValue], [[Value]],
       [Integer -> g -> (Eval Value, g)])
    Maybe (Maybe Integer, [TValue], [[Value]], [Gen g Concrete])
    forall a. Maybe a
    Nothing

    {- | Given a fully-evaluated type, try to compute the number of values in it.
    Returns `Nothing` for infinite types, user-defined types, polymorphic types,
    and, currently, function spaces.  Of course, we can easily compute the
    sizes of function spaces, but we can't easily enumerate their inhabitants. -}
    typeSize :: TValue -> Maybe Integer
    typeSize :: TValue -> Maybe Integer
    typeSize TValue
    ty = case TValue
    ty of
      TValue
    TVBit -> Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just Integer
    2
      TValue
    TVInteger -> Maybe Integer
    forall a. Maybe a
    Nothing
      TValue
    TVRational -> Maybe Integer
    forall a. Maybe a
    Nothing
      TVIntMod Integer
    n -> Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just Integer
    n
      TVFloat Integer
    e Integer
    p -> Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just (Integer
    2 Integer -> Integer -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^ (Integer
    eInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +Integer
    p))
      TVArray{} -> Maybe Integer
    forall a. Maybe a
    Nothing
      TVStream{} -> Maybe Integer
    forall a. Maybe a
    Nothing
      TVSeq Integer
    n TValue
    el -> (Integer -> Integer -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^ Integer
    n) (Integer -> Integer) -> Maybe Integer -> Maybe Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TValue -> Maybe Integer
    typeSize TValue
    el
      TVTuple [TValue]
    els -> [Integer] -> Integer
    forall a. Num a => [a] -> a
    forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
    product ([Integer] -> Integer) -> Maybe [Integer] -> Maybe Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (TValue -> Maybe Integer) -> [TValue] -> Maybe [Integer]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM TValue -> Maybe Integer
    typeSize [TValue]
    els
      TVRec RecordMap Ident TValue
    fs -> RecordMap Ident Integer -> Integer
    forall a. Num a => RecordMap Ident a -> a
    forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
    product (RecordMap Ident Integer -> Integer)
    -> Maybe (RecordMap Ident Integer) -> Maybe Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (TValue -> Maybe Integer)
    -> RecordMap Ident TValue -> Maybe (RecordMap Ident Integer)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> RecordMap Ident a -> f (RecordMap Ident b)
    traverse TValue -> Maybe Integer
    typeSize RecordMap Ident TValue
    fs
      TVFun{} -> Maybe Integer
    forall a. Maybe a
    Nothing
      TVAbstract{} -> Maybe Integer
    forall a. Maybe a
    Nothing
      TVNewtype Newtype
    _ [Either Nat' TValue]
    _ RecordMap Ident TValue
    tbody -> TValue -> Maybe Integer
    typeSize (RecordMap Ident TValue -> TValue
    TVRec RecordMap Ident TValue
    tbody)

    {- | Returns all the values in a type.  Returns an empty list of values,
    for types where 'typeSize' returned 'Nothing'. -}
    typeValues :: TValue -> [Value]
    typeValues :: TValue -> [Value]
    typeValues TValue
    ty =
      case TValue
    ty of
        TValue
    TVBit       -> [ SBit Concrete -> Value
    forall sym. SBit sym -> GenValue sym
    VBit Bool
    SBit Concrete
    False, SBit Concrete -> Value
    forall sym. SBit sym -> GenValue sym
    VBit Bool
    SBit Concrete
    True ]
        TValue
    TVInteger   -> []
        TValue
    TVRational  -> []
        TVIntMod Integer
    n  -> [ SInteger Concrete -> Value
    forall sym. SInteger sym -> GenValue sym
    VInteger Integer
    SInteger Concrete
    x | Integer
    x <- [ Integer
    0 .. (Integer
    nInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1) ] ]
        TVFloat Integer
    e Integer
    p -> [ SFloat Concrete -> Value
    forall sym. SFloat sym -> GenValue sym
    VFloat (Integer -> Integer -> Integer -> BF
    floatFromBits Integer
    e Integer
    p Integer
    v) | Integer
    v <- [Integer
    0 .. Integer
    2Integer -> Integer -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^(Integer
    eInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +Integer
    p) Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1] ]
        TVArray{}   -> []
        TVStream{}  -> []
        TVSeq Integer
    n TValue
    TVBit ->
          [ Integer -> WordValue Concrete -> Value
    forall sym. Integer -> WordValue sym -> GenValue sym
    VWord Integer
    n (SWord Concrete -> WordValue Concrete
    forall sym. SWord sym -> WordValue sym
    wordVal (Integer -> Integer -> BV
    BV Integer
    n Integer
    x))
          | Integer
    x <- [ Integer
    0 .. Integer
    2Integer -> Integer -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^Integer
    n Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1 ]
          ]
        TVSeq Integer
    n TValue
    el ->
          [ Integer -> SeqMap Concrete Value -> Value
    forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
    VSeq Integer
    n (Concrete -> [SEval Concrete Value] -> SeqMap Concrete Value
    forall sym a. Backend sym => sym -> [SEval sym a] -> SeqMap sym a
    finiteSeqMap Concrete
    Concrete ((Value -> Eval Value) -> [Value] -> [Eval Value]
    forall a b. (a -> b) -> [a] -> [b]
    map Value -> Eval Value
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure [Value]
    xs))
          | [Value]
    xs <- [[Value]] -> [[Value]]
    forall (t :: * -> *) (m :: * -> *) a.
    (Traversable t, Monad m) =>
    t (m a) -> m (t a)
    forall (m :: * -> *) a. Monad m => [m a] -> m [a]
    sequence (Integer -> [Value] -> [[Value]]
    forall i a. Integral i => i -> a -> [a]
    genericReplicate Integer
    n (TValue -> [Value]
    typeValues TValue
    el))
          ]
        TVTuple [TValue]
    ts ->
          [ [SEval Concrete Value] -> Value
    forall sym. [SEval sym (GenValue sym)] -> GenValue sym
    VTuple ((Value -> Eval Value) -> [Value] -> [Eval Value]
    forall a b. (a -> b) -> [a] -> [b]
    map Value -> Eval Value
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure [Value]
    xs)
          | [Value]
    xs <- [[Value]] -> [[Value]]
    forall (t :: * -> *) (m :: * -> *) a.
    (Traversable t, Monad m) =>
    t (m a) -> m (t a)
    forall (m :: * -> *) a. Monad m => [m a] -> m [a]
    sequence ((TValue -> [Value]) -> [TValue] -> [[Value]]
    forall a b. (a -> b) -> [a] -> [b]
    map TValue -> [Value]
    typeValues [TValue]
    ts)
          ]
        TVRec RecordMap Ident TValue
    fs ->
          [ RecordMap Ident (SEval Concrete Value) -> Value
    forall sym.
    RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
    VRecord ((Value -> Eval Value)
    -> RecordMap Ident Value -> RecordMap Ident (Eval Value)
    forall a b. (a -> b) -> RecordMap Ident a -> RecordMap Ident b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Value -> Eval Value
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure RecordMap Ident Value
    xs)
          | RecordMap Ident Value
    xs <- (TValue -> [Value])
    -> RecordMap Ident TValue -> [RecordMap Ident Value]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> RecordMap Ident a -> f (RecordMap Ident b)
    traverse TValue -> [Value]
    typeValues RecordMap Ident TValue
    fs
          ]
        TVFun{} -> []
        TVAbstract{} -> []
        TVNewtype Newtype
    _ [Either Nat' TValue]
    _ RecordMap Ident TValue
    tbody -> TValue -> [Value]
    typeValues (RecordMap Ident TValue -> TValue
    TVRec RecordMap Ident TValue
    tbody)

    --------------------------------------------------------------------------------
    -- Driver function

    exhaustiveTests :: MonadIO m =>
      (Integer -> m ()) {- ^ progress callback -} ->
      Value {- ^ function under test -} ->
      [[Value]] {- ^ exhaustive set of test values -} ->
      m (TestResult, Integer)
    exhaustiveTests :: forall (m :: * -> *).
    MonadIO m =>
    (Integer -> m ()) -> Value -> [[Value]] -> m (TestResult, Integer)
    exhaustiveTests Integer -> m ()
    ppProgress Value
    val = Integer -> [[Value]] -> m (TestResult, Integer)
    go Integer
    0
      where
      go :: Integer -> [[Value]] -> m (TestResult, Integer)
    go !Integer
    testNum [] = (TestResult, Integer) -> m (TestResult, Integer)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TestResult
    Pass, Integer
    testNum)
      go !Integer
    testNum ([Value]
    vs:[[Value]]
    vss) =
        do Integer -> m ()
    ppProgress Integer
    testNum
           TestResult
    res <- IO TestResult -> m TestResult
    forall a. IO a -> m a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (Value -> [Value] -> IO TestResult
    evalTest Value
    val [Value]
    vs)
           case TestResult
    res of
             TestResult
    Pass -> Integer -> [[Value]] -> m (TestResult, Integer)
    go (Integer
    testNumInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +Integer
    1) [[Value]]
    vss
             TestResult
    failure -> (TestResult, Integer) -> m (TestResult, Integer)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TestResult
    failure, Integer
    testNum)

    randomTests :: (MonadIO m, RandomGen g) =>
      (Integer -> m ()) {- ^ progress callback -} ->
      Integer {- ^ Maximum number of tests to run -} ->
      Value {- ^ function under test -} ->
      [Gen g Concrete] {- ^ input value generators -} ->
      g {- ^ Inital random generator -} ->
      m (TestResult, Integer)
    randomTests :: forall (m :: * -> *) g.
    (MonadIO m, RandomGen g) =>
    (Integer -> m ())
    -> Integer
    -> Value
    -> [Gen g Concrete]
    -> g
    -> m (TestResult, Integer)
    randomTests Integer -> m ()
    ppProgress Integer
    maxTests Value
    val [Gen g Concrete]
    gens g
    g = ((TestResult, Integer), g) -> (TestResult, Integer)
    forall a b. (a, b) -> a
    fst (((TestResult, Integer), g) -> (TestResult, Integer))
    -> m ((TestResult, Integer), g) -> m (TestResult, Integer)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Integer -> m ())
    -> Integer
    -> Value
    -> [Gen g Concrete]
    -> g
    -> m ((TestResult, Integer), g)
    forall (m :: * -> *) g.
    (MonadIO m, RandomGen g) =>
    (Integer -> m ())
    -> Integer
    -> Value
    -> [Gen g Concrete]
    -> g
    -> m ((TestResult, Integer), g)
    randomTests' Integer -> m ()
    ppProgress Integer
    maxTests Value
    val [Gen g Concrete]
    gens g
    g

    randomTests' :: (MonadIO m, RandomGen g) =>
      (Integer -> m ()) {- ^ progress callback -} ->
      Integer {- ^ Maximum number of tests to run -} ->
      Value {- ^ function under test -} ->
      [Gen g Concrete] {- ^ input value generators -} ->
      g {- ^ Inital random generator -} ->
      m ((TestResult, Integer), g)
    randomTests' :: forall (m :: * -> *) g.
    (MonadIO m, RandomGen g) =>
    (Integer -> m ())
    -> Integer
    -> Value
    -> [Gen g Concrete]
    -> g
    -> m ((TestResult, Integer), g)
    randomTests' Integer -> m ()
    ppProgress Integer
    maxTests Value
    val [Gen g Concrete]
    gens = Integer -> g -> m ((TestResult, Integer), g)
    go Integer
    0
      where
      go :: Integer -> g -> m ((TestResult, Integer), g)
    go !Integer
    testNum g
    g
        | Integer
    testNum Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Integer
    maxTests = ((TestResult, Integer), g) -> m ((TestResult, Integer), g)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((TestResult
    Pass, Integer
    testNum), g
    g)
        | Bool
    otherwise =
          do Integer -> m ()
    ppProgress Integer
    testNum
             let sz' :: Integer
    sz' = Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    div (Integer
    100 Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    * (Integer
    1 Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    testNum)) Integer
    maxTests
             (TestResult
    res, g
    g') <- IO (TestResult, g) -> m (TestResult, g)
    forall a. IO a -> m a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (Value -> [Gen g Concrete] -> Integer -> g -> IO (TestResult, g)
    forall g.
    RandomGen g =>
    Value -> [Gen g Concrete] -> Integer -> g -> IO (TestResult, g)
    runOneTest Value
    val [Gen g Concrete]
    gens Integer
    sz' g
    g)
             case TestResult
    res of
               TestResult
    Pass -> Integer -> g -> m ((TestResult, Integer), g)
    go (Integer
    testNumInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +Integer
    1) g
    g'
               TestResult
    failure -> ((TestResult, Integer), g) -> m ((TestResult, Integer), g)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((TestResult
    failure, Integer
    testNum), g
    g)