{-# OPTIONS_HADDOCK not-home #-}

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- | Base case discovery.
--
-- === Warning
--
-- This is an internal module: it is not subject to any versioning policy,
-- breaking changes can happen at any time.
--
-- If something here seems useful, please report it or create a pull request to
-- export it from an external module.

module Generic.Random.Internal.BaseCase where

import Control.Applicative
import Data.Proxy
import Data.Kind (Type)
import GHC.Generics
import GHC.TypeLits
import Test.QuickCheck

import Generic.Random.Internal.Generic

-- | Decrease size to ensure termination for
-- recursive types, looking for base cases once the size reaches 0.
--
-- > genericArbitrary' (17 % 19 % 23 % ()) :: Gen a
--
-- N.B.: This replaces the generator for fields of type @[t]@ with
-- @'Test.QuickCheck.listOf'' arbitrary@ instead of @'Test.QuickCheck.listOf' arbitrary@ (i.e., @arbitrary@ for
-- lists).
genericArbitrary'
  :: (GArbitrary SizedOptsDef a, BaseCase a)
  => Weights a  -- ^ List of weights for every constructor
  -> Gen a
genericArbitrary' :: Weights a -> Gen a
genericArbitrary' Weights a
w = Weights a -> Gen a
forall a. GArbitrary SizedOptsDef a => Weights a -> Gen a
genericArbitraryRec Weights a
w Gen a -> Gen a -> Gen a
forall a. Gen a -> Gen a -> Gen a
`withBaseCase` Gen a
forall a. BaseCase a => Gen a
baseCase

-- | Equivalent to @'genericArbitrary'' 'uniform'@.
--
-- > genericArbitraryU' :: Gen a
--
-- N.B.: This replaces the generator for fields of type @[t]@ with
-- @'Test.QuickCheck.listOf'' arbitrary@ instead of @'Test.QuickCheck.listOf' arbitrary@ (i.e., @arbitrary@ for
-- lists).
genericArbitraryU'
  :: (GArbitrary SizedOptsDef a, BaseCase a, GUniformWeight a)
  => Gen a
genericArbitraryU' :: Gen a
genericArbitraryU' = Weights a -> Gen a
forall a.
(GArbitrary SizedOptsDef a, BaseCase a) =>
Weights a -> Gen a
genericArbitrary' Weights a
forall a. UniformWeight_ (Rep a) => Weights a
uniform

-- | Run the first generator if the size is positive.
-- Run the second if the size is zero.
--
-- > defaultGen `withBaseCase` baseCaseGen
withBaseCase :: Gen a -> Gen a -> Gen a
withBaseCase :: Gen a -> Gen a -> Gen a
withBaseCase Gen a
def Gen a
bc = (Int -> Gen a) -> Gen a
forall a. (Int -> Gen a) -> Gen a
sized ((Int -> Gen a) -> Gen a) -> (Int -> Gen a) -> Gen a
forall a b. (a -> b) -> a -> b
$ \Int
sz ->
  if Int
sz Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 then Gen a
def else Gen a
bc


-- | Find a base case of type @a@ with maximum depth @z@,
-- recursively using 'BaseCaseSearch' instances to search deeper levels.
--
-- @y@ is the depth of a base case, if found.
--
-- @e@ is the original type the search started with, that @a@ appears in.
-- It is used for error reporting.
class BaseCaseSearch (a :: Type) (z :: Nat) (y :: Maybe Nat) (e :: Type) where
  baseCaseSearch :: prox y -> proxy '(z, e) -> IfM y Gen Proxy a


instance {-# OVERLAPPABLE #-} GBaseCaseSearch a z y e => BaseCaseSearch a z y e where
  baseCaseSearch :: prox y -> proxy '(z, e) -> IfM y Gen Proxy a
baseCaseSearch = prox y -> proxy '(z, e) -> IfM y Gen Proxy a
forall k t k a (z :: k) (y :: Maybe t) (e :: k)
       (prox :: Maybe t -> *) (proxy :: (k, k) -> *).
GBaseCaseSearch a z y e =>
prox y -> proxy '(z, e) -> IfM y Gen Proxy a
gBaseCaseSearch


instance (y ~ 'Just 0) => BaseCaseSearch Char z y e where
  baseCaseSearch :: prox y -> proxy '(z, e) -> IfM y Gen Proxy Char
baseCaseSearch prox y
_ proxy '(z, e)
_ = IfM y Gen Proxy Char
forall a. Arbitrary a => Gen a
arbitrary

instance (y ~ 'Just 0) => BaseCaseSearch Int z y e where
  baseCaseSearch :: prox y -> proxy '(z, e) -> IfM y Gen Proxy Int
baseCaseSearch prox y
_ proxy '(z, e)
_ = IfM y Gen Proxy Int
forall a. Arbitrary a => Gen a
arbitrary

instance (y ~ 'Just 0) => BaseCaseSearch Integer z y e where
  baseCaseSearch :: prox y -> proxy '(z, e) -> IfM y Gen Proxy Integer
baseCaseSearch prox y
_ proxy '(z, e)
_ = IfM y Gen Proxy Integer
forall a. Arbitrary a => Gen a
arbitrary

instance (y ~ 'Just 0) => BaseCaseSearch Float z y e where
  baseCaseSearch :: prox y -> proxy '(z, e) -> IfM y Gen Proxy Float
baseCaseSearch prox y
_ proxy '(z, e)
_ = IfM y Gen Proxy Float
forall a. Arbitrary a => Gen a
arbitrary

instance (y ~ 'Just 0) => BaseCaseSearch Double z y e where
  baseCaseSearch :: prox y -> proxy '(z, e) -> IfM y Gen Proxy Double
baseCaseSearch prox y
_ proxy '(z, e)
_ = IfM y Gen Proxy Double
forall a. Arbitrary a => Gen a
arbitrary

instance (y ~ 'Just 0) => BaseCaseSearch Word z y e where
  baseCaseSearch :: prox y -> proxy '(z, e) -> IfM y Gen Proxy Word
baseCaseSearch prox y
_ proxy '(z, e)
_ = IfM y Gen Proxy Word
forall a. Arbitrary a => Gen a
arbitrary

instance (y ~ 'Just 0) => BaseCaseSearch () z y e where
  baseCaseSearch :: prox y -> proxy '(z, e) -> IfM y Gen Proxy ()
baseCaseSearch prox y
_ proxy '(z, e)
_ = IfM y Gen Proxy ()
forall a. Arbitrary a => Gen a
arbitrary

instance (y ~ 'Just 0) => BaseCaseSearch Bool z y e where
  baseCaseSearch :: prox y -> proxy '(z, e) -> IfM y Gen Proxy Bool
baseCaseSearch prox y
_ proxy '(z, e)
_ = IfM y Gen Proxy Bool
forall a. Arbitrary a => Gen a
arbitrary

instance (y ~ 'Just 0) => BaseCaseSearch [a] z y e where
  baseCaseSearch :: prox y -> proxy '(z, e) -> IfM y Gen Proxy [a]
baseCaseSearch prox y
_ proxy '(z, e)
_ = [a] -> Gen [a]
forall (m :: * -> *) a. Monad m => a -> m a
return []

instance (y ~ 'Just 0) => BaseCaseSearch Ordering z y e where
  baseCaseSearch :: prox y -> proxy '(z, e) -> IfM y Gen Proxy Ordering
baseCaseSearch prox y
_ proxy '(z, e)
_ = IfM y Gen Proxy Ordering
forall a. Arbitrary a => Gen a
arbitrary

-- Either and (,) use Generics


class BaseCaseSearching_ a z y where
  baseCaseSearching_ :: proxy y -> proxy2 '(z, a) -> IfM y Gen Proxy a -> Gen a

instance BaseCaseSearching_ a z ('Just m) where
  baseCaseSearching_ :: proxy ('Just m)
-> proxy2 '(z, a) -> IfM ('Just m) Gen Proxy a -> Gen a
baseCaseSearching_ proxy ('Just m)
_ proxy2 '(z, a)
_ = IfM ('Just m) Gen Proxy a -> Gen a
forall a. a -> a
id

instance BaseCaseSearching a (z + 1) => BaseCaseSearching_ a z 'Nothing where
  baseCaseSearching_ :: proxy 'Nothing
-> proxy2 '(z, a) -> IfM 'Nothing Gen Proxy a -> Gen a
baseCaseSearching_ proxy 'Nothing
_ proxy2 '(z, a)
_ IfM 'Nothing Gen Proxy a
_ = Proxy '(z + 1, a) -> Gen a
forall k a (z :: k) (proxy :: (k, *) -> *).
BaseCaseSearching a z =>
proxy '(z, a) -> Gen a
baseCaseSearching (Proxy '(z + 1, a)
forall k (t :: k). Proxy t
Proxy :: Proxy '(z + 1, a))

-- | Progressively increase the depth bound for 'BaseCaseSearch'.
class BaseCaseSearching a z where
  baseCaseSearching :: proxy '(z, a) -> Gen a

instance (BaseCaseSearch a z y a, BaseCaseSearching_ a z y) => BaseCaseSearching a z where
  baseCaseSearching :: proxy '(z, a) -> Gen a
baseCaseSearching proxy '(z, a)
z = Proxy y -> proxy '(z, a) -> IfM y Gen Proxy a -> Gen a
forall k t a (z :: k) (y :: Maybe t) (proxy :: Maybe t -> *)
       (proxy2 :: (k, *) -> *).
BaseCaseSearching_ a z y =>
proxy y -> proxy2 '(z, a) -> IfM y Gen Proxy a -> Gen a
baseCaseSearching_ Proxy y
y proxy '(z, a)
z (Proxy y -> proxy '(z, a) -> IfM y Gen Proxy a
forall a (z :: Nat) (y :: Maybe Nat) e (prox :: Maybe Nat -> *)
       (proxy :: (Nat, *) -> *).
BaseCaseSearch a z y e =>
prox y -> proxy '(z, e) -> IfM y Gen Proxy a
baseCaseSearch Proxy y
y proxy '(z, a)
z)
    where
      y :: Proxy y
y = Proxy y
forall k (t :: k). Proxy t
Proxy :: Proxy y

-- | Custom instances can override the default behavior.
class BaseCase a where
  -- | Generator of base cases.
  baseCase :: Gen a

-- | Overlappable
instance {-# OVERLAPPABLE #-} BaseCaseSearching a 0 => BaseCase a where
  baseCase :: Gen a
baseCase = Proxy '(0, a) -> Gen a
forall k a (z :: k) (proxy :: (k, *) -> *).
BaseCaseSearching a z =>
proxy '(z, a) -> Gen a
baseCaseSearching (Proxy '(0, a)
forall k (t :: k). Proxy t
Proxy :: Proxy '(0, a))


type family IfM (b :: Maybe t) (c :: k) (d :: k) :: k
type instance IfM ('Just t) c d = c
type instance IfM 'Nothing c d = d

type (==) m n = IsEQ (CmpNat m n)

type family IsEQ (e :: Ordering) :: Bool
type instance IsEQ 'EQ = 'True
type instance IsEQ 'GT = 'False
type instance IsEQ 'LT = 'False

type family (||?) (b :: Maybe Nat) (c :: Maybe Nat) :: Maybe Nat
type instance 'Just m ||? 'Just n = 'Just (Min m n)
type instance m ||? 'Nothing = m
type instance 'Nothing ||? n = n

type family (&&?) (b :: Maybe Nat) (c :: Maybe Nat) :: Maybe Nat
type instance 'Just m &&? 'Just n = 'Just (Max m n)
type instance m &&? 'Nothing = 'Nothing
type instance 'Nothing &&? n = 'Nothing

type Max m n = MaxOf (CmpNat m n) m n

type family MaxOf (e :: Ordering) (m :: k) (n :: k) :: k
type instance MaxOf 'GT m n = m
type instance MaxOf 'EQ m n = m
type instance MaxOf 'LT m n = n

type Min m n = MinOf (CmpNat m n) m n

type family MinOf (e :: Ordering) (m :: k) (n :: k) :: k
type instance MinOf 'GT m n = n
type instance MinOf 'EQ m n = n
type instance MinOf 'LT m n = m

class Alternative (IfM y Weighted Proxy)
  => GBCS (f :: k -> Type) (z :: Nat) (y :: Maybe Nat) (e :: Type) where
  gbcs :: prox y -> proxy '(z, e) -> IfM y Weighted Proxy (f p)

instance GBCS f z y e => GBCS (M1 i c f) z y e where
  gbcs :: prox y -> proxy '(z, e) -> IfM y Weighted Proxy (M1 i c f p)
gbcs prox y
y proxy '(z, e)
z = (f p -> M1 i c f p)
-> IfM y Weighted Proxy (f p) -> IfM y Weighted Proxy (M1 i c f p)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f p -> M1 i c f p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (prox y -> proxy '(z, e) -> IfM y Weighted Proxy (f p)
forall k (f :: k -> *) (z :: Nat) (y :: Maybe Nat) e
       (prox :: Maybe Nat -> *) (proxy :: (Nat, *) -> *) (p :: k).
GBCS f z y e =>
prox y -> proxy '(z, e) -> IfM y Weighted Proxy (f p)
gbcs prox y
y proxy '(z, e)
z)

instance
  ( Alternative (IfM y Weighted Proxy)  -- logically redundant, but GHC isn't clever
                                        -- enough to deduce; see #32
  , GBCSSum f g z e yf yg
  , GBCS f z yf e
  , GBCS g z yg e
  , y ~ (yf ||? yg)
  ) => GBCS (f :+: g) z y e where
  gbcs :: prox y -> proxy '(z, e) -> IfM y Weighted Proxy ((:+:) f g p)
gbcs prox y
_ proxy '(z, e)
z = Proxy '(yf, yg)
-> proxy '(z, e)
-> IfM yf Weighted Proxy (f p)
-> IfM yg Weighted Proxy (g p)
-> IfM (yf ||? yg) Weighted Proxy ((:+:) f g p)
forall k k k (f :: k -> *) (g :: k -> *) (z :: k) (e :: k)
       (yf :: Maybe Nat) (yg :: Maybe Nat)
       (prox :: (Maybe Nat, Maybe Nat) -> *) (proxy :: (k, k) -> *)
       (p :: k).
GBCSSum f g z e yf yg =>
prox '(yf, yg)
-> proxy '(z, e)
-> IfM yf Weighted Proxy (f p)
-> IfM yg Weighted Proxy (g p)
-> IfM (yf ||? yg) Weighted Proxy ((:+:) f g p)
gbcsSum (Proxy '(yf, yg)
forall k (t :: k). Proxy t
Proxy :: Proxy '(yf, yg)) proxy '(z, e)
z
    (Proxy yf -> proxy '(z, e) -> IfM yf Weighted Proxy (f p)
forall k (f :: k -> *) (z :: Nat) (y :: Maybe Nat) e
       (prox :: Maybe Nat -> *) (proxy :: (Nat, *) -> *) (p :: k).
GBCS f z y e =>
prox y -> proxy '(z, e) -> IfM y Weighted Proxy (f p)
gbcs (Proxy yf
forall k (t :: k). Proxy t
Proxy :: Proxy yf) proxy '(z, e)
z)
    (Proxy yg -> proxy '(z, e) -> IfM yg Weighted Proxy (g p)
forall k (f :: k -> *) (z :: Nat) (y :: Maybe Nat) e
       (prox :: Maybe Nat -> *) (proxy :: (Nat, *) -> *) (p :: k).
GBCS f z y e =>
prox y -> proxy '(z, e) -> IfM y Weighted Proxy (f p)
gbcs (Proxy yg
forall k (t :: k). Proxy t
Proxy :: Proxy yg) proxy '(z, e)
z)

class Alternative (IfM (yf ||? yg) Weighted Proxy) => GBCSSum f g z e yf yg where
  gbcsSum
    :: prox '(yf, yg)
    -> proxy '(z, e)
    -> IfM yf Weighted Proxy (f p)
    -> IfM yg Weighted Proxy (g p)
    -> IfM (yf ||? yg) Weighted Proxy ((f :+: g) p)

instance GBCSSum f g z e 'Nothing 'Nothing where
  gbcsSum :: prox '( 'Nothing, 'Nothing)
-> proxy '(z, e)
-> IfM 'Nothing Weighted Proxy (f p)
-> IfM 'Nothing Weighted Proxy (g p)
-> IfM ('Nothing ||? 'Nothing) Weighted Proxy ((:+:) f g p)
gbcsSum prox '( 'Nothing, 'Nothing)
_ proxy '(z, e)
_ IfM 'Nothing Weighted Proxy (f p)
_ IfM 'Nothing Weighted Proxy (g p)
_ = IfM ('Nothing ||? 'Nothing) Weighted Proxy ((:+:) f g p)
forall k (t :: k). Proxy t
Proxy

instance GBCSSum f g z e ('Just m) 'Nothing where
  gbcsSum :: prox '( 'Just m, 'Nothing)
-> proxy '(z, e)
-> IfM ('Just m) Weighted Proxy (f p)
-> IfM 'Nothing Weighted Proxy (g p)
-> IfM ('Just m ||? 'Nothing) Weighted Proxy ((:+:) f g p)
gbcsSum prox '( 'Just m, 'Nothing)
_ proxy '(z, e)
_ IfM ('Just m) Weighted Proxy (f p)
f IfM 'Nothing Weighted Proxy (g p)
_ = (f p -> (:+:) f g p) -> Weighted (f p) -> Weighted ((:+:) f g p)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f p -> (:+:) f g p
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 Weighted (f p)
IfM ('Just m) Weighted Proxy (f p)
f

instance GBCSSum f g z e 'Nothing ('Just n) where
  gbcsSum :: prox '( 'Nothing, 'Just n)
-> proxy '(z, e)
-> IfM 'Nothing Weighted Proxy (f p)
-> IfM ('Just n) Weighted Proxy (g p)
-> IfM ('Nothing ||? 'Just n) Weighted Proxy ((:+:) f g p)
gbcsSum prox '( 'Nothing, 'Just n)
_ proxy '(z, e)
_ IfM 'Nothing Weighted Proxy (f p)
_ IfM ('Just n) Weighted Proxy (g p)
g = (g p -> (:+:) f g p) -> Weighted (g p) -> Weighted ((:+:) f g p)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap g p -> (:+:) f g p
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 Weighted (g p)
IfM ('Just n) Weighted Proxy (g p)
g

instance GBCSSumCompare f g z e (CmpNat m n)
  => GBCSSum f g z e ('Just m) ('Just n) where
  gbcsSum :: prox '( 'Just m, 'Just n)
-> proxy '(z, e)
-> IfM ('Just m) Weighted Proxy (f p)
-> IfM ('Just n) Weighted Proxy (g p)
-> IfM ('Just m ||? 'Just n) Weighted Proxy ((:+:) f g p)
gbcsSum prox '( 'Just m, 'Just n)
_ = Proxy (CmpNat m n)
-> proxy '(z, e)
-> Weighted (f p)
-> Weighted (g p)
-> Weighted ((:+:) f g p)
forall k k k k (f :: k -> *) (g :: k -> *) (z :: k) (e :: k)
       (o :: k) (proxy0 :: k -> *) (proxy :: (k, k) -> *) (p :: k).
GBCSSumCompare f g z e o =>
proxy0 o
-> proxy '(z, e)
-> Weighted (f p)
-> Weighted (g p)
-> Weighted ((:+:) f g p)
gbcsSumCompare (Proxy (CmpNat m n)
forall k (t :: k). Proxy t
Proxy :: Proxy (CmpNat m n))

class GBCSSumCompare f g z e o where
  gbcsSumCompare
    :: proxy0 o
    -> proxy '(z, e)
    -> Weighted (f p)
    -> Weighted (g p)
    -> Weighted ((f :+: g) p)

instance GBCSSumCompare f g z e 'EQ where
  gbcsSumCompare :: proxy0 'EQ
-> proxy '(z, e)
-> Weighted (f p)
-> Weighted (g p)
-> Weighted ((:+:) f g p)
gbcsSumCompare proxy0 'EQ
_ proxy '(z, e)
_ Weighted (f p)
f Weighted (g p)
g = (f p -> (:+:) f g p) -> Weighted (f p) -> Weighted ((:+:) f g p)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f p -> (:+:) f g p
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 Weighted (f p)
f Weighted ((:+:) f g p)
-> Weighted ((:+:) f g p) -> Weighted ((:+:) f g p)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (g p -> (:+:) f g p) -> Weighted (g p) -> Weighted ((:+:) f g p)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap g p -> (:+:) f g p
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 Weighted (g p)
g

instance GBCSSumCompare f g z e 'LT where
  gbcsSumCompare :: proxy0 'LT
-> proxy '(z, e)
-> Weighted (f p)
-> Weighted (g p)
-> Weighted ((:+:) f g p)
gbcsSumCompare proxy0 'LT
_ proxy '(z, e)
_ Weighted (f p)
f Weighted (g p)
_ = (f p -> (:+:) f g p) -> Weighted (f p) -> Weighted ((:+:) f g p)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f p -> (:+:) f g p
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 Weighted (f p)
f

instance GBCSSumCompare f g z e 'GT where
  gbcsSumCompare :: proxy0 'GT
-> proxy '(z, e)
-> Weighted (f p)
-> Weighted (g p)
-> Weighted ((:+:) f g p)
gbcsSumCompare proxy0 'GT
_ proxy '(z, e)
_ Weighted (f p)
_ Weighted (g p)
g = (g p -> (:+:) f g p) -> Weighted (g p) -> Weighted ((:+:) f g p)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap g p -> (:+:) f g p
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 Weighted (g p)
g

instance
  ( Alternative (IfM y Weighted Proxy)  -- logically redundant, but GHC isn't clever
                                        -- enough to deduce; see #32
  , GBCSProduct f g z e yf yg
  , GBCS f z yf e
  , GBCS g z yg e
  , y ~ (yf &&? yg)
  ) => GBCS (f :*: g) z y e where
  gbcs :: prox y -> proxy '(z, e) -> IfM y Weighted Proxy ((:*:) f g p)
gbcs prox y
_ proxy '(z, e)
z = Proxy '(yf, yg)
-> proxy '(z, e)
-> IfM yf Weighted Proxy (f p)
-> IfM yg Weighted Proxy (g p)
-> IfM (yf &&? yg) Weighted Proxy ((:*:) f g p)
forall k k k (f :: k -> *) (g :: k -> *) (z :: k) (e :: k)
       (yf :: Maybe Nat) (yg :: Maybe Nat)
       (prox :: (Maybe Nat, Maybe Nat) -> *) (proxy :: (k, k) -> *)
       (p :: k).
GBCSProduct f g z e yf yg =>
prox '(yf, yg)
-> proxy '(z, e)
-> IfM yf Weighted Proxy (f p)
-> IfM yg Weighted Proxy (g p)
-> IfM (yf &&? yg) Weighted Proxy ((:*:) f g p)
gbcsProduct (Proxy '(yf, yg)
forall k (t :: k). Proxy t
Proxy :: Proxy '(yf, yg)) proxy '(z, e)
z
    (Proxy yf -> proxy '(z, e) -> IfM yf Weighted Proxy (f p)
forall k (f :: k -> *) (z :: Nat) (y :: Maybe Nat) e
       (prox :: Maybe Nat -> *) (proxy :: (Nat, *) -> *) (p :: k).
GBCS f z y e =>
prox y -> proxy '(z, e) -> IfM y Weighted Proxy (f p)
gbcs (Proxy yf
forall k (t :: k). Proxy t
Proxy :: Proxy yf) proxy '(z, e)
z)
    (Proxy yg -> proxy '(z, e) -> IfM yg Weighted Proxy (g p)
forall k (f :: k -> *) (z :: Nat) (y :: Maybe Nat) e
       (prox :: Maybe Nat -> *) (proxy :: (Nat, *) -> *) (p :: k).
GBCS f z y e =>
prox y -> proxy '(z, e) -> IfM y Weighted Proxy (f p)
gbcs (Proxy yg
forall k (t :: k). Proxy t
Proxy :: Proxy yg) proxy '(z, e)
z)

class Alternative (IfM (yf &&? yg) Weighted Proxy) => GBCSProduct f g z e yf yg where
  gbcsProduct
    :: prox '(yf, yg)
    -> proxy '(z, e)
    -> IfM yf Weighted Proxy (f p)
    -> IfM yg Weighted Proxy (g p)
    -> IfM (yf &&? yg) Weighted Proxy ((f :*: g) p)

instance {-# OVERLAPPABLE #-} ((yf &&? yg) ~ 'Nothing) => GBCSProduct f g z e yf yg where
  gbcsProduct :: prox '(yf, yg)
-> proxy '(z, e)
-> IfM yf Weighted Proxy (f p)
-> IfM yg Weighted Proxy (g p)
-> IfM (yf &&? yg) Weighted Proxy ((:*:) f g p)
gbcsProduct prox '(yf, yg)
_ proxy '(z, e)
_ IfM yf Weighted Proxy (f p)
_ IfM yg Weighted Proxy (g p)
_ = IfM (yf &&? yg) Weighted Proxy ((:*:) f g p)
forall k (t :: k). Proxy t
Proxy

instance GBCSProduct f g z e ('Just m) ('Just n) where
  gbcsProduct :: prox '( 'Just m, 'Just n)
-> proxy '(z, e)
-> IfM ('Just m) Weighted Proxy (f p)
-> IfM ('Just n) Weighted Proxy (g p)
-> IfM ('Just m &&? 'Just n) Weighted Proxy ((:*:) f g p)
gbcsProduct prox '( 'Just m, 'Just n)
_ proxy '(z, e)
_ IfM ('Just m) Weighted Proxy (f p)
f IfM ('Just n) Weighted Proxy (g p)
g = (f p -> g p -> (:*:) f g p)
-> Weighted (f p) -> Weighted (g p) -> Weighted ((:*:) f g p)
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 f p -> g p -> (:*:) f g p
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
(:*:) Weighted (f p)
IfM ('Just m) Weighted Proxy (f p)
f Weighted (g p)
IfM ('Just n) Weighted Proxy (g p)
g

class IsMaybe b where
  ifMmap :: proxy b -> (c a -> c' a') -> (d a -> d' a') -> IfM b c d a -> IfM b c' d' a'
  ifM :: proxy b -> c a -> d a -> IfM b c d a

instance IsMaybe ('Just t) where
  ifMmap :: proxy ('Just t)
-> (c a -> c' a')
-> (d a -> d' a')
-> IfM ('Just t) c d a
-> IfM ('Just t) c' d' a'
ifMmap proxy ('Just t)
_ c a -> c' a'
f d a -> d' a'
_ IfM ('Just t) c d a
a = c a -> c' a'
f c a
IfM ('Just t) c d a
a
  ifM :: proxy ('Just t) -> c a -> d a -> IfM ('Just t) c d a
ifM proxy ('Just t)
_ c a
f d a
_ = c a
IfM ('Just t) c d a
f

instance IsMaybe 'Nothing where
  ifMmap :: proxy 'Nothing
-> (c a -> c' a')
-> (d a -> d' a')
-> IfM 'Nothing c d a
-> IfM 'Nothing c' d' a'
ifMmap proxy 'Nothing
_ c a -> c' a'
_ d a -> d' a'
g IfM 'Nothing c d a
a = d a -> d' a'
g d a
IfM 'Nothing c d a
a
  ifM :: proxy 'Nothing -> c a -> d a -> IfM 'Nothing c d a
ifM proxy 'Nothing
_ c a
_ d a
g = d a
IfM 'Nothing c d a
g

instance {-# OVERLAPPABLE #-}
  ( BaseCaseSearch c (z - 1) y e
  , (z == 0) ~ 'False
  , Alternative (IfM y Weighted Proxy)
  , IsMaybe y
  ) => GBCS (K1 i c) z y e where
  gbcs :: prox y -> proxy '(z, e) -> IfM y Weighted Proxy (K1 i c p)
gbcs prox y
y proxy '(z, e)
_ =
    (c -> K1 i c p)
-> IfM y Weighted Proxy c -> IfM y Weighted Proxy (K1 i c p)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap c -> K1 i c p
forall k i c (p :: k). c -> K1 i c p
K1
      (prox y
-> (Gen c -> Weighted c)
-> (Proxy c -> Proxy c)
-> IfM y Gen Proxy c
-> IfM y Weighted Proxy c
forall t (b :: Maybe t) k k (proxy :: Maybe t -> *) (c :: k -> *)
       (a :: k) (c' :: k -> *) (a' :: k) (d :: k -> *) (d' :: k -> *).
IsMaybe b =>
proxy b
-> (c a -> c' a')
-> (d a -> d' a')
-> IfM b c d a
-> IfM b c' d' a'
ifMmap prox y
y
        Gen c -> Weighted c
forall a. Gen a -> Weighted a
liftGen
        (Proxy c -> Proxy c
forall a. a -> a
id :: Proxy c -> Proxy c)
        (prox y -> Proxy '(z - 1, e) -> IfM y Gen Proxy c
forall a (z :: Nat) (y :: Maybe Nat) e (prox :: Maybe Nat -> *)
       (proxy :: (Nat, *) -> *).
BaseCaseSearch a z y e =>
prox y -> proxy '(z, e) -> IfM y Gen Proxy a
baseCaseSearch prox y
y (Proxy '(z - 1, e)
forall k (t :: k). Proxy t
Proxy :: Proxy '(z - 1, e))))

instance (y ~ 'Nothing) => GBCS (K1 i c) 0 y e where
  gbcs :: prox y -> proxy '(0, e) -> IfM y Weighted Proxy (K1 i c p)
gbcs prox y
_ proxy '(0, e)
_ = IfM y Weighted Proxy (K1 i c p)
forall (f :: * -> *) a. Alternative f => f a
empty

instance (y ~ 'Just 0) => GBCS U1 z y e where
  gbcs :: prox y -> proxy '(z, e) -> IfM y Weighted Proxy (U1 p)
gbcs prox y
_ proxy '(z, e)
_ = U1 p -> Weighted (U1 p)
forall (f :: * -> *) a. Applicative f => a -> f a
pure U1 p
forall k (p :: k). U1 p
U1

instance {-# INCOHERENT #-}
  ( TypeError
      (     'Text "Unrecognized Rep: "
      ':<>: 'ShowType f
      ':$$: 'Text "Possible causes:"
      ':$$: 'Text "    Missing ("
      ':<>: 'ShowType (BaseCase e)
      ':<>: 'Text ") constraint"
      ':$$: 'Text "    Missing Generic instance"
    )
  , Alternative (IfM y Weighted Proxy)
  ) => GBCS f z y e where
  gbcs :: prox y -> proxy '(z, e) -> IfM y Weighted Proxy (f p)
gbcs = [Char] -> prox y -> proxy '(z, e) -> IfM y Weighted Proxy (f p)
forall a. HasCallStack => [Char] -> a
error [Char]
"Type error"

class GBaseCaseSearch a z y e where
  gBaseCaseSearch :: prox y -> proxy '(z, e) -> IfM y Gen Proxy a

instance (Generic a, GBCS (Rep a) z y e, IsMaybe y)
  => GBaseCaseSearch a z y e where
  gBaseCaseSearch :: prox y -> proxy '(z, e) -> IfM y Gen Proxy a
gBaseCaseSearch prox y
y proxy '(z, e)
z = prox y
-> (Weighted (Rep a Any) -> Gen a)
-> (Proxy (Rep a Any) -> Proxy a)
-> IfM y Weighted Proxy (Rep a Any)
-> IfM y Gen Proxy a
forall t (b :: Maybe t) k k (proxy :: Maybe t -> *) (c :: k -> *)
       (a :: k) (c' :: k -> *) (a' :: k) (d :: k -> *) (d' :: k -> *).
IsMaybe b =>
proxy b
-> (c a -> c' a')
-> (d a -> d' a')
-> IfM b c d a
-> IfM b c' d' a'
ifMmap prox y
y
    (\(Weighted Maybe (Int -> Gen (Rep a Any), Int)
gn) -> case Maybe (Int -> Gen (Rep a Any), Int)
gn of
      Just (Int -> Gen (Rep a Any)
g, Int
n) -> (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
0, Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Gen Int -> (Int -> Gen a) -> Gen a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Rep a Any -> a) -> Gen (Rep a Any) -> Gen a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Rep a Any -> a
forall a x. Generic a => Rep a x -> a
to (Gen (Rep a Any) -> Gen a)
-> (Int -> Gen (Rep a Any)) -> Int -> Gen a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Gen (Rep a Any)
g
      Maybe (Int -> Gen (Rep a Any), Int)
Nothing -> [Char] -> Gen a
forall a. HasCallStack => [Char] -> a
error [Char]
"How could this happen?")
    (\Proxy (Rep a Any)
Proxy -> Proxy a
forall k (t :: k). Proxy t
Proxy)
    (prox y -> proxy '(z, e) -> IfM y Weighted Proxy (Rep a Any)
forall k (f :: k -> *) (z :: Nat) (y :: Maybe Nat) e
       (prox :: Maybe Nat -> *) (proxy :: (Nat, *) -> *) (p :: k).
GBCS f z y e =>
prox y -> proxy '(z, e) -> IfM y Weighted Proxy (f p)
gbcs prox y
y proxy '(z, e)
z)