{-# LANGUAGE ConstraintKinds     #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications    #-}

-- | QuickCheck utilities
module Test.Util.QuickCheck (
    -- * Generic QuickCheck utilities
    checkGenerator
  , checkInvariant
  , checkShrinker
    -- * Comparison functions
  , expectRight
  , ge
  , gt
  , le
  , lt
  , strictlyIncreasing
    -- * Comparing maps
  , isSubmapOfBy
    -- * Improved variants
  , elements
  , (=:=)
    -- * SOP
  , cshrinkNP
  , shrinkNP
    -- * Convenience
  , collects
  ) where

import           Control.Monad.Except
import           Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import           Data.Proxy
import           Data.SOP.Strict
import           GHC.Stack (HasCallStack)

import           Ouroboros.Consensus.Util (repeatedly)
import           Ouroboros.Consensus.Util.Condense (Condense, condense)
import           Ouroboros.Consensus.Util.SOP

import           Test.QuickCheck hiding (elements)
import qualified Test.QuickCheck as QC

{-------------------------------------------------------------------------------
  Generic QuickCheck utilities
-------------------------------------------------------------------------------}

-- | Test the generator
--
-- Uses explicit 'forAll' as we don't want to assume a correct shrinker.
checkGenerator :: (Arbitrary a, Show a) => (a -> Property) -> Property
checkGenerator :: (a -> Property) -> Property
checkGenerator a -> Property
p = Gen a -> (a -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll Gen a
forall a. Arbitrary a => Gen a
arbitrary ((a -> Property) -> Property) -> (a -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ a -> Property
p

-- | Test the shrinker
checkShrinker :: forall a. (Arbitrary a, Show a) => (a -> Property) -> Property
checkShrinker :: (a -> Property) -> Property
checkShrinker a -> Property
p =
    -- Starting point, some arbitrary value
    -- Explicit 'forAll': don't shrink when testing the shrinker
    Gen a -> (a -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll Gen a
forall a. Arbitrary a => Gen a
arbitrary a -> Property
go
  where
    go :: a -> Property
    go :: a -> Property
go a
a =
        if [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (a -> [a]
forall a. Arbitrary a => a -> [a]
shrink a
a) then
          Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True
        else
          -- Nested 'forAll': testing that /all/ shrunk values satisfy the
          -- property is too expensive. Since we're not shrinking, nesting
          -- 'forAll' is ok.
          Gen a -> (a -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll ([a] -> Gen a
forall a. HasCallStack => [a] -> Gen a
elements (a -> [a]
forall a. Arbitrary a => a -> [a]
shrink a
a)) ((a -> Property) -> Property) -> (a -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \a
a' -> a -> Property
p a
a' Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. a -> Property
go a
a'

-- | Check invariant
checkInvariant :: (a -> Except String ()) -> (a -> Property)
checkInvariant :: (a -> Except String ()) -> a -> Property
checkInvariant a -> Except String ()
f = () -> Either String () -> Property
forall a b. (Show a, Show b, Eq b) => b -> Either a b -> Property
expectRight () (Either String () -> Property)
-> (a -> Either String ()) -> a -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Except String () -> Either String ()
forall e a. Except e a -> Either e a
runExcept (Except String () -> Either String ())
-> (a -> Except String ()) -> a -> Either String ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Except String ()
f

{-------------------------------------------------------------------------------
  Comparison functions
-------------------------------------------------------------------------------}

infix 4 `lt`
infix 4 `le`
infix 4 `gt`
infix 4 `ge`

-- | Like '<', but prints a counterexample when it fails.
lt :: (Ord a, Show a) => a -> a -> Property
a
x lt :: a -> a -> Property
`lt` a
y = String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (a -> String
forall a. Show a => a -> String
show a
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" >= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
y) (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
y

-- | Like '<=', but prints a counterexample when it fails.
le :: (Ord a, Show a) => a -> a -> Property
a
x le :: a -> a -> Property
`le` a
y = String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (a -> String
forall a. Show a => a -> String
show a
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" > " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
y) (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
y

-- | Like '>', but prints a counterexample when it fails.
gt :: (Ord a, Show a) => a -> a -> Property
a
x gt :: a -> a -> Property
`gt` a
y = String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (a -> String
forall a. Show a => a -> String
show a
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" <= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
y) (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
y

-- | Like '>=', but prints a counterexample when it fails.
ge :: (Ord a, Show a) => a -> a -> Property
a
x ge :: a -> a -> Property
`ge` a
y = String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (a -> String
forall a. Show a => a -> String
show a
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" < " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
y) (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
y

strictlyIncreasing :: forall a. (Show a, Ord a) => [a] -> Property
strictlyIncreasing :: [a] -> Property
strictlyIncreasing [a]
xs =
    String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample ([a] -> String
forall a. Show a => a -> String
show [a]
xs) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ [a] -> Property
go [a]
xs
  where
    go :: [a] -> Property
    go :: [a] -> Property
go []       = Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True
    go [a
_]      = Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True
    go (a
x:a
y:[a]
zs) = a
x a -> a -> Property
forall a. (Ord a, Show a) => a -> a -> Property
`lt` a
y Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. [a] -> Property
go (a
ya -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
zs)

-- | Check that we have the expected 'Right' value
--
-- @expectRight b ab@ is roughly equivalent to @Right b === ab@, but avoids an
-- equality constraint on @a@.
expectRight :: (Show a, Show b, Eq b) => b -> Either a b -> Property
expectRight :: b -> Either a b -> Property
expectRight b
b (Right b
b') = b
b b -> b -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== b
b'
expectRight b
_ (Left a
a)   = String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"Unexpected left " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
a) (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$
                             Bool
False

{-------------------------------------------------------------------------------
  Comparing maps
-------------------------------------------------------------------------------}

isSubmapOfBy :: (Ord k, Show k, Show a, Show b)
             => (a -> b -> Property) -> Map k a -> Map k b -> Property
isSubmapOfBy :: (a -> b -> Property) -> Map k a -> Map k b -> Property
isSubmapOfBy a -> b -> Property
p Map k a
l Map k b
r = [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin [
      case k -> Map k b -> Maybe b
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup k
k Map k b
r of
        Maybe b
Nothing -> String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"key " String -> String -> String
forall a. [a] -> [a] -> [a]
++ k -> String
forall a. Show a => a -> String
show k
k
                                String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" with value " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
a
                                String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" not present in other map") (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
                     Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
False
        Just b
b  -> String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"key " String -> String -> String
forall a. [a] -> [a] -> [a]
++ k -> String
forall a. Show a => a -> String
show k
k
                                String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" with values " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
a
                                String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" and " String -> String -> String
forall a. [a] -> [a] -> [a]
++ b -> String
forall a. Show a => a -> String
show b
b
                                String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" doesn't satisfy the property") (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
                     a -> b -> Property
p a
a b
b
    | (k
k, a
a) <- Map k a -> [(k, a)]
forall k a. Map k a -> [(k, a)]
Map.toList Map k a
l
    ]

{-------------------------------------------------------------------------------
  Improved variants
-------------------------------------------------------------------------------}

-- | Generates one of the given values. The input list must be non-empty.
--
-- NOTE unlike the standard @elements@, this variant has a 'HasCallStack'
-- constraint, which makes debugging the 'error' much easier.
elements :: HasCallStack => [a] -> Gen a
elements :: [a] -> Gen a
elements [] = String -> Gen a
forall a. HasCallStack => String -> a
error String
"Test.Util.QuickCheck.elements used with empty list"
elements [a]
xs = [a] -> Gen a
forall a. [a] -> Gen a
QC.elements [a]
xs

-- | Like '===', but uses 'Condense' instead of 'Show' when it fails.
infix 4 =:=
(=:=) :: (Eq a, Condense a) => a -> a -> Property
a
x =:= :: a -> a -> Property
=:= a
y =
    String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (a -> String
forall a. Condense a => a -> String
condense a
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ Bool -> String
interpret Bool
res String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Condense a => a -> String
condense a
y) Bool
res
  where
    res :: Bool
res = a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y
    interpret :: Bool -> String
interpret Bool
True  = String
" == "
    interpret Bool
False = String
" /= "

{-------------------------------------------------------------------------------
  SOP
-------------------------------------------------------------------------------}

cshrinkNP :: forall proxy c f g xs.
             All c xs
          => proxy c
          -> (forall a. c a => f a -> g a)    -- For elements we don't shrink
          -> (forall a. c a => f a -> [g a])
          -> NP f xs
          -> [NP g xs]
cshrinkNP :: proxy c
-> (forall a. c a => f a -> g a)
-> (forall a. c a => f a -> [g a])
-> NP f xs
-> [NP g xs]
cshrinkNP proxy c
p forall a. c a => f a -> g a
g forall a. c a => f a -> [g a]
f = NP f xs -> [NP g xs]
forall (xs' :: [*]). All c xs' => NP f xs' -> [NP g xs']
go
  where
    go :: All c xs' => NP f xs' -> [NP g xs']
    go :: NP f xs' -> [NP g xs']
go NP f xs'
Nil       = [] -- Can't shrink the empty list
    go (f x
x :* NP f xs
xs) = [[NP g (x : xs)]] -> [NP g (x : xs)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [
          -- Shrink the head of the list
          [ g x
x' g x -> NP g xs -> NP g (x : xs)
forall k (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* proxy c -> (forall a. c a => f a -> g a) -> NP f xs -> NP g xs
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
       (f' :: k -> *).
(AllN (Prod h) c xs, HAp h) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs
hcmap proxy c
p forall a. c a => f a -> g a
g NP f xs
xs | g x
x' <- f x -> [g x]
forall a. c a => f a -> [g a]
f f x
x ]

          -- Or shrink the tail of the list
        , [ f x -> g x
forall a. c a => f a -> g a
g f x
x g x -> NP g xs -> NP g (x : xs)
forall k (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP g xs
xs' | NP g xs
xs' <- NP f xs -> [NP g xs]
forall (xs' :: [*]). All c xs' => NP f xs' -> [NP g xs']
go NP f xs
xs ]
        ]

shrinkNP :: (forall a. f a -> g a)    -- For elements we don't shrink
         -> (forall a. f a -> [g a])
         -> NP f xs
         -> [NP g xs]
shrinkNP :: (forall a. f a -> g a)
-> (forall a. f a -> [g a]) -> NP f xs -> [NP g xs]
shrinkNP forall a. f a -> g a
g forall a. f a -> [g a]
f NP f xs
np = NP f xs -> (SListI xs => [NP g xs]) -> [NP g xs]
forall k (a :: k -> *) (xs :: [k]) r.
NP a xs -> (SListI xs => r) -> r
npToSListI NP f xs
np ((SListI xs => [NP g xs]) -> [NP g xs])
-> (SListI xs => [NP g xs]) -> [NP g xs]
forall a b. (a -> b) -> a -> b
$ Proxy Top
-> (forall a. Top a => f a -> g a)
-> (forall a. Top a => f a -> [g a])
-> NP f xs
-> [NP g xs]
forall (proxy :: (* -> Constraint) -> *) (c :: * -> Constraint)
       (f :: * -> *) (g :: * -> *) (xs :: [*]).
All c xs =>
proxy c
-> (forall a. c a => f a -> g a)
-> (forall a. c a => f a -> [g a])
-> NP f xs
-> [NP g xs]
cshrinkNP (Proxy Top
forall k (t :: k). Proxy t
Proxy @Top) forall a. f a -> g a
forall a. Top a => f a -> g a
g forall a. f a -> [g a]
forall a. Top a => f a -> [g a]
f NP f xs
np

{-------------------------------------------------------------------------------
  Convenience
-------------------------------------------------------------------------------}

collects :: Show a => [a] -> Property -> Property
collects :: [a] -> Property -> Property
collects = (a -> Property -> Property) -> [a] -> Property -> Property
forall a b. (a -> b -> b) -> [a] -> b -> b
repeatedly a -> Property -> Property
forall a prop. (Show a, Testable prop) => a -> prop -> Property
collect