module Data.Yoko.Algebra
(Alg, Algebra(..), Algebras, SiblingAlgs, algebras, CataD(..), catas, cata,
module Data.Yoko.Reduce) where
import Type.Yoko
import Data.Yoko.Generic
import Data.Yoko.Reflect
import Data.Yoko.Reduce
type Alg m t = AnRMNUni m (DCs t) -> Med m t
newtype Algebra m t = Alg (Alg m t)
type instance Unwrap (Algebra m) t = Alg m t
instance Wrapper (Algebra m) where wrap = Alg; unwrap (Alg x) = x
data ReduceD m t where
ReduceD :: (Reduce m (DCs t), t ~ LeftmostRange (DCs t)) => ReduceD m t
instance (Reduce m (DCs t), t ~ LeftmostRange (DCs t)
) => t ::: ReduceD m where inhabits = ReduceD
type Algebras ts m = Each ts (Algebra m)
type SiblingAlgs t m = Algebras (Siblings t) m
algebras :: forall ts m. (ts ::: All (ReduceD m)) => [qP|m|] -> Algebras ts m
algebras _ = each [qP|ReduceD m :: *->*|] $ \ReduceD -> reduce
data CataD ts m t where
CataD :: (DT t, ts ~ Siblings t, t ::: Uni ts,
DCs t ::: All
(YieldsArrowTSSD
(AsComp (RMMap (SiblingsU t) (FromAt m) IdM :. N))),
ts ::: All (CataD ts m)
) => CataD ts m t
instance (DT t, ts ~ Siblings t, t ::: Uni ts,
DCs t ::: All
(YieldsArrowTSSD
(AsComp (RMMap (SiblingsU t) (FromAt m) IdM :. N))),
ts ::: All (CataD ts m)
) => t ::: CataD ts m where inhabits = CataD
catas :: forall m ts. (ts ::: All (CataD ts m)) =>
Algebras ts m -> Each ts (FromAt m IdM)
catas fs = each [qP|CataD ts m :: *->*|] $ \d@CataD -> cataD d fs
cataD :: forall m t. CataD (Siblings t) m t -> SiblingAlgs t m -> t -> Med m t
cataD CataD fs =
prjEach (inhabitsFor [qP|t|]) fs .
appNTtoNP (eachArrow $ AsComp $ composeWith [qP|N :: *->*|] $
RMMap $ catas fs) . firstNP toUni . disband
cata :: (t ::: CataD (Siblings t) m) => SiblingAlgs t m -> t -> Med m t
cata = cataD inhabits