{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
module Type.Membership
  ( -- * Membership
  Membership
  , getMemberId
  , mkMembership
  , leadership
  , nextMembership
  , testMembership
  , compareMembership
  , impossibleMembership
  , reifyMembership
  , Member
  -- * Association
  , Assoc(..)
  , type (>:)
  , Lookup(..)
  , KeyOf
  , KeyIs
  , proxyKeyOf
  , stringKeyOf
  , TargetOf
  , proxyTargetOf
  , TargetIs
  , KeyTargetAre
  -- * Enumeration
  , Generate(..)
  , Forall(..)
  , ForallF
  -- * Reexports
  , Proxy(..)
  ) where

import Data.Constraint
import Data.Proxy
import Data.String
import GHC.TypeLits
import Type.Membership.Internal

-- | Every type-level list is an instance of 'Generate'.
class Generate (xs :: [k]) where
  -- | Enumerate all possible 'Membership's of @xs@.
  henumerate :: (forall x. Membership xs x -> r -> r) -> r -> r

  -- | Count the number of memberships.
  hcount :: proxy xs -> Int

  -- | Enumerate 'Membership's and construct an 'HList'.
  hgenerateList :: Applicative f
    => (forall x. Membership xs x -> f (h x)) -> f (HList h xs)

instance Generate '[] where
  henumerate :: (forall (x :: k). Membership '[] x -> r -> r) -> r -> r
henumerate forall (x :: k). Membership '[] x -> r -> r
_ r
r = r
r

  hcount :: proxy '[] -> Int
hcount proxy '[]
_ = Int
0

  hgenerateList :: (forall (x :: k). Membership '[] x -> f (h x)) -> f (HList h '[])
hgenerateList forall (x :: k). Membership '[] x -> f (h x)
_ = HList h '[] -> f (HList h '[])
forall (f :: * -> *) a. Applicative f => a -> f a
pure HList h '[]
forall k (h :: k -> *). HList h '[]
HNil

instance Generate xs => Generate (x ': xs) where
  henumerate :: (forall (x :: k). Membership (x : xs) x -> r -> r) -> r -> r
henumerate forall (x :: k). Membership (x : xs) x -> r -> r
f r
r = Membership (x : xs) x -> r -> r
forall (x :: k). Membership (x : xs) x -> r -> r
f Membership (x : xs) x
forall k (x :: k) (xs :: [k]). Membership (x : xs) x
leadership (r -> r) -> r -> r
forall a b. (a -> b) -> a -> b
$ (forall (x :: k). Membership xs x -> r -> r) -> r -> r
forall k (xs :: [k]) r.
Generate xs =>
(forall (x :: k). Membership xs x -> r -> r) -> r -> r
henumerate (Membership (x : xs) x -> r -> r
forall (x :: k). Membership (x : xs) x -> r -> r
f (Membership (x : xs) x -> r -> r)
-> (Membership xs x -> Membership (x : xs) x)
-> Membership xs x
-> r
-> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Membership xs x -> Membership (x : xs) x
forall k (xs :: [k]) (y :: k) (x :: k).
Membership xs y -> Membership (x : xs) y
nextMembership) r
r

  hcount :: proxy (x : xs) -> Int
hcount proxy (x : xs)
_ = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Proxy xs -> Int
forall k (xs :: [k]) (proxy :: [k] -> *).
Generate xs =>
proxy xs -> Int
hcount (Proxy xs
forall k (t :: k). Proxy t
Proxy :: Proxy xs)

  -- | Enumerate 'Membership's and construct an 'HList'.
  hgenerateList :: (forall (x :: k). Membership (x : xs) x -> f (h x))
-> f (HList h (x : xs))
hgenerateList forall (x :: k). Membership (x : xs) x -> f (h x)
f = h x -> HList h xs -> HList h (x : xs)
forall a (h :: a -> *) (x :: a) (xs :: [a]).
h x -> HList h xs -> HList h (x : xs)
HCons (h x -> HList h xs -> HList h (x : xs))
-> f (h x) -> f (HList h xs -> HList h (x : xs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Membership (x : xs) x -> f (h x)
forall (x :: k). Membership (x : xs) x -> f (h x)
f Membership (x : xs) x
forall k (x :: k) (xs :: [k]). Membership (x : xs) x
leadership f (HList h xs -> HList h (x : xs))
-> f (HList h xs) -> f (HList h (x : xs))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall (x :: k). Membership xs x -> f (h x)) -> f (HList h xs)
forall k (xs :: [k]) (f :: * -> *) (h :: k -> *).
(Generate xs, Applicative f) =>
(forall (x :: k). Membership xs x -> f (h x)) -> f (HList h xs)
hgenerateList (Membership (x : xs) x -> f (h x)
forall (x :: k). Membership (x : xs) x -> f (h x)
f (Membership (x : xs) x -> f (h x))
-> (Membership xs x -> Membership (x : xs) x)
-> Membership xs x
-> f (h x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Membership xs x -> Membership (x : xs) x
forall k (xs :: [k]) (y :: k) (x :: k).
Membership xs y -> Membership (x : xs) y
nextMembership)

-- | Every element in @xs@ satisfies @c@
class (ForallF c xs, Generate xs) => Forall (c :: k -> Constraint) (xs :: [k]) where
  -- | Enumerate all possible 'Membership's of @xs@ with an additional context.
  henumerateFor :: proxy c -> proxy' xs -> (forall x. c x => Membership xs x -> r -> r) -> r -> r

  hgenerateListFor :: Applicative f
    => proxy c -> (forall x. c x => Membership xs x -> f (h x)) -> f (HList h xs)

instance Forall c '[] where
  henumerateFor :: proxy c
-> proxy' '[]
-> (forall (x :: k). c x => Membership '[] x -> r -> r)
-> r
-> r
henumerateFor proxy c
_ proxy' '[]
_ forall (x :: k). c x => Membership '[] x -> r -> r
_ r
r = r
r

  hgenerateListFor :: proxy c
-> (forall (x :: k). c x => Membership '[] x -> f (h x))
-> f (HList h '[])
hgenerateListFor proxy c
_ forall (x :: k). c x => Membership '[] x -> f (h x)
_ = HList h '[] -> f (HList h '[])
forall (f :: * -> *) a. Applicative f => a -> f a
pure HList h '[]
forall k (h :: k -> *). HList h '[]
HNil

instance (c x, Forall c xs) => Forall c (x ': xs) where
  henumerateFor :: proxy c
-> proxy' (x : xs)
-> (forall (x :: a). c x => Membership (x : xs) x -> r -> r)
-> r
-> r
henumerateFor proxy c
p proxy' (x : xs)
_ forall (x :: a). c x => Membership (x : xs) x -> r -> r
f r
r = Membership (x : xs) x -> r -> r
forall (x :: a). c x => Membership (x : xs) x -> r -> r
f Membership (x : xs) x
forall k (x :: k) (xs :: [k]). Membership (x : xs) x
leadership (r -> r) -> r -> r
forall a b. (a -> b) -> a -> b
$ proxy c
-> Proxy xs
-> (forall (x :: a). c x => Membership xs x -> r -> r)
-> r
-> r
forall k (c :: k -> Constraint) (xs :: [k])
       (proxy :: (k -> Constraint) -> *) (proxy' :: [k] -> *) r.
Forall c xs =>
proxy c
-> proxy' xs
-> (forall (x :: k). c x => Membership xs x -> r -> r)
-> r
-> r
henumerateFor proxy c
p (Proxy xs
forall k (t :: k). Proxy t
Proxy :: Proxy xs) (Membership (x : xs) x -> r -> r
forall (x :: a). c x => Membership (x : xs) x -> r -> r
f (Membership (x : xs) x -> r -> r)
-> (Membership xs x -> Membership (x : xs) x)
-> Membership xs x
-> r
-> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Membership xs x -> Membership (x : xs) x
forall k (xs :: [k]) (y :: k) (x :: k).
Membership xs y -> Membership (x : xs) y
nextMembership) r
r

  hgenerateListFor :: proxy c
-> (forall (x :: a). c x => Membership (x : xs) x -> f (h x))
-> f (HList h (x : xs))
hgenerateListFor proxy c
p forall (x :: a). c x => Membership (x : xs) x -> f (h x)
f = h x -> HList h xs -> HList h (x : xs)
forall a (h :: a -> *) (x :: a) (xs :: [a]).
h x -> HList h xs -> HList h (x : xs)
HCons (h x -> HList h xs -> HList h (x : xs))
-> f (h x) -> f (HList h xs -> HList h (x : xs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Membership (x : xs) x -> f (h x)
forall (x :: a). c x => Membership (x : xs) x -> f (h x)
f Membership (x : xs) x
forall k (x :: k) (xs :: [k]). Membership (x : xs) x
leadership f (HList h xs -> HList h (x : xs))
-> f (HList h xs) -> f (HList h (x : xs))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> proxy c
-> (forall (x :: a). c x => Membership xs x -> f (h x))
-> f (HList h xs)
forall k (c :: k -> Constraint) (xs :: [k]) (f :: * -> *)
       (proxy :: (k -> Constraint) -> *) (h :: k -> *).
(Forall c xs, Applicative f) =>
proxy c
-> (forall (x :: k). c x => Membership xs x -> f (h x))
-> f (HList h xs)
hgenerateListFor proxy c
p (Membership (x : xs) x -> f (h x)
forall (x :: a). c x => Membership (x : xs) x -> f (h x)
f (Membership (x : xs) x -> f (h x))
-> (Membership xs x -> Membership (x : xs) x)
-> Membership xs x
-> f (h x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Membership xs x -> Membership (x : xs) x
forall k (xs :: [k]) (y :: k) (x :: k).
Membership xs y -> Membership (x : xs) y
nextMembership)

-- | HACK: Without this, the constraints are not propagated well.
type family ForallF (c :: k -> Constraint) (xs :: [k]) :: Constraint where
  ForallF c '[] = ()
  ForallF c (x ': xs) = (c x, Forall c xs)

-- | Take the type of the key
type family KeyOf (kv :: Assoc k v) :: k where
  KeyOf (k ':> v) = k

-- | Proxy-level 'KeyOf'. This is useful when using 'symbolVal'.
proxyKeyOf :: proxy kv -> Proxy (KeyOf kv)
proxyKeyOf :: proxy kv -> Proxy (KeyOf kv)
proxyKeyOf proxy kv
_ = Proxy (KeyOf kv)
forall k (t :: k). Proxy t
Proxy

-- | Get a string from a proxy of @'Assoc' 'Symbol' v@.
stringKeyOf :: (IsString a, KnownSymbol (KeyOf kv)) => proxy kv -> a
stringKeyOf :: proxy kv -> a
stringKeyOf = String -> a
forall a. IsString a => String -> a
fromString (String -> a) -> (proxy kv -> String) -> proxy kv -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy (KeyOf kv) -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (Proxy (KeyOf kv) -> String)
-> (proxy kv -> Proxy (KeyOf kv)) -> proxy kv -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. proxy kv -> Proxy (KeyOf kv)
forall k v (proxy :: Assoc k v -> *) (kv :: Assoc k v).
proxy kv -> Proxy (KeyOf kv)
proxyKeyOf
{-# INLINE stringKeyOf #-}

-- | Constraint applied to 'KeyOf'
class (pk (KeyOf kv)) => KeyIs pk kv where

instance (pk k) => KeyIs pk (k ':> v)

-- | Take the type of the value
type family TargetOf (kv :: Assoc k v) :: v where
  TargetOf (k ':> v) = v

-- | Proxy-level 'TargetOf'.
proxyTargetOf :: proxy kv -> Proxy (TargetOf kv)
proxyTargetOf :: proxy kv -> Proxy (TargetOf kv)
proxyTargetOf proxy kv
_ = Proxy (TargetOf kv)
forall k (t :: k). Proxy t
Proxy

-- | Constraint applied to 'TargetOf'
class (pv (TargetOf kv)) => TargetIs pv kv where

instance (pv v) => TargetIs pv (k ':> v)

-- | Combined constraint for 'Assoc'
class (pk (KeyOf kv), pv (TargetOf kv)) => KeyTargetAre pk pv kv where

instance (pk k, pv v) => KeyTargetAre pk pv (k ':> v)