{-# LANGUAGE AllowAmbiguousTypes  #-}
{-# LANGUAGE PolyKinds            #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans -Wno-deprecations #-}
module Data.Barbie.Internal.Product
  ( ProductB(buniq, bprod)
  , CanDeriveProductB
  , gbprodDefault, gbuniqDefault
  , GProductB(..)
  )

where

import Barbies.Internal.FunctorB (FunctorB)
import Barbies.Internal.Trivial (Unit)
import Barbies.Internal.Wrappers (Barbie(..))
import qualified Barbies.Internal.ApplicativeB as App

import Data.Functor.Product (Product (..))
import Data.Kind            (Type)
import Data.Proxy           (Proxy (..))

import Data.Generics.GenericN


{-# DEPRECATED ProductB "Use ApplicativeB" #-}
{-# DEPRECATED buniq "Use bpure" #-}
class App.ApplicativeB b => ProductB (b :: (k -> Type) -> Type) where
  bprod :: b f -> b g -> b (f `Product` g)

  buniq :: (forall a . f a) -> b f

  default bprod :: CanDeriveProductB b f g => b f -> b g -> b (f `Product` g)
  bprod = b f -> b g -> b (Product f g)
forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
CanDeriveProductB b f g =>
b f -> b g -> b (Product f g)
gbprodDefault

  default buniq :: CanDeriveProductB b f f => (forall a . f a) -> b f
  buniq = (forall (a :: k). f a) -> b f
forall k (b :: (k -> *) -> *) (f :: k -> *).
CanDeriveProductB b f f =>
(forall (a :: k). f a) -> b f
gbuniqDefault



type CanDeriveProductB b f g
  = ( GenericN (b f)
    , GenericN (b g)
    , GenericN (b (f `Product` g))
    , GProductB f g (RepN (b f)) (RepN (b g)) (RepN (b (f `Product` g)))
    )

instance {-# OVERLAPPABLE #-} (ProductB b, FunctorB b) => App.ApplicativeB b where
  bpure :: (forall (a :: k). f a) -> b f
bpure = (forall (a :: k). f a) -> b f
forall k (b :: (k -> *) -> *) (f :: k -> *).
ProductB b =>
(forall (a :: k). f a) -> b f
Data.Barbie.Internal.Product.buniq
  bprod :: b f -> b g -> b (Product f g)
bprod = b f -> b g -> b (Product f g)
forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
ProductB b =>
b f -> b g -> b (Product f g)
Data.Barbie.Internal.Product.bprod

instance ProductB Unit where

instance ProductB b => ProductB (Barbie b) where
    buniq :: (forall (a :: k). f a) -> Barbie b f
buniq forall (a :: k). f a
x = b f -> Barbie b f
forall k (b :: (k -> *) -> *) (f :: k -> *). b f -> Barbie b f
Barbie ((forall (a :: k). f a) -> b f
forall k (b :: (k -> *) -> *) (f :: k -> *).
ProductB b =>
(forall (a :: k). f a) -> b f
buniq forall (a :: k). f a
x)
    bprod :: Barbie b f -> Barbie b g -> Barbie b (Product f g)
bprod (Barbie b f
l) (Barbie b g
r) = b (Product f g) -> Barbie b (Product f g)
forall k (b :: (k -> *) -> *) (f :: k -> *). b f -> Barbie b f
Barbie (b f -> b g -> b (Product f g)
forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
ProductB b =>
b f -> b g -> b (Product f g)
bprod b f
l b g
r)

-- ======================================
-- Generic derivation of instances
-- ======================================

-- | Default implementation of 'bprod' based on 'Generic'.
gbprodDefault
  :: forall b f g
  .  CanDeriveProductB b f g
  => b f -> b g -> b (f `Product` g)
gbprodDefault :: b f -> b g -> b (Product f g)
gbprodDefault b f
l b g
r
  = RepN (b (Product f g)) Any -> b (Product f g)
forall a x. GenericN a => RepN a x -> a
toN (RepN (b (Product f g)) Any -> b (Product f g))
-> RepN (b (Product f g)) Any -> b (Product f g)
forall a b. (a -> b) -> a -> b
$ Proxy f
-> Proxy g
-> Zip (Rep (Indexed b 1 (Param 0 f))) (Rep (b f)) Any
-> Zip (Rep (Indexed b 1 (Param 0 g))) (Rep (b g)) Any
-> Zip
     (Rep (Indexed b 1 (Param 0 (Product f g))))
     (Rep (b (Product f g)))
     Any
forall k k (f :: k -> *) (g :: k -> *) (repbf :: k -> *)
       (repbg :: k -> *) (repbfg :: k -> *) (x :: k).
GProductB f g repbf repbg repbfg =>
Proxy f -> Proxy g -> repbf x -> repbg x -> repbfg x
gbprod (Proxy f
forall k (t :: k). Proxy t
Proxy @f) (Proxy g
forall k (t :: k). Proxy t
Proxy @g) (b f -> RepN (b f) Any
forall a x. GenericN a => a -> RepN a x
fromN b f
l) (b g -> RepN (b g) Any
forall a x. GenericN a => a -> RepN a x
fromN b g
r)
{-# INLINE gbprodDefault #-}

gbuniqDefault:: forall b f . CanDeriveProductB b f f => (forall a . f a) -> b f
gbuniqDefault :: (forall (a :: k). f a) -> b f
gbuniqDefault forall (a :: k). f a
x
  = RepN (b f) Any -> b f
forall a x. GenericN a => RepN a x -> a
toN (RepN (b f) Any -> b f) -> RepN (b f) Any -> b f
forall a b. (a -> b) -> a -> b
$ Proxy f
-> Proxy (Zip (Rep (Indexed b 1 (Param 0 f))) (Rep (b f)))
-> Proxy
     (Zip
        (Rep (Indexed b 1 (Param 0 (Product f f))))
        (Rep (b (Product f f))))
-> (forall (a :: k). f a)
-> Zip (Rep (Indexed b 1 (Param 0 f))) (Rep (b f)) Any
forall k k (f :: k -> *) (g :: k -> *) (repbf :: k -> *)
       (repbg :: k -> *) (repbfg :: k -> *) (x :: k).
(GProductB f g repbf repbg repbfg, f ~ g, repbf ~ repbg) =>
Proxy f
-> Proxy repbf -> Proxy repbfg -> (forall (a :: k). f a) -> repbf x
gbuniq (Proxy f
forall k (t :: k). Proxy t
Proxy @f) (Proxy (RepN (b f))
forall k (t :: k). Proxy t
Proxy @(RepN (b f))) (Proxy (RepN (b (Product f f)))
forall k (t :: k). Proxy t
Proxy @(RepN (b (f `Product` f)))) forall (a :: k). f a
x
{-# INLINE gbuniqDefault #-}

class GProductB (f :: k -> Type) (g :: k -> Type) repbf repbg repbfg where
  gbprod :: Proxy f -> Proxy g -> repbf x -> repbg x -> repbfg x

  gbuniq :: (f ~ g, repbf ~ repbg) => Proxy f -> Proxy repbf -> Proxy repbfg -> (forall a . f a) -> repbf x

-- ----------------------------------
-- Trivial cases
-- ----------------------------------

instance GProductB f g repf repg repfg => GProductB f g (M1 i c repf)
                                                        (M1 i c repg)
                                                        (M1 i c repfg) where
  gbprod :: Proxy f
-> Proxy g -> M1 i c repf x -> M1 i c repg x -> M1 i c repfg x
gbprod Proxy f
pf Proxy g
pg (M1 repf x
l) (M1 repg x
r) = repfg x -> M1 i c repfg x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (Proxy f -> Proxy g -> repf x -> repg x -> repfg x
forall k k (f :: k -> *) (g :: k -> *) (repbf :: k -> *)
       (repbg :: k -> *) (repbfg :: k -> *) (x :: k).
GProductB f g repbf repbg repbfg =>
Proxy f -> Proxy g -> repbf x -> repbg x -> repbfg x
gbprod Proxy f
pf Proxy g
pg repf x
l repg x
r)
  {-# INLINE gbprod #-}

  gbuniq :: Proxy f
-> Proxy (M1 i c repf)
-> Proxy (M1 i c repfg)
-> (forall (a :: k). f a)
-> M1 i c repf x
gbuniq Proxy f
pf Proxy (M1 i c repf)
_ Proxy (M1 i c repfg)
_ forall (a :: k). f a
x = repf x -> M1 i c repf x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (Proxy f
-> Proxy repf -> Proxy repfg -> (forall (a :: k). f a) -> repf x
forall k k (f :: k -> *) (g :: k -> *) (repbf :: k -> *)
       (repbg :: k -> *) (repbfg :: k -> *) (x :: k).
(GProductB f g repbf repbg repbfg, f ~ g, repbf ~ repbg) =>
Proxy f
-> Proxy repbf -> Proxy repbfg -> (forall (a :: k). f a) -> repbf x
gbuniq Proxy f
pf (Proxy repf
forall k (t :: k). Proxy t
Proxy @repf) (Proxy repfg
forall k (t :: k). Proxy t
Proxy @repfg) forall (a :: k). f a
x)
  {-# INLINE gbuniq #-}


instance GProductB f g U1 U1 U1 where
  gbprod :: Proxy f -> Proxy g -> U1 x -> U1 x -> U1 x
gbprod Proxy f
_ Proxy g
_ U1 x
U1 U1 x
U1 = U1 x
forall k (p :: k). U1 p
U1
  {-# INLINE gbprod #-}

  gbuniq :: Proxy f -> Proxy U1 -> Proxy U1 -> (forall (a :: k). f a) -> U1 x
gbuniq Proxy f
_ Proxy U1
_ Proxy U1
_ forall (a :: k). f a
_ = U1 x
forall k (p :: k). U1 p
U1
  {-# INLINE gbuniq #-}

instance
  ( GProductB f g lf lg lfg
  , GProductB f g rf rg rfg
  ) => GProductB f g (lf  :*: rf)
                     (lg  :*: rg)
                     (lfg :*: rfg) where
  gbprod :: Proxy f
-> Proxy g -> (:*:) lf rf x -> (:*:) lg rg x -> (:*:) lfg rfg x
gbprod Proxy f
pf Proxy g
pg (lf x
l1 :*: rf x
l2) (lg x
r1 :*: rg x
r2)
    = (lf x
l1 lf x -> lg x -> lfg x
`lprod` lg x
r1) lfg x -> rfg x -> (:*:) lfg rfg x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: (rf x
l2 rf x -> rg x -> rfg x
`rprod` rg x
r2)
    where
      lprod :: lf x -> lg x -> lfg x
lprod = Proxy f -> Proxy g -> lf x -> lg x -> lfg x
forall k k (f :: k -> *) (g :: k -> *) (repbf :: k -> *)
       (repbg :: k -> *) (repbfg :: k -> *) (x :: k).
GProductB f g repbf repbg repbfg =>
Proxy f -> Proxy g -> repbf x -> repbg x -> repbfg x
gbprod Proxy f
pf Proxy g
pg
      rprod :: rf x -> rg x -> rfg x
rprod = Proxy f -> Proxy g -> rf x -> rg x -> rfg x
forall k k (f :: k -> *) (g :: k -> *) (repbf :: k -> *)
       (repbg :: k -> *) (repbfg :: k -> *) (x :: k).
GProductB f g repbf repbg repbfg =>
Proxy f -> Proxy g -> repbf x -> repbg x -> repbfg x
gbprod Proxy f
pf Proxy g
pg
  {-# INLINE gbprod #-}

  gbuniq :: Proxy f
-> Proxy (lf :*: rf)
-> Proxy (lfg :*: rfg)
-> (forall (a :: k). f a)
-> (:*:) lf rf x
gbuniq Proxy f
pf Proxy (lf :*: rf)
_ Proxy (lfg :*: rfg)
_ forall (a :: k). f a
x = (Proxy f -> Proxy lf -> Proxy lfg -> (forall (a :: k). f a) -> lf x
forall k k (f :: k -> *) (g :: k -> *) (repbf :: k -> *)
       (repbg :: k -> *) (repbfg :: k -> *) (x :: k).
(GProductB f g repbf repbg repbfg, f ~ g, repbf ~ repbg) =>
Proxy f
-> Proxy repbf -> Proxy repbfg -> (forall (a :: k). f a) -> repbf x
gbuniq Proxy f
pf (Proxy lf
forall k (t :: k). Proxy t
Proxy @lf) (Proxy lfg
forall k (t :: k). Proxy t
Proxy @lfg) forall (a :: k). f a
x lf x -> rf x -> (:*:) lf rf x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: Proxy f -> Proxy rf -> Proxy rfg -> (forall (a :: k). f a) -> rf x
forall k k (f :: k -> *) (g :: k -> *) (repbf :: k -> *)
       (repbg :: k -> *) (repbfg :: k -> *) (x :: k).
(GProductB f g repbf repbg repbfg, f ~ g, repbf ~ repbg) =>
Proxy f
-> Proxy repbf -> Proxy repbfg -> (forall (a :: k). f a) -> repbf x
gbuniq Proxy f
pf (Proxy rf
forall k (t :: k). Proxy t
Proxy @rf) (Proxy rfg
forall k (t :: k). Proxy t
Proxy @rfg) forall (a :: k). f a
x)
  {-# INLINE gbuniq #-}

-- --------------------------------
-- The interesting cases
-- --------------------------------

type P0 = Param 0

instance GProductB f g (Rec (P0 f a_or_pma) (f a))
                       (Rec (P0 g a_or_pma) (g a))
                       (Rec (P0 (f `Product` g) a_or_pma) ((f `Product` g) a)) where
  gbprod :: Proxy f
-> Proxy g
-> Rec (P0 f a_or_pma) (f a) x
-> Rec (P0 g a_or_pma) (g a) x
-> Rec (P0 (Product f g) a_or_pma) (Product f g a) x
gbprod Proxy f
_ Proxy g
_ (Rec (K1 f a
fa)) (Rec (K1 g a
ga))
    = K1 R (Product f g a) x
-> Rec (P0 (Product f g) a_or_pma) (Product f g a) x
forall k p a (x :: k). K1 R a x -> Rec p a x
Rec (Product f g a -> K1 R (Product f g a) x
forall k i c (p :: k). c -> K1 i c p
K1 (f a -> g a -> Product f g a
forall k (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair f a
fa g a
ga))
  {-# INLINE gbprod #-}

  gbuniq :: Proxy f
-> Proxy (Rec (P0 f a_or_pma) (f a))
-> Proxy (Rec (P0 (Product f g) a_or_pma) (Product f g a))
-> (forall (a :: k). f a)
-> Rec (P0 f a_or_pma) (f a) x
gbuniq Proxy f
_ Proxy (Rec (P0 f a_or_pma) (f a))
_ Proxy (Rec (P0 (Product f g) a_or_pma) (Product f g a))
_ forall (a :: k). f a
x = K1 R (f a) x -> Rec (P0 f a_or_pma) (f a) x
forall k p a (x :: k). K1 R a x -> Rec p a x
Rec (f a -> K1 R (f a) x
forall k i c (p :: k). c -> K1 i c p
K1 f a
forall (a :: k). f a
x)
  {-# INLINE gbuniq #-}


-- b' is b, maybe with 'Param' annotations
instance
  ( ProductB b
  ) => GProductB f g (Rec (b' (P0 f)) (b f))
                     (Rec (b' (P0 g)) (b g))
                     (Rec (b' (P0 (f `Product` g))) (b (f `Product` g))) where
  gbprod :: Proxy f
-> Proxy g
-> Rec (b' (P0 f)) (b f) x
-> Rec (b' (P0 g)) (b g) x
-> Rec (b' (P0 (Product f g))) (b (Product f g)) x
gbprod Proxy f
_ Proxy g
_ (Rec (K1 b f
bf)) (Rec (K1 b g
bg))
    = K1 R (b (Product f g)) x
-> Rec (b' (P0 (Product f g))) (b (Product f g)) x
forall k p a (x :: k). K1 R a x -> Rec p a x
Rec (b (Product f g) -> K1 R (b (Product f g)) x
forall k i c (p :: k). c -> K1 i c p
K1 (b f
bf b f -> b g -> b (Product f g)
forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
ProductB b =>
b f -> b g -> b (Product f g)
`bprod` b g
bg))
  {-# INLINE gbprod #-}

  gbuniq :: Proxy f
-> Proxy (Rec (b' (P0 f)) (b f))
-> Proxy (Rec (b' (P0 (Product f g))) (b (Product f g)))
-> (forall (a :: k). f a)
-> Rec (b' (P0 f)) (b f) x
gbuniq Proxy f
_ Proxy (Rec (b' (P0 f)) (b f))
_ Proxy (Rec (b' (P0 (Product f g))) (b (Product f g)))
_ forall (a :: k). f a
x = K1 R (b f) x -> Rec (b' (P0 f)) (b f) x
forall k p a (x :: k). K1 R a x -> Rec p a x
Rec (b f -> K1 R (b f) x
forall k i c (p :: k). c -> K1 i c p
K1 ((forall (a :: k). f a) -> b f
forall k (b :: (k -> *) -> *) (f :: k -> *).
ProductB b =>
(forall (a :: k). f a) -> b f
buniq forall (a :: k). f a
x))
  {-# INLINE gbuniq #-}


-- --------------------------------
-- Instances for base types
-- --------------------------------

instance ProductB Proxy where
  bprod :: Proxy f -> Proxy g -> Proxy (Product f g)
bprod Proxy f
_ Proxy g
_ = Proxy (Product f g)
forall k (t :: k). Proxy t
Proxy
  {-# INLINE bprod #-}

  buniq :: (forall (a :: k). f a) -> Proxy f
buniq forall (a :: k). f a
_ = Proxy f
forall k (t :: k). Proxy t
Proxy
  {-# INLINE buniq #-}

instance (ProductB a, ProductB b) => ProductB (Product a b) where
  bprod :: Product a b f -> Product a b g -> Product a b (Product f g)
bprod (Pair a f
ll b f
lr) (Pair a g
rl b g
rr) = a (Product f g) -> b (Product f g) -> Product a b (Product f g)
forall k (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair (a f -> a g -> a (Product f g)
forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
ProductB b =>
b f -> b g -> b (Product f g)
bprod a f
ll a g
rl) (b f -> b g -> b (Product f g)
forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
ProductB b =>
b f -> b g -> b (Product f g)
bprod b f
lr b g
rr)
  {-# INLINE bprod #-}

  buniq :: (forall (a :: k). f a) -> Product a b f
buniq forall (a :: k). f a
x = a f -> b f -> Product a b f
forall k (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair ((forall (a :: k). f a) -> a f
forall k (b :: (k -> *) -> *) (f :: k -> *).
ProductB b =>
(forall (a :: k). f a) -> b f
buniq forall (a :: k). f a
x) ((forall (a :: k). f a) -> b f
forall k (b :: (k -> *) -> *) (f :: k -> *).
ProductB b =>
(forall (a :: k). f a) -> b f
buniq forall (a :: k). f a
x)
  {-# INLINE buniq #-}