{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

module Internal.Test.QuickCheck.Quid
    where

import Control.DeepSeq
    ( NFData )
import Data.Data
    ( Data )
import Data.Hashable
    ( Hashable (..) )
import GHC.Generics
    ( Generic )
import Numeric.Natural
    ( Natural )
import Test.QuickCheck
    ( Arbitrary (..)
    , CoArbitrary (..)
    , Function (..)
    , Gen
    , chooseInteger
    , coarbitraryShow
    , functionMap
    , shrinkMapBy
    , sized
    )
import Test.QuickCheck.Function
    ( (:->) )

import qualified Data.List as L

--------------------------------------------------------------------------------
-- Quids
--------------------------------------------------------------------------------

newtype Quid = Quid
    { Quid -> Natural
unQuid :: Natural }
    deriving (Typeable Quid
Typeable Quid =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Quid -> c Quid)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Quid)
-> (Quid -> Constr)
-> (Quid -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Quid))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Quid))
-> ((forall b. Data b => b -> b) -> Quid -> Quid)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Quid -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Quid -> r)
-> (forall u. (forall d. Data d => d -> u) -> Quid -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Quid -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Quid -> m Quid)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Quid -> m Quid)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Quid -> m Quid)
-> Data Quid
Quid -> Constr
Quid -> DataType
(forall b. Data b => b -> b) -> Quid -> Quid
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Quid -> u
forall u. (forall d. Data d => d -> u) -> Quid -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Quid -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Quid -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Quid -> m Quid
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Quid -> m Quid
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Quid
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Quid -> c Quid
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Quid)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Quid)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Quid -> c Quid
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Quid -> c Quid
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Quid
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Quid
$ctoConstr :: Quid -> Constr
toConstr :: Quid -> Constr
$cdataTypeOf :: Quid -> DataType
dataTypeOf :: Quid -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Quid)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Quid)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Quid)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Quid)
$cgmapT :: (forall b. Data b => b -> b) -> Quid -> Quid
gmapT :: (forall b. Data b => b -> b) -> Quid -> Quid
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Quid -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Quid -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Quid -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Quid -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Quid -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Quid -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Quid -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Quid -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Quid -> m Quid
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Quid -> m Quid
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Quid -> m Quid
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Quid -> m Quid
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Quid -> m Quid
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Quid -> m Quid
Data, Quid -> Quid -> Bool
(Quid -> Quid -> Bool) -> (Quid -> Quid -> Bool) -> Eq Quid
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Quid -> Quid -> Bool
== :: Quid -> Quid -> Bool
$c/= :: Quid -> Quid -> Bool
/= :: Quid -> Quid -> Bool
Eq, (forall x. Quid -> Rep Quid x)
-> (forall x. Rep Quid x -> Quid) -> Generic Quid
forall x. Rep Quid x -> Quid
forall x. Quid -> Rep Quid x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Quid -> Rep Quid x
from :: forall x. Quid -> Rep Quid x
$cto :: forall x. Rep Quid x -> Quid
to :: forall x. Rep Quid x -> Quid
Generic, Eq Quid
Eq Quid =>
(Quid -> Quid -> Ordering)
-> (Quid -> Quid -> Bool)
-> (Quid -> Quid -> Bool)
-> (Quid -> Quid -> Bool)
-> (Quid -> Quid -> Bool)
-> (Quid -> Quid -> Quid)
-> (Quid -> Quid -> Quid)
-> Ord Quid
Quid -> Quid -> Bool
Quid -> Quid -> Ordering
Quid -> Quid -> Quid
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Quid -> Quid -> Ordering
compare :: Quid -> Quid -> Ordering
$c< :: Quid -> Quid -> Bool
< :: Quid -> Quid -> Bool
$c<= :: Quid -> Quid -> Bool
<= :: Quid -> Quid -> Bool
$c> :: Quid -> Quid -> Bool
> :: Quid -> Quid -> Bool
$c>= :: Quid -> Quid -> Bool
>= :: Quid -> Quid -> Bool
$cmax :: Quid -> Quid -> Quid
max :: Quid -> Quid -> Quid
$cmin :: Quid -> Quid -> Quid
min :: Quid -> Quid -> Quid
Ord)
    deriving newtype (Eq Quid
Eq Quid => (Int -> Quid -> Int) -> (Quid -> Int) -> Hashable Quid
Int -> Quid -> Int
Quid -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: Int -> Quid -> Int
hashWithSalt :: Int -> Quid -> Int
$chash :: Quid -> Int
hash :: Quid -> Int
Hashable, Quid -> ()
(Quid -> ()) -> NFData Quid
forall a. (a -> ()) -> NFData a
$crnf :: Quid -> ()
rnf :: Quid -> ()
NFData, Integer -> Quid
Quid -> Quid
Quid -> Quid -> Quid
(Quid -> Quid -> Quid)
-> (Quid -> Quid -> Quid)
-> (Quid -> Quid -> Quid)
-> (Quid -> Quid)
-> (Quid -> Quid)
-> (Quid -> Quid)
-> (Integer -> Quid)
-> Num Quid
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
$c+ :: Quid -> Quid -> Quid
+ :: Quid -> Quid -> Quid
$c- :: Quid -> Quid -> Quid
- :: Quid -> Quid -> Quid
$c* :: Quid -> Quid -> Quid
* :: Quid -> Quid -> Quid
$cnegate :: Quid -> Quid
negate :: Quid -> Quid
$cabs :: Quid -> Quid
abs :: Quid -> Quid
$csignum :: Quid -> Quid
signum :: Quid -> Quid
$cfromInteger :: Integer -> Quid
fromInteger :: Integer -> Quid
Num)

instance Arbitrary Quid where
    arbitrary :: Gen Quid
arbitrary = Gen Quid
arbitraryQuid
    shrink :: Quid -> [Quid]
shrink = Quid -> [Quid]
shrinkQuid

instance CoArbitrary Quid where
    coarbitrary :: forall b. Quid -> Gen b -> Gen b
coarbitrary = Quid -> Gen b -> Gen b
forall b. Quid -> Gen b -> Gen b
coarbitraryQuid

instance Function Quid where
    function :: forall b. (Quid -> b) -> Quid :-> b
function = (Quid -> b) -> Quid :-> b
forall b. (Quid -> b) -> Quid :-> b
functionQuid

--------------------------------------------------------------------------------
-- Generation and shrinking of arbitrary quids
--------------------------------------------------------------------------------

arbitraryQuid :: Gen Quid
arbitraryQuid :: Gen Quid
arbitraryQuid = (Int -> Gen Quid) -> Gen Quid
forall a. (Int -> Gen a) -> Gen a
sized ((Int -> Gen Quid) -> Gen Quid) -> (Int -> Gen Quid) -> Gen Quid
forall a b. (a -> b) -> a -> b
$ \Int
i -> (Quid, Quid) -> Gen Quid
chooseQuid (Natural -> Quid
Quid Natural
0, Natural -> Quid
Quid (Natural -> Quid) -> Natural -> Quid
forall a b. (a -> b) -> a -> b
$ (Natural
2 Natural -> Int -> Natural
forall a b. (Num a, Integral b) => a -> b -> a
^ Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
0 Int
i) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1)

chooseQuid :: (Quid, Quid) -> Gen Quid
chooseQuid :: (Quid, Quid) -> Gen Quid
chooseQuid (Quid Natural
n1, Quid Natural
n2) = Natural -> Quid
Quid (Natural -> Quid) -> Gen Natural -> Gen Quid
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Natural, Natural) -> Gen Natural
chooseNatural (Natural
n1, Natural
n2)

coarbitraryQuid :: Quid -> Gen a -> Gen a
coarbitraryQuid :: forall b. Quid -> Gen b -> Gen b
coarbitraryQuid = Natural -> Gen a -> Gen a
forall a b. Show a => a -> Gen b -> Gen b
coarbitraryShow (Natural -> Gen a -> Gen a)
-> (Quid -> Natural) -> Quid -> Gen a -> Gen a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Quid -> Natural
unQuid

functionQuid :: (Quid -> a) -> Quid :-> a
functionQuid :: forall b. (Quid -> b) -> Quid :-> b
functionQuid = (Quid -> String) -> (String -> Quid) -> (Quid -> a) -> Quid :-> a
forall b a c.
Function b =>
(a -> b) -> (b -> a) -> (a -> c) -> a :-> c
functionMap (Natural -> String
forall a. Show a => a -> String
show (Natural -> String) -> (Quid -> Natural) -> Quid -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Quid -> Natural
unQuid) (Natural -> Quid
Quid (Natural -> Quid) -> (String -> Natural) -> String -> Quid
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Natural
forall a. Read a => String -> a
read)

shrinkQuid :: Quid -> [Quid]
shrinkQuid :: Quid -> [Quid]
shrinkQuid = (Natural -> Quid)
-> (Quid -> Natural) -> (Natural -> [Natural]) -> Quid -> [Quid]
forall a b. (a -> b) -> (b -> a) -> (a -> [a]) -> b -> [b]
shrinkMapBy Natural -> Quid
Quid Quid -> Natural
unQuid Natural -> [Natural]
shrinkNatural

--------------------------------------------------------------------------------
-- Conversion between quids and natural numbers
--------------------------------------------------------------------------------

naturalToQuid :: Natural -> Quid
naturalToQuid :: Natural -> Quid
naturalToQuid = Natural -> Quid
Quid

quidToNatural :: Quid -> Natural
quidToNatural :: Quid -> Natural
quidToNatural = Quid -> Natural
unQuid

--------------------------------------------------------------------------------
-- Natural number support
--------------------------------------------------------------------------------

chooseNatural :: (Natural, Natural) -> Gen Natural
chooseNatural :: (Natural, Natural) -> Gen Natural
chooseNatural (Natural
p, Natural
q) = forall a b. (Integral a, Num b) => a -> b
fromIntegral @Integer @Natural (Integer -> Natural) -> Gen Integer -> Gen Natural
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
    (Integer, Integer) -> Gen Integer
chooseInteger (Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
p, Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
q)

shrinkNatural :: Natural -> [Natural]
shrinkNatural :: Natural -> [Natural]
shrinkNatural Natural
n
    | Natural
n Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
0 = []
    | Bool
otherwise = [Natural] -> [Natural]
forall a. Eq a => [a] -> [a]
L.nub ([Natural] -> [Natural]) -> [Natural] -> [Natural]
forall a b. (a -> b) -> a -> b
$ Natural
0 Natural -> [Natural] -> [Natural]
forall a. a -> [a] -> [a]
: [Natural]
as [Natural] -> [Natural] -> [Natural]
forall a. Semigroup a => a -> a -> a
<> [Natural]
bs
  where
    as :: [Natural]
as = (Natural -> Bool) -> [Natural] -> [Natural]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
<= Natural
n Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`div` Natural
2) ((Natural -> Natural) -> Natural -> [Natural]
forall a. (a -> a) -> a -> [a]
iterate (Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
2) Natural
1)
    bs :: [Natural]
bs = (Natural
n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
-) (Natural -> Natural) -> [Natural] -> [Natural]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Natural] -> [Natural]
forall a. [a] -> [a]
reverse [Natural]
as