{-|
Copyright   : (c) Hisaket VioletRed, 2022
License     : AGPL-3.0-or-later
Maintainer  : hisaket@outlook.jp
Stability   : experimental
-}

module Polysemy.FS.Scoped.Internal.MembersProof where

import Polysemy ( Members, Effect, EffectRow )
import Polysemy.Internal.Union ( membership, ElemOf (There), )
import Polysemy.Internal.Sing ( SList (SEnd, SCons) )

data MembersProof (es :: EffectRow) (r :: EffectRow) where
    EmptyMembersProof :: MembersProof '[] r
    MembersProof :: ElemOf e r -> MembersProof es r -> MembersProof (e ': es) r

membersProof :: Members es r => SList es -> MembersProof es r
membersProof :: SList es -> MembersProof es r
membersProof = \case
    SList es
SEnd -> MembersProof es r
forall (r :: EffectRow). MembersProof '[] r
EmptyMembersProof
    SCons SList xs
xs -> ElemOf x r -> MembersProof xs r -> MembersProof (x : xs) r
forall (e :: Effect) (r :: EffectRow) (es :: EffectRow).
ElemOf e r -> MembersProof es r -> MembersProof (e : es) r
MembersProof ElemOf x r
forall (e :: Effect) (r :: EffectRow). Member e r => ElemOf e r
membership (MembersProof xs r -> MembersProof (x : xs) r)
-> MembersProof xs r -> MembersProof (x : xs) r
forall a b. (a -> b) -> a -> b
$ SList xs -> MembersProof xs r
forall (es :: EffectRow) (r :: EffectRow).
Members es r =>
SList es -> MembersProof es r
membersProof SList xs
xs

membersProofId :: SList l -> MembersProof l l
membersProofId :: SList l -> MembersProof l l
membersProofId = \case
    SList l
SEnd -> MembersProof l l
forall (r :: EffectRow). MembersProof '[] r
EmptyMembersProof
    SCons SList xs
xs -> MembersProof xs xs -> MembersProof (x : xs) (x : xs)
forall (l :: EffectRow) (e :: Effect).
MembersProof l l -> MembersProof (e : l) (e : l)
weakenIdMP (MembersProof xs xs -> MembersProof (x : xs) (x : xs))
-> MembersProof xs xs -> MembersProof (x : xs) (x : xs)
forall a b. (a -> b) -> a -> b
$ SList xs -> MembersProof xs xs
forall (l :: EffectRow). SList l -> MembersProof l l
membersProofId SList xs
xs

weakenIdMP :: MembersProof l l -> MembersProof (e ': l) (e ': l)
weakenIdMP :: MembersProof l l -> MembersProof (e : l) (e : l)
weakenIdMP MembersProof l l
pr = ElemOf e (e : l)
-> MembersProof l (e : l) -> MembersProof (e : l) (e : l)
forall (e :: Effect) (r :: EffectRow) (es :: EffectRow).
ElemOf e r -> MembersProof es r -> MembersProof (e : es) r
MembersProof ElemOf e (e : l)
forall (e :: Effect) (r :: EffectRow). Member e r => ElemOf e r
membership (MembersProof l (e : l) -> MembersProof (e : l) (e : l))
-> MembersProof l (e : l) -> MembersProof (e : l) (e : l)
forall a b. (a -> b) -> a -> b
$ MembersProof l l -> MembersProof l (e : l)
forall (es :: EffectRow) (r :: EffectRow) (e :: Effect).
MembersProof es r -> MembersProof es (e : r)
weakenRightMP MembersProof l l
pr

weakenRightMP :: MembersProof es r -> MembersProof es (e ': r)
weakenRightMP :: MembersProof es r -> MembersProof es (e : r)
weakenRightMP = \case
    MembersProof es r
EmptyMembersProof -> MembersProof es (e : r)
forall (r :: EffectRow). MembersProof '[] r
EmptyMembersProof
    MembersProof ElemOf e r
pf MembersProof es r
pfs -> ElemOf e (e : r)
-> MembersProof es (e : r) -> MembersProof (e : es) (e : r)
forall (e :: Effect) (r :: EffectRow) (es :: EffectRow).
ElemOf e r -> MembersProof es r -> MembersProof (e : es) r
MembersProof (ElemOf e r -> ElemOf e (e : r)
forall k (r' :: [k]) (e :: k) (e' :: k) (r :: [k]).
(r' ~ (e' : r)) =>
ElemOf e r -> ElemOf e r'
There ElemOf e r
pf) (MembersProof es (e : r) -> MembersProof (e : es) (e : r))
-> MembersProof es (e : r) -> MembersProof (e : es) (e : r)
forall a b. (a -> b) -> a -> b
$ MembersProof es r -> MembersProof es (e : r)
forall (es :: EffectRow) (r :: EffectRow) (e :: Effect).
MembersProof es r -> MembersProof es (e : r)
weakenRightMP MembersProof es r
pfs