    -- |
    -- Module      :  Cryptol.Testing.Concrete
    -- Copyright   :  (c) 2013-2016 Galois, Inc.
    -- License     :  BSD3
    -- Maintainer  :  cryptol@galois.com
    -- Stability   :  provisional
    -- Portability :  portable

    {-# LANGUAGE RecordWildCards #-}
    module Cryptol.Testing.Concrete where

    import Control.Monad (join, liftM2)

    import Cryptol.Eval.Monad
    import Cryptol.Eval.Value
    import Cryptol.TypeCheck.AST
    import Cryptol.Utils.Panic (panic)

    import qualified Control.Exception as X
    import Data.List(genericReplicate)

    import Prelude ()
    import Prelude.Compat

    -- | 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 EvalError [Value]

    isPass :: TestResult -> Bool
    isPass :: TestResult -> Bool
    isPass Pass = Bool
    True
    isPass _    = 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.
    runOneTest :: EvalOpts -> Value -> [Value] -> IO TestResult
    runOneTest :: EvalOpts -> Value -> [Value] -> IO TestResult
    runOneTest evOpts :: EvalOpts
    evOpts v0 :: Value
    v0 vs0 :: [Value]
    vs0 = IO TestResult
    run IO TestResult -> (EvalError -> IO TestResult) -> IO TestResult
    forall e a. Exception e => IO a -> (e -> IO a) -> IO a
    `X.catch` EvalError -> IO TestResult
    forall (m :: * -> *). Monad m => EvalError -> m TestResult
    handle
      where
        run :: IO TestResult
    run = do
          Bool
    result <- EvalOpts -> Eval Bool -> IO Bool
    forall a. EvalOpts -> Eval a -> IO a
    runEval EvalOpts
    evOpts (Value -> [Value] -> Eval Bool
    go Value
    v0 [Value]
    vs0)
          if Bool
    result
            then TestResult -> IO TestResult
    forall (m :: * -> *) a. Monad m => a -> m a
    return TestResult
    Pass
            else TestResult -> IO TestResult
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Value] -> TestResult
    FailFalse [Value]
    vs0)
        handle :: EvalError -> m TestResult
    handle e :: EvalError
    e = TestResult -> m TestResult
    forall (m :: * -> *) a. Monad m => a -> m a
    return (EvalError -> [Value] -> TestResult
    FailError EvalError
    e [Value]
    vs0)

        go :: Value -> [Value] -> Eval Bool
        go :: Value -> [Value] -> Eval Bool
    go (VFun f :: Eval Value -> Eval Value
    f) (v :: Value
    v : vs :: [Value]
    vs) = Eval (Eval Bool) -> Eval Bool
    forall (m :: * -> *) a. Monad m => m (m a) -> m a
    join (Value -> [Value] -> Eval Bool
    go (Value -> [Value] -> Eval Bool)
    -> Eval Value -> Eval ([Value] -> Eval Bool)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Eval Value -> Eval Value
    f (Value -> Eval Value
    forall a. a -> Eval a
    ready Value
    v)) Eval ([Value] -> Eval Bool) -> Eval [Value] -> Eval (Eval Bool)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> [Value] -> Eval [Value]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Value]
    vs)
        go (VFun _) []       = String -> [String] -> Eval Bool
    forall a. HasCallStack => String -> [String] -> a
    panic "Not enough arguments while applying function"
                               []
        go (VBit b :: Bool
    b) []       = Bool -> Eval Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    b
        go v :: Value
    v vs :: [Value]
    vs              = do Doc
    vdoc    <- PPOpts -> Value -> Eval Doc
    forall b w i. BitWord b w i => PPOpts -> GenValue b w i -> Eval Doc
    ppValue 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)
    mapM (PPOpts -> Value -> Eval Doc
    forall b w i. BitWord b w i => PPOpts -> GenValue b w i -> Eval Doc
    ppValue PPOpts
    defaultPPOpts) [Value]
    vs
                                  String -> [String] -> Eval Bool
    forall a. HasCallStack => String -> [String] -> a
    panic "Type error while running test" ([String] -> Eval Bool) -> [String] -> Eval Bool
    forall a b. (a -> b) -> a -> b
    $
                                   [ "Function:"
                                   , Doc -> String
    forall a. Show a => a -> String
    show Doc
    vdoc
                                   , "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 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 (Maybe Integer, [Type], [[Value]])
    testableType :: Type -> Maybe (Maybe Integer, [Type], [[Value]])
    testableType ty :: Type
    ty =
      case Type -> Type
    tNoUser Type
    ty of
        TCon (TC TCFun) [t1 :: Type
    t1,t2 :: Type
    t2] ->
          do let sz :: Maybe Integer
    sz = Type -> Maybe Integer
    typeSize Type
    t1
             (tot :: Maybe Integer
    tot,ts :: [Type]
    ts,vss :: [[Value]]
    vss) <- Type -> Maybe (Maybe Integer, [Type], [[Value]])
    testableType Type
    t2
             (Maybe Integer, [Type], [[Value]])
    -> Maybe (Maybe Integer, [Type], [[Value]])
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((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, Type
    t1Type -> [Type] -> [Type]
    forall a. a -> [a] -> [a]
    :[Type]
    ts, [ Value
    v Value -> [Value] -> [Value]
    forall a. a -> [a] -> [a]
    : [Value]
    vs | Value
    v <- Type -> [Value]
    typeValues Type
    t1, [Value]
    vs <- [[Value]]
    vss ])
        TCon (TC TCBit) [] -> (Maybe Integer, [Type], [[Value]])
    -> Maybe (Maybe Integer, [Type], [[Value]])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just 1, [], [[]])
        _ -> Maybe (Maybe Integer, [Type], [[Value]])
    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 :: Type -> Maybe Integer
    typeSize :: Type -> Maybe Integer
    typeSize ty :: Type
    ty =
      case Type
    ty of
        TVar _      -> Maybe Integer
    forall a. Maybe a
    Nothing
        TUser _ _ t :: Type
    t -> Type -> Maybe Integer
    typeSize Type
    t
        TRec fs :: [(Ident, Type)]
    fs     -> [Integer] -> Integer
    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
    <$> ((Ident, Type) -> Maybe Integer)
    -> [(Ident, Type)] -> Maybe [Integer]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (Type -> Maybe Integer
    typeSize (Type -> Maybe Integer)
    -> ((Ident, Type) -> Type) -> (Ident, Type) -> Maybe Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Ident, Type) -> Type
    forall a b. (a, b) -> b
    snd) [(Ident, Type)]
    fs
        TCon (TC tc :: TC
    tc) ts :: [Type]
    ts ->
          case (TC
    tc, [Type]
    ts) of
            (TCNum _, _)     -> Maybe Integer
    forall a. Maybe a
    Nothing
            (TCInf, _)       -> Maybe Integer
    forall a. Maybe a
    Nothing
            (TCBit, _)       -> Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just 2
            (TCInteger, _)   -> Maybe Integer
    forall a. Maybe a
    Nothing
            (TCIntMod, [sz :: Type
    sz]) -> case Type -> Type
    tNoUser Type
    sz of
                                  TCon (TC (TCNum n :: Integer
    n)) _ -> Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just Integer
    n
                                  _                     -> Maybe Integer
    forall a. Maybe a
    Nothing
            (TCIntMod, _)    -> Maybe Integer
    forall a. Maybe a
    Nothing
            (TCSeq, [sz :: Type
    sz,el :: Type
    el]) -> case Type -> Type
    tNoUser Type
    sz of
                                  TCon (TC (TCNum n :: Integer
    n)) _ -> (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
    <$> Type -> Maybe Integer
    typeSize Type
    el
                                  _                     -> Maybe Integer
    forall a. Maybe a
    Nothing
            (TCSeq, _)       -> Maybe Integer
    forall a. Maybe a
    Nothing
            (TCFun, _)       -> Maybe Integer
    forall a. Maybe a
    Nothing
            (TCTuple _, els :: [Type]
    els) -> [Integer] -> Integer
    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
    <$> (Type -> Maybe Integer) -> [Type] -> Maybe [Integer]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM Type -> Maybe Integer
    typeSize [Type]
    els
            (TCAbstract _, _) -> Maybe Integer
    forall a. Maybe a
    Nothing
            (TCNewtype _, _) -> Maybe Integer
    forall a. Maybe a
    Nothing

        TCon _ _ -> Maybe Integer
    forall a. Maybe a
    Nothing

    {- | Returns all the values in a type.  Returns an empty list of values,
    for types where 'typeSize' returned 'Nothing'. -}
    typeValues :: Type -> [Value]
    typeValues :: Type -> [Value]
    typeValues ty :: Type
    ty =
      case Type
    ty of
        TVar _      -> []
        TUser _ _ t :: Type
    t -> Type -> [Value]
    typeValues Type
    t
        TRec fs :: [(Ident, Type)]
    fs     -> [ [(Ident, Eval Value)] -> Value
    forall b w i. [(Ident, Eval (GenValue b w i))] -> GenValue b w i
    VRecord [(Ident, Eval Value)]
    xs
                       | [(Ident, Eval Value)]
    xs <- [[(Ident, Eval Value)]] -> [[(Ident, Eval Value)]]
    forall (t :: * -> *) (m :: * -> *) a.
    (Traversable t, Monad m) =>
    t (m a) -> m (t a)
    sequence [ [ (Ident
    f,Value -> Eval Value
    forall a. a -> Eval a
    ready Value
    v) | Value
    v <- Type -> [Value]
    typeValues Type
    t ]
                                        | (f :: Ident
    f,t :: Type
    t) <- [(Ident, Type)]
    fs ]
                       ]
        TCon (TC tc :: TC
    tc) ts :: [Type]
    ts ->
          case TC
    tc of
            TCNum _     -> []
            TCInf       -> []
            TCBit       -> [ Bool -> Value
    forall b w i. b -> GenValue b w i
    VBit Bool
    False, Bool -> Value
    forall b w i. b -> GenValue b w i
    VBit Bool
    True ]
            TCInteger   -> []
            TCIntMod    ->
              case (Type -> Type) -> [Type] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map Type -> Type
    tNoUser [Type]
    ts of
                [ TCon (TC (TCNum n :: Integer
    n)) _ ] | 0 Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    n ->
                  [ Integer -> Value
    forall b w i. i -> GenValue b w i
    VInteger Integer
    x | Integer
    x <- [ 0 .. Integer
    n Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - 1 ] ]
                _ -> []
            TCSeq       ->
              case (Type -> Type) -> [Type] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map Type -> Type
    tNoUser [Type]
    ts of
                [ TCon (TC (TCNum n :: Integer
    n)) _, TCon (TC TCBit) [] ] ->
                  [ Integer -> Eval (WordValue Bool BV Integer) -> Value
    forall b w i. Integer -> Eval (WordValue b w i) -> GenValue b w i
    VWord Integer
    n (WordValue Bool BV Integer -> Eval (WordValue Bool BV Integer)
    forall a. a -> Eval a
    ready (BV -> WordValue Bool BV Integer
    forall b w i. w -> WordValue b w i
    WordVal (Integer -> Integer -> BV
    BV Integer
    n Integer
    x))) | Integer
    x <- [ 0 .. 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
    - 1 ] ]

                [ TCon (TC (TCNum n :: Integer
    n)) _, t :: Type
    t ] ->
                  [ Integer -> SeqMap Bool BV Integer -> Value
    forall b w i. Integer -> SeqMap b w i -> GenValue b w i
    VSeq Integer
    n ([Eval Value] -> SeqMap Bool BV Integer
    forall b w i. [Eval (GenValue b w i)] -> SeqMap b w i
    finiteSeqMap ((Value -> Eval Value) -> [Value] -> [Eval Value]
    forall a b. (a -> b) -> [a] -> [b]
    map Value -> Eval Value
    forall a. a -> Eval a
    ready [Value]
    xs))
                  | [Value]
    xs <- [[Value]] -> [[Value]]
    forall (t :: * -> *) (m :: * -> *) a.
    (Traversable t, Monad m) =>
    t (m a) -> m (t a)
    sequence ([[Value]] -> [[Value]]) -> [[Value]] -> [[Value]]
    forall a b. (a -> b) -> a -> b
    $ Integer -> [Value] -> [[Value]]
    forall i a. Integral i => i -> a -> [a]
    genericReplicate Integer
    n
                                   ([Value] -> [[Value]]) -> [Value] -> [[Value]]
    forall a b. (a -> b) -> a -> b
    $ Type -> [Value]
    typeValues Type
    t ]
                _ -> []

            TCFun       -> []  -- We don't generate function values.
            TCTuple _   -> [ [Eval Value] -> Value
    forall b w i. [Eval (GenValue b w i)] -> GenValue b w i
    VTuple ((Value -> Eval Value) -> [Value] -> [Eval Value]
    forall a b. (a -> b) -> [a] -> [b]
    map Value -> Eval Value
    forall a. a -> Eval a
    ready [Value]
    xs)
                           | [Value]
    xs <- [[Value]] -> [[Value]]
    forall (t :: * -> *) (m :: * -> *) a.
    (Traversable t, Monad m) =>
    t (m a) -> m (t a)
    sequence ((Type -> [Value]) -> [Type] -> [[Value]]
    forall a b. (a -> b) -> [a] -> [b]
    map Type -> [Value]
    typeValues [Type]
    ts)
                           ]
            TCAbstract _ -> []
            TCNewtype _ -> []

        TCon _ _ -> []

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

    data TestSpec m s = TestSpec {
        TestSpec m s -> Integer -> s -> m (TestResult, s)
    testFn :: Integer -> s -> m (TestResult, s)
      , TestSpec m s -> String
    testProp :: String -- ^ The property as entered by the user
      , TestSpec m s -> Integer
    testTotal :: Integer
      , TestSpec m s -> Maybe Integer
    testPossible :: Maybe Integer -- ^ Nothing indicates infinity
      , TestSpec m s -> Integer -> Integer -> m ()
    testRptProgress :: Integer -> Integer -> m ()
      , TestSpec m s -> m ()
    testClrProgress :: m ()
      , TestSpec m s -> TestResult -> m ()
    testRptFailure :: TestResult -> m ()
      , TestSpec m s -> m ()
    testRptSuccess :: m ()
      }

    data TestReport = TestReport {
        TestReport -> TestResult
    reportResult :: TestResult
      , TestReport -> String
    reportProp :: String -- ^ The property as entered by the user
      , TestReport -> Integer
    reportTestsRun :: Integer
      , TestReport -> Maybe Integer
    reportTestsPossible :: Maybe Integer
      }

    runTests :: Monad m => TestSpec m s -> s -> m TestReport
    runTests :: TestSpec m s -> s -> m TestReport
    runTests TestSpec {..} st0 :: s
    st0 = Integer -> s -> m TestReport
    go 0 s
    st0
      where
      go :: Integer -> s -> m TestReport
    go testNum :: Integer
    testNum _ | Integer
    testNum Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Integer
    testTotal = do
        m ()
    testRptSuccess
        TestReport -> m TestReport
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TestReport -> m TestReport) -> TestReport -> m TestReport
    forall a b. (a -> b) -> a -> b
    $ TestResult -> String -> Integer -> Maybe Integer -> TestReport
    TestReport TestResult
    Pass String
    testProp Integer
    testNum Maybe Integer
    testPossible
      go testNum :: Integer
    testNum st :: s
    st =
       do Integer -> Integer -> m ()
    testRptProgress Integer
    testNum Integer
    testTotal
          (TestResult, s)
    res <- Integer -> s -> m (TestResult, s)
    testFn (Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    div (100 Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    * (1 Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    testNum)) Integer
    testTotal) s
    st
          m ()
    testClrProgress
          case (TestResult, s)
    res of
            (Pass, st' :: s
    st') -> do -- delProgress -- unnecessary?
              Integer -> s -> m TestReport
    go (Integer
    testNum Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + 1) s
    st'
            (failure :: TestResult
    failure, _st' :: s
    _st') -> do
              TestResult -> m ()
    testRptFailure TestResult
    failure
              TestReport -> m TestReport
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TestReport -> m TestReport) -> TestReport -> m TestReport
    forall a b. (a -> b) -> a -> b
    $ TestResult -> String -> Integer -> Maybe Integer -> TestReport
    TestReport TestResult
    failure String
    testProp Integer
    testNum Maybe Integer
    testPossible