{-# 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),
  QuantifyConstraints,
  isEmptyQ,
  generateQ,
  shrinkQ,
  arbitraryQ,
  exactlyQ,
  elementsQ,
  oneofQ,
  frequencyQ,
  mapQ,
  whereQ,
  chooseQ,
  withGenQ,
  hasNoVariablesQ,
  validQuantification,
  Quantifiable (..),
) where

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

-- | A `Quantification` over a type @a@ is a generator that can be used to generate random values in
-- DL scenarios.
--
-- A `Quantification` is similar to a  `Test.QuickCheck.Arbitrary`, it groups together:
--
-- * A standard QuickCheck _generator_ in the `Gen` monad, which can be "empty",
-- * A _shrinking_ strategy for generated values in the case of a
--   failures ensuring they stay within the domain,
-- * A _predicate_ allowing finer grained control on generation
--   and shrinking process, e.g in the case the range of the generator
--   depends on trace context.
--
-- NOTE: Leaving the possibility of generating `Nothing` is useful to simplify the generation
-- process for `elements` or `frequency` which may normally crash when the list to select
-- elements from is empty. This makes writing `DL` formulas cleaner, removing the need to
-- handle non-existence cases explicitly.
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 = Maybe (Gen a) -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe (Gen a) -> Bool)
-> (Quantification a -> Maybe (Gen a)) -> Quantification a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Quantification a -> Maybe (Gen a)
forall a. Quantification a -> Maybe (Gen a)
genQ

generateQ :: Quantification a -> Gen a
generateQ :: forall a. Quantification a -> Gen a
generateQ Quantification a
q = Maybe (Gen a) -> Gen a
forall a. HasCallStack => Maybe a -> a
fromJust (Quantification a -> Maybe (Gen a)
forall a. Quantification a -> Maybe (Gen a)
genQ Quantification a
q) Gen a -> (a -> Bool) -> Gen a
forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` Quantification a -> a -> Bool
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 = (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
filter (Quantification a -> a -> Bool
forall a. Quantification a -> a -> Bool
isaQ Quantification a
q) (Quantification a -> a -> [a]
forall a. Quantification a -> a -> [a]
shrQ Quantification a
q a
a)

-- | Construct a `Quantification a` from its constituents.
-- Note the predicate provided is used to restrict both the range of values
-- generated and the list of possible shrinked values.
withGenQ :: Gen a -> (a -> Bool) -> (a -> [a]) -> Quantification a
withGenQ :: forall a. Gen a -> (a -> Bool) -> (a -> [a]) -> Quantification a
withGenQ Gen a
gen a -> Bool
isA = Maybe (Gen a) -> (a -> Bool) -> (a -> [a]) -> Quantification a
forall a.
Maybe (Gen a) -> (a -> Bool) -> (a -> [a]) -> Quantification a
Quantification (Gen a -> Maybe (Gen a)
forall a. a -> Maybe a
Just (Gen a -> Maybe (Gen a)) -> Gen a -> Maybe (Gen a)
forall a b. (a -> b) -> a -> b
$ Gen a
gen Gen a -> (a -> Bool) -> Gen a
forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` a -> Bool
isA) a -> Bool
isA

-- | 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 = Maybe (Gen a) -> (a -> Bool) -> (a -> [a]) -> Quantification a
forall a.
Maybe (Gen a) -> (a -> Bool) -> (a -> [a]) -> Quantification a
Quantification (Gen a -> Maybe (Gen a)
forall a. a -> Maybe a
Just Gen a
forall a. Arbitrary a => Gen a
arbitrary) (Bool -> a -> Bool
forall a b. a -> b -> a
const Bool
True) a -> [a]
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 =
  Maybe (Gen a) -> (a -> Bool) -> (a -> [a]) -> Quantification a
forall a.
Maybe (Gen a) -> (a -> Bool) -> (a -> [a]) -> Quantification a
Quantification
    (Gen a -> Maybe (Gen a)
forall a. a -> Maybe a
Just (Gen a -> Maybe (Gen a)) -> Gen a -> Maybe (Gen a)
forall a b. (a -> b) -> a -> b
$ a -> Gen a
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a)
    (a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a)
    ([a] -> 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) =
  Maybe (Gen a) -> (a -> Bool) -> (a -> [a]) -> Quantification a
forall a.
Maybe (Gen a) -> (a -> Bool) -> (a -> [a]) -> Quantification a
Quantification
    (Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
b) Maybe () -> Maybe (Gen a) -> Maybe (Gen a)
forall a b. Maybe a -> Maybe b -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Gen a -> Maybe (Gen a)
forall a. a -> Maybe a
Just ((a, a) -> Gen a
forall a. Random a => (a, a) -> Gen a
choose (a, a)
r))
    a -> Bool
is
    ((a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
filter a -> Bool
is ([a] -> [a]) -> (a -> [a]) -> a -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> [a]
forall a. Arbitrary a => a -> [a]
shrink)
  where
    is :: a -> Bool
is a
x = a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
x Bool -> Bool -> Bool
&& a
x a -> a -> Bool
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 = Maybe (Gen a) -> (a -> Bool) -> (a -> [a]) -> Quantification a
forall a.
Maybe (Gen a) -> (a -> Bool) -> (a -> [a]) -> Quantification a
Quantification Maybe (Gen a)
g (a -> [a] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [a]
as) (\a
a -> (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
a) [a]
as)
  where
    g :: Maybe (Gen a)
g
      | [a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
as = Maybe (Gen a)
forall a. Maybe a
Nothing
      | Bool
otherwise = Gen a -> Maybe (Gen a)
forall a. a -> Maybe a
Just ([a] -> Gen a
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 =
  Maybe (Gen a) -> (a -> Bool) -> (a -> [a]) -> Quantification a
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0, Just Gen a
g <- [Quantification a -> Maybe (Gen a)
forall a. Quantification a -> Maybe (Gen a)
genQ Quantification a
q]] of
        [] -> Maybe (Gen a)
forall a. Maybe a
Nothing
        [(Int, Gen a)]
igs -> Gen a -> Maybe (Gen a)
forall a. a -> Maybe a
Just ([(Int, Gen a)] -> Gen a
forall a. [(Int, Gen a)] -> Gen a
frequency [(Int, Gen a)]
igs)
    )
    ([(Int, Quantification a)] -> a -> Bool
forall {a} {t}.
(Ord a, Num a) =>
[(a, Quantification t)] -> t -> Bool
isa [(Int, Quantification a)]
iqs)
    ([(Int, Quantification a)] -> a -> [a]
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 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
0 Bool -> Bool -> Bool
&& Quantification t -> t -> 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 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
0, Quantification t -> t -> Bool
forall a. Quantification a -> a -> Bool
isaQ Quantification t
q t
a, t
a' <- Quantification t -> t -> [t]
forall a. Quantification a -> a -> [a]
shrQ Quantification t
q t
a]
        [t] -> [t] -> [t]
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 = [(Int, Quantification a)] -> Quantification a
forall a. [(Int, Quantification a)] -> Quantification a
frequencyQ ([(Int, Quantification a)] -> Quantification a)
-> [(Int, Quantification a)] -> Quantification a
forall a b. (a -> b) -> a -> b
$ (Quantification a -> (Int, Quantification a))
-> [Quantification a] -> [(Int, Quantification a)]
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 =
  Maybe (Gen b) -> (b -> Bool) -> (b -> [b]) -> Quantification b
forall a.
Maybe (Gen a) -> (a -> Bool) -> (a -> [a]) -> Quantification a
Quantification
    ((a -> b
f (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (Gen a -> Gen b) -> Maybe (Gen a) -> Maybe (Gen b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Quantification a -> Maybe (Gen a)
forall a. Quantification a -> Maybe (Gen a)
genQ Quantification a
q)
    (Quantification a -> a -> Bool
forall a. Quantification a -> a -> Bool
isaQ Quantification a
q (a -> Bool) -> (b -> a) -> b -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> a
g)
    ((a -> b) -> [a] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map a -> b
f ([a] -> [b]) -> (b -> [a]) -> b -> [b]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Quantification a -> a -> [a]
forall a. Quantification a -> a -> [a]
shrQ Quantification a
q (a -> [a]) -> (b -> a) -> b -> [a]
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 =
  Maybe (Gen a) -> (a -> Bool) -> (a -> [a]) -> Quantification a
forall a.
Maybe (Gen a) -> (a -> Bool) -> (a -> [a]) -> Quantification a
Quantification
    ( case Quantification a -> Maybe (Gen a)
forall a. Quantification a -> Maybe (Gen a)
genQ Quantification a
q of
        Just Gen a
g | Double -> Gen a -> (a -> Bool) -> Bool
forall a. Double -> Gen a -> (a -> Bool) -> Bool
canGenerate Double
0.01 Gen a
g a -> Bool
p -> Gen a -> Maybe (Gen a)
forall a. a -> Maybe a
Just (Gen a
g Gen a -> (a -> Bool) -> Gen a
forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` a -> Bool
p)
        Maybe (Gen a)
_ -> Maybe (Gen a)
forall a. Maybe a
Nothing
    )
    (\a
a -> a -> Bool
p a
a Bool -> Bool -> Bool
&& Quantification a -> a -> Bool
forall a. Quantification a -> a -> Bool
isaQ Quantification a
q a
a)
    (\a
a -> if a -> Bool
p a
a then (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
filter a -> Bool
p (Quantification a -> a -> [a]
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' =
  Maybe (Gen (a, b))
-> ((a, b) -> Bool)
-> ((a, b) -> [(a, b)])
-> Quantification (a, b)
forall a.
Maybe (Gen a) -> (a -> Bool) -> (a -> [a]) -> Quantification a
Quantification
    ((a -> b -> (a, b)) -> Gen a -> Gen b -> Gen (a, b)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (,) (Gen a -> Gen b -> Gen (a, b))
-> Maybe (Gen a) -> Maybe (Gen b -> Gen (a, b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Quantification a -> Maybe (Gen a)
forall a. Quantification a -> Maybe (Gen a)
genQ Quantification a
q Maybe (Gen b -> Gen (a, b)) -> Maybe (Gen b) -> Maybe (Gen (a, b))
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Quantification b -> Maybe (Gen b)
forall a. Quantification a -> Maybe (Gen a)
genQ Quantification b
q')
    (\(a
a, b
a') -> Quantification a -> a -> Bool
forall a. Quantification a -> a -> Bool
isaQ Quantification a
q a
a Bool -> Bool -> Bool
&& Quantification b -> b -> Bool
forall a. Quantification a -> a -> Bool
isaQ Quantification b
q' b
a')
    (\(a
a, b
a') -> (a -> (a, b)) -> [a] -> [(a, b)]
forall a b. (a -> b) -> [a] -> [b]
map (,b
a') (Quantification a -> a -> [a]
forall a. Quantification a -> a -> [a]
shrQ Quantification a
q a
a) [(a, b)] -> [(a, b)] -> [(a, b)]
forall a. [a] -> [a] -> [a]
++ (b -> (a, b)) -> [b] -> [(a, b)]
forall a b. (a -> b) -> [a] -> [b]
map (a
a,) (Quantification b -> b -> [b]
forall a. Quantification a -> a -> [a]
shrQ Quantification b
q' b
a'))

-- | Wrap a Quantification in `HasNoVariables` to indicate that you know
-- what you're doing and there are no symbolic variables in the thing you
-- are quantifying over. WARNING: use this function carefully as there is
-- no guarantee that you won't get bitten by very strange failures if you
-- were in fact not honest about the lack of variables.
hasNoVariablesQ :: Quantification a -> Quantification (HasNoVariables a)
hasNoVariablesQ :: forall a. Quantification a -> Quantification (HasNoVariables a)
hasNoVariablesQ = Quantification a -> Quantification (HasNoVariables a)
forall a b. Coercible a b => a -> b
coerce

type QuantifyConstraints a = (Eq a, Show a, Typeable a, HasVariables 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
  QuantifyConstraints (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 QuantifyConstraints a => Quantifiable (Quantification a) where
  type Quantifies (Quantification a) = a
  quantify :: Quantification a -> Quantification (Quantifies (Quantification a))
quantify = Quantification a -> Quantification a
Quantification a -> Quantification (Quantifies (Quantification a))
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) = Quantification (Quantifies a)
-> Quantification (Quantifies b)
-> Quantification (Quantifies a, Quantifies b)
forall a b.
Quantification a -> Quantification b -> Quantification (a, b)
pairQ (a -> Quantification (Quantifies a)
forall q. Quantifiable q => q -> Quantification (Quantifies q)
quantify a
a) (b -> Quantification (Quantifies b)
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) = ((Quantifies a, (Quantifies b, Quantifies c))
 -> (Quantifies a, Quantifies b, Quantifies c),
 (Quantifies a, Quantifies b, Quantifies c)
 -> (Quantifies a, (Quantifies b, Quantifies c)))
-> Quantification (Quantifies a, (Quantifies b, Quantifies c))
-> Quantification (Quantifies a, Quantifies b, Quantifies c)
forall a b.
(a -> b, b -> a) -> Quantification a -> Quantification b
mapQ ((Quantifies a, (Quantifies b, Quantifies c))
-> (Quantifies a, Quantifies b, Quantifies c)
forall {a} {b} {c}. (a, (b, c)) -> (a, b, c)
to, (Quantifies a, Quantifies b, Quantifies c)
-> (Quantifies a, (Quantifies b, Quantifies c))
forall {a} {a} {b}. (a, a, b) -> (a, (a, b))
from) (a -> Quantification (Quantifies a)
forall q. Quantifiable q => q -> Quantification (Quantifies q)
quantify a
a Quantification (Quantifies a)
-> Quantification (Quantifies b, Quantifies c)
-> Quantification (Quantifies a, (Quantifies b, Quantifies c))
forall a b.
Quantification a -> Quantification b -> Quantification (a, b)
`pairQ` (b -> Quantification (Quantifies b)
forall q. Quantifiable q => q -> Quantification (Quantifies q)
quantify b
b Quantification (Quantifies b)
-> Quantification (Quantifies c)
-> Quantification (Quantifies b, Quantifies c)
forall a b.
Quantification a -> Quantification b -> Quantification (a, b)
`pairQ` c -> Quantification (Quantifies c)
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) =
    ((Quantifies a, (Quantifies b, (Quantifies c, Quantifies d)))
 -> (Quantifies a, Quantifies b, Quantifies c, Quantifies d),
 (Quantifies a, Quantifies b, Quantifies c, Quantifies d)
 -> (Quantifies a, (Quantifies b, (Quantifies c, Quantifies d))))
-> Quantification
     (Quantifies a, (Quantifies b, (Quantifies c, Quantifies d)))
-> Quantification
     (Quantifies a, Quantifies b, Quantifies c, Quantifies d)
forall a b.
(a -> b, b -> a) -> Quantification a -> Quantification b
mapQ ((Quantifies a, (Quantifies b, (Quantifies c, Quantifies d)))
-> (Quantifies a, Quantifies b, Quantifies c, Quantifies d)
forall {a} {b} {c} {d}. (a, (b, (c, d))) -> (a, b, c, d)
to, (Quantifies a, Quantifies b, Quantifies c, Quantifies d)
-> (Quantifies a, (Quantifies b, (Quantifies c, Quantifies d)))
forall {a} {a} {a} {b}. (a, a, a, b) -> (a, (a, (a, b)))
from) (a -> Quantification (Quantifies a)
forall q. Quantifiable q => q -> Quantification (Quantifies q)
quantify a
a Quantification (Quantifies a)
-> Quantification (Quantifies b, (Quantifies c, Quantifies d))
-> Quantification
     (Quantifies a, (Quantifies b, (Quantifies c, Quantifies d)))
forall a b.
Quantification a -> Quantification b -> Quantification (a, b)
`pairQ` (b -> Quantification (Quantifies b)
forall q. Quantifiable q => q -> Quantification (Quantifies q)
quantify b
b Quantification (Quantifies b)
-> Quantification (Quantifies c, Quantifies d)
-> Quantification (Quantifies b, (Quantifies c, Quantifies d))
forall a b.
Quantification a -> Quantification b -> Quantification (a, b)
`pairQ` (c -> Quantification (Quantifies c)
forall q. Quantifiable q => q -> Quantification (Quantifies q)
quantify c
c Quantification (Quantifies c)
-> Quantification (Quantifies d)
-> Quantification (Quantifies c, Quantifies d)
forall a b.
Quantification a -> Quantification b -> Quantification (a, b)
`pairQ` d -> Quantification (Quantifies d)
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) =
    ((Quantifies a,
  (Quantifies b, (Quantifies c, (Quantifies d, Quantifies e))))
 -> (Quantifies a, Quantifies b, Quantifies c, Quantifies d,
     Quantifies e),
 (Quantifies a, Quantifies b, Quantifies c, Quantifies d,
  Quantifies e)
 -> (Quantifies a,
     (Quantifies b, (Quantifies c, (Quantifies d, Quantifies e)))))
-> Quantification
     (Quantifies a,
      (Quantifies b, (Quantifies c, (Quantifies d, Quantifies e))))
-> Quantification
     (Quantifies a, Quantifies b, Quantifies c, Quantifies d,
      Quantifies e)
forall a b.
(a -> b, b -> a) -> Quantification a -> Quantification b
mapQ ((Quantifies a,
 (Quantifies b, (Quantifies c, (Quantifies d, Quantifies e))))
-> (Quantifies a, Quantifies b, Quantifies c, Quantifies d,
    Quantifies e)
forall {a} {b} {c} {d} {e}.
(a, (b, (c, (d, e)))) -> (a, b, c, d, e)
to, (Quantifies a, Quantifies b, Quantifies c, Quantifies d,
 Quantifies e)
-> (Quantifies a,
    (Quantifies b, (Quantifies c, (Quantifies d, Quantifies e))))
forall {a} {a} {a} {a} {b}.
(a, a, a, a, b) -> (a, (a, (a, (a, b))))
from) (a -> Quantification (Quantifies a)
forall q. Quantifiable q => q -> Quantification (Quantifies q)
quantify a
a Quantification (Quantifies a)
-> Quantification
     (Quantifies b, (Quantifies c, (Quantifies d, Quantifies e)))
-> Quantification
     (Quantifies a,
      (Quantifies b, (Quantifies c, (Quantifies d, Quantifies e))))
forall a b.
Quantification a -> Quantification b -> Quantification (a, b)
`pairQ` (b -> Quantification (Quantifies b)
forall q. Quantifiable q => q -> Quantification (Quantifies q)
quantify b
b Quantification (Quantifies b)
-> Quantification (Quantifies c, (Quantifies d, Quantifies e))
-> Quantification
     (Quantifies b, (Quantifies c, (Quantifies d, Quantifies e)))
forall a b.
Quantification a -> Quantification b -> Quantification (a, b)
`pairQ` (c -> Quantification (Quantifies c)
forall q. Quantifiable q => q -> Quantification (Quantifies q)
quantify c
c Quantification (Quantifies c)
-> Quantification (Quantifies d, Quantifies e)
-> Quantification (Quantifies c, (Quantifies d, Quantifies e))
forall a b.
Quantification a -> Quantification b -> Quantification (a, b)
`pairQ` (d -> Quantification (Quantifies d)
forall q. Quantifiable q => q -> Quantification (Quantifies q)
quantify d
d Quantification (Quantifies d)
-> Quantification (Quantifies e)
-> Quantification (Quantifies d, Quantifies e)
forall a b.
Quantification a -> Quantification b -> Quantification (a, b)
`pairQ` e -> Quantification (Quantifies e)
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 [] = Maybe (Gen [Quantifies a])
-> ([Quantifies a] -> Bool)
-> ([Quantifies a] -> [[Quantifies a]])
-> Quantification [Quantifies a]
forall a.
Maybe (Gen a) -> (a -> Bool) -> (a -> [a]) -> Quantification a
Quantification (Gen [Quantifies a] -> Maybe (Gen [Quantifies a])
forall a. a -> Maybe a
Just (Gen [Quantifies a] -> Maybe (Gen [Quantifies a]))
-> Gen [Quantifies a] -> Maybe (Gen [Quantifies a])
forall a b. (a -> b) -> a -> b
$ [Quantifies a] -> Gen [Quantifies a]
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return []) [Quantifies a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([[Quantifies a]] -> [Quantifies a] -> [[Quantifies a]]
forall a b. a -> b -> a
const [])
  quantify (a
a : [a]
as) =
    ((Quantifies a, [Quantifies a]) -> [Quantifies a],
 [Quantifies a] -> (Quantifies a, [Quantifies a]))
-> Quantification (Quantifies a, [Quantifies a])
-> Quantification [Quantifies a]
forall a b.
(a -> b, b -> a) -> Quantification a -> Quantification b
mapQ ((Quantifies a, [Quantifies a]) -> [Quantifies a]
forall {a}. (a, [a]) -> [a]
to, [Quantifies a] -> (Quantifies a, [Quantifies a])
forall {a}. [a] -> (a, [a])
from) (Quantification (Quantifies a)
-> Quantification [Quantifies a]
-> Quantification (Quantifies a, [Quantifies a])
forall a b.
Quantification a -> Quantification b -> Quantification (a, b)
pairQ (a -> Quantification (Quantifies a)
forall q. Quantifiable q => q -> Quantification (Quantifies q)
quantify a
a) ([a] -> Quantification (Quantifies [a])
forall q. Quantifiable q => q -> Quantification (Quantifies q)
quantify [a]
as))
      Quantification [Quantifies a]
-> ([Quantifies a] -> Bool) -> Quantification [Quantifies a]
forall a. Quantification a -> (a -> Bool) -> Quantification a
`whereQ` (Bool -> Bool
not (Bool -> Bool)
-> ([Quantifies a] -> Bool) -> [Quantifies a] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Quantifies a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null)
    where
      to :: (a, [a]) -> [a]
to (a
x, [a]
xs) = a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
xs
      from :: [a] -> (a, [a])
from (a
x : [a]
xs) = (a
x, [a]
xs)
      from [] = [Char] -> (a, [a])
forall a. HasCallStack => [Char] -> a
error [Char]
"quantify: impossible"

-- | Turns a `Quantification` into a `Property` to enable QuickChecking its
-- validity.
validQuantification :: Show a => Quantification a -> Property
validQuantification :: forall a. Show a => Quantification a -> Property
validQuantification Quantification a
q =
  Gen a -> (a -> [a]) -> (a -> Bool) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> [a]) -> (a -> prop) -> Property
forAllShrink (Maybe (Gen a) -> Gen a
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (Gen a) -> Gen a) -> Maybe (Gen a) -> Gen a
forall a b. (a -> b) -> a -> b
$ Quantification a -> Maybe (Gen a)
forall a. Quantification a -> Maybe (Gen a)
genQ Quantification a
q) (Quantification a -> a -> [a]
forall a. Quantification a -> a -> [a]
shrinkQ Quantification a
q) ((a -> Bool) -> Property) -> (a -> Bool) -> Property
forall a b. (a -> b) -> a -> b
$ Quantification a -> a -> Bool
forall a. Quantification a -> a -> Bool
isaQ Quantification a
q