Cryptol.Testing.Concrete

Documentation

data TestResult

A test result is either a pass, a failure due to evaluating to False, or a failure due to an exception raised during evaluation

Constructors

Pass

FailFalse [Value]

FailError EvalError [Value]

isPass :: TestResult -> Bool

runOneTest :: EvalOpts -> Value -> [Value] -> IO TestResult

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 EvalErrors.

testableType :: Type -> Maybe (Maybe Integer, [Type], [[Value]])

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.

typeSize :: Type -> Maybe Integer

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.

typeValues :: Type -> [Value]

Returns all the values in a type. Returns an empty list of values, for types where typeSize returned Nothing.

data TestSpec m s

Constructors

TestSpec

Fields

• testFn :: Integer -> s -> m (TestResult, s)
• testProp :: String

  The property as entered by the user

• testTotal :: Integer
• testPossible :: Maybe Integer

  Nothing indicates infinity

• testRptProgress :: Integer -> Integer -> m ()
• testClrProgress :: m ()
• testRptFailure :: TestResult -> m ()
• testRptSuccess :: m ()

data TestReport

Constructors

TestReport

Fields

• reportResult :: TestResult
• reportProp :: String

  The property as entered by the user

• reportTestsRun :: Integer
• reportTestsPossible :: Maybe Integer

runTests :: Monad m => TestSpec m s -> s -> m TestReport