module Data.Yoko.Reduce (AnRMNUni, Reduce(..), ReduceDC(..)) where
import Type.Yoko
import Data.Yoko.Generic
import Data.Yoko.Reflect
type AnRMNUni m ts = AnRMN m (Uni ts)
class (dcs ::: All IsDC) => Reduce m dcs where
reduce :: AnRMNUni m dcs -> Med m (LeftmostRange dcs)
instance (Med m (LeftmostRange ts) ~ Med m (LeftmostRange us),
Reduce m ts, Reduce m us) => Reduce m (ts :+ us) where
reduce = reduce `two` reduce
instance ReduceDC m dc => Reduce m (N dc) where
reduce = reduceDC . unRMNUni where
unRMNUni :: AnRMNUni m (N dc) -> RMN m dc
unRMNUni (NP (Uni (Here Refl)) x) = x
class DC dc => ReduceDC m dc where reduceDC :: RMN m dc -> Med m (Range dc)
type OneOf ts = NP (Uni ts)
two :: (OneOf ts f -> a) -> (OneOf us f -> a) -> (OneOf (ts :+ us) f -> a)
two f g (NP (Uni tag) x) = case tag of
OnLeft u -> f $ NP (Uni u) x
OnRight v -> g $ NP (Uni v) x