{-# LANGUAGE AllowAmbiguousTypes   #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UndecidableInstances  #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Generics.Sum.Internal.Typed
-- Copyright   :  (C) 2019 Csongor Kiss
-- License     :  BSD3
-- Maintainer  :  Csongor Kiss <kiss.csongor.kiss@gmail.com>
-- Stability   :  experimental
-- Portability :  non-portable
--
-- Derive constructor-field-type-based prisms generically.
--
-----------------------------------------------------------------------------

module Data.Generics.Sum.Internal.Typed
  ( GAsType (..)
  ) where

import Data.Kind
import GHC.Generics
import Data.Tagged

import Data.Generics.Internal.Families
import Data.Generics.Product.Internal.HList
import Data.Generics.Internal.Profunctor.Iso
import Data.Generics.Internal.Profunctor.Prism

-- |As 'AsType' but over generic representations as defined by "GHC.Generics".
class GAsType (f :: Type -> Type) (as :: [Type]) where
  _GTyped :: Prism (f x) (f x) (HList as) (HList as)
-- We create this specialised version as we use it in the subtype prism
-- If we don't create it, the opportunity for specialisation is only
-- created after specialisation happens, I think a late specialisation pass
-- would pick up this case.
{-# SPECIALISE _GTyped  :: (Tagged b b -> Tagged t t) #-}


instance
  ( GIsList f f as as
  ) => GAsType (M1 C meta f) as where
  _GTyped :: p (HList as) (HList as) -> p (M1 C meta f x) (M1 C meta f x)
_GTyped = p (f x) (f x) -> p (M1 C meta f x) (M1 C meta f x)
forall i (c :: Meta) (f :: * -> *) p (g :: * -> *).
Iso (M1 i c f p) (M1 i c g p) (f p) (g p)
mIso (p (f x) (f x) -> p (M1 C meta f x) (M1 C meta f x))
-> (p (HList as) (HList as) -> p (f x) (f x))
-> p (HList as) (HList as)
-> p (M1 C meta f x) (M1 C meta f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p (HList as) (HList as) -> p (f x) (f x)
forall (f :: * -> *) (g :: * -> *) (as :: [*]) (bs :: [*]) x.
GIsList f g as bs =>
Iso (f x) (g x) (HList as) (HList bs)
glist
  {-# INLINE[0] _GTyped #-}

instance GSumAsType (HasPartialTypeP a l) l r a => GAsType (l :+: r) a where
  _GTyped :: p (HList a) (HList a) -> p ((:+:) l r x) ((:+:) l r x)
_GTyped = forall (contains :: Bool) (l :: * -> *) (r :: * -> *) (a :: [*]) x.
GSumAsType contains l r a =>
Prism ((:+:) l r x) ((:+:) l r x) (HList a) (HList a)
forall (l :: * -> *) (r :: * -> *) (a :: [*]) x.
GSumAsType (HasPartialTypeP a l) l r a =>
Prism ((:+:) l r x) ((:+:) l r x) (HList a) (HList a)
_GSumTyped @(HasPartialTypeP a l)
  {-# INLINE[0] _GTyped #-}

instance GAsType f a => GAsType (M1 D meta f) a where
  _GTyped :: p (HList a) (HList a) -> p (M1 D meta f x) (M1 D meta f x)
_GTyped = p (f x) (f x) -> p (M1 D meta f x) (M1 D meta f x)
forall i (c :: Meta) (f :: * -> *) p (g :: * -> *).
Iso (M1 i c f p) (M1 i c g p) (f p) (g p)
mIso (p (f x) (f x) -> p (M1 D meta f x) (M1 D meta f x))
-> (p (HList a) (HList a) -> p (f x) (f x))
-> p (HList a) (HList a)
-> p (M1 D meta f x) (M1 D meta f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p (HList a) (HList a) -> p (f x) (f x)
forall (f :: * -> *) (as :: [*]) x.
GAsType f as =>
Prism (f x) (f x) (HList as) (HList as)
_GTyped
  {-# INLINE[0] _GTyped #-}

class GSumAsType (contains :: Bool) l r (a :: [Type]) where
  _GSumTyped :: Prism ((l :+: r) x) ((l :+: r) x) (HList a) (HList a)

instance GAsType l a => GSumAsType 'True l r a where
  _GSumTyped :: p (HList a) (HList a) -> p ((:+:) l r x) ((:+:) l r x)
_GSumTyped = p (l x) (l x) -> p ((:+:) l r x) ((:+:) l r x)
forall (a :: * -> *) (c :: * -> *) x (b :: * -> *).
Prism ((:+:) a c x) ((:+:) b c x) (a x) (b x)
left (p (l x) (l x) -> p ((:+:) l r x) ((:+:) l r x))
-> (p (HList a) (HList a) -> p (l x) (l x))
-> p (HList a) (HList a)
-> p ((:+:) l r x) ((:+:) l r x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p (HList a) (HList a) -> p (l x) (l x)
forall (f :: * -> *) (as :: [*]) x.
GAsType f as =>
Prism (f x) (f x) (HList as) (HList as)
_GTyped
  {-# INLINE[0] _GSumTyped #-}

instance GAsType r a => GSumAsType 'False l r a where
  _GSumTyped :: p (HList a) (HList a) -> p ((:+:) l r x) ((:+:) l r x)
_GSumTyped = p (r x) (r x) -> p ((:+:) l r x) ((:+:) l r x)
forall (a :: * -> *) (b :: * -> *) x (c :: * -> *).
Prism ((:+:) a b x) ((:+:) a c x) (b x) (c x)
right (p (r x) (r x) -> p ((:+:) l r x) ((:+:) l r x))
-> (p (HList a) (HList a) -> p (r x) (r x))
-> p (HList a) (HList a)
-> p ((:+:) l r x) ((:+:) l r x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p (HList a) (HList a) -> p (r x) (r x)
forall (f :: * -> *) (as :: [*]) x.
GAsType f as =>
Prism (f x) (f x) (HList as) (HList as)
_GTyped
  {-# INLINE[0] _GSumTyped #-}