module Data.Yoko.Cata
(Algebras, SiblingAlgs, algebras, CataU(..), catas, cata,
module Data.Yoko.Reduce) where
import Type.Yoko
import Data.Yoko.Generic
import Data.Yoko.Reflect
import Data.Yoko.Reduce
type Algebras ts m = Each ts (Algebra m)
type SiblingAlgs t m = Algebras (Siblings t) m
algebras :: forall ts m. (ts ::: All (AlgebraU m)) => [qP|m|] -> Algebras ts m
algebras _ = each [qP|AlgebraU m :: *->*|] $ \AlgebraU -> algebraDT
data CataU ts m t where
CataU :: (DT t, ts ~ Siblings t, ts ::: Exists ((:=:) t),
DCs t ::: All
(YieldsArrowTSSU
(AsComp (RMMap (SiblingsU t) (FromAt m) IdM :. N))),
ts ::: All (CataU ts m)
) => CataU ts m t
instance (DT t, ts ~ Siblings t, ts ::: Exists ((:=:) t),
DCs t ::: All
(YieldsArrowTSSU
(AsComp (RMMap (SiblingsU t) (FromAt m) IdM :. N))),
ts ::: All (CataU ts m)
) => t ::: CataU ts m where inhabits = CataU
catas :: forall m ts. (ts ::: All (CataU ts m)) =>
Algebras ts m -> Each ts (FromAt m IdM)
catas fs = each [qP|CataU ts m :: *->*|] $ \d@CataU -> cataD d fs
cataD :: forall m t. CataU (Siblings t) m t -> SiblingAlgs t m -> t -> Med m t
cataD CataU fs =
appNT fs (inhabits :: Uni (Siblings t) t) .
appNTtoNP (eachArrow $ AsComp $ composeWith [qP|N :: *->*|] $
RMMap $ catas fs) . disband
cata :: (t ::: CataU (Siblings t) m) => SiblingAlgs t m -> t -> Med m t
cata = cataD inhabits