{-# 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 :: Optic' p f (t xs h) (h x)
piece = Membership xs x -> Optic' p f (t xs h) (h x)
forall k (f :: Type -> Type) (p :: Type -> Type -> Type)
       (t :: [k] -> (k -> Type) -> Type) (xs :: [k]) (h :: k -> Type)
       (x :: k).
(Extensible f p t, ExtensibleConstr t xs h x) =>
Membership xs x -> Optic' p f (t xs h) (h x)
pieceAt Membership xs x
forall k (xs :: [k]) (x :: k). Member xs x => Membership xs x
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 :: Optic' p f (t xs h) (h (k ':> v))
pieceAssoc = Membership xs (k ':> v) -> Optic' p f (t xs h) (h (k ':> v))
forall k (f :: Type -> Type) (p :: Type -> Type -> Type)
       (t :: [k] -> (k -> Type) -> Type) (xs :: [k]) (h :: k -> Type)
       (x :: k).
(Extensible f p t, ExtensibleConstr t xs h x) =>
Membership xs x -> Optic' p f (t xs h) (h x)
pieceAt Membership xs (k ':> v)
forall k k1 (xs :: [Assoc k k1]) (k2 :: k) (v :: k1).
Lookup xs k2 v =>
Membership xs (k2 ':> v)
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 :: Membership xs x -> Optic' p f (t xs h) (Repr h x)
itemAt Membership xs x
m = Membership xs x -> Optic' p f (t xs h) (h x)
forall k (f :: Type -> Type) (p :: Type -> Type -> Type)
       (t :: [k] -> (k -> Type) -> Type) (xs :: [k]) (h :: k -> Type)
       (x :: k).
(Extensible f p t, ExtensibleConstr t xs h x) =>
Membership xs x -> Optic' p f (t xs h) (h x)
pieceAt Membership xs x
m Optic' p f (t xs h) (h x)
-> (p (Repr h x) (f (Repr h x)) -> p (h x) (f (h x)))
-> Optic' p f (t xs h) (Repr h x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p (Repr h x) (f (Repr h x)) -> p (h x) (f (h x))
forall k (h :: k -> Type) (f :: Type -> Type)
       (p :: Type -> Type -> Type) (v :: k).
(Wrapper h, Functor f, Profunctor p) =>
Optic' p f (h v) (Repr h v)
_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 :: proxy x -> Optic' p f (t xs h) (Repr h x)
item proxy x
p = Optic' p f (t xs h) (h x)
forall k (x :: k) (xs :: [k]) (f :: Type -> Type)
       (p :: Type -> Type -> Type) (t :: [k] -> (k -> Type) -> Type)
       (h :: k -> Type).
(x ∈ xs, Extensible f p t, ExtensibleConstr t xs h x) =>
Optic' p f (t xs h) (h x)
piece Optic' p f (t xs h) (h x)
-> (p (Repr h x) (f (Repr h x)) -> p (h x) (f (h x)))
-> Optic' p f (t xs h) (Repr h x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. proxy x -> p (Repr h x) (f (Repr h x)) -> p (h x) (f (h x))
forall k (f :: Type -> Type) (p :: Type -> Type -> Type)
       (h :: k -> Type) (proxy :: k -> Type) (v :: k).
(Functor f, Profunctor p, Wrapper h) =>
proxy v -> Optic' p f (h v) (Repr h v)
_WrapperAs proxy x
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 :: proxy k -> Optic' p f (t xs h) (Repr h (k ':> v))
itemAssoc proxy k
p = Optic' p f (t xs h) (h (k ':> v))
forall k v (xs :: [Assoc k v]) (k :: k) (v :: v)
       (f :: Type -> Type) (p :: Type -> Type -> Type)
       (t :: [Assoc k v] -> (Assoc k v -> Type) -> Type)
       (h :: Assoc k v -> Type).
(Lookup xs k v, Extensible f p t,
 ExtensibleConstr t xs h (k ':> v)) =>
Optic' p f (t xs h) (h (k ':> v))
pieceAssoc Optic' p f (t xs h) (h (k ':> v))
-> (p (Repr h (k ':> v)) (f (Repr h (k ':> v)))
    -> p (h (k ':> v)) (f (h (k ':> v))))
-> Optic' p f (t xs h) (Repr h (k ':> v))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy (k ':> v)
-> p (Repr h (k ':> v)) (f (Repr h (k ':> v)))
-> p (h (k ':> v)) (f (h (k ':> v)))
forall k (f :: Type -> Type) (p :: Type -> Type -> Type)
       (h :: k -> Type) (proxy :: k -> Type) (v :: k).
(Functor f, Profunctor p, Wrapper h) =>
proxy v -> Optic' p f (h v) (Repr h v)
_WrapperAs (proxy k -> Proxy (k ':> v)
forall k v (proxy :: k -> Type) (k :: k) (v :: v).
proxy k -> Proxy (k ':> v)
proxyKey proxy k
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 :: Optic' p f (t xs h) (Repr h (k ':> v))
itemKey = Optic' p f (t xs h) (h (k ':> v))
forall k v (xs :: [Assoc k v]) (k :: k) (v :: v)
       (f :: Type -> Type) (p :: Type -> Type -> Type)
       (t :: [Assoc k v] -> (Assoc k v -> Type) -> Type)
       (h :: Assoc k v -> Type).
(Lookup xs k v, Extensible f p t,
 ExtensibleConstr t xs h (k ':> v)) =>
Optic' p f (t xs h) (h (k ':> v))
pieceAssoc Optic' p f (t xs h) (h (k ':> v))
-> (p (Repr h (k ':> v)) (f (Repr h (k ':> v)))
    -> p (h (k ':> v)) (f (h (k ':> v))))
-> Optic' p f (t xs h) (Repr h (k ':> v))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy (k ':> v)
-> p (Repr h (k ':> v)) (f (Repr h (k ':> v)))
-> p (h (k ':> v)) (f (h (k ':> v)))
forall k (f :: Type -> Type) (p :: Type -> Type -> Type)
       (h :: k -> Type) (proxy :: k -> Type) (v :: k).
(Functor f, Profunctor p, Wrapper h) =>
proxy v -> Optic' p f (h v) (Repr h v)
_WrapperAs (Proxy (k ':> v)
forall k (t :: k). Proxy t
Proxy @(k ':> v))
{-# INLINE itemKey #-}

proxyKey :: proxy k -> Proxy (k ':> v)
proxyKey :: proxy k -> Proxy (k ':> v)
proxyKey proxy k
_ = Proxy (k ':> v)
forall k (t :: k). Proxy t
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