module Data.Yoko.View
where
import Data.Yoko.W
import Data.Yoko.TypeBasics
import Data.Yoko.Representation
import Type.Digits (Digit)
type family Tag (dc :: k) :: Digit
type family Codomain (dc :: k) :: k
type family Codomain0 (dcs :: * -> * -> *) :: *
type family Codomain1 (dcs :: * -> * -> *) :: * -> *
type family Codomain2 (dcs :: * -> * -> *) :: * -> * -> *
type instance Codomain0 (N dc) = Codomain dc
type instance Codomain1 (N dc) = Codomain dc
type instance Codomain2 (N dc) = Codomain dc
type instance Codomain0 (l :+: r) = Codomain0 l
type instance Codomain1 (l :+: r) = Codomain1 l
type instance Codomain2 (l :+: r) = Codomain2 l
data DTPos k = NonRecDT | RecDT [k] [k]
type family DTs (t :: k) :: DTPos k
type NumDTs t = NumDTs' (DTs t)
type family NumDTs' (t :: DTPos k) :: Nat
type instance NumDTs' NonRecDT = Z
type instance NumDTs' (RecDT l r) = S (Length' (Length r) l)
type SiblingDTs t = SiblingDTs' t (DTs t)
type family SiblingDTs' (t :: k) (dpos :: DTPos k) :: [k]
type instance SiblingDTs' t NonRecDT = '[]
type instance SiblingDTs' t (RecDT l r) = Append l (t ': r)
class (Generic dc, DT (Codomain dc)) => DC dc where rejoin :: Sym dc (Codomain dc) p1 p0
type family DCs (t :: k) :: * -> * -> *
class DT t where disband :: W t (DCs t) p1 p0
type family Eval (r :: * -> * -> *) :: *
type instance Eval (T0 Dep t) = t
type instance Eval (l :+: r) = Eval l
type instance Eval (C (dc :: *) r) = Codomain dc
type instance Eval (N dc) = Codomain dc
data SubstSpec star = Sub0 star | Sub1 star | Sub10 star star
type family Subst (spec :: SubstSpec *) (r :: * -> * -> *) :: * -> * -> *
type instance Subst spec (N dc) = N dc
type instance Subst spec (l :+: r) = Subst spec l :+: Subst spec r
type instance Subst spec (C dc r) = C dc (Subst spec r)
type instance Subst spec U = U
type instance Subst spec (l :*: r) = Subst spec l :*: Subst spec r
type instance Subst (Sub0 par0 ) Par0 = T0 Dep par0
type instance Subst (Sub1 par1 ) Par0 = Par0
type instance Subst (Sub10 par1 par0) Par0 = T0 Dep par0
type instance Subst (Sub1 par1 ) Par1 = T0 Dep par1
type instance Subst (Sub10 par1 par0) Par1 = T0 Dep par1
type instance Subst (Sub0 par0) (T1 (Rec lbl) t a) = T0 (Rec lbl) (t (Eval (Subst (Sub0 par0) a)))
type instance Subst (Sub1 par1) (T2 (Rec lbl) t b a) =
T1 (Rec lbl) (t (Eval (Subst (Sub1 par1) b))) (Subst (Sub1 par1) a)
type instance Subst (Sub10 par1 par0) (T2 (Rec lbl) t b a) =
T0 (Rec lbl) (t (Eval (Subst (Sub10 par1 par0) b)) (Eval (Subst (Sub10 par1 par0) a)))
type instance Subst spec (T0 Dep t) = T0 Dep t
type instance Subst spec (T1 Dep f x ) = T1 Dep f (Subst spec x)
type instance Subst spec (T2 Dep f x y) = T2 Dep f (Subst spec x) (Subst spec y)
type Subst0 t p0 = Subst (Sub0 p0) (Rep t)
type Subst1 t p1 = Subst (Sub1 p1) (Rep t)
type Subst10 t p1 p0 = Subst (Sub10 p1 p0) (Rep t)