{-# 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 = SEnd
  {-# INLINE singList #-}

instance KnownList xs => KnownList (x ': xs) where
  singList = SCons singList
  {-# INLINE singList #-}


extendMembership :: forall r e l. SList l -> ElemOf e r -> ElemOf e (Append l r)
extendMembership SEnd pr = pr
extendMembership (SCons l) pr = There (extendMembership l pr)


splitMembership :: forall r e l
                 . SList l
                -> ElemOf e (Append l r)
                -> Either (ElemOf e l) (ElemOf e r)
splitMembership SEnd pr = Right pr
splitMembership (SCons _) Here = Left Here
splitMembership (SCons sl) (There pr) = first There (splitMembership @r sl pr)

injectMembership :: forall right e left mid
                  . SList left
                 -> SList mid
                 -> ElemOf e (Append left right)
                 -> ElemOf e (Append left (Append mid right))
injectMembership SEnd sm pr = extendMembership sm pr
injectMembership (SCons _) _ Here = Here
injectMembership (SCons sl) sm (There pr) = There (injectMembership @right sl sm 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 Here = Here
lengthenMembership (There xs) = There (lengthenMembership @r xs)

weakenN :: SList l -> Union r m a -> Union (Append l r) m a
weakenN sl (Union pr e) = Union (extendMembership sl pr) 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 sl sm (Union pr e) = Union (injectMembership @right sl sm pr) e
{-# INLINE weakenMid #-}

weakenAlgN :: SList l -> Algebra (Append l r) m -> Algebra r m
weakenAlgN sl alg u = alg (weakenN sl 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 sl sm alg u = alg (weakenMid @right sl sm 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 sl sm reform = \n alg u -> reform n alg (weakenMid @right sl sm 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 = weakenReformMid @r (singList @'[e]) (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 = weakenReformMid @r (singList @'[e]) (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 = weakenReformMid @r (singList @top) (singList @new)
{-# INLINE weakenReformUnderMany #-}