module Polysemy.Check.Arbitrary.Generic where

import Control.Applicative (liftA2)
import Data.Kind (Type)
import GHC.Exts (type (~~))
import Generics.Kind
import Test.QuickCheck
import Polysemy
import Polysemy.Check.Arbitrary.AnyEff
import Polysemy.Internal (send)


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

type a :~~~: b = 'Kon (~~) ':@: a ':@: b


------------------------------------------------------------------------------
-- | Given @'GArbitraryK' a ('RepK' (e m a))@, this typeclass computes
-- generators for every well-typed constructor of @e m a@. It is capable of
-- building generators for GADTs.
class GArbitraryK (a :: Type) (f :: LoT Type -> Type) where
  garbitraryk :: [Gen (f x)]

instance GArbitraryK a U1 where
  garbitraryk :: [Gen (U1 x)]
garbitraryk = Gen (U1 x) -> [Gen (U1 x)]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Gen (U1 x) -> [Gen (U1 x)]) -> Gen (U1 x) -> [Gen (U1 x)]
forall a b. (a -> b) -> a -> b
$ U1 x -> Gen (U1 x)
forall (f :: * -> *) a. Applicative f => a -> f a
pure U1 x
forall k (p :: k). U1 p
U1

instance (GArbitraryK1 (f :*: g)) => GArbitraryK a (f :*: g) where
  garbitraryk :: [Gen ((:*:) f g x)]
garbitraryk = [Gen ((:*:) f g x)]
forall (f :: LoT * -> *) (x :: LoT *).
GArbitraryK1 f =>
[Gen (f x)]
garbitraryk1

instance (GArbitraryK1 (Field b)) => GArbitraryK a (Field b) where
  garbitraryk :: [Gen (Field b x)]
garbitraryk = [Gen (Field b x)]
forall (f :: LoT * -> *) (x :: LoT *).
GArbitraryK1 f =>
[Gen (f x)]
garbitraryk1

instance (GArbitraryK a f, GArbitraryK a g) => GArbitraryK a (f :+: g) where
  garbitraryk :: [Gen ((:+:) f g x)]
garbitraryk = (Gen (f x) -> Gen ((:+:) f g x))
-> [Gen (f x)] -> [Gen ((:+:) f g x)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((f x -> (:+:) f g x) -> Gen (f x) -> Gen ((:+:) f g x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f x -> (:+:) f g x
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1) (forall (x :: LoT *). GArbitraryK a f => [Gen (f x)]
forall a (f :: LoT * -> *) (x :: LoT *).
GArbitraryK a f =>
[Gen (f x)]
garbitraryk @a @f)
             [Gen ((:+:) f g x)] -> [Gen ((:+:) f g x)] -> [Gen ((:+:) f g x)]
forall a. Semigroup a => a -> a -> a
<> (Gen (g x) -> Gen ((:+:) f g x))
-> [Gen (g x)] -> [Gen ((:+:) f g x)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((g x -> (:+:) f g x) -> Gen (g x) -> Gen ((:+:) f g x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap g x -> (:+:) f g x
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1) (forall (x :: LoT *). GArbitraryK a g => [Gen (g x)]
forall a (f :: LoT * -> *) (x :: LoT *).
GArbitraryK a f =>
[Gen (f x)]
garbitraryk @a @g)

instance GArbitraryK1 f => GArbitraryK a ('Kon (a ~~ a) :=>: f) where
  garbitraryk :: [Gen ((:=>:) ('Kon (a ~~ a)) f x)]
garbitraryk = (f x -> (:=>:) ('Kon (a ~~ a)) f x)
-> Gen (f x) -> Gen ((:=>:) ('Kon (a ~~ a)) f x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f x -> (:=>:) ('Kon (a ~~ a)) f x
forall d (c :: Atom d Constraint) (x :: LoT d) (f :: LoT d -> *).
Interpret c x =>
f x -> (:=>:) c f x
SuchThat (Gen (f x) -> Gen ((:=>:) ('Kon (a ~~ a)) f x))
-> [Gen (f x)] -> [Gen ((:=>:) ('Kon (a ~~ a)) f x)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Gen (f x)]
forall (f :: LoT * -> *) (x :: LoT *).
GArbitraryK1 f =>
[Gen (f x)]
garbitraryk1

instance {-# INCOHERENT #-} GArbitraryK a ('Kon (a ~~ b) :=>: f) where
  garbitraryk :: [Gen ((:=>:) ('Kon (a ~~ b)) f x)]
garbitraryk = []

instance {-# INCOHERENT #-} GArbitraryK a ('Kon (b ~~ c) :=>: f) where
  garbitraryk :: [Gen ((:=>:) ('Kon (b ~~ c)) f x)]
garbitraryk = []

instance (GArbitraryK a f) => GArbitraryK a (M1 _1 _2 f) where
  garbitraryk :: [Gen (M1 _1 _2 f x)]
garbitraryk = (f x -> M1 _1 _2 f x) -> Gen (f x) -> Gen (M1 _1 _2 f x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f x -> M1 _1 _2 f x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (Gen (f x) -> Gen (M1 _1 _2 f x))
-> [Gen (f x)] -> [Gen (M1 _1 _2 f x)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (f :: LoT * -> *) (x :: LoT *).
GArbitraryK a f =>
[Gen (f x)]
forall (f :: LoT * -> *) (x :: LoT *).
GArbitraryK a f =>
[Gen (f x)]
garbitraryk @a


------------------------------------------------------------------------------
-- | @genEff \@e \@a \@m@ gets a generator capable of producing every
-- well-typed GADT constructor of @e m a@.
genEff :: forall e a m. (GArbitraryK a (RepK (e m a)), GenericK (e m a)) => Gen (e m a)
genEff :: Gen (e m a)
genEff = (RepK (e m a) Any -> e m a)
-> Gen (RepK (e m a) Any) -> Gen (e m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RepK (e m a) Any -> e m a
forall k (f :: k) (x :: LoT k). GenericK f => RepK f x -> f :@@: x
toK (Gen (RepK (e m a) Any) -> Gen (e m a))
-> Gen (RepK (e m a) Any) -> Gen (e m a)
forall a b. (a -> b) -> a -> b
$ [Gen (RepK (e m a) Any)] -> Gen (RepK (e m a) Any)
forall a. [Gen a] -> Gen a
oneof ([Gen (RepK (e m a) Any)] -> Gen (RepK (e m a) Any))
-> [Gen (RepK (e m a) Any)] -> Gen (RepK (e m a) Any)
forall a b. (a -> b) -> a -> b
$ forall (x :: LoT *).
GArbitraryK a (RepK (e m a)) =>
[Gen (RepK (e m a) x)]
forall a (f :: LoT * -> *) (x :: LoT *).
GArbitraryK a f =>
[Gen (f x)]
garbitraryk @a @(RepK (e m a))


------------------------------------------------------------------------------
-- | Like @GArbitraryK@, but gets run after we've already discharged the @a
-- ~ T@ GADT constraint.
class GArbitraryK1 (f :: LoT Type -> Type) where
  garbitraryk1 :: [Gen (f x)]

instance (GArbitraryK1 f, GArbitraryK1 g) => GArbitraryK1 (f :*: g) where
  garbitraryk1 :: [Gen ((:*:) f g x)]
garbitraryk1 = (Gen (f x) -> Gen (g x) -> Gen ((:*:) f g x))
-> [Gen (f x)] -> [Gen (g x)] -> [Gen ((:*:) f g x)]
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 ((f x -> g x -> (:*:) f g x)
-> Gen (f x) -> Gen (g x) -> Gen ((:*:) f g x)
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 f x -> g x -> (:*:) f g x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
(:*:)) [Gen (f x)]
forall (f :: LoT * -> *) (x :: LoT *).
GArbitraryK1 f =>
[Gen (f x)]
garbitraryk1 [Gen (g x)]
forall (f :: LoT * -> *) (x :: LoT *).
GArbitraryK1 f =>
[Gen (f x)]
garbitraryk1

instance GArbitraryKTerm t => GArbitraryK1 (Field ('Kon t)) where
  garbitraryk1 :: [Gen (Field ('Kon t) x)]
garbitraryk1 = Gen (Field ('Kon t) x) -> [Gen (Field ('Kon t) x)]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Gen (Field ('Kon t) x) -> [Gen (Field ('Kon t) x)])
-> Gen (Field ('Kon t) x) -> [Gen (Field ('Kon t) x)]
forall a b. (a -> b) -> a -> b
$ (t -> Field ('Kon t) x) -> Gen t -> Gen (Field ('Kon t) x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap t -> Field ('Kon t) x
forall d (t :: Atom d *) (x :: LoT d). Interpret t x -> Field t x
Field Gen t
forall t. GArbitraryKTerm t => Gen t
garbitrarykterm

instance (GArbitraryK1 f) => GArbitraryK1 (M1 _1 _2 f) where
  garbitraryk1 :: [Gen (M1 _1 _2 f x)]
garbitraryk1 = (f x -> M1 _1 _2 f x) -> Gen (f x) -> Gen (M1 _1 _2 f x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f x -> M1 _1 _2 f x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (Gen (f x) -> Gen (M1 _1 _2 f x))
-> [Gen (f x)] -> [Gen (M1 _1 _2 f x)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Gen (f x)]
forall (f :: LoT * -> *) (x :: LoT *).
GArbitraryK1 f =>
[Gen (f x)]
garbitraryk1

instance GArbitraryK1 U1 where
  garbitraryk1 :: [Gen (U1 x)]
garbitraryk1 = Gen (U1 x) -> [Gen (U1 x)]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Gen (U1 x) -> [Gen (U1 x)]) -> Gen (U1 x) -> [Gen (U1 x)]
forall a b. (a -> b) -> a -> b
$ U1 x -> Gen (U1 x)
forall (f :: * -> *) a. Applicative f => a -> f a
pure U1 x
forall k (p :: k). U1 p
U1


class GArbitraryKTerm (t :: Type) where
  garbitrarykterm :: Gen t

instance {-# OVERLAPPING #-} ArbitraryEffOfType a r r => GArbitraryKTerm (Sem r a) where
  garbitrarykterm :: Gen (Sem r a)
garbitrarykterm = do
    SomeEffOfType act :: e (Sem r) a
act <- [Gen (SomeEffOfType r a)] -> Gen (SomeEffOfType r a)
forall a. [Gen a] -> Gen a
oneof ([Gen (SomeEffOfType r a)] -> Gen (SomeEffOfType r a))
-> [Gen (SomeEffOfType r a)] -> Gen (SomeEffOfType r a)
forall a b. (a -> b) -> a -> b
$ ArbitraryEffOfType a r r => [Gen (SomeEffOfType r a)]
forall a (es :: EffectRow) (r :: EffectRow).
ArbitraryEffOfType a es r =>
[Gen (SomeEffOfType r a)]
genSomeEffOfType @a @r @r
    Sem r a -> Gen (Sem r a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Sem r a -> Gen (Sem r a)) -> Sem r a -> Gen (Sem r a)
forall a b. (a -> b) -> a -> b
$ e (Sem r) a -> Sem r a
forall (e :: (* -> *) -> * -> *) (r :: EffectRow) a.
Member e r =>
e (Sem r) a -> Sem r a
send e (Sem r) a
act

instance {-# OVERLAPPING #-} (CoArbitrary a, GArbitraryKTerm b) => GArbitraryKTerm (a -> b) where
  garbitrarykterm :: Gen (a -> b)
garbitrarykterm = Gen b -> Gen (a -> b)
forall (f :: * -> *) a. Arbitrary1 f => Gen a -> Gen (f a)
liftArbitrary Gen b
forall t. GArbitraryKTerm t => Gen t
garbitrarykterm

instance Arbitrary a => GArbitraryKTerm a where
  garbitrarykterm :: Gen a
garbitrarykterm = Gen a
forall a. Arbitrary a => Gen a
arbitrary