{-# LANGUAGE AllowAmbiguousTypes #-}
{-# OPTIONS_HADDOCK not-home #-}
module Control.Effect.Internal.KnownList where

import Data.Bifunctor
import Control.Effect.Internal.Membership
import Control.Effect.Internal.Union


-- | Remove the prefix @xs@ from the list @r@.
--
-- 'Control.Effect.IntroC', 'Control.Effect.ReinterpretC' and friends don't
-- as much introduce effects as they /hide/ them, through removing effects from
-- the derived effects that the transformed carrier carries.
-- This is done thorugh 'StripPrefix'.
--
-- For example:
--
-- @
--    'Control.Effect.Derivs' ('Control.Effect.ReinterpretSimpleC' e '[newE, newE2])
--  = e ': 'StripPrefix' '[newE, newE2] ('Control.Effcet.Derivs' m)
-- @
--
type family StripPrefix xs r where
  StripPrefix '[] r = r
  StripPrefix (x ': xs) (x ': r) = StripPrefix xs r

data SList l where
  SEnd  :: SList '[]
  SCons :: SList xs -> SList (x ': xs)

class KnownList l where
  singList :: SList l

instance KnownList '[] where
  singList :: SList '[]
singList = SList '[]
forall a. SList '[]
SEnd
  {-# INLINE singList #-}

instance KnownList xs => KnownList (x ': xs) where
  singList :: SList (x : xs)
singList = SList xs -> SList (x : xs)
forall a (xs :: [a]) (x :: a). SList xs -> SList (x : xs)
SCons SList xs
forall a (l :: [a]). KnownList l => SList l
singList
  {-# INLINE singList #-}


extendMembership :: forall r e l. SList l -> ElemOf e r -> ElemOf e (Append l r)
extendMembership :: SList l -> ElemOf e r -> ElemOf e (Append l r)
extendMembership SList l
SEnd ElemOf e r
pr = ElemOf e r
ElemOf e (Append l r)
pr
extendMembership (SCons SList xs
l) ElemOf e r
pr = ElemOf e (Append xs r) -> ElemOf e (x : Append xs r)
forall a (e :: a) (r :: [a]) (_e :: a).
ElemOf e r -> ElemOf e (_e : r)
There (SList xs -> ElemOf e r -> ElemOf e (Append xs r)
forall a (r :: [a]) (e :: a) (l :: [a]).
SList l -> ElemOf e r -> ElemOf e (Append l r)
extendMembership SList xs
l ElemOf e r
pr)


splitMembership :: forall r e l
                 . SList l
                -> ElemOf e (Append l r)
                -> Either (ElemOf e l) (ElemOf e r)
splitMembership :: SList l
-> ElemOf e (Append l r) -> Either (ElemOf e l) (ElemOf e r)
splitMembership SList l
SEnd ElemOf e (Append l r)
pr = ElemOf e r -> Either (ElemOf e l) (ElemOf e r)
forall a b. b -> Either a b
Right ElemOf e r
ElemOf e (Append l r)
pr
splitMembership (SCons SList xs
_) ElemOf e (Append l r)
Here = ElemOf e (e : xs) -> Either (ElemOf e (e : xs)) (ElemOf e r)
forall a b. a -> Either a b
Left ElemOf e (e : xs)
forall a (e :: a) (r :: [a]). ElemOf e (e : r)
Here
splitMembership (SCons SList xs
sl) (There ElemOf e r
pr) = (ElemOf e xs -> ElemOf e (x : xs))
-> Either (ElemOf e xs) (ElemOf e r)
-> Either (ElemOf e (x : xs)) (ElemOf e r)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ElemOf e xs -> ElemOf e (x : xs)
forall a (e :: a) (r :: [a]) (_e :: a).
ElemOf e r -> ElemOf e (_e : r)
There (SList xs
-> ElemOf e (Append xs r) -> Either (ElemOf e xs) (ElemOf e r)
forall a (r :: [a]) (e :: a) (l :: [a]).
SList l
-> ElemOf e (Append l r) -> Either (ElemOf e l) (ElemOf e r)
splitMembership @r SList xs
sl ElemOf e r
ElemOf e (Append xs r)
pr)

injectMembership :: forall right e left mid
                  . SList left
                 -> SList mid
                 -> ElemOf e (Append left right)
                 -> ElemOf e (Append left (Append mid right))
injectMembership :: SList left
-> SList mid
-> ElemOf e (Append left right)
-> ElemOf e (Append left (Append mid right))
injectMembership SList left
SEnd SList mid
sm ElemOf e (Append left right)
pr = SList mid -> ElemOf e right -> ElemOf e (Append mid right)
forall a (r :: [a]) (e :: a) (l :: [a]).
SList l -> ElemOf e r -> ElemOf e (Append l r)
extendMembership SList mid
sm ElemOf e right
ElemOf e (Append left right)
pr
injectMembership (SCons SList xs
_) SList mid
_ ElemOf e (Append left right)
Here = ElemOf e (Append left (Append mid right))
forall a (e :: a) (r :: [a]). ElemOf e (e : r)
Here
injectMembership (SCons SList xs
sl) SList mid
sm (There ElemOf e r
pr) = ElemOf e (Append xs (Append mid right))
-> ElemOf e (x : Append xs (Append mid right))
forall a (e :: a) (r :: [a]) (_e :: a).
ElemOf e r -> ElemOf e (_e : r)
There (SList xs
-> SList mid
-> ElemOf e (Append xs right)
-> ElemOf e (Append xs (Append mid right))
forall a (right :: [a]) (e :: a) (left :: [a]) (mid :: [a]).
SList left
-> SList mid
-> ElemOf e (Append left right)
-> ElemOf e (Append left (Append mid right))
injectMembership @right SList xs
sl SList mid
sm ElemOf e r
ElemOf e (Append xs right)
pr)

-- TODO(KingoftheHomeless): This is safe to unsafeCoerce, but would it wreck optimizations?
lengthenMembership :: forall r e l. ElemOf e l -> ElemOf e (Append l r)
lengthenMembership :: ElemOf e l -> ElemOf e (Append l r)
lengthenMembership ElemOf e l
Here = ElemOf e (Append l r)
forall a (e :: a) (r :: [a]). ElemOf e (e : r)
Here
lengthenMembership (There ElemOf e r
xs) = ElemOf e (Append r r) -> ElemOf e (_e : Append r r)
forall a (e :: a) (r :: [a]) (_e :: a).
ElemOf e r -> ElemOf e (_e : r)
There (ElemOf e r -> ElemOf e (Append r r)
forall a (r :: [a]) (e :: a) (l :: [a]).
ElemOf e l -> ElemOf e (Append l r)
lengthenMembership @r ElemOf e r
xs)

weakenN :: SList l -> Union r m a -> Union (Append l r) m a
weakenN :: SList l -> Union r m a -> Union (Append l r) m a
weakenN SList l
sl (Union ElemOf e r
pr e z a
e) = ElemOf e (Append l r) -> e z a -> Union (Append l r) m a
forall (z :: * -> *) (m :: * -> *) (e :: Effect) (r :: [Effect]) a.
Coercible z m =>
ElemOf e r -> e z a -> Union r m a
Union (SList l -> ElemOf e r -> ElemOf e (Append l r)
forall a (r :: [a]) (e :: a) (l :: [a]).
SList l -> ElemOf e r -> ElemOf e (Append l r)
extendMembership SList l
sl ElemOf e r
pr) e z a
e
{-# INLINE weakenN #-}

weakenMid :: forall right m a left mid
           . SList left -> SList mid
          -> Union (Append left right) m a
          -> Union (Append left (Append mid right)) m a
weakenMid :: SList left
-> SList mid
-> Union (Append left right) m a
-> Union (Append left (Append mid right)) m a
weakenMid SList left
sl SList mid
sm (Union ElemOf e (Append left right)
pr e z a
e) = ElemOf e (Append left (Append mid right))
-> e z a -> Union (Append left (Append mid right)) m a
forall (z :: * -> *) (m :: * -> *) (e :: Effect) (r :: [Effect]) a.
Coercible z m =>
ElemOf e r -> e z a -> Union r m a
Union (SList left
-> SList mid
-> ElemOf e (Append left right)
-> ElemOf e (Append left (Append mid right))
forall a (right :: [a]) (e :: a) (left :: [a]) (mid :: [a]).
SList left
-> SList mid
-> ElemOf e (Append left right)
-> ElemOf e (Append left (Append mid right))
injectMembership @right SList left
sl SList mid
sm ElemOf e (Append left right)
pr) e z a
e
{-# INLINE weakenMid #-}

weakenAlgN :: SList l -> Algebra (Append l r) m -> Algebra r m
weakenAlgN :: SList l -> Algebra (Append l r) m -> Algebra r m
weakenAlgN SList l
sl Algebra (Append l r) m
alg Union r m x
u = Union (Append l r) m x -> m x
Algebra (Append l r) m
alg (SList l -> Union r m x -> Union (Append l r) m x
forall (l :: [Effect]) (r :: [Effect]) (m :: * -> *) a.
SList l -> Union r m a -> Union (Append l r) m a
weakenN SList l
sl Union r m x
u)
{-# INLINE weakenAlgN #-}

weakenAlgMid :: forall right m left mid
              . SList left -> SList mid
             -> Algebra (Append left (Append mid right)) m
             -> Algebra (Append left right) m
weakenAlgMid :: SList left
-> SList mid
-> Algebra (Append left (Append mid right)) m
-> Algebra (Append left right) m
weakenAlgMid SList left
sl SList mid
sm Algebra (Append left (Append mid right)) m
alg Union (Append left right) m x
u = Union (Append left (Append mid right)) m x -> m x
Algebra (Append left (Append mid right)) m
alg (SList left
-> SList mid
-> Union (Append left right) m x
-> Union (Append left (Append mid right)) m x
forall (right :: [Effect]) (m :: * -> *) a (left :: [Effect])
       (mid :: [Effect]).
SList left
-> SList mid
-> Union (Append left right) m a
-> Union (Append left (Append mid right)) m a
weakenMid @right SList left
sl SList mid
sm Union (Append left right) m x
u)
{-# INLINE weakenAlgMid #-}


weakenReformMid :: forall right p m z a left mid
                 . SList left -> SList mid
                -> Reformulation' (Append left (Append mid right)) p m z a
                -> Reformulation' (Append left right) p m z a
weakenReformMid :: SList left
-> SList mid
-> Reformulation' (Append left (Append mid right)) p m z a
-> Reformulation' (Append left right) p m z a
weakenReformMid SList left
sl SList mid
sm Reformulation' (Append left (Append mid right)) p m z a
reform = \forall x. m x -> z x
n Algebra p z
alg Union (Append left right) z a
u -> Reformulation' (Append left (Append mid right)) p m z a
reform forall x. m x -> z x
n Algebra p z
alg (SList left
-> SList mid
-> Union (Append left right) z a
-> Union (Append left (Append mid right)) z a
forall (right :: [Effect]) (m :: * -> *) a (left :: [Effect])
       (mid :: [Effect]).
SList left
-> SList mid
-> Union (Append left right) m a
-> Union (Append left (Append mid right)) m a
weakenMid @right SList left
sl SList mid
sm Union (Append left right) z a
u)
{-# INLINE weakenReformMid #-}


-- | Weaken a 'Reformulation' by removing a number of derived effects under
-- the topmost effect.
--
-- This needs a type application to specify what effects to remove.
weakenReformUnder :: forall new e r p m z a
                   . KnownList new
                  => Reformulation' (e ': Append new r) p m z a
                  -> Reformulation' (e ': r) p m z a
weakenReformUnder :: Reformulation' (e : Append new r) p m z a
-> Reformulation' (e : r) p m z a
weakenReformUnder = SList '[e]
-> SList new
-> Reformulation' (Append '[e] (Append new r)) p m z a
-> Reformulation' (Append '[e] r) p m z a
forall (right :: [Effect]) (p :: [Effect]) (m :: * -> *)
       (z :: * -> *) a (left :: [Effect]) (mid :: [Effect]).
SList left
-> SList mid
-> Reformulation' (Append left (Append mid right)) p m z a
-> Reformulation' (Append left right) p m z a
weakenReformMid @r (KnownList '[e] => SList '[e]
forall a (l :: [a]). KnownList l => SList l
singList @'[e]) (KnownList new => SList new
forall a (l :: [a]). KnownList l => SList l
singList @new)
{-# INLINE weakenReformUnder #-}

-- | Weaken a 'Reformulation' by removing a derived effect under
-- the topmost effect.
weakenReformUnder1 :: forall e' e r p m z a
                    . Reformulation' (e ': e' ': r) p m z a
                   -> Reformulation' (e ': r) p m z a
weakenReformUnder1 :: Reformulation' (e : e' : r) p m z a
-> Reformulation' (e : r) p m z a
weakenReformUnder1 = SList '[e]
-> SList '[e']
-> Reformulation' (Append '[e] (Append '[e'] r)) p m z a
-> Reformulation' (Append '[e] r) p m z a
forall (right :: [Effect]) (p :: [Effect]) (m :: * -> *)
       (z :: * -> *) a (left :: [Effect]) (mid :: [Effect]).
SList left
-> SList mid
-> Reformulation' (Append left (Append mid right)) p m z a
-> Reformulation' (Append left right) p m z a
weakenReformMid @r (KnownList '[e] => SList '[e]
forall a (l :: [a]). KnownList l => SList l
singList @'[e]) (KnownList '[e'] => SList '[e']
forall a (l :: [a]). KnownList l => SList l
singList @'[e'])
{-# INLINE weakenReformUnder1 #-}

-- | Weaken a 'Reformulation' by removing a number of derived effects under
-- a number of topmost effects.
--
-- This needs a type application to specify the top effects of the stack
-- underneath which effects are removed, and another
-- type application to specify what effects to remove.
--
-- For example:
--
-- @
-- weakenReformUnderMany \@'['Control.Effect.Error.Catch' e] \@'['Control.Effect.Optional.Optional' ((->) e)]
--   :: Reformulation ('Control.Effect.Error.Catch' e ': 'Control.Effect.Optional.Optional' ((->) e) ': r) p m
--   -> Reformulation ('Control.Effect.Error.Catch' e ': r) p m
-- @
weakenReformUnderMany :: forall top new r p m z a
                       . ( KnownList top
                         , KnownList new
                         )
                      => Reformulation' (Append top (Append new r)) p m z a
                      -> Reformulation' (Append top r) p m z a
weakenReformUnderMany :: Reformulation' (Append top (Append new r)) p m z a
-> Reformulation' (Append top r) p m z a
weakenReformUnderMany = SList top
-> SList new
-> Reformulation' (Append top (Append new r)) p m z a
-> Reformulation' (Append top r) p m z a
forall (right :: [Effect]) (p :: [Effect]) (m :: * -> *)
       (z :: * -> *) a (left :: [Effect]) (mid :: [Effect]).
SList left
-> SList mid
-> Reformulation' (Append left (Append mid right)) p m z a
-> Reformulation' (Append left right) p m z a
weakenReformMid @r (KnownList top => SList top
forall a (l :: [a]). KnownList l => SList l
singList @top) (KnownList new => SList new
forall a (l :: [a]). KnownList l => SList l
singList @new)
{-# INLINE weakenReformUnderMany #-}