module Data.Type.Remove where
import Type.Class.Higher
import Type.Class.Known
import Type.Class.Witness
import Type.Family.Constraint
import Type.Family.List
import Type.Family.Nat
import Data.Type.Length
import Data.Type.Index
import Data.Type.Subset
import Data.Type.Product
import Data.Type.Sum
import Control.Arrow (second,right)
data Remove :: [k] -> k -> [k] -> * where
RZ :: Remove (a :< as) a as
RS :: !(Remove as a bs)
-> Remove (b :< as) a (b :< bs)
deriving instance Eq (Remove as a bs)
deriving instance Ord (Remove as a bs)
deriving instance Show (Remove as a bs)
instance Eq1 (Remove as a)
instance Ord1 (Remove as a)
instance Show1 (Remove as a)
instance Eq2 (Remove as)
instance Ord2 (Remove as)
instance Show2 (Remove as)
instance Eq3 Remove
instance Ord3 Remove
instance Show3 Remove
instance Read3 Remove where
readsPrec3 d = readParen (d > 10) $ \s0 ->
[ (Some3 RZ,s1)
| ("RZ",s1) <- lex s0
] ++
[ (i >>--- Some3 . RS,s2)
| ("RS",s1) <- lex s0
, (i,s2) <- readsPrec3 11 s1
]
instance TestEquality (Remove as a) where
testEquality = \case
RZ -> \case
RZ -> qed
_ -> Nothing
RS x -> \case
RS y -> x =?= y //? qed
_ -> Nothing
remLen :: Remove as a bs -> S (Len bs) :~: Len as
remLen = \case
RZ -> Refl
RS r -> remLen r // Refl
elimRemove :: (forall xs. p (a :< xs) a xs)
-> (forall x xs ys. Remove xs a ys -> p xs a ys -> p (x :< xs) a (x :< ys))
-> Remove as a bs
-> p as a bs
elimRemove z s = \case
RZ -> z
RS r -> s r $ elimRemove z s r
remIx :: Remove as a bs -> Index as a
remIx = \case
RZ -> IZ
RS r -> IS $ remIx r
remSub :: Length bs -> Remove as a bs -> Subset as bs
remSub = \case
LZ -> \case
RZ -> Ø
LS l -> \case
RZ -> IS IZ :< map1 (IS . IS) subRefl \\ l
RS r -> IZ :< map1 IS (remSub l r)
ixRem :: Index as a -> Some (Remove as a)
ixRem = \case
IZ -> Some RZ
IS x -> ixRem x >>- Some . RS
remProd :: Remove as a bs -> Prod f as -> (f a,Prod f bs)
remProd = \case
RZ -> (,) <$> head' <*> tail'
RS r -> \(a :< as) -> second (a :<) $ remProd r as
remSum :: Remove as a bs -> Sum f as -> Either (f a) (Sum f bs)
remSum = \case
RZ -> \case
InL a -> Left a
InR b -> Right b
RS r -> \case
InL a -> Right $ InL a
InR b -> right InR $ remSum r b
class Without (as :: [k]) (a :: k) (bs :: [k]) | as a -> bs where
without :: Remove as a bs
instance (as ~ bs) => Without (a :< as) a bs where
without = RZ
instance (cs ~ (b :< bs), Without as a bs) => Without (b :< as) a cs where
without = RS without
instance Witness ØC (Without as a bs) (Remove as a bs) where
(\\) r = \case
RZ -> r
RS x -> r \\ x
instance (Without as a bs) => Known (Remove as a) bs where
type KnownC (Remove as a) bs = Without as a bs
known = without