module Data.Type.List.Proof.Member (
Member(..),
toEq, weakenL, same, weakenR, split
) where
import Data.Type.List.List
import Data.Type.List.Proof.Append
import Data.Type.Equality ((:=:)(..))
import Data.Proxy (Proxy(..))
import Data.Typeable
import Unsafe.Coerce
data Member ctx a where
Member_Base :: Member (ctx :> a) a
Member_Step :: Member ctx a -> Member (ctx :> b) a
deriving Typeable
instance Show (Member r a) where showsPrec p = showsPrecMember (p > 10)
showsPrecMember _ Member_Base = showString "Member_Base"
showsPrecMember p (Member_Step prf) = showParen p $
showString "Member_Step" . showsPrec 10 prf
toEq :: Member (Nil :> a) b -> b :=: a
toEq Member_Base = Refl
toEq _ = error "Should not happen! (toEq)"
weakenL :: Proxy r1 -> Member r2 a -> Member (r1 :++: r2) a
weakenL _ Member_Base = Member_Base
weakenL tag (Member_Step mem) = Member_Step (weakenL tag mem)
same :: Member r a -> Member r b -> Maybe (a :=: b)
same Member_Base Member_Base = Just $ unsafeCoerce Refl
same (Member_Step mem1) (Member_Step mem2) = same mem1 mem2
same _ _ = Nothing
weakenR :: Member r1 a -> Append r1 r2 r -> Member r a
weakenR mem Append_Base = mem
weakenR mem (Append_Step app) = Member_Step (weakenR mem app)
split ::
Append r1 r2 r -> Member r a -> Either (Member r1 a) (Member r2 a)
split app mem = case app of
Append_Base -> Left mem
Append_Step app' -> case mem of
Member_Base -> Right Member_Base
Member_Step mem' -> case split app' mem' of
Left prf -> Left prf
Right prf -> Right (Member_Step prf)