{-# LANGUAGE PolyKinds    #-}
{-# LANGUAGE TypeFamilies #-}
module Barbies.Generics.Distributive
  ( GDistributive(..)
  )

where

import Data.Generics.GenericN
import Data.Proxy (Proxy (..))

import Data.Functor.Compose   (Compose (..))
import Data.Distributive      (Distributive(..))

import GHC.TypeLits (Nat)

class (Functor f) => GDistributive (n :: Nat) f repbg repbfg where
  gdistribute :: Proxy n -> f (repbg x) -> repbfg x

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

instance
  ( GDistributive n f bg bfg
  ) => GDistributive n f (M1 i c bg) (M1 i c bfg)
  where
  gdistribute :: Proxy n -> f (M1 i c bg x) -> M1 i c bfg x
gdistribute Proxy n
pn = bfg x -> M1 i c bfg x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (bfg x -> M1 i c bfg x)
-> (f (M1 i c bg x) -> bfg x) -> f (M1 i c bg x) -> M1 i c bfg x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy n -> f (bg x) -> bfg x
forall k (n :: Nat) (f :: * -> *) (repbg :: k -> *)
       (repbfg :: k -> *) (x :: k).
GDistributive n f repbg repbfg =>
Proxy n -> f (repbg x) -> repbfg x
gdistribute Proxy n
pn (f (bg x) -> bfg x)
-> (f (M1 i c bg x) -> f (bg x)) -> f (M1 i c bg x) -> bfg x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (M1 i c bg x -> bg x) -> f (M1 i c bg x) -> f (bg x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap M1 i c bg x -> bg x
forall i (c :: Meta) k (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1
  {-# INLINE gdistribute #-}


instance
  ( Functor f
  ) => GDistributive n f U1 U1
  where
  gdistribute :: Proxy n -> f (U1 x) -> U1 x
gdistribute Proxy n
_ = U1 x -> f (U1 x) -> U1 x
forall a b. a -> b -> a
const U1 x
forall k (p :: k). U1 p
U1
  {-# INLINE gdistribute #-}


fstF :: (l :*: r) a -> l a
fstF :: (:*:) l r a -> l a
fstF (l a
x :*: r a
_y) = l a
x

sndF :: (l :*: r) a -> r a
sndF :: (:*:) l r a -> r a
sndF (l a
_x :*: r a
y) = r a
y

instance
  ( GDistributive n f l l'
  , GDistributive n f r r'
  )
  => GDistributive n f (l :*: r) (l' :*: r')
  where
  gdistribute :: Proxy n -> f ((:*:) l r x) -> (:*:) l' r' x
gdistribute Proxy n
pn f ((:*:) l r x)
lr = Proxy n -> f (l x) -> l' x
forall k (n :: Nat) (f :: * -> *) (repbg :: k -> *)
       (repbfg :: k -> *) (x :: k).
GDistributive n f repbg repbfg =>
Proxy n -> f (repbg x) -> repbfg x
gdistribute Proxy n
pn ((:*:) l r x -> l x
forall k (l :: k -> *) (r :: k -> *) (a :: k). (:*:) l r a -> l a
fstF ((:*:) l r x -> l x) -> f ((:*:) l r x) -> f (l x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f ((:*:) l r x)
lr) l' x -> r' x -> (:*:) l' r' x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: Proxy n -> f (r x) -> r' x
forall k (n :: Nat) (f :: * -> *) (repbg :: k -> *)
       (repbfg :: k -> *) (x :: k).
GDistributive n f repbg repbfg =>
Proxy n -> f (repbg x) -> repbfg x
gdistribute Proxy n
pn ((:*:) l r x -> r x
forall k (l :: k -> *) (r :: k -> *) (a :: k). (:*:) l r a -> r a
sndF ((:*:) l r x -> r x) -> f ((:*:) l r x) -> f (r x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f ((:*:) l r x)
lr)
  {-# INLINE gdistribute #-}


-- ---------------------------------------------------------
-- The interesting cases.
-- There are more interesting cases for specific values of n
-- ---------------------------------------------------------

type P = Param

instance
  ( Functor f
  ) =>
  GDistributive n f (Rec (P n g a) (g a)) (Rec (P n (Compose f g) a) (Compose f g a))
  where
  gdistribute :: Proxy n
-> f (Rec (P n g a) (g a) x)
-> Rec (P n (Compose f g) a) (Compose f g a) x
gdistribute Proxy n
_ = K1 R (Compose f g a) x
-> Rec (P n (Compose f g) a) (Compose f g a) x
forall k p a (x :: k). K1 R a x -> Rec p a x
Rec (K1 R (Compose f g a) x
 -> Rec (P n (Compose f g) a) (Compose f g a) x)
-> (f (Rec (P n g a) (g a) x) -> K1 R (Compose f g a) x)
-> f (Rec (P n g a) (g a) x)
-> Rec (P n (Compose f g) a) (Compose f g a) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f g a -> K1 R (Compose f g a) x
forall k i c (p :: k). c -> K1 i c p
K1 (Compose f g a -> K1 R (Compose f g a) x)
-> (f (Rec (P n g a) (g a) x) -> Compose f g a)
-> f (Rec (P n g a) (g a) x)
-> K1 R (Compose f g a) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (g a) -> Compose f g a
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f (g a) -> Compose f g a)
-> (f (Rec (P n g a) (g a) x) -> f (g a))
-> f (Rec (P n g a) (g a) x)
-> Compose f g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (g a) -> f (g a)
forall a. a -> a
id (f (g a) -> f (g a))
-> (f (Rec (P n g a) (g a) x) -> f (g a))
-> f (Rec (P n g a) (g a) x)
-> f (g a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rec (P n g a) (g a) x -> g a)
-> f (Rec (P n g a) (g a) x) -> f (g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (K1 R (g a) x -> g a
forall i c k (p :: k). K1 i c p -> c
unK1 (K1 R (g a) x -> g a)
-> (Rec (P n g a) (g a) x -> K1 R (g a) x)
-> Rec (P n g a) (g a) x
-> g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec (P n g a) (g a) x -> K1 R (g a) x
forall p a k (x :: k). Rec p a x -> K1 R a x
unRec)
  {-# INLINE gdistribute #-}

instance
  ( Functor f
  , Distributive h
  ) =>
  GDistributive n f (Rec (h (P n g a)) (h (g a))) (Rec (h (P n (Compose f g) a)) (h (Compose f g a)))
  where
  gdistribute :: Proxy n
-> f (Rec (h (P n g a)) (h (g a)) x)
-> Rec (h (P n (Compose f g) a)) (h (Compose f g a)) x
gdistribute Proxy n
_ = K1 R (h (Compose f g a)) x
-> Rec (h (P n (Compose f g) a)) (h (Compose f g a)) x
forall k p a (x :: k). K1 R a x -> Rec p a x
Rec (K1 R (h (Compose f g a)) x
 -> Rec (h (P n (Compose f g) a)) (h (Compose f g a)) x)
-> (f (Rec (h (P n g a)) (h (g a)) x)
    -> K1 R (h (Compose f g a)) x)
-> f (Rec (h (P n g a)) (h (g a)) x)
-> Rec (h (P n (Compose f g) a)) (h (Compose f g a)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. h (Compose f g a) -> K1 R (h (Compose f g a)) x
forall k i c (p :: k). c -> K1 i c p
K1 (h (Compose f g a) -> K1 R (h (Compose f g a)) x)
-> (f (Rec (h (P n g a)) (h (g a)) x) -> h (Compose f g a))
-> f (Rec (h (P n g a)) (h (g a)) x)
-> K1 R (h (Compose f g a)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (g a) -> Compose f g a) -> h (f (g a)) -> h (Compose f g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (g a) -> Compose f g a
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (h (f (g a)) -> h (Compose f g a))
-> (f (Rec (h (P n g a)) (h (g a)) x) -> h (f (g a)))
-> f (Rec (h (P n g a)) (h (g a)) x)
-> h (Compose f g a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (h (g a)) -> h (f (g a))
forall (g :: * -> *) (f :: * -> *) a.
(Distributive g, Functor f) =>
f (g a) -> g (f a)
distribute (f (h (g a)) -> h (f (g a)))
-> (f (Rec (h (P n g a)) (h (g a)) x) -> f (h (g a)))
-> f (Rec (h (P n g a)) (h (g a)) x)
-> h (f (g a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rec (h (P n g a)) (h (g a)) x -> h (g a))
-> f (Rec (h (P n g a)) (h (g a)) x) -> f (h (g a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (K1 R (h (g a)) x -> h (g a)
forall i c k (p :: k). K1 i c p -> c
unK1 (K1 R (h (g a)) x -> h (g a))
-> (Rec (h (P n g a)) (h (g a)) x -> K1 R (h (g a)) x)
-> Rec (h (P n g a)) (h (g a)) x
-> h (g a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec (h (P n g a)) (h (g a)) x -> K1 R (h (g a)) x
forall p a k (x :: k). Rec p a x -> K1 R a x
unRec)
  {-# INLINE gdistribute #-}