content: {-# LANGUAGE AllowAmbiguousTypes #-}
  {-# LANGUAGE MultiParamTypeClasses, UndecidableInstances, ScopedTypeVariables, TypeFamilies #-}
  {-# LANGUAGE TypeApplications #-}
  {-# LANGUAGE UndecidableSuperClasses #-}
  -----------------------------------------------------------------------------
  -- |
  -- Module      :  Data.Extensible.Class
  -- Copyright   :  (c) Fumiaki Kinoshita 2018
  -- License     :  BSD3
  --
  -- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
  --
  -----------------------------------------------------------------------------
  module Data.Extensible.Class (
    -- * Class
     Extensible(..)
    , piece
    , pieceAssoc
    , itemAt
    , item
    , itemAssoc
    , itemKey
    -- * Membership
    , Membership
    , mkMembership
    , getMemberId
    , compareMembership
    , leadership
    -- * Member
    , Member(..)
    , type (∈)
    , FindType
    -- * Generation
    , Generate(..)
    , Forall(..)
    , ForallF
    -- * Association
    , Assoc(..)
    , type (>:)
    , Lookup(..)
    -- * Misc
    , Head
    , Last
    ) where
  import Data.Constraint
  import Data.Extensible.Internal.Rig (Optic')
  import Data.Extensible.Wrapper
  import Data.Kind
  import Data.Profunctor
  import Type.Membership
  import Type.Membership.Internal
  
  -- | This class allows us to use 'pieceAt' for both sums and products.
  class (Functor f, Profunctor p) => Extensible f p (t :: [k] -> (k -> Type) -> Type) where
    type ExtensibleConstr t (xs :: [k]) (h :: k -> Type) (x :: k) :: Constraint
    type ExtensibleConstr t xs h x = ()
    pieceAt :: ExtensibleConstr t xs h x => Membership xs x -> Optic' p f (t xs h) (h x)
  
  -- | Accessor for an element.
  piece :: (x ∈ xs, Extensible f p t, ExtensibleConstr t xs h x) => Optic' p f (t xs h) (h x)
  piece = pieceAt membership
  {-# INLINE piece #-}
  
  -- | Like 'piece', but reckon membership from its key.
  pieceAssoc :: (Lookup xs k v, Extensible f p t, ExtensibleConstr t xs h (k ':> v)) => Optic' p f (t xs h) (h (k ':> v))
  pieceAssoc = pieceAt association
  {-# INLINE pieceAssoc #-}
  
  -- | Access a specified element through a wrapper.
  itemAt :: (Wrapper h, Extensible f p t, ExtensibleConstr t xs h x) => Membership xs x -> Optic' p f (t xs h) (Repr h x)
  itemAt m = pieceAt m . _Wrapper
  {-# INLINE itemAt #-}
  
  -- | Access an element through a wrapper.
  item :: (Wrapper h, Extensible f p t, x ∈ xs, ExtensibleConstr t xs h x) => proxy x -> Optic' p f (t xs h) (Repr h x)
  item p = piece . _WrapperAs p
  {-# INLINE item #-}
  
  -- | Access an element specified by the key type through a wrapper.
  itemAssoc :: (Wrapper h, Extensible f p t, Lookup xs k v, ExtensibleConstr t xs h (k ':> v))
    => proxy k -> Optic' p f (t xs h) (Repr h (k ':> v))
  itemAssoc p = pieceAssoc . _WrapperAs (proxyKey p)
  {-# INLINE itemAssoc #-}
  
  -- | Access an element specified by the key type through a wrapper.
  itemKey :: forall k v xs h f p t. (Wrapper h, Extensible f p t, Lookup xs k v, ExtensibleConstr t xs h (k ':> v))
    => Optic' p f (t xs h) (Repr h (k ':> v))
  itemKey = pieceAssoc . _WrapperAs (Proxy @(k ':> v))
  {-# INLINE itemKey #-}
  
  proxyKey :: proxy k -> Proxy (k ':> v)
  proxyKey _ = Proxy
  {-# INLINE proxyKey #-}
  
  -- | First element
  type family Head (xs :: [k]) :: k where
    Head (x ': xs) = x
  
  -- | Last element
  type family Last (x :: [k]) :: k where
    Last '[x] = x
    Last (x ': xs) = Last xs
  