{-# OPTIONS_GHC -Wno-redundant-constraints #-}
{-# OPTIONS_HADDOCK not-home #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.OpenUnion.Internal where
import Data.Kind (Type)
import GHC.TypeLits (TypeError, ErrorMessage(..))
import Unsafe.Coerce (unsafeCoerce)
data Union (r :: [Type -> Type]) a where
Union :: {-# UNPACK #-} !Word -> t a -> Union r a
unsafeInj :: Word -> t a -> Union r a
unsafeInj :: Word -> t a -> Union r a
unsafeInj = Word -> t a -> Union r a
forall k (t :: k -> *) (a :: k) (r :: [* -> *]).
Word -> t a -> Union r a
Union
{-# INLINE unsafeInj #-}
unsafePrj :: Word -> Union r a -> Maybe (t a)
unsafePrj :: Word -> Union r a -> Maybe (t a)
unsafePrj Word
n (Union Word
n' t a
x)
| Word
n Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
n' = t a -> Maybe (t a)
forall a. a -> Maybe a
Just (t a -> t a
forall a b. a -> b
unsafeCoerce t a
x)
| Bool
otherwise = Maybe (t a)
forall a. Maybe a
Nothing
{-# INLINE unsafePrj #-}
newtype P t r = P {P t r -> Word
unP :: Word}
class FindElem (t :: Type -> Type) (r :: [Type -> Type]) where
elemNo :: P t r
instance FindElem t (t ': r) where
elemNo :: P t (t : r)
elemNo = Word -> P t (t : r)
forall k k (t :: k) (r :: k). Word -> P t r
P Word
0
instance {-# OVERLAPPABLE #-} FindElem t r => FindElem t (t' ': r) where
elemNo :: P t (t' : r)
elemNo = Word -> P t (t' : r)
forall k k (t :: k) (r :: k). Word -> P t r
P (Word -> P t (t' : r)) -> Word -> P t (t' : r)
forall a b. (a -> b) -> a -> b
$ Word
1 Word -> Word -> Word
forall a. Num a => a -> a -> a
+ P t r -> Word
forall k (t :: k) k (r :: k). P t r -> Word
unP (P t r
forall (t :: * -> *) (r :: [* -> *]). FindElem t r => P t r
elemNo :: P t r)
class IfNotFound (t :: Type -> Type) (r :: [Type -> Type]) (w :: [Type -> Type])
instance TypeError ('Text "‘" ':<>: 'ShowType t
':<>: 'Text "’ is not a member of the type-level list"
':$$: 'Text " ‘" ':<>: 'ShowType w ':<>: 'Text "’"
':$$: 'Text "In the constraint ("
':<>: 'ShowType (Member t w) ':<>: 'Text ")")
=> IfNotFound t '[] w
instance IfNotFound t (t ': r) w
instance {-# OVERLAPPABLE #-} IfNotFound t r w => IfNotFound t (t' ': r) w
instance {-# INCOHERENT #-} IfNotFound t r w
class FindElem eff effs => Member (eff :: Type -> Type) effs where
inj :: eff a -> Union effs a
prj :: Union effs a -> Maybe (eff a)
instance (FindElem t r, IfNotFound t r r) => Member t r where
inj :: t a -> Union r a
inj = Word -> t a -> Union r a
forall k (t :: k -> *) (a :: k) (r :: [* -> *]).
Word -> t a -> Union r a
unsafeInj (Word -> t a -> Union r a) -> Word -> t a -> Union r a
forall a b. (a -> b) -> a -> b
$ P t r -> Word
forall k (t :: k) k (r :: k). P t r -> Word
unP (P t r
forall (t :: * -> *) (r :: [* -> *]). FindElem t r => P t r
elemNo :: P t r)
{-# INLINE inj #-}
prj :: Union r a -> Maybe (t a)
prj = Word -> Union r a -> Maybe (t a)
forall k (r :: [* -> *]) (a :: k) (t :: k -> *).
Word -> Union r a -> Maybe (t a)
unsafePrj (Word -> Union r a -> Maybe (t a))
-> Word -> Union r a -> Maybe (t a)
forall a b. (a -> b) -> a -> b
$ P t r -> Word
forall k (t :: k) k (r :: k). P t r -> Word
unP (P t r
forall (t :: * -> *) (r :: [* -> *]). FindElem t r => P t r
elemNo :: P t r)
{-# INLINE prj #-}
decomp :: Union (t ': r) a -> Either (Union r a) (t a)
decomp :: Union (t : r) a -> Either (Union r a) (t a)
decomp (Union Word
0 t a
a) = t a -> Either (Union r a) (t a)
forall a b. b -> Either a b
Right (t a -> Either (Union r a) (t a))
-> t a -> Either (Union r a) (t a)
forall a b. (a -> b) -> a -> b
$ t a -> t a
forall a b. a -> b
unsafeCoerce t a
a
decomp (Union Word
n t a
a) = Union r a -> Either (Union r a) (t a)
forall a b. a -> Either a b
Left (Union r a -> Either (Union r a) (t a))
-> Union r a -> Either (Union r a) (t a)
forall a b. (a -> b) -> a -> b
$ Word -> t a -> Union r a
forall k (t :: k -> *) (a :: k) (r :: [* -> *]).
Word -> t a -> Union r a
Union (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
1) t a
a
{-# INLINE [2] decomp #-}
decomp0 :: Union '[t] a -> Either (Union '[] a) (t a)
decomp0 :: Union '[t] a -> Either (Union '[] a) (t a)
decomp0 (Union Word
_ t a
a) = t a -> Either (Union '[] a) (t a)
forall a b. b -> Either a b
Right (t a -> Either (Union '[] a) (t a))
-> t a -> Either (Union '[] a) (t a)
forall a b. (a -> b) -> a -> b
$ t a -> t a
forall a b. a -> b
unsafeCoerce t a
a
{-# INLINE decomp0 #-}
{-# RULES "decomp/singleton" decomp = decomp0 #-}
extract :: Union '[t] a -> t a
(Union Word
_ t a
a) = t a -> t a
forall a b. a -> b
unsafeCoerce t a
a
{-# INLINE extract #-}
weaken :: Union r a -> Union (any ': r) a
weaken :: Union r a -> Union (any : r) a
weaken (Union Word
n t a
a) = Word -> t a -> Union (any : r) a
forall k (t :: k -> *) (a :: k) (r :: [* -> *]).
Word -> t a -> Union r a
Union (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
+ Word
1) t a
a
{-# INLINE weaken #-}
infixr 5 :++:
type family xs :++: ys where
'[] :++: ys = ys
(x ': xs) :++: ys = x ': (xs :++: ys)
class Weakens q where
weakens :: Union r a -> Union (q :++: r) a
instance Weakens '[] where
weakens :: Union r a -> Union ('[] :++: r) a
weakens = Union r a -> Union ('[] :++: r) a
forall a. a -> a
id
{-# INLINE weakens #-}
instance Weakens xs => Weakens (x ': xs) where
weakens :: Union r a -> Union ((x : xs) :++: r) a
weakens Union r a
u = Union (xs :++: r) a -> Union (x : (xs :++: r)) a
forall k (r :: [* -> *]) (a :: k) (any :: * -> *).
Union r a -> Union (any : r) a
weaken (Union r a -> Union (xs :++: r) a
forall (q :: [* -> *]) k (r :: [* -> *]) (a :: k).
Weakens q =>
Union r a -> Union (q :++: r) a
weakens @xs Union r a
u)
{-# INLINEABLE weakens #-}