{-# OPTIONS_GHC -fno-warn-name-shadowing #-}

-- | This module defines Quantifications, which are used together with
--   forAllQ in DynamicLogic. A `Quantification t` can be used to generate
--   a `t`, shrink a `t`, and recognise a generated `t`.
module Test.QuickCheck.DynamicLogic.Quantify (
  Quantification (isaQ),
  isEmptyQ,
  generateQ,
  shrinkQ,
  arbitraryQ,
  exactlyQ,
  elementsQ,
  oneofQ,
  frequencyQ,
  mapQ,
  whereQ,
  chooseQ,
  withGenQ,
  validQuantification,
  Quantifiable (..),
) where

import Control.Monad
import Data.Maybe
import Data.Typeable
import System.Random
import Test.QuickCheck
import Test.QuickCheck.DynamicLogic.CanGenerate

-- | A `Quantification` over a type @a@ is a generator that can be used with
--   `Plutus.Contract.Test.ContractModel.forAllQ` to generate random values in
--   DL scenarios. In addition to a QuickCheck generator a `Quantification` contains a shrinking
--   strategy that ensures that shrunk values stay in the range of the generator.
data Quantification a = Quantification
  { forall a. Quantification a -> Maybe (Gen a)
genQ :: Maybe (Gen a)
  , forall a. Quantification a -> a -> Bool
isaQ :: a -> Bool
  , forall a. Quantification a -> a -> [a]
shrQ :: a -> [a]
  }

isEmptyQ :: Quantification a -> Bool
isEmptyQ :: forall a. Quantification a -> Bool
isEmptyQ = forall a. Maybe a -> Bool
isNothing forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Quantification a -> Maybe (Gen a)
genQ

generateQ :: Quantification a -> Gen a
generateQ :: forall a. Quantification a -> Gen a
generateQ Quantification a
q = forall a. HasCallStack => Maybe a -> a
fromJust (forall a. Quantification a -> Maybe (Gen a)
genQ Quantification a
q) forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` forall a. Quantification a -> a -> Bool
isaQ Quantification a
q

shrinkQ :: Quantification a -> a -> [a]
shrinkQ :: forall a. Quantification a -> a -> [a]
shrinkQ Quantification a
q a
a = forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Quantification a -> a -> Bool
isaQ Quantification a
q) (forall a. Quantification a -> a -> [a]
shrQ Quantification a
q a
a)

-- | Wrap a `Gen a` generator in a `Quantification a`.
-- Uses given shrinker.
withGenQ :: Gen a -> (a -> [a]) -> Quantification a
withGenQ :: forall a. Gen a -> (a -> [a]) -> Quantification a
withGenQ Gen a
gen = forall a.
Maybe (Gen a) -> (a -> Bool) -> (a -> [a]) -> Quantification a
Quantification (forall a. a -> Maybe a
Just Gen a
gen) (forall a b. a -> b -> a
const Bool
True)

-- | Pack up an `Arbitrary` instance as a `Quantification`. Treats all values as being in range.
arbitraryQ :: Arbitrary a => Quantification a
arbitraryQ :: forall a. Arbitrary a => Quantification a
arbitraryQ = forall a.
Maybe (Gen a) -> (a -> Bool) -> (a -> [a]) -> Quantification a
Quantification (forall a. a -> Maybe a
Just forall a. Arbitrary a => Gen a
arbitrary) (forall a b. a -> b -> a
const Bool
True) forall a. Arbitrary a => a -> [a]
shrink

-- | Generates exactly the given value. Does not shrink.
exactlyQ :: Eq a => a -> Quantification a
exactlyQ :: forall a. Eq a => a -> Quantification a
exactlyQ a
a =
  forall a.
Maybe (Gen a) -> (a -> Bool) -> (a -> [a]) -> Quantification a
Quantification
    (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return a
a)
    (forall a. Eq a => a -> a -> Bool
== a
a)
    (forall a b. a -> b -> a
const [])

-- | Generate a random value in a given range (inclusive).
chooseQ :: (Arbitrary a, Random a, Ord a) => (a, a) -> Quantification a
chooseQ :: forall a.
(Arbitrary a, Random a, Ord a) =>
(a, a) -> Quantification a
chooseQ r :: (a, a)
r@(a
a, a
b) =
  forall a.
Maybe (Gen a) -> (a -> Bool) -> (a -> [a]) -> Quantification a
Quantification
    (forall (f :: * -> *). Alternative f => Bool -> f ()
guard (a
a forall a. Ord a => a -> a -> Bool
<= a
b) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a. a -> Maybe a
Just (forall a. Random a => (a, a) -> Gen a
choose (a, a)
r))
    a -> Bool
is
    (forall a. (a -> Bool) -> [a] -> [a]
filter a -> Bool
is forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Arbitrary a => a -> [a]
shrink)
 where
  is :: a -> Bool
is a
x = a
a forall a. Ord a => a -> a -> Bool
<= a
x Bool -> Bool -> Bool
&& a
x forall a. Ord a => a -> a -> Bool
<= a
b

-- | Pick a random value from a list. Treated as an empty choice if the list is empty:
--
-- @
-- `Plutus.Contract.Test.ContractModel.forAllQ` (`elementsQ` []) == `Control.Applicative.empty`
-- @
elementsQ :: Eq a => [a] -> Quantification a
elementsQ :: forall a. Eq a => [a] -> Quantification a
elementsQ [a]
as = forall a.
Maybe (Gen a) -> (a -> Bool) -> (a -> [a]) -> Quantification a
Quantification Maybe (Gen a)
g (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [a]
as) (\a
a -> forall a. (a -> Bool) -> [a] -> [a]
takeWhile (forall a. Eq a => a -> a -> Bool
/= a
a) [a]
as)
 where
  g :: Maybe (Gen a)
g
    | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
as = forall a. Maybe a
Nothing
    | Bool
otherwise = forall a. a -> Maybe a
Just (forall a. [a] -> Gen a
elements [a]
as)

-- | Choose from a weighted list of quantifications. Treated as an `Control.Applicative.empty`
--   choice if no quantification has weight > 0.
frequencyQ :: [(Int, Quantification a)] -> Quantification a
frequencyQ :: forall a. [(Int, Quantification a)] -> Quantification a
frequencyQ [(Int, Quantification a)]
iqs =
  forall a.
Maybe (Gen a) -> (a -> Bool) -> (a -> [a]) -> Quantification a
Quantification
    ( case [(Int
i, Gen a
g) | (Int
i, Quantification a
q) <- [(Int, Quantification a)]
iqs, Int
i forall a. Ord a => a -> a -> Bool
> Int
0, Just Gen a
g <- [forall a. Quantification a -> Maybe (Gen a)
genQ Quantification a
q]] of
        [] -> forall a. Maybe a
Nothing
        [(Int, Gen a)]
igs -> forall a. a -> Maybe a
Just (forall a. [(Int, Gen a)] -> Gen a
frequency [(Int, Gen a)]
igs)
    )
    (forall {a} {t}.
(Ord a, Num a) =>
[(a, Quantification t)] -> t -> Bool
isa [(Int, Quantification a)]
iqs)
    (forall {a} {t}.
(Ord a, Num a) =>
[(a, Quantification t)] -> t -> [t]
shr [(Int, Quantification a)]
iqs)
 where
  isa :: [(a, Quantification t)] -> t -> Bool
isa [] t
_ = Bool
False
  isa ((a
i, Quantification t
q) : [(a, Quantification t)]
iqs) t
a = (a
i forall a. Ord a => a -> a -> Bool
> a
0 Bool -> Bool -> Bool
&& forall a. Quantification a -> a -> Bool
isaQ Quantification t
q t
a) Bool -> Bool -> Bool
|| [(a, Quantification t)] -> t -> Bool
isa [(a, Quantification t)]
iqs t
a
  shr :: [(a, Quantification t)] -> t -> [t]
shr [] t
_ = []
  shr ((a
i, Quantification t
q) : [(a, Quantification t)]
iqs) t
a =
    [t
a' | a
i forall a. Ord a => a -> a -> Bool
> a
0, forall a. Quantification a -> a -> Bool
isaQ Quantification t
q t
a, t
a' <- forall a. Quantification a -> a -> [a]
shrQ Quantification t
q t
a]
      forall a. [a] -> [a] -> [a]
++ [(a, Quantification t)] -> t -> [t]
shr [(a, Quantification t)]
iqs t
a

-- | Choose from a list of quantifications. Same as `frequencyQ` with all weights the same (and >
--   0).
oneofQ :: [Quantification a] -> Quantification a
oneofQ :: forall a. [Quantification a] -> Quantification a
oneofQ [Quantification a]
qs = forall a. [(Int, Quantification a)] -> Quantification a
frequencyQ forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (Int
1,) [Quantification a]
qs

-- | `Quantification` is not a `Functor`, since it also keeps track of the range of the generators.
--   However, if you have two functions
-- @
-- to   :: a -> b
-- from :: b -> a
-- @
--   satisfying @from . to = id@ you can go from a quantification over @a@ to one over @b@. Note
--   that the @from@ function need only be defined on the image of @to@.
mapQ :: (a -> b, b -> a) -> Quantification a -> Quantification b
mapQ :: forall a b.
(a -> b, b -> a) -> Quantification a -> Quantification b
mapQ (a -> b
f, b -> a
g) Quantification a
q =
  forall a.
Maybe (Gen a) -> (a -> Bool) -> (a -> [a]) -> Quantification a
Quantification
    ((a -> b
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Quantification a -> Maybe (Gen a)
genQ Quantification a
q)
    (forall a. Quantification a -> a -> Bool
isaQ Quantification a
q forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> a
g)
    (forall a b. (a -> b) -> [a] -> [b]
map a -> b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Quantification a -> a -> [a]
shrQ Quantification a
q forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> a
g)

-- | Restrict the range of a quantification.
whereQ :: Quantification a -> (a -> Bool) -> Quantification a
whereQ :: forall a. Quantification a -> (a -> Bool) -> Quantification a
whereQ Quantification a
q a -> Bool
p =
  forall a.
Maybe (Gen a) -> (a -> Bool) -> (a -> [a]) -> Quantification a
Quantification
    ( case forall a. Quantification a -> Maybe (Gen a)
genQ Quantification a
q of
        Just Gen a
g | forall a. Double -> Gen a -> (a -> Bool) -> Bool
canGenerate Double
0.01 Gen a
g a -> Bool
p -> forall a. a -> Maybe a
Just (Gen a
g forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` a -> Bool
p)
        Maybe (Gen a)
_ -> forall a. Maybe a
Nothing
    )
    (\a
a -> a -> Bool
p a
a Bool -> Bool -> Bool
&& forall a. Quantification a -> a -> Bool
isaQ Quantification a
q a
a)
    (\a
a -> if a -> Bool
p a
a then forall a. (a -> Bool) -> [a] -> [a]
filter a -> Bool
p (forall a. Quantification a -> a -> [a]
shrQ Quantification a
q a
a) else [])

pairQ :: Quantification a -> Quantification b -> Quantification (a, b)
pairQ :: forall a b.
Quantification a -> Quantification b -> Quantification (a, b)
pairQ Quantification a
q Quantification b
q' =
  forall a.
Maybe (Gen a) -> (a -> Bool) -> (a -> [a]) -> Quantification a
Quantification
    (forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Quantification a -> Maybe (Gen a)
genQ Quantification a
q forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Quantification a -> Maybe (Gen a)
genQ Quantification b
q')
    (\(a
a, b
a') -> forall a. Quantification a -> a -> Bool
isaQ Quantification a
q a
a Bool -> Bool -> Bool
&& forall a. Quantification a -> a -> Bool
isaQ Quantification b
q' b
a')
    (\(a
a, b
a') -> forall a b. (a -> b) -> [a] -> [b]
map (,b
a') (forall a. Quantification a -> a -> [a]
shrQ Quantification a
q a
a) forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (a
a,) (forall a. Quantification a -> a -> [a]
shrQ Quantification b
q' b
a'))

-- | Generalization of `Quantification`s, which lets you treat lists and tuples of quantifications
--   as quantifications. For instance,
--
-- @
--   ...
--   (die1, die2) <- `Plutus.Contract.Test.ContractModel.forAllQ` (`chooseQ` (1, 6), `chooseQ` (1, 6))
--   ...
-- @
class
  (Eq (Quantifies q), Show (Quantifies q), Typeable (Quantifies q)) =>
  Quantifiable q
  where
  -- | The type of values quantified over.
  --
  -- @
  -- `Quantifies` (`Quantification` a) = a
  -- @
  type Quantifies q

  -- | Computing the actual `Quantification`.
  quantify :: q -> Quantification (Quantifies q)

instance (Eq a, Show a, Typeable a) => Quantifiable (Quantification a) where
  type Quantifies (Quantification a) = a
  quantify :: Quantification a -> Quantification (Quantifies (Quantification a))
quantify = forall a. a -> a
id

instance (Quantifiable a, Quantifiable b) => Quantifiable (a, b) where
  type Quantifies (a, b) = (Quantifies a, Quantifies b)
  quantify :: (a, b) -> Quantification (Quantifies (a, b))
quantify (a
a, b
b) = forall a b.
Quantification a -> Quantification b -> Quantification (a, b)
pairQ (forall q. Quantifiable q => q -> Quantification (Quantifies q)
quantify a
a) (forall q. Quantifiable q => q -> Quantification (Quantifies q)
quantify b
b)

instance (Quantifiable a, Quantifiable b, Quantifiable c) => Quantifiable (a, b, c) where
  type Quantifies (a, b, c) = (Quantifies a, Quantifies b, Quantifies c)
  quantify :: (a, b, c) -> Quantification (Quantifies (a, b, c))
quantify (a
a, b
b, c
c) = forall a b.
(a -> b, b -> a) -> Quantification a -> Quantification b
mapQ (forall {a} {b} {c}. (a, (b, c)) -> (a, b, c)
to, forall {a} {a} {b}. (a, a, b) -> (a, (a, b))
from) (forall q. Quantifiable q => q -> Quantification (Quantifies q)
quantify a
a forall a b.
Quantification a -> Quantification b -> Quantification (a, b)
`pairQ` (forall q. Quantifiable q => q -> Quantification (Quantifies q)
quantify b
b forall a b.
Quantification a -> Quantification b -> Quantification (a, b)
`pairQ` forall q. Quantifiable q => q -> Quantification (Quantifies q)
quantify c
c))
   where
    to :: (a, (b, c)) -> (a, b, c)
to (a
a, (b
b, c
c)) = (a
a, b
b, c
c)
    from :: (a, a, b) -> (a, (a, b))
from (a
a, a
b, b
c) = (a
a, (a
b, b
c))

instance (Quantifiable a, Quantifiable b, Quantifiable c, Quantifiable d) => Quantifiable (a, b, c, d) where
  type
    Quantifies (a, b, c, d) =
      (Quantifies a, Quantifies b, Quantifies c, Quantifies d)
  quantify :: (a, b, c, d) -> Quantification (Quantifies (a, b, c, d))
quantify (a
a, b
b, c
c, d
d) =
    forall a b.
(a -> b, b -> a) -> Quantification a -> Quantification b
mapQ (forall {a} {b} {c} {d}. (a, (b, (c, d))) -> (a, b, c, d)
to, forall {a} {a} {a} {b}. (a, a, a, b) -> (a, (a, (a, b)))
from) (forall q. Quantifiable q => q -> Quantification (Quantifies q)
quantify a
a forall a b.
Quantification a -> Quantification b -> Quantification (a, b)
`pairQ` (forall q. Quantifiable q => q -> Quantification (Quantifies q)
quantify b
b forall a b.
Quantification a -> Quantification b -> Quantification (a, b)
`pairQ` (forall q. Quantifiable q => q -> Quantification (Quantifies q)
quantify c
c forall a b.
Quantification a -> Quantification b -> Quantification (a, b)
`pairQ` forall q. Quantifiable q => q -> Quantification (Quantifies q)
quantify d
d)))
   where
    to :: (a, (b, (c, d))) -> (a, b, c, d)
to (a
a, (b
b, (c
c, d
d))) = (a
a, b
b, c
c, d
d)
    from :: (a, a, a, b) -> (a, (a, (a, b)))
from (a
a, a
b, a
c, b
d) = (a
a, (a
b, (a
c, b
d)))

instance
  (Quantifiable a, Quantifiable b, Quantifiable c, Quantifiable d, Quantifiable e) =>
  Quantifiable (a, b, c, d, e)
  where
  type
    Quantifies (a, b, c, d, e) =
      (Quantifies a, Quantifies b, Quantifies c, Quantifies d, Quantifies e)
  quantify :: (a, b, c, d, e) -> Quantification (Quantifies (a, b, c, d, e))
quantify (a
a, b
b, c
c, d
d, e
e) =
    forall a b.
(a -> b, b -> a) -> Quantification a -> Quantification b
mapQ (forall {a} {b} {c} {d} {e}.
(a, (b, (c, (d, e)))) -> (a, b, c, d, e)
to, forall {a} {a} {a} {a} {b}.
(a, a, a, a, b) -> (a, (a, (a, (a, b))))
from) (forall q. Quantifiable q => q -> Quantification (Quantifies q)
quantify a
a forall a b.
Quantification a -> Quantification b -> Quantification (a, b)
`pairQ` (forall q. Quantifiable q => q -> Quantification (Quantifies q)
quantify b
b forall a b.
Quantification a -> Quantification b -> Quantification (a, b)
`pairQ` (forall q. Quantifiable q => q -> Quantification (Quantifies q)
quantify c
c forall a b.
Quantification a -> Quantification b -> Quantification (a, b)
`pairQ` (forall q. Quantifiable q => q -> Quantification (Quantifies q)
quantify d
d forall a b.
Quantification a -> Quantification b -> Quantification (a, b)
`pairQ` forall q. Quantifiable q => q -> Quantification (Quantifies q)
quantify e
e))))
   where
    to :: (a, (b, (c, (d, e)))) -> (a, b, c, d, e)
to (a
a, (b
b, (c
c, (d
d, e
e)))) = (a
a, b
b, c
c, d
d, e
e)
    from :: (a, a, a, a, b) -> (a, (a, (a, (a, b))))
from (a
a, a
b, a
c, a
d, b
e) = (a
a, (a
b, (a
c, (a
d, b
e))))

instance Quantifiable a => Quantifiable [a] where
  type Quantifies [a] = [Quantifies a]
  quantify :: [a] -> Quantification (Quantifies [a])
quantify [] = forall a.
Maybe (Gen a) -> (a -> Bool) -> (a -> [a]) -> Quantification a
Quantification (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return []) forall (t :: * -> *) a. Foldable t => t a -> Bool
null (forall a b. a -> b -> a
const [])
  quantify (a
a : [a]
as) =
    forall a b.
(a -> b, b -> a) -> Quantification a -> Quantification b
mapQ (forall {a}. (a, [a]) -> [a]
to, forall {a}. [a] -> (a, [a])
from) (forall a b.
Quantification a -> Quantification b -> Quantification (a, b)
pairQ (forall q. Quantifiable q => q -> Quantification (Quantifies q)
quantify a
a) (forall q. Quantifiable q => q -> Quantification (Quantifies q)
quantify [a]
as))
      forall a. Quantification a -> (a -> Bool) -> Quantification a
`whereQ` (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Bool
null)
   where
    to :: (a, [a]) -> [a]
to (a
x, [a]
xs) = a
x forall a. a -> [a] -> [a]
: [a]
xs
    from :: [a] -> (a, [a])
from (a
x : [a]
xs) = (a
x, [a]
xs)
    from [] = forall a. HasCallStack => [Char] -> a
error [Char]
"quantify: impossible"

validQuantification :: Show a => Quantification a -> Property
validQuantification :: forall a. Show a => Quantification a -> Property
validQuantification Quantification a
q =
  forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> [a]) -> (a -> prop) -> Property
forAllShrink (forall a. HasCallStack => Maybe a -> a
fromJust forall a b. (a -> b) -> a -> b
$ forall a. Quantification a -> Maybe (Gen a)
genQ Quantification a
q) (forall a. Quantification a -> a -> [a]
shrinkQ Quantification a
q) forall a b. (a -> b) -> a -> b
$ forall a. Quantification a -> a -> Bool
isaQ Quantification a
q