    {-# LANGUAGE ExistentialQuantification #-}
    {-# LANGUAGE GeneralizedNewtypeDeriving #-}
    {-# LANGUAGE RankNTypes #-}

    {- |
    Module      : Test.Verification
    Description : Testing abstraction layer
    Copyright   : (c) Galois Inc, 2020
    License     : BSD3
    Maintainer  : kquick@galois.com

    This is a testing abstraction layer that allows the integration of
    test properties and functions into the What4 library without requiring
    a binding to a specific testing library or version thereof
    (e.g. QuickCheck, Hedgehog, etc.).  All test properties and functions
    should be specified using the primary set of functions in this module,
    and then the actual test code will specify a binding of these
    abstractions to a specific test library.

    In this way, the What4 can implement not only local tests but the test
    functionality can be exported to enable downstream modules to perform
    extended testing.

    The actual tests should be written using only the functions exported
    in the testing exports section of this module.  Note that only the set
    of functions needed for What4 is defined by this testing abstraction;
    if additional testing functions are needed, the GenEnv context should be
    extended to add an adaptation entry and the function should be defined
    here for use by the tests.

    The overlap (common subset) between testing libraries such as
    QuickCheck and Hedgehog is only of moderate size: both libraries (and
    especially Hedgehog) provide functionality that is not present in the
    other library.  This module does not attempt to provide full coverage
    for the functionality in both libraries; the intent is that test
    functions can be written using the proxy functions defined here and
    that downstream code using either of QuickCheck or Hedgehog can
    utilize these support functions in their own tests.  As such, it is
    recommended that the What4 integrated tests are limited in expression
    to the common subset that can be described here.

    A specific test configuration will need to use the functions and
    definitions in the concretization exports to bind these abstracted
    test functions to the specific library being used by that test suite.

    For example, to bind to QuickCheck, specify:

    > import QuickCheck
    > import qualified Test.Verification as V
    >
    > quickCheckGenerators = V.GenEnv { V.genChooseBool = elements [ True, False ]
    >                                 , V.genChooseInteger = \r -> choose r
    >                                 , V.genChooseInt = \r -> choose r
    >                                 , V.genGetSize = getSize
    >                                 }
    >
    > genTest :: String -> V.Gen V.Property -> TestTree
    > genTest nm p = testProperty nm
    >                (property $ V.toNativeProperty quickCheckGenerators p)

    -}

    module Test.Verification
      (
        -- * Testing definitions

        -- | These definitions should be used by the tests themselves.  Most
        -- of these parallel a corresponding function in QuickCheck or
        -- Hedgehog, so the adaptation is minimal.
        assuming
      , (==>)
      , property
      , chooseBool
      , chooseInt
      , chooseInteger
      , Gen
      , getSize
      , Verifiable(..)

        -- * Test concretization

        -- | Used by test implementation functions to map from this
        -- Verification abstraction to the actual test mechanism
        -- (e.g. QuickCheck, HedgeHog, etc.)
      , Property(..)
      , Assumption(..)
      , GenEnv(..)
      , toNativeProperty
      )
    where

    import Control.Monad.Trans (lift)
    import Control.Monad.Trans.Reader

    -- | Local definition of a Property: intended to be a proxy for a
    -- QuickCheck Property or a Hedgehog Property.  The 'toNativeProperty'
    -- implementation function converts from these proxy Properties to the
    -- native Property implementation.
    --
    -- Tests should only use the 'Property' type as an output; the
    -- constructors and internals should be used only by the test
    -- concretization.
    data Property = BoolProperty Bool
                  | AssumptionProp Assumption
      deriving Int -> Property -> ShowS
    [Property] -> ShowS
    Property -> String
    (Int -> Property -> ShowS)
    -> (Property -> String) -> ([Property] -> ShowS) -> Show Property
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Property -> ShowS
    showsPrec :: Int -> Property -> ShowS
    $cshow :: Property -> String
    show :: Property -> String
    $cshowList :: [Property] -> ShowS
    showList :: [Property] -> ShowS
    Show

    -- | A class specifying things that can be verified by constructing a
    -- local Property.
    class Verifiable prop where
      verifying :: prop -> Property

    instance Verifiable Bool where verifying :: Bool -> Property
    verifying = Bool -> Property
    BoolProperty

    -- | Used by testing code to assert a boolean property.
    property :: Bool -> Property
    property :: Bool -> Property
    property = Bool -> Property
    forall prop. Verifiable prop => prop -> Property
    verifying

    -- | Internal data structure to store the two elements to the '==>'
    -- assumption operator.
    data Assumption  = Assuming { Assumption -> Bool
    preCondition :: Bool,
                                  Assumption -> Property
    assumedProp :: Property }
      deriving Int -> Assumption -> ShowS
    [Assumption] -> ShowS
    Assumption -> String
    (Int -> Assumption -> ShowS)
    -> (Assumption -> String)
    -> ([Assumption] -> ShowS)
    -> Show Assumption
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Assumption -> ShowS
    showsPrec :: Int -> Assumption -> ShowS
    $cshow :: Assumption -> String
    show :: Assumption -> String
    $cshowList :: [Assumption] -> ShowS
    showList :: [Assumption] -> ShowS
    Show

    -- | The named form of the '==>' assumption operator
    assuming :: Verifiable t => Bool -> t -> Property
    assuming :: forall t. Verifiable t => Bool -> t -> Property
    assuming Bool
    precond t
    test = Assumption -> Property
    AssumptionProp (Assumption -> Property) -> Assumption -> Property
    forall a b. (a -> b) -> a -> b
    $ Bool -> Property -> Assumption
    Assuming Bool
    precond (Property -> Assumption) -> Property -> Assumption
    forall a b. (a -> b) -> a -> b
    $ t -> Property
    forall prop. Verifiable prop => prop -> Property
    verifying t
    test

    -- | The assumption operator that performs the property test (second
    -- element) only when the first argument is true (the assumption guard
    -- for the test).  This is the analog to the corresponding QuickCheck
    -- ==> operator.
    (==>) :: Verifiable t => Bool -> t -> Property
    ==> :: forall t. Verifiable t => Bool -> t -> Property
    (==>) = Bool -> t -> Property
    forall t. Verifiable t => Bool -> t -> Property
    assuming
    infixr 0 ==>

    instance Verifiable Property where
      verifying :: Property -> Property
    verifying = Property -> Property
    forall a. a -> a
    id

    -- ----------------------------------------------------------------------

    -- | This is the reader environment for the surface level proxy
    -- testing monad.  This environment will be provided by the actual
    -- test code to map these proxy operations to the specific testing
    -- implementation.
    data GenEnv m = GenEnv { forall (m :: Type -> Type). GenEnv m -> m Bool
    genChooseBool :: m Bool
                           , forall (m :: Type -> Type). GenEnv m -> (Int, Int) -> m Int
    genChooseInt :: (Int, Int) -> m Int
                           , forall (m :: Type -> Type).
    GenEnv m -> (Integer, Integer) -> m Integer
    genChooseInteger :: (Integer, Integer) -> m Integer
                           , forall (m :: Type -> Type). GenEnv m -> m Int
    genGetSize :: m Int
                           }

    -- | This is the generator monad for the Verification proxy tests.
    -- The inner monad will be the actual test implementation's monadic
    -- generator, and the 'a' return type is the type returned by running
    -- this monad.
    --
    -- Tests should only use the 'Gen TYPE' as an output; the
    -- constructors and internals should be used only by the test
    -- concretization.
    newtype Gen a =
      Gen { forall a.
    Gen a
    -> forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m a
    unGen :: forall m. Monad m => ReaderT (GenEnv m) m a }

    instance Functor Gen where
      fmap :: forall a b. (a -> b) -> Gen a -> Gen b
    fmap a -> b
    f (Gen forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m a
    m) = (forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m b)
    -> Gen b
    forall a.
    (forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m a)
    -> Gen a
    Gen ((a -> b) -> ReaderT (GenEnv m) m a -> ReaderT (GenEnv m) m b
    forall a b.
    (a -> b) -> ReaderT (GenEnv m) m a -> ReaderT (GenEnv m) m b
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    fmap a -> b
    f ReaderT (GenEnv m) m a
    forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m a
    m)

    instance Applicative Gen where
      pure :: forall a. a -> Gen a
    pure a
    x = (forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m a)
    -> Gen a
    forall a.
    (forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m a)
    -> Gen a
    Gen (a -> ReaderT (GenEnv m) m a
    forall a. a -> ReaderT (GenEnv m) m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure a
    x)
      (Gen forall (m :: Type -> Type).
    Monad m =>
    ReaderT (GenEnv m) m (a -> b)
    f) <*> :: forall a b. Gen (a -> b) -> Gen a -> Gen b
    <*> (Gen forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m a
    x) = (forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m b)
    -> Gen b
    forall a.
    (forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m a)
    -> Gen a
    Gen (ReaderT (GenEnv m) m (a -> b)
    forall (m :: Type -> Type).
    Monad m =>
    ReaderT (GenEnv m) m (a -> b)
    f ReaderT (GenEnv m) m (a -> b)
    -> ReaderT (GenEnv m) m a -> ReaderT (GenEnv m) m b
    forall a b.
    ReaderT (GenEnv m) m (a -> b)
    -> ReaderT (GenEnv m) m a -> ReaderT (GenEnv m) m b
    forall (f :: Type -> Type) a b.
    Applicative f =>
    f (a -> b) -> f a -> f b
    <*> ReaderT (GenEnv m) m a
    forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m a
    x)

    instance Monad Gen where
      Gen forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m a
    x >>= :: forall a b. Gen a -> (a -> Gen b) -> Gen b
    >>= a -> Gen b
    f = (forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m b)
    -> Gen b
    forall a.
    (forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m a)
    -> Gen a
    Gen (ReaderT (GenEnv m) m a
    forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m a
    x ReaderT (GenEnv m) m a
    -> (a -> ReaderT (GenEnv m) m b) -> ReaderT (GenEnv m) m b
    forall a b.
    ReaderT (GenEnv m) m a
    -> (a -> ReaderT (GenEnv m) m b) -> ReaderT (GenEnv m) m b
    forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a
    x' -> Gen b
    -> forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m b
    forall a.
    Gen a
    -> forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m a
    unGen (a -> Gen b
    f a
    x'))

    -- | A test generator that returns True or False
    chooseBool :: Gen Bool
    chooseBool :: Gen Bool
    chooseBool = (forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m Bool)
    -> Gen Bool
    forall a.
    (forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m a)
    -> Gen a
    Gen ((GenEnv m -> m Bool) -> ReaderT (GenEnv m) m (m Bool)
    forall (m :: Type -> Type) r a.
    Monad m =>
    (r -> a) -> ReaderT r m a
    asks GenEnv m -> m Bool
    forall (m :: Type -> Type). GenEnv m -> m Bool
    genChooseBool ReaderT (GenEnv m) m (m Bool)
    -> (m Bool -> ReaderT (GenEnv m) m Bool)
    -> ReaderT (GenEnv m) m Bool
    forall a b.
    ReaderT (GenEnv m) m a
    -> (a -> ReaderT (GenEnv m) m b) -> ReaderT (GenEnv m) m b
    forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
    >>= m Bool -> ReaderT (GenEnv m) m Bool
    forall (m :: Type -> Type) a.
    Monad m =>
    m a -> ReaderT (GenEnv m) m a
    forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift)

    -- | A test generator that returns an 'Int' value between the
    -- specified (inclusive) bounds.
    chooseInt :: (Int, Int) -> Gen Int
    chooseInt :: (Int, Int) -> Gen Int
    chooseInt (Int, Int)
    r = (forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m Int)
    -> Gen Int
    forall a.
    (forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m a)
    -> Gen a
    Gen ((GenEnv m -> (Int, Int) -> m Int)
    -> ReaderT (GenEnv m) m ((Int, Int) -> m Int)
    forall (m :: Type -> Type) r a.
    Monad m =>
    (r -> a) -> ReaderT r m a
    asks GenEnv m -> (Int, Int) -> m Int
    forall (m :: Type -> Type). GenEnv m -> (Int, Int) -> m Int
    genChooseInt ReaderT (GenEnv m) m ((Int, Int) -> m Int)
    -> (((Int, Int) -> m Int) -> ReaderT (GenEnv m) m Int)
    -> ReaderT (GenEnv m) m Int
    forall a b.
    ReaderT (GenEnv m) m a
    -> (a -> ReaderT (GenEnv m) m b) -> ReaderT (GenEnv m) m b
    forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
    >>= m Int -> ReaderT (GenEnv m) m Int
    forall (m :: Type -> Type) a.
    Monad m =>
    m a -> ReaderT (GenEnv m) m a
    forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (m Int -> ReaderT (GenEnv m) m Int)
    -> (((Int, Int) -> m Int) -> m Int)
    -> ((Int, Int) -> m Int)
    -> ReaderT (GenEnv m) m Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (((Int, Int) -> m Int) -> (Int, Int) -> m Int
    forall a b. (a -> b) -> a -> b
    $ (Int, Int)
    r))

    -- | A test generator that returns an 'Integer' value between the
    -- specified (inclusive) bounds.
    chooseInteger :: (Integer, Integer) -> Gen Integer
    chooseInteger :: (Integer, Integer) -> Gen Integer
    chooseInteger (Integer, Integer)
    r = (forall (m :: Type -> Type).
     Monad m =>
     ReaderT (GenEnv m) m Integer)
    -> Gen Integer
    forall a.
    (forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m a)
    -> Gen a
    Gen ((GenEnv m -> (Integer, Integer) -> m Integer)
    -> ReaderT (GenEnv m) m ((Integer, Integer) -> m Integer)
    forall (m :: Type -> Type) r a.
    Monad m =>
    (r -> a) -> ReaderT r m a
    asks GenEnv m -> (Integer, Integer) -> m Integer
    forall (m :: Type -> Type).
    GenEnv m -> (Integer, Integer) -> m Integer
    genChooseInteger ReaderT (GenEnv m) m ((Integer, Integer) -> m Integer)
    -> (((Integer, Integer) -> m Integer)
        -> ReaderT (GenEnv m) m Integer)
    -> ReaderT (GenEnv m) m Integer
    forall a b.
    ReaderT (GenEnv m) m a
    -> (a -> ReaderT (GenEnv m) m b) -> ReaderT (GenEnv m) m b
    forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
    >>= m Integer -> ReaderT (GenEnv m) m Integer
    forall (m :: Type -> Type) a.
    Monad m =>
    m a -> ReaderT (GenEnv m) m a
    forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (m Integer -> ReaderT (GenEnv m) m Integer)
    -> (((Integer, Integer) -> m Integer) -> m Integer)
    -> ((Integer, Integer) -> m Integer)
    -> ReaderT (GenEnv m) m Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (((Integer, Integer) -> m Integer)
    -> (Integer, Integer) -> m Integer
    forall a b. (a -> b) -> a -> b
    $ (Integer, Integer)
    r))

    -- | A test generator that returns the current shrink size of the
    -- generator functionality.
    getSize :: Gen Int
    getSize :: Gen Int
    getSize = (forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m Int)
    -> Gen Int
    forall a.
    (forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m a)
    -> Gen a
    Gen ((GenEnv m -> m Int) -> ReaderT (GenEnv m) m (m Int)
    forall (m :: Type -> Type) r a.
    Monad m =>
    (r -> a) -> ReaderT r m a
    asks GenEnv m -> m Int
    forall (m :: Type -> Type). GenEnv m -> m Int
    genGetSize ReaderT (GenEnv m) m (m Int)
    -> (m Int -> ReaderT (GenEnv m) m Int) -> ReaderT (GenEnv m) m Int
    forall a b.
    ReaderT (GenEnv m) m a
    -> (a -> ReaderT (GenEnv m) m b) -> ReaderT (GenEnv m) m b
    forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
    >>= m Int -> ReaderT (GenEnv m) m Int
    forall (m :: Type -> Type) a.
    Monad m =>
    m a -> ReaderT (GenEnv m) m a
    forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift)

    -- | This function should be called by the testing code to convert the
    -- proxy tests in this module into the native tests (e.g. QuickCheck
    -- or Hedgehog).  This function is provided with the mapping
    -- environment between the proxy tests here and the native
    -- equivalents, and a local Generator monad expression, returning a
    -- native Generator equivalent.
    toNativeProperty :: Monad m => GenEnv m -> Gen b -> m b
    toNativeProperty :: forall (m :: Type -> Type) b. Monad m => GenEnv m -> Gen b -> m b
    toNativeProperty GenEnv m
    gens (Gen forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m b
    gprops) = ReaderT (GenEnv m) m b -> GenEnv m -> m b
    forall r (m :: Type -> Type) a. ReaderT r m a -> r -> m a
    runReaderT ReaderT (GenEnv m) m b
    forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m b
    gprops GenEnv m
    gens