{-# LANGUAGE CPP #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Type.Membership.Internal (
  -- * Membership
  Membership
  , getMemberId
  , mkMembership
  , leadership
  , nextMembership
  , testMembership
  , compareMembership
  , impossibleMembership
  , reifyMembership
  -- * Member class
  , Member(..)
  , type (∈)
  , FindType
  -- * Association
  , Assoc(..)
  , type (>:)
  , Lookup(..)
  , FindAssoc
  -- * Sugar
  , Elaborate
  , Elaborated(..)
  -- * HList
  , HList(..)
  , hfoldrWithIndex
  , htraverseWithIndex
  -- * Miscellaneous
  , module Data.Type.Equality
  , module Data.Proxy
  ) where
import Control.DeepSeq (NFData)
import Data.Type.Equality
import Data.Proxy
import Control.Monad
import Unsafe.Coerce
import qualified Data.Kind as K
import Data.Hashable
import Data.Text.Prettyprint.Doc
import Data.Typeable
import Language.Haskell.TH hiding (Pred)
import Language.Haskell.TH.Lift
#if MIN_VERSION_template_haskell(2,17,0)
import Language.Haskell.TH.Syntax
#endif
import Data.Semigroup (Semigroup(..))
import GHC.TypeLits

-- | A witness that of @x@ is a member of a type level set @xs@.
newtype Membership (xs :: [k]) (x :: k) = Membership
  { Membership xs x -> Int
getMemberId :: Int -- ^ get the position as an 'Int'.
  } deriving (Typeable, Membership xs x -> ()
(Membership xs x -> ()) -> NFData (Membership xs x)
forall a. (a -> ()) -> NFData a
forall k (xs :: [k]) (x :: k). Membership xs x -> ()
rnf :: Membership xs x -> ()
$crnf :: forall k (xs :: [k]) (x :: k). Membership xs x -> ()
NFData)

instance Show (Membership xs x) where
  show :: Membership xs x -> String
show (Membership Int
n) = String
"$(mkMembership " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"

instance Pretty (Membership xs x) where
  pretty :: Membership xs x -> Doc ann
pretty (Membership Int
n) = Doc ann
"$(mkMembership " Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Int
n Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
")"

instance Eq (Membership xs x) where
  Membership xs x
_ == :: Membership xs x -> Membership xs x -> Bool
== Membership xs x
_ = Bool
True

instance Ord (Membership xs x) where
  compare :: Membership xs x -> Membership xs x -> Ordering
compare Membership xs x
_ Membership xs x
_ = Ordering
EQ

instance Semigroup (Membership xs x) where
  Membership xs x
x <> :: Membership xs x -> Membership xs x -> Membership xs x
<> Membership xs x
_ = Membership xs x
x

-- | Generates a 'Membership' that corresponds to the given ordinal (0-origin).
#if MIN_VERSION_template_haskell(2,17,0)
mkMembership :: Quote m => Int -> m Exp
#else
mkMembership :: Int -> Q Exp
#endif
mkMembership :: Int -> Q Exp
mkMembership Int
n = do
  let names :: [Name]
names = (String -> Name) -> [String] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map String -> Name
mkName ([String] -> [Name]) -> [String] -> [Name]
forall a b. (a -> b) -> a -> b
$ Int -> [String] -> [String]
forall a. Int -> [a] -> [a]
take (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ (Int -> [String]) -> [Int] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((Int -> String -> [String]) -> String -> Int -> [String]
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> String -> [String]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM [Char
'a'..Char
'z']) [Int
1..]
  let rest :: Name
rest = String -> Name
mkName String
"any"
  let cons :: Type -> Type -> Type
cons Type
x Type
xs = Type
PromotedConsT Type -> Type -> Type
`AppT` Type
x Type -> Type -> Type
`AppT` Type
xs
  let t :: Type
t = (Type -> Type -> Type) -> Type -> [Type] -> Type
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Type -> Type -> Type
cons (Name -> Type
VarT Name
rest) ((Name -> Type) -> [Name] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Type
VarT [Name]
names)
  Q Exp -> TypeQ -> Q Exp
sigE (Name -> Q Exp
conE 'Membership Q Exp -> Q Exp -> Q Exp
`appE` Lit -> Q Exp
litE (Integer -> Lit
IntegerL (Integer -> Lit) -> Integer -> Lit
forall a b. (a -> b) -> a -> b
$ Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
n))
#if MIN_VERSION_template_haskell(2,17,0)
    $ forallT (PlainTV rest SpecifiedSpec : map (PlainTV `flip` SpecifiedSpec) names) (pure [])
#else
    (TypeQ -> Q Exp) -> TypeQ -> Q Exp
forall a b. (a -> b) -> a -> b
$ [TyVarBndr] -> CxtQ -> TypeQ -> TypeQ
forallT (Name -> TyVarBndr
PlainTV Name
rest TyVarBndr -> [TyVarBndr] -> [TyVarBndr]
forall a. a -> [a] -> [a]
: (Name -> TyVarBndr) -> [Name] -> [TyVarBndr]
forall a b. (a -> b) -> [a] -> [b]
map Name -> TyVarBndr
PlainTV [Name]
names) ([Type] -> CxtQ
forall (f :: * -> *) a. Applicative f => a -> f a
pure [])
#endif
    (TypeQ -> TypeQ) -> TypeQ -> TypeQ
forall a b. (a -> b) -> a -> b
$ Name -> TypeQ
conT ''Membership TypeQ -> TypeQ -> TypeQ
`appT` Type -> TypeQ
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t TypeQ -> TypeQ -> TypeQ
`appT` Name -> TypeQ
varT ([Name]
names [Name] -> Int -> Name
forall a. [a] -> Int -> a
!! Int
n)

instance Lift (Membership xs x) where
  lift :: Membership xs x -> Q Exp
lift (Membership Int
i) = Int -> Q Exp
mkMembership Int
i
#if MIN_VERSION_template_haskell(2,17,0)
  liftTyped (Membership i) = Code $ TExp <$> mkMembership i
#endif
-- | @x@ is a member of @xs@
class Member xs x where
  membership :: Membership xs x

instance (Elaborate x (FindType x xs) ~ 'Expecting pos, KnownNat pos) => Member xs x where
  membership :: Membership xs x
membership = Int -> Membership xs x
forall k (xs :: [k]) (x :: k). Int -> Membership xs x
Membership (Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy pos -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy pos
forall k (t :: k). Proxy t
Proxy :: Proxy pos))
  {-# INLINE membership #-}

instance Hashable (Membership xs x) where
  hashWithSalt :: Int -> Membership xs x -> Int
hashWithSalt Int
s = Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s (Int -> Int) -> (Membership xs x -> Int) -> Membership xs x -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Membership xs x -> Int
forall k (xs :: [k]) (x :: k). Membership xs x -> Int
getMemberId

-- | A readable type search result
data Elaborated k v = Expecting v | Missing k | Duplicate k

-- | Make the result more readable
type family Elaborate (key :: k) (xs :: [v]) :: Elaborated k v where
  Elaborate k '[] = 'Missing k
  Elaborate k '[x] = 'Expecting x
  Elaborate k xs = 'Duplicate k

-- | Find a type associated to the specified key.
type family FindAssoc (n :: Nat) (key :: k) (xs :: [Assoc k v]) where
  FindAssoc n k ((k ':> v) ': xs) = (n ':> v) ': FindAssoc (1 + n) k xs
  FindAssoc n k ((k' ':> v) ': xs) = FindAssoc (1 + n) k xs
  FindAssoc n k '[] = '[]

-- | Embodies a type equivalence to ensure that the 'Membership' points the first element.
testMembership :: Membership (y ': xs) x -> (x :~: y -> r) -> (Membership xs x -> r) -> r
testMembership :: Membership (y : xs) x
-> ((x :~: y) -> r) -> (Membership xs x -> r) -> r
testMembership (Membership Int
0) (x :~: y) -> r
l Membership xs x -> r
_ = (x :~: y) -> r
l ((Any :~: Any) -> x :~: y
forall a b. a -> b
unsafeCoerce Any :~: Any
forall k (a :: k). a :~: a
Refl)
testMembership (Membership Int
n) (x :~: y) -> r
_ Membership xs x -> r
r = Membership xs x -> r
r (Int -> Membership xs x
forall k (xs :: [k]) (x :: k). Int -> Membership xs x
Membership (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1))
{-# INLINE testMembership #-}

-- | Compare two 'Membership's.
compareMembership :: Membership xs x -> Membership xs y -> Either Ordering (x :~: y)
compareMembership :: Membership xs x -> Membership xs y -> Either Ordering (x :~: y)
compareMembership (Membership Int
m) (Membership Int
n) = case Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Int
m Int
n of
  Ordering
EQ -> (x :~: y) -> Either Ordering (x :~: y)
forall a b. b -> Either a b
Right ((Any :~: Any) -> x :~: y
forall a b. a -> b
unsafeCoerce Any :~: Any
forall k (a :: k). a :~: a
Refl)
  Ordering
x -> Ordering -> Either Ordering (x :~: y)
forall a b. a -> Either a b
Left Ordering
x
{-# INLINE compareMembership #-}

-- | There is no 'Membership' of an empty list.
impossibleMembership :: Membership '[] x -> r
impossibleMembership :: Membership '[] x -> r
impossibleMembership Membership '[] x
_ = String -> r
forall a. HasCallStack => String -> a
error String
"Impossible"

-- | This 'Membership' points to the first element
leadership :: Membership (x ': xs) x
leadership :: Membership (x : xs) x
leadership = Int -> Membership (x : xs) x
forall k (xs :: [k]) (x :: k). Int -> Membership xs x
Membership Int
0
{-# INLINE leadership #-}

-- | The next membership
nextMembership :: Membership xs y -> Membership (x ': xs) y
nextMembership :: Membership xs y -> Membership (x : xs) y
nextMembership (Membership Int
n) = Int -> Membership (x : xs) y
forall k (xs :: [k]) (x :: k). Int -> Membership xs x
Membership (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
{-# INLINE nextMembership #-}

-- | Make up a 'Membership' from an integer.
reifyMembership :: Int -> (forall x. Membership xs x -> r) -> r
reifyMembership :: Int -> (forall (x :: k). Membership xs x -> r) -> r
reifyMembership Int
n forall (x :: k). Membership xs x -> r
k = Membership xs Any -> r
forall (x :: k). Membership xs x -> r
k (Int -> Membership xs Any
forall k (xs :: [k]) (x :: k). Int -> Membership xs x
Membership Int
n)

-- | Unicode flipped alias for 'Member'
type x ∈ xs = Member xs x

-- | FindType types
type family FindType (x :: k) (xs :: [k]) :: [Nat] where
  FindType x (x ': xs) = 0 ': MapSucc (FindType x xs)
  FindType x (y ': ys) = MapSucc (FindType x ys)
  FindType x '[] = '[]

-- | Ideally, it will be 'Map Succ'
type family MapSucc (xs :: [Nat]) :: [Nat] where
  MapSucc '[] = '[]
  MapSucc (x ': xs) = (1 + x) ': MapSucc xs

-- | The kind of key-value pairs
data Assoc k v = k :> v
infix 0 :>

-- | A synonym for (':>')
type (>:) = '(:>)

-- | @'Lookup' xs k v@ is essentially identical to @(k :> v) ∈ xs@
-- , but the type @v@ is inferred from @k@ and @xs@.
class Lookup xs k v | k xs -> v where
  association :: Membership xs (k ':> v)

instance (Elaborate k (FindAssoc 0 k xs) ~ 'Expecting (n ':> v), KnownNat n) => Lookup xs k v where
  association :: Membership xs (k ':> v)
association = Int -> Membership xs (k ':> v)
forall k (xs :: [k]) (x :: k). Int -> Membership xs x
Membership (Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall k (t :: k). Proxy t
Proxy :: Proxy n))

data HList (h :: k -> K.Type) (xs :: [k]) where
  HNil :: HList h '[]
  HCons :: h x -> HList h xs -> HList h (x ': xs)

infixr 5 `HCons`

hfoldrWithIndex :: forall h r xs. (forall x. Membership xs x -> h x -> r -> r) -> r -> HList h xs -> r
hfoldrWithIndex :: (forall (x :: k). Membership xs x -> h x -> r -> r)
-> r -> HList h xs -> r
hfoldrWithIndex forall (x :: k). Membership xs x -> h x -> r -> r
f r
r = Int -> HList h xs -> r
forall (t :: [k]). Int -> HList h t -> r
go Int
0 where
  go :: Int -> HList h t -> r
  go :: Int -> HList h t -> r
go !Int
k (HCons h x
x HList h xs
xs) = Membership xs x -> h x -> r -> r
forall (x :: k). Membership xs x -> h x -> r -> r
f (Int -> Membership xs x
forall k (xs :: [k]) (x :: k). Int -> Membership xs x
Membership Int
k) h x
x (r -> r) -> r -> r
forall a b. (a -> b) -> a -> b
$ Int -> HList h xs -> r
forall (t :: [k]). Int -> HList h t -> r
go (Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) HList h xs
xs
  go Int
_ HList h t
HNil = r
r
{-# INLINE hfoldrWithIndex #-}

htraverseWithIndex :: forall f g h xs. Applicative f
    => (forall x. Membership xs x -> g x -> f (h x)) -> HList g xs -> f (HList h xs)
htraverseWithIndex :: (forall (x :: k). Membership xs x -> g x -> f (h x))
-> HList g xs -> f (HList h xs)
htraverseWithIndex forall (x :: k). Membership xs x -> g x -> f (h x)
f = Int -> HList g xs -> f (HList h xs)
forall (t :: [k]). Int -> HList g t -> f (HList h t)
go Int
0 where
  go :: Int -> HList g t -> f (HList h t)
  go :: Int -> HList g t -> f (HList h t)
go !Int
k (HCons g x
x HList g xs
xs) = 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 xs x -> g x -> f (h x)
forall (x :: k). Membership xs x -> g x -> f (h x)
f (Int -> Membership xs x
forall k (xs :: [k]) (x :: k). Int -> Membership xs x
Membership Int
k) g x
x 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
<*> Int -> HList g xs -> f (HList h xs)
forall (t :: [k]). Int -> HList g t -> f (HList h t)
go (Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) HList g xs
xs
  go Int
_ HList g t
HNil = HList h '[] -> f (HList h '[])
forall (f :: * -> *) a. Applicative f => a -> f a
pure HList h '[]
forall k (h :: k -> *). HList h '[]
HNil
{-# INLINE htraverseWithIndex #-}