{-# LANGUAGE PolyKinds    #-}
{-# LANGUAGE TypeFamilies #-}
module Barbies.Generics.Bare
  ( GBare(..)
  )

where

import Data.Functor.Identity (Identity(..))

import Data.Coerce (Coercible, coerce)
import Data.Generics.GenericN
import Data.Proxy (Proxy(..))
import GHC.TypeLits (Nat)


class GBare (n :: Nat) repbi repbb where
  gstrip :: Proxy n -> repbi x -> repbb x
  gcover :: Proxy n -> repbb x -> repbi x

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

instance GBare n repbi repbb => GBare n (M1 i k repbi) (M1 i k repbb) where
  gstrip :: Proxy n -> M1 i k repbi x -> M1 i k repbb x
gstrip Proxy n
pn = repbb x -> M1 i k repbb x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (repbb x -> M1 i k repbb x)
-> (M1 i k repbi x -> repbb x) -> M1 i k repbi x -> M1 i k repbb x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy n -> repbi x -> repbb x
forall k (n :: Nat) (repbi :: k -> *) (repbb :: k -> *) (x :: k).
GBare n repbi repbb =>
Proxy n -> repbi x -> repbb x
gstrip Proxy n
pn (repbi x -> repbb x)
-> (M1 i k repbi x -> repbi x) -> M1 i k repbi x -> repbb x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1 i k repbi x -> repbi x
forall i (c :: Meta) k (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1
  {-# INLINE gstrip #-}

  gcover :: Proxy n -> M1 i k repbb x -> M1 i k repbi x
gcover Proxy n
pn = repbi x -> M1 i k repbi x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (repbi x -> M1 i k repbi x)
-> (M1 i k repbb x -> repbi x) -> M1 i k repbb x -> M1 i k repbi x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy n -> repbb x -> repbi x
forall k (n :: Nat) (repbi :: k -> *) (repbb :: k -> *) (x :: k).
GBare n repbi repbb =>
Proxy n -> repbb x -> repbi x
gcover Proxy n
pn (repbb x -> repbi x)
-> (M1 i k repbb x -> repbb x) -> M1 i k repbb x -> repbi x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1 i k repbb x -> repbb x
forall i (c :: Meta) k (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1
  {-# INLINE gcover #-}


instance GBare n V1 V1 where
  gstrip :: Proxy n -> V1 x -> V1 x
gstrip Proxy n
_ V1 x
_ = V1 x
forall a. HasCallStack => a
undefined
  gcover :: Proxy n -> V1 x -> V1 x
gcover Proxy n
_ V1 x
_ = V1 x
forall a. HasCallStack => a
undefined

instance GBare n U1 U1 where
  gstrip :: Proxy n -> U1 x -> U1 x
gstrip Proxy n
_ = U1 x -> U1 x
forall a. a -> a
id
  {-# INLINE gstrip #-}

  gcover :: Proxy n -> U1 x -> U1 x
gcover Proxy n
_ = U1 x -> U1 x
forall a. a -> a
id
  {-# INLINE gcover #-}


instance (GBare n l l', GBare n r r') => GBare n (l :*: r) (l' :*: r') where
  gstrip :: Proxy n -> (:*:) l r x -> (:*:) l' r' x
gstrip Proxy n
pn (l x
l :*: r x
r) = (Proxy n -> l x -> l' x
forall k (n :: Nat) (repbi :: k -> *) (repbb :: k -> *) (x :: k).
GBare n repbi repbb =>
Proxy n -> repbi x -> repbb x
gstrip Proxy n
pn l x
l) l' x -> r' x -> (:*:) l' r' x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: Proxy n -> r x -> r' x
forall k (n :: Nat) (repbi :: k -> *) (repbb :: k -> *) (x :: k).
GBare n repbi repbb =>
Proxy n -> repbi x -> repbb x
gstrip Proxy n
pn r x
r
  {-# INLINE gstrip #-}

  gcover :: Proxy n -> (:*:) l' r' x -> (:*:) l r x
gcover Proxy n
pn (l' x
l :*: r' x
r) = (Proxy n -> l' x -> l x
forall k (n :: Nat) (repbi :: k -> *) (repbb :: k -> *) (x :: k).
GBare n repbi repbb =>
Proxy n -> repbb x -> repbi x
gcover Proxy n
pn l' x
l) l x -> r x -> (:*:) l r x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: Proxy n -> r' x -> r x
forall k (n :: Nat) (repbi :: k -> *) (repbb :: k -> *) (x :: k).
GBare n repbi repbb =>
Proxy n -> repbb x -> repbi x
gcover Proxy n
pn r' x
r
  {-# INLINE gcover #-}


instance (GBare n l l', GBare n r r') => GBare n (l :+: r) (l' :+: r') where
  gstrip :: Proxy n -> (:+:) l r x -> (:+:) l' r' x
gstrip Proxy n
pn = \case
    L1 l x
l -> l' x -> (:+:) l' r' x
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (Proxy n -> l x -> l' x
forall k (n :: Nat) (repbi :: k -> *) (repbb :: k -> *) (x :: k).
GBare n repbi repbb =>
Proxy n -> repbi x -> repbb x
gstrip Proxy n
pn l x
l)
    R1 r x
r -> r' x -> (:+:) l' r' x
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (Proxy n -> r x -> r' x
forall k (n :: Nat) (repbi :: k -> *) (repbb :: k -> *) (x :: k).
GBare n repbi repbb =>
Proxy n -> repbi x -> repbb x
gstrip Proxy n
pn r x
r)
  {-# INLINE gstrip #-}

  gcover :: Proxy n -> (:+:) l' r' x -> (:+:) l r x
gcover Proxy n
pn = \case
    L1 l' x
l -> l x -> (:+:) l r x
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (Proxy n -> l' x -> l x
forall k (n :: Nat) (repbi :: k -> *) (repbb :: k -> *) (x :: k).
GBare n repbi repbb =>
Proxy n -> repbb x -> repbi x
gcover Proxy n
pn l' x
l)
    R1 r' x
r -> r x -> (:+:) l r x
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (Proxy n -> r' x -> r x
forall k (n :: Nat) (repbi :: k -> *) (repbb :: k -> *) (x :: k).
GBare n repbi repbb =>
Proxy n -> repbb x -> repbi x
gcover Proxy n
pn r' x
r)
  {-# INLINE gcover #-}

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

type P = Param

instance Coercible a b => GBare n (Rec (P n Identity a) (Identity a)) (Rec b b) where
  gstrip :: Proxy n -> Rec (P n Identity a) (Identity a) x -> Rec b b x
gstrip Proxy n
_ = Rec (P n Identity a) (Identity a) x -> Rec b b x
coerce
  {-# INLINE gstrip #-}

  gcover :: Proxy n -> Rec b b x -> Rec (P n Identity a) (Identity a) x
gcover Proxy n
_ = Rec b b x -> Rec (P n Identity a) (Identity a) x
coerce
  {-# INLINE gcover #-}

instance repbi ~ repbb => GBare n (Rec repbi repbi) (Rec repbb repbb) where
  gstrip :: Proxy n -> Rec repbi repbi x -> Rec repbb repbb x
gstrip Proxy n
_ = Rec repbi repbi x -> Rec repbb repbb x
forall a. a -> a
id
  {-# INLINE gstrip #-}

  gcover :: Proxy n -> Rec repbb repbb x -> Rec repbi repbi x
gcover Proxy n
_ = Rec repbb repbb x -> Rec repbi repbi x
forall a. a -> a
id
  {-# INLINE gcover #-}