module Data.Yoko.ReflectBase where
import Type.Yoko
import Data.Yoko.Generic
type family Tag dc
type family Recurs t
class (DT (Range dc), dc ::: DCU (Range dc), Generic dc) => DC dc where
occName :: [qP|dc|] -> String
type Range dc
tag :: DCOf (Range dc) dc; tag = inhabits
to :: Range dc -> Maybe (RMNI dc)
to (disband -> NP tg fds) = case eqT tg (tag :: DCOf (Range dc) dc) of
Just Refl -> Just fds
_ -> Nothing
fr :: RMNI dc -> Range dc
data DCOf t dc where DCOf :: (DC dc, t ~ Range dc) => DCU t dc -> DCOf t dc
instance (DC dc, t ~ Range dc) => dc ::: DCOf t where inhabits = DCOf inhabits
type instance Inhabitants (DCOf t) = Inhabitants (DCU t)
instance Finite (DCU t) => Finite (DCOf t) where toUni (DCOf x) = toUni x
type instance Pred (DCOf t) dc = Elem dc (DCs t)
instance EqT (DCU t) => EqT (DCOf t) where eqT (DCOf x) (DCOf y) = eqT x y
data SiblingOf t s where SiblingOf :: (s ::: Uni (Siblings t), Siblings s ~ Siblings t, DT s) => Uni (Siblings t) s -> SiblingOf t s
instance (s ::: Uni (Siblings t), Siblings s ~ Siblings t, DT s) => s ::: SiblingOf t where inhabits = SiblingOf inhabits
type instance Inhabitants (SiblingOf t) = Siblings t
instance Finite (SiblingOf t) where toUni (SiblingOf x) = x
type instance Pred (SiblingOf t) s = Elem s (Siblings t)
instance EqT (SiblingOf t) where eqT (SiblingOf x) (SiblingOf y) = eqT x y
type AnRMN m u = NP u (RM m :. N)
type Disbanded m t = AnRMN m (DCOf t)
disbanded :: DC dc => RMN m dc -> Disbanded m (Range dc)
disbanded fds = NP tag fds
band :: Disbanded IdM t -> t
band (NP (DCOf _) fds) = fr fds
type family LeftmostRange dcs
type instance LeftmostRange (N dc) = Range dc
type instance LeftmostRange (c :+ d) = LeftmostRange c
type DCs t = Inhabitants (DCOf t)
class (Finite (DCU t), EqT (DCU t),
DCs t ::: All (DCOf t),
Siblings t ::: All (SiblingOf t)
) => DT t where
packageName :: [qP|t|] -> String
moduleName :: [qP|t|] -> String
type Siblings t
data DCU t :: * -> *
disband :: t -> Disbanded IdM t