module Data.Comp.MultiParam.Algebra (
Alg,
free,
cata,
cata',
appCxt,
AlgM,
freeM,
cataM,
AlgM',
Compose(..),
freeM',
cataM',
CxtFun,
SigFun,
TermHom,
appTermHom,
appTermHom',
compTermHom,
appSigFun,
appSigFun',
compSigFun,
termHom,
compAlg,
CxtFunM,
SigFunM,
TermHomM,
sigFunM,
termHom',
appTermHomM,
appTermHomM',
termHomM,
appSigFunM,
appSigFunM',
compTermHomM,
compSigFunM,
compAlgM,
compAlgM'
) where
import Prelude hiding (sequence, mapM)
import Control.Monad hiding (sequence, mapM)
import Data.Functor.Compose
import Data.Comp.MultiParam.Term
import Data.Comp.MultiParam.HDifunctor
import Data.Comp.MultiParam.HDitraversable
import Unsafe.Coerce (unsafeCoerce)
type Alg f a = f a a :-> a
free :: forall h f a b. HDifunctor f
=> Alg f a -> (b :-> a) -> Cxt h f a b :-> a
free f g = run
where run :: Cxt h f a b :-> a
run (Term t) = f (hfmap run t)
run (Hole x) = g x
run (Place p) = p
cata :: forall f a. HDifunctor f => Alg f a -> Term f :-> a
cata f = run . coerceCxt
where run :: Trm f a :-> a
run (Term t) = f (hfmap run t)
run (Place x) = x
cata' :: HDifunctor f => Alg f a -> Cxt h f a a :-> a
cata' f = free f id
appCxt :: HDifunctor f => Cxt Hole f a (Cxt h f a b) :-> Cxt h f a b
appCxt (Term t) = Term (hfmap appCxt t)
appCxt (Hole x) = x
appCxt (Place p) = Place p
type AlgM m f a = NatM m (f a a) a
freeM :: forall m h f a b. (HDitraversable f m a, Monad m)
=> AlgM m f a -> NatM m b a -> NatM m (Cxt h f a b) a
freeM f g = run
where run :: NatM m (Cxt h f a b) a
run (Term t) = f =<< hdimapM run t
run (Hole x) = g x
run (Place p) = return p
cataM :: forall m f a. (HDitraversable f m a, Monad m)
=> AlgM m f a -> NatM m (Term f) a
cataM algm = run . coerceCxt
where run :: NatM m (Trm f a) a
run (Term t) = algm =<< hdimapM run t
run (Place x) = return x
type AlgM' m f a = NatM m (f a (Compose m a)) a
freeM' :: forall m h f a b. (HDifunctor f, Monad m)
=> AlgM' m f a -> NatM m b a -> NatM m (Cxt h f a b) a
freeM' f g = run
where run :: NatM m (Cxt h f a b) a
run (Term t) = f $ hfmap (Compose . run) t
run (Hole x) = g x
run (Place p) = return p
cataM' :: forall m f a. (HDifunctor f, Monad m)
=> AlgM' m f a -> NatM m (Term f) a
cataM' algm = run . coerceCxt
where run :: NatM m (Trm f a) a
run (Term t) = algm $ hfmap (Compose . run) t
run (Place x) = return x
type SigFun f g = forall a b. f a b :-> g a b
type CxtFun f g = forall h. SigFun (Cxt h f) (Cxt h g)
type TermHom f g = SigFun f (Context g)
appTermHom :: forall f g. (HDifunctor f, HDifunctor g)
=> TermHom f g -> CxtFun f g
appTermHom f = run where
run :: CxtFun f g
run (Term t) = appCxt (f (hfmap run t))
run (Hole x) = Hole x
run (Place p) = Place p
appTermHom' :: forall f g. (HDifunctor g)
=> TermHom f g -> CxtFun f g
appTermHom' f = run where
run :: CxtFun f g
run (Term t) = appCxt (hfmapCxt run (f t))
run (Hole x) = Hole x
run (Place p) = Place p
compTermHom :: (HDifunctor g, HDifunctor h)
=> TermHom g h -> TermHom f g -> TermHom f h
compTermHom f g = appTermHom f . g
compAlg :: (HDifunctor f, HDifunctor g) => Alg g a -> TermHom f g -> Alg f a
compAlg alg talg = cata' alg . talg
appSigFun :: forall f g. (HDifunctor f) => SigFun f g -> CxtFun f g
appSigFun f = run where
run :: CxtFun f g
run (Term t) = Term (f (hfmap run t))
run (Hole x) = Hole x
run (Place p) = Place p
appSigFun' :: forall f g. (HDifunctor g) => SigFun f g -> CxtFun f g
appSigFun' f = run where
run :: CxtFun f g
run (Term t) = Term (hfmap run (f t))
run (Hole x) = Hole x
run (Place p) = Place p
compSigFun :: SigFun g h -> SigFun f g -> SigFun f h
compSigFun f g = f . g
termHom :: HDifunctor g => SigFun f g -> TermHom f g
termHom f = simpCxt . f
type SigFunM m f g = forall a b. NatM m (f a b) (g a b)
type CxtFunM m f g = forall h . SigFunM m (Cxt h f) (Cxt h g)
type CxtFunM' m f g = forall h b . NatM m (Cxt h f Any b) (Cxt h g Any b)
coerceCxtFunM :: CxtFunM' m f g -> CxtFunM m f g
coerceCxtFunM = unsafeCoerce
type TermHomM m f g = SigFunM m f (Cxt Hole g)
sigFunM :: Monad m => SigFun f g -> SigFunM m f g
sigFunM f = return . f
termHom' :: (HDifunctor f, HDifunctor g, Monad m)
=> SigFunM m f g -> TermHomM m f g
termHom' f = liftM (Term . hfmap Hole) . f
termHomM :: (HDifunctor g, Monad m) => SigFun f g -> TermHomM m f g
termHomM f = sigFunM $ termHom f
appTermHomM :: forall f g m. (HDitraversable f m Any, HDifunctor g, Monad m)
=> TermHomM m f g -> CxtFunM m f g
appTermHomM f = coerceCxtFunM run
where run :: CxtFunM' m f g
run (Term t) = liftM appCxt (f =<< hdimapM run t)
run (Hole x) = return (Hole x)
run (Place p) = return (Place p)
appTermHomM' :: forall f g m. (HDitraversable g m Any, Monad m)
=> TermHomM m f g -> CxtFunM m f g
appTermHomM' f = coerceCxtFunM run
where run :: CxtFunM' m f g
run (Term t) = liftM appCxt (hdimapMCxt run =<< f t)
run (Hole x) = return (Hole x)
run (Place p) = return (Place p)
appSigFunM :: forall m f g. (HDitraversable f m Any, Monad m)
=> SigFunM m f g -> CxtFunM m f g
appSigFunM f = coerceCxtFunM run
where run :: CxtFunM' m f g
run (Term t) = liftM Term (f =<< hdimapM run t)
run (Hole x) = return (Hole x)
run (Place p) = return (Place p)
appSigFunM' :: forall m f g. (HDitraversable g m Any, Monad m)
=> SigFunM m f g -> CxtFunM m f g
appSigFunM' f = coerceCxtFunM run
where run :: CxtFunM' m f g
run (Term t) = liftM Term (hdimapM run =<< f t)
run (Hole x) = return (Hole x)
run (Place p) = return (Place p)
compTermHomM :: (HDitraversable g m Any, HDifunctor h, Monad m)
=> TermHomM m g h -> TermHomM m f g -> TermHomM m f h
compTermHomM f g = appTermHomM f <=< g
compAlgM :: (HDitraversable g m a, Monad m)
=> AlgM m g a -> TermHomM m f g -> AlgM m f a
compAlgM alg talg = freeM alg return <=< talg
compAlgM' :: (HDitraversable g m a, Monad m) => AlgM m g a
-> TermHom f g -> AlgM m f a
compAlgM' alg talg = freeM alg return . talg
compSigFunM :: Monad m => SigFunM m g h -> SigFunM m f g -> SigFunM m f h
compSigFunM f g a = g a >>= f
#ifndef NO_RULES
#endif