{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
module Data.Comp.Algebra (
Alg,
free,
cata,
cata',
appCxt,
AlgM,
algM,
freeM,
cataM,
cataM',
CxtFun,
SigFun,
Hom,
appHom,
appHom',
compHom,
appSigFun,
appSigFun',
compSigFun,
compSigFunHom,
compHomSigFun,
compAlgSigFun,
hom,
compAlg,
compCoalg,
compCVCoalg,
CxtFunM,
SigFunM,
HomM,
SigFunMD,
HomMD,
sigFunM,
hom',
appHomM,
appHomM',
homM,
homMD,
appSigFunM,
appSigFunM',
appSigFunMD,
compHomM,
compSigFunM,
compSigFunHomM,
compHomSigFunM,
compAlgSigFunM,
compAlgM,
compAlgM',
Coalg,
ana,
ana',
CoalgM,
anaM,
RAlg,
para,
RAlgM,
paraM,
RCoalg,
apo,
RCoalgM,
apoM,
CVAlg,
histo,
CVAlgM,
histoM,
CVCoalg,
futu,
CVCoalg',
futu',
CVCoalgM,
futuM
) where
import Control.Monad hiding (mapM, sequence)
import Data.Comp.Ops
import Data.Comp.Term
import Data.Traversable
import Prelude hiding (mapM, sequence)
type Alg f a = f a -> a
free :: forall f h a b . (Functor f) => Alg f b -> (a -> b) -> Cxt h f a -> b
free :: forall (f :: * -> *) h a b.
Functor f =>
Alg f b -> (a -> b) -> Cxt h f a -> b
free Alg f b
f a -> b
g = Cxt h f a -> b
run
where run :: Cxt h f a -> b
run :: Cxt h f a -> b
run (Hole a
x) = a -> b
g a
x
run (Term f (Cxt h f a)
t) = Alg f b
f (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Cxt h f a -> b
run f (Cxt h f a)
t)
cata :: forall f a . (Functor f) => Alg f a -> Term f -> a
{-# NOINLINE [1] cata #-}
cata :: forall (f :: * -> *) a. Functor f => Alg f a -> Term f -> a
cata Alg f a
f = Term f -> a
run
where run :: Term f -> a
run :: Term f -> a
run = Alg f a
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term f -> a
run forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. Cxt NoHole f a -> f (Cxt NoHole f a)
unTerm
cata' :: (Functor f) => Alg f a -> Cxt h f a -> a
{-# INLINE cata' #-}
cata' :: forall (f :: * -> *) a h. Functor f => Alg f a -> Cxt h f a -> a
cata' Alg f a
f = forall (f :: * -> *) h a b.
Functor f =>
Alg f b -> (a -> b) -> Cxt h f a -> b
free Alg f a
f forall a. a -> a
id
appCxt :: (Functor f) => Context f (Cxt h f a) -> Cxt h f a
appCxt :: forall (f :: * -> *) h a.
Functor f =>
Context f (Cxt h f a) -> Cxt h f a
appCxt (Hole Cxt h f a
x) = Cxt h f a
x
appCxt (Term f (Cxt Hole f (Cxt h f a))
t) = forall (b :: * -> *) a c. b (Cxt a b c) -> Cxt a b c
Term (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (f :: * -> *) h a.
Functor f =>
Context f (Cxt h f a) -> Cxt h f a
appCxt f (Cxt Hole f (Cxt h f a))
t)
type AlgM m f a = f a -> m a
algM :: (Traversable f, Monad m) => AlgM m f a -> Alg f (m a)
algM :: forall (f :: * -> *) (m :: * -> *) a.
(Traversable f, Monad m) =>
AlgM m f a -> Alg f (m a)
algM AlgM m f a
f f (m a)
x = forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence f (m a)
x forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= AlgM m f a
f
freeM :: forall h f a m b. (Traversable f, Monad m) =>
AlgM m f b -> (a -> m b) -> Cxt h f a -> m b
freeM :: forall h (f :: * -> *) a (m :: * -> *) b.
(Traversable f, Monad m) =>
AlgM m f b -> (a -> m b) -> Cxt h f a -> m b
freeM AlgM m f b
algm a -> m b
var = Cxt h f a -> m b
run
where run :: Cxt h f a -> m b
run :: Cxt h f a -> m b
run (Hole a
x) = a -> m b
var a
x
run (Term f (Cxt h f a)
t) = AlgM m f b
algm forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Cxt h f a -> m b
run f (Cxt h f a)
t
cataM :: forall f m a. (Traversable f, Monad m) => AlgM m f a -> Term f -> m a
{-# NOINLINE [1] cataM #-}
cataM :: forall (f :: * -> *) (m :: * -> *) a.
(Traversable f, Monad m) =>
AlgM m f a -> Term f -> m a
cataM AlgM m f a
algm = Term f -> m a
run
where run :: Term f -> m a
run :: Term f -> m a
run = AlgM m f a
algm forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Term f -> m a
run forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. Cxt NoHole f a -> f (Cxt NoHole f a)
unTerm
cataM' :: forall h f a m . (Traversable f, Monad m)
=> AlgM m f a -> Cxt h f a -> m a
{-# NOINLINE [1] cataM' #-}
cataM' :: forall h (f :: * -> *) a (m :: * -> *).
(Traversable f, Monad m) =>
AlgM m f a -> Cxt h f a -> m a
cataM' AlgM m f a
f = Cxt h f a -> m a
run
where run :: Cxt h f a -> m a
run :: Cxt h f a -> m a
run (Hole a
x) = forall (m :: * -> *) a. Monad m => a -> m a
return a
x
run (Term f (Cxt h f a)
t) = AlgM m f a
f forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Cxt h f a -> m a
run f (Cxt h f a)
t
type CxtFun f g = forall a h. Cxt h f a -> Cxt h g a
type SigFun f g = forall a. f a -> g a
type Hom f g = SigFun f (Context g)
appHom :: forall f g . (Functor f, Functor g) => Hom f g -> CxtFun f g
{-# NOINLINE [1] appHom #-}
appHom :: forall (f :: * -> *) (g :: * -> *).
(Functor f, Functor g) =>
Hom f g -> CxtFun f g
appHom Hom f g
f = CxtFun f g
run where
run :: CxtFun f g
run :: CxtFun f g
run (Hole a
x) = forall c (b :: * -> *). c -> Cxt Hole b c
Hole a
x
run (Term f (Cxt h f a)
t) = forall (f :: * -> *) h a.
Functor f =>
Context f (Cxt h f a) -> Cxt h f a
appCxt (Hom f g
f (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CxtFun f g
run f (Cxt h f a)
t))
appHom' :: forall f g . (Functor g) => Hom f g -> CxtFun f g
{-# NOINLINE [1] appHom' #-}
appHom' :: forall (f :: * -> *) (g :: * -> *).
Functor g =>
Hom f g -> CxtFun f g
appHom' Hom f g
f = CxtFun f g
run where
run :: CxtFun f g
run :: CxtFun f g
run (Hole a
x) = forall c (b :: * -> *). c -> Cxt Hole b c
Hole a
x
run (Term f (Cxt h f a)
t) = forall (f :: * -> *) h a.
Functor f =>
Context f (Cxt h f a) -> Cxt h f a
appCxt (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CxtFun f g
run (Hom f g
f f (Cxt h f a)
t))
compHom :: (Functor g, Functor h) => Hom g h -> Hom f g -> Hom f h
compHom :: forall (g :: * -> *) (h :: * -> *) (f :: * -> *).
(Functor g, Functor h) =>
Hom g h -> Hom f g -> Hom f h
compHom Hom g h
f Hom f g
g = forall (f :: * -> *) (g :: * -> *).
(Functor f, Functor g) =>
Hom f g -> CxtFun f g
appHom Hom g h
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. Hom f g
g
compAlg :: (Functor g) => Alg g a -> Hom f g -> Alg f a
compAlg :: forall (g :: * -> *) a (f :: * -> *).
Functor g =>
Alg g a -> Hom f g -> Alg f a
compAlg Alg g a
alg Hom f g
talg = forall (f :: * -> *) a h. Functor f => Alg f a -> Cxt h f a -> a
cata' Alg g a
alg forall b c a. (b -> c) -> (a -> b) -> a -> c
. Hom f g
talg
compCoalg :: Hom f g -> Coalg f a -> CVCoalg' g a
compCoalg :: forall (f :: * -> *) (g :: * -> *) a.
Hom f g -> Coalg f a -> CVCoalg' g a
compCoalg Hom f g
hom Coalg f a
coa = Hom f g
hom forall b c a. (b -> c) -> (a -> b) -> a -> c
. Coalg f a
coa
compCVCoalg :: (Functor f, Functor g)
=> Hom f g -> CVCoalg' f a -> CVCoalg' g a
compCVCoalg :: forall (f :: * -> *) (g :: * -> *) a.
(Functor f, Functor g) =>
Hom f g -> CVCoalg' f a -> CVCoalg' g a
compCVCoalg Hom f g
hom CVCoalg' f a
coa = forall (f :: * -> *) (g :: * -> *).
(Functor f, Functor g) =>
Hom f g -> CxtFun f g
appHom Hom f g
hom forall b c a. (b -> c) -> (a -> b) -> a -> c
. CVCoalg' f a
coa
appSigFun :: (Functor f) => SigFun f g -> CxtFun f g
{-# NOINLINE [1] appSigFun #-}
appSigFun :: forall (f :: * -> *) (g :: * -> *).
Functor f =>
SigFun f g -> CxtFun f g
appSigFun SigFun f g
f = Cxt h f a -> Cxt h g a
run
where run :: Cxt h f a -> Cxt h g a
run (Term f (Cxt h f a)
t) = forall (b :: * -> *) a c. b (Cxt a b c) -> Cxt a b c
Term forall a b. (a -> b) -> a -> b
$ SigFun f g
f forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Cxt h f a -> Cxt h g a
run f (Cxt h f a)
t
run (Hole a
x) = forall c (b :: * -> *). c -> Cxt Hole b c
Hole a
x
appSigFun' :: (Functor g) => SigFun f g -> CxtFun f g
{-# NOINLINE [1] appSigFun' #-}
appSigFun' :: forall (g :: * -> *) (f :: * -> *).
Functor g =>
SigFun f g -> CxtFun f g
appSigFun' SigFun f g
f = Cxt h f a -> Cxt h g a
run
where run :: Cxt h f a -> Cxt h g a
run (Term f (Cxt h f a)
t) = forall (b :: * -> *) a c. b (Cxt a b c) -> Cxt a b c
Term forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Cxt h f a -> Cxt h g a
run forall a b. (a -> b) -> a -> b
$ SigFun f g
f f (Cxt h f a)
t
run (Hole a
x) = forall c (b :: * -> *). c -> Cxt Hole b c
Hole a
x
compSigFun :: SigFun g h -> SigFun f g -> SigFun f h
compSigFun :: forall (g :: * -> *) (h :: * -> *) (f :: * -> *).
SigFun g h -> SigFun f g -> SigFun f h
compSigFun SigFun g h
f SigFun f g
g = SigFun g h
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. SigFun f g
g
compSigFunHom :: (Functor g) => SigFun g h -> Hom f g -> Hom f h
compSigFunHom :: forall (g :: * -> *) (h :: * -> *) (f :: * -> *).
Functor g =>
SigFun g h -> Hom f g -> Hom f h
compSigFunHom SigFun g h
f Hom f g
g = forall (f :: * -> *) (g :: * -> *).
Functor f =>
SigFun f g -> CxtFun f g
appSigFun SigFun g h
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. Hom f g
g
compHomSigFun :: Hom g h -> SigFun f g -> Hom f h
compHomSigFun :: forall (g :: * -> *) (h :: * -> *) (f :: * -> *).
Hom g h -> SigFun f g -> Hom f h
compHomSigFun Hom g h
f SigFun f g
g = Hom g h
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. SigFun f g
g
compAlgSigFun :: Alg g a -> SigFun f g -> Alg f a
compAlgSigFun :: forall (g :: * -> *) a (f :: * -> *).
Alg g a -> SigFun f g -> Alg f a
compAlgSigFun Alg g a
f SigFun f g
g = Alg g a
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. SigFun f g
g
hom :: (Functor g) => SigFun f g -> Hom f g
hom :: forall (g :: * -> *) (f :: * -> *).
Functor g =>
SigFun f g -> Hom f g
hom SigFun f g
f = forall (f :: * -> *) a. Functor f => f a -> Context f a
simpCxt forall b c a. (b -> c) -> (a -> b) -> a -> c
. SigFun f g
f
type CxtFunM m f g = forall a h. Cxt h f a -> m (Cxt h g a)
type SigFunM m f g = forall a. f a -> m (g a)
type SigFunMD m f g = forall a. f (m a) -> m (g a)
type HomM m f g = SigFunM m f (Context g)
type HomMD m f g = SigFunMD m f (Context g)
sigFunM :: (Monad m) => SigFun f g -> SigFunM m f g
sigFunM :: forall (m :: * -> *) (f :: * -> *) (g :: * -> *).
Monad m =>
SigFun f g -> SigFunM m f g
sigFunM SigFun f g
f = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. SigFun f g
f
hom' :: (Functor f, Functor g, Monad m) => SigFunM m f g -> HomM m f g
hom' :: forall (f :: * -> *) (g :: * -> *) (m :: * -> *).
(Functor f, Functor g, Monad m) =>
SigFunM m f g -> HomM m f g
hom' SigFunM m f g
f = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (forall (b :: * -> *) a c. b (Cxt a b c) -> Cxt a b c
Term forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall c (b :: * -> *). c -> Cxt Hole b c
Hole) forall b c a. (b -> c) -> (a -> b) -> a -> c
. SigFunM m f g
f
homM :: (Functor g, Monad m) => SigFunM m f g -> HomM m f g
homM :: forall (g :: * -> *) (m :: * -> *) (f :: * -> *).
(Functor g, Monad m) =>
SigFunM m f g -> HomM m f g
homM SigFunM m f g
f = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall (f :: * -> *) a. Functor f => f a -> Context f a
simpCxt forall b c a. (b -> c) -> (a -> b) -> a -> c
. SigFunM m f g
f
appHomM :: forall f g m . (Traversable f, Functor g, Monad m)
=> HomM m f g -> CxtFunM m f g
{-# NOINLINE [1] appHomM #-}
appHomM :: forall (f :: * -> *) (g :: * -> *) (m :: * -> *).
(Traversable f, Functor g, Monad m) =>
HomM m f g -> CxtFunM m f g
appHomM HomM m f g
f = forall h a. Cxt h f a -> m (Cxt h g a)
run
where run :: Cxt h f a -> m (Cxt h g a)
run :: forall h a. Cxt h f a -> m (Cxt h g a)
run (Hole a
x) = forall (m :: * -> *) a. Monad m => a -> m a
return (forall c (b :: * -> *). c -> Cxt Hole b c
Hole a
x)
run (Term f (Cxt h f a)
t) = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall (f :: * -> *) h a.
Functor f =>
Context f (Cxt h f a) -> Cxt h f a
appCxt forall b c a. (b -> c) -> (a -> b) -> a -> c
. HomM m f g
f forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall h a. Cxt h f a -> m (Cxt h g a)
run f (Cxt h f a)
t
appHomM' :: forall f g m . (Traversable g, Monad m)
=> HomM m f g -> CxtFunM m f g
{-# NOINLINE [1] appHomM' #-}
appHomM' :: forall (f :: * -> *) (g :: * -> *) (m :: * -> *).
(Traversable g, Monad m) =>
HomM m f g -> CxtFunM m f g
appHomM' HomM m f g
f = forall h a. Cxt h f a -> m (Cxt h g a)
run
where run :: Cxt h f a -> m (Cxt h g a)
run :: forall h a. Cxt h f a -> m (Cxt h g a)
run (Hole a
x) = forall (m :: * -> *) a. Monad m => a -> m a
return (forall c (b :: * -> *). c -> Cxt Hole b c
Hole a
x)
run (Term f (Cxt h f a)
t) = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall (f :: * -> *) h a.
Functor f =>
Context f (Cxt h f a) -> Cxt h f a
appCxt forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall h a. Cxt h f a -> m (Cxt h g a)
run forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< HomM m f g
f f (Cxt h f a)
t
homMD :: forall f g m . (Traversable f, Functor g, Monad m)
=> HomMD m f g -> CxtFunM m f g
homMD :: forall (f :: * -> *) (g :: * -> *) (m :: * -> *).
(Traversable f, Functor g, Monad m) =>
HomMD m f g -> CxtFunM m f g
homMD HomMD m f g
f = forall h a. Cxt h f a -> m (Cxt h g a)
run
where run :: Cxt h f a -> m (Cxt h g a)
run :: forall h a. Cxt h f a -> m (Cxt h g a)
run (Hole a
x) = forall (m :: * -> *) a. Monad m => a -> m a
return (forall c (b :: * -> *). c -> Cxt Hole b c
Hole a
x)
run (Term f (Cxt h f a)
t) = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall (f :: * -> *) h a.
Functor f =>
Context f (Cxt h f a) -> Cxt h f a
appCxt (HomMD m f g
f (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall h a. Cxt h f a -> m (Cxt h g a)
run f (Cxt h f a)
t))
appSigFunM :: (Traversable f, Monad m) => SigFunM m f g -> CxtFunM m f g
{-# NOINLINE [1] appSigFunM #-}
appSigFunM :: forall (f :: * -> *) (m :: * -> *) (g :: * -> *).
(Traversable f, Monad m) =>
SigFunM m f g -> CxtFunM m f g
appSigFunM SigFunM m f g
f = Cxt h f a -> m (Cxt h g a)
run
where run :: Cxt h f a -> m (Cxt h g a)
run (Term f (Cxt h f a)
t) = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall (b :: * -> *) a c. b (Cxt a b c) -> Cxt a b c
Term forall b c a. (b -> c) -> (a -> b) -> a -> c
. SigFunM m f g
f forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Cxt h f a -> m (Cxt h g a)
run f (Cxt h f a)
t
run (Hole a
x) = forall (m :: * -> *) a. Monad m => a -> m a
return (forall c (b :: * -> *). c -> Cxt Hole b c
Hole a
x)
appSigFunM' :: (Traversable g, Monad m) => SigFunM m f g -> CxtFunM m f g
{-# NOINLINE [1] appSigFunM' #-}
appSigFunM' :: forall (g :: * -> *) (m :: * -> *) (f :: * -> *).
(Traversable g, Monad m) =>
SigFunM m f g -> CxtFunM m f g
appSigFunM' SigFunM m f g
f = Cxt h f a -> m (Cxt h g a)
run
where run :: Cxt h f a -> m (Cxt h g a)
run (Term f (Cxt h f a)
t) = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall (b :: * -> *) a c. b (Cxt a b c) -> Cxt a b c
Term forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Cxt h f a -> m (Cxt h g a)
run forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SigFunM m f g
f f (Cxt h f a)
t
run (Hole a
x) = forall (m :: * -> *) a. Monad m => a -> m a
return (forall c (b :: * -> *). c -> Cxt Hole b c
Hole a
x)
appSigFunMD :: forall f g m . (Traversable f, Functor g, Monad m)
=> SigFunMD m f g -> CxtFunM m f g
appSigFunMD :: forall (f :: * -> *) (g :: * -> *) (m :: * -> *).
(Traversable f, Functor g, Monad m) =>
SigFunMD m f g -> CxtFunM m f g
appSigFunMD SigFunMD m f g
f = forall h a. Cxt h f a -> m (Cxt h g a)
run
where run :: Cxt h f a -> m (Cxt h g a)
run :: forall h a. Cxt h f a -> m (Cxt h g a)
run (Hole a
x) = forall (m :: * -> *) a. Monad m => a -> m a
return (forall c (b :: * -> *). c -> Cxt Hole b c
Hole a
x)
run (Term f (Cxt h f a)
t) = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall (b :: * -> *) a c. b (Cxt a b c) -> Cxt a b c
Term (SigFunMD m f g
f (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall h a. Cxt h f a -> m (Cxt h g a)
run f (Cxt h f a)
t))
compHomM :: (Traversable g, Functor h, Monad m)
=> HomM m g h -> HomM m f g -> HomM m f h
compHomM :: forall (g :: * -> *) (h :: * -> *) (m :: * -> *) (f :: * -> *).
(Traversable g, Functor h, Monad m) =>
HomM m g h -> HomM m f g -> HomM m f h
compHomM HomM m g h
f HomM m f g
g = forall (f :: * -> *) (g :: * -> *) (m :: * -> *).
(Traversable f, Functor g, Monad m) =>
HomM m f g -> CxtFunM m f g
appHomM HomM m g h
f forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< HomM m f g
g
compHomM' :: (Traversable h, Monad m)
=> HomM m g h -> HomM m f g -> HomM m f h
compHomM' :: forall (h :: * -> *) (m :: * -> *) (g :: * -> *) (f :: * -> *).
(Traversable h, Monad m) =>
HomM m g h -> HomM m f g -> HomM m f h
compHomM' HomM m g h
f HomM m f g
g = forall (f :: * -> *) (g :: * -> *) (m :: * -> *).
(Traversable g, Monad m) =>
HomM m f g -> CxtFunM m f g
appHomM' HomM m g h
f forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< HomM m f g
g
compAlgM :: (Traversable g, Monad m) => AlgM m g a -> HomM m f g -> AlgM m f a
compAlgM :: forall (g :: * -> *) (m :: * -> *) a (f :: * -> *).
(Traversable g, Monad m) =>
AlgM m g a -> HomM m f g -> AlgM m f a
compAlgM AlgM m g a
alg HomM m f g
talg = forall h (f :: * -> *) a (m :: * -> *).
(Traversable f, Monad m) =>
AlgM m f a -> Cxt h f a -> m a
cataM' AlgM m g a
alg forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< HomM m f g
talg
compAlgM' :: (Traversable g, Monad m) => AlgM m g a -> Hom f g -> AlgM m f a
compAlgM' :: forall (g :: * -> *) (m :: * -> *) a (f :: * -> *).
(Traversable g, Monad m) =>
AlgM m g a -> Hom f g -> AlgM m f a
compAlgM' AlgM m g a
alg Hom f g
talg = forall h (f :: * -> *) a (m :: * -> *).
(Traversable f, Monad m) =>
AlgM m f a -> Cxt h f a -> m a
cataM' AlgM m g a
alg forall b c a. (b -> c) -> (a -> b) -> a -> c
. Hom f g
talg
compSigFunM :: (Monad m) => SigFunM m g h -> SigFunM m f g -> SigFunM m f h
compSigFunM :: forall (m :: * -> *) (g :: * -> *) (h :: * -> *) (f :: * -> *).
Monad m =>
SigFunM m g h -> SigFunM m f g -> SigFunM m f h
compSigFunM SigFunM m g h
f SigFunM m f g
g = SigFunM m g h
f forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< SigFunM m f g
g
compSigFunHomM :: (Traversable g, Functor h, Monad m)
=> SigFunM m g h -> HomM m f g -> HomM m f h
compSigFunHomM :: forall (g :: * -> *) (h :: * -> *) (m :: * -> *) (f :: * -> *).
(Traversable g, Functor h, Monad m) =>
SigFunM m g h -> HomM m f g -> HomM m f h
compSigFunHomM SigFunM m g h
f HomM m f g
g = forall (f :: * -> *) (m :: * -> *) (g :: * -> *).
(Traversable f, Monad m) =>
SigFunM m f g -> CxtFunM m f g
appSigFunM SigFunM m g h
f forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< HomM m f g
g
compSigFunHomM' :: (Traversable h, Monad m)
=> SigFunM m g h -> HomM m f g -> HomM m f h
compSigFunHomM' :: forall (h :: * -> *) (m :: * -> *) (g :: * -> *) (f :: * -> *).
(Traversable h, Monad m) =>
SigFunM m g h -> HomM m f g -> HomM m f h
compSigFunHomM' SigFunM m g h
f HomM m f g
g = forall (g :: * -> *) (m :: * -> *) (f :: * -> *).
(Traversable g, Monad m) =>
SigFunM m f g -> CxtFunM m f g
appSigFunM' SigFunM m g h
f forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< HomM m f g
g
compHomSigFunM :: (Monad m) => HomM m g h -> SigFunM m f g -> HomM m f h
compHomSigFunM :: forall (m :: * -> *) (g :: * -> *) (h :: * -> *) (f :: * -> *).
Monad m =>
HomM m g h -> SigFunM m f g -> HomM m f h
compHomSigFunM HomM m g h
f SigFunM m f g
g = HomM m g h
f forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< SigFunM m f g
g
compAlgSigFunM :: (Monad m) => AlgM m g a -> SigFunM m f g -> AlgM m f a
compAlgSigFunM :: forall (m :: * -> *) (g :: * -> *) a (f :: * -> *).
Monad m =>
AlgM m g a -> SigFunM m f g -> AlgM m f a
compAlgSigFunM AlgM m g a
f SigFunM m f g
g = AlgM m g a
f forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< SigFunM m f g
g
type Coalg f a = a -> f a
ana :: forall a f . Functor f => Coalg f a -> a -> Term f
ana :: forall a (f :: * -> *). Functor f => Coalg f a -> a -> Term f
ana Coalg f a
f = a -> Term f
run
where run :: a -> Term f
run :: a -> Term f
run a
t = forall (b :: * -> *) a c. b (Cxt a b c) -> Cxt a b c
Term forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Term f
run (Coalg f a
f a
t)
ana' :: forall a f . Functor f => Coalg f a -> a -> Term f
ana' :: forall a (f :: * -> *). Functor f => Coalg f a -> a -> Term f
ana' Coalg f a
f a
t = forall (f :: * -> *). (forall a. Alg f a -> a) -> Term f
build (forall b. a -> Alg f b -> b
run a
t)
where run :: forall b . a -> Alg f b -> b
run :: forall b. a -> Alg f b -> b
run a
t Alg f b
con = a -> b
run' a
t where
run' :: a -> b
run' :: a -> b
run' a
t = Alg f b
con forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
run' (Coalg f a
f a
t)
{-# INLINE [2] ana' #-}
build :: (forall a. Alg f a -> a) -> Term f
{-# INLINE [1] build #-}
build :: forall (f :: * -> *). (forall a. Alg f a -> a) -> Term f
build forall a. Alg f a -> a
g = forall a. Alg f a -> a
g forall (b :: * -> *) a c. b (Cxt a b c) -> Cxt a b c
Term
type CoalgM m f a = a -> m (f a)
anaM :: forall a m f. (Traversable f, Monad m)
=> CoalgM m f a -> a -> m (Term f)
anaM :: forall a (m :: * -> *) (f :: * -> *).
(Traversable f, Monad m) =>
CoalgM m f a -> a -> m (Term f)
anaM CoalgM m f a
f = a -> m (Term f)
run
where run :: a -> m (Term f)
run :: a -> m (Term f)
run a
t = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall (b :: * -> *) a c. b (Cxt a b c) -> Cxt a b c
Term forall a b. (a -> b) -> a -> b
$ CoalgM m f a
f a
t forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM a -> m (Term f)
run
type RAlg f a = f (Term f, a) -> a
para :: (Functor f) => RAlg f a -> Term f -> a
para :: forall (f :: * -> *) a. Functor f => RAlg f a -> Term f -> a
para RAlg f a
f = forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. Functor f => Alg f a -> Term f -> a
cata f (Term f, a) -> (Term f, a)
run
where run :: f (Term f, a) -> (Term f, a)
run f (Term f, a)
t = (forall (b :: * -> *) a c. b (Cxt a b c) -> Cxt a b c
Term forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst f (Term f, a)
t, RAlg f a
f f (Term f, a)
t)
type RAlgM m f a = f (Term f, a) -> m a
paraM :: (Traversable f, Monad m) =>
RAlgM m f a -> Term f -> m a
paraM :: forall (f :: * -> *) (m :: * -> *) a.
(Traversable f, Monad m) =>
RAlgM m f a -> Term f -> m a
paraM RAlgM m f a
f = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) (m :: * -> *) a.
(Traversable f, Monad m) =>
AlgM m f a -> Term f -> m a
cataM f (Term f, a) -> m (Term f, a)
run
where run :: f (Term f, a) -> m (Term f, a)
run f (Term f, a)
t = do
a
a <- RAlgM m f a
f f (Term f, a)
t
forall (m :: * -> *) a. Monad m => a -> m a
return (forall (b :: * -> *) a c. b (Cxt a b c) -> Cxt a b c
Term forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst f (Term f, a)
t, a
a)
type RCoalg f a = a -> f (Either (Term f) a)
apo :: (Functor f) => RCoalg f a -> a -> Term f
apo :: forall (f :: * -> *) a. Functor f => RCoalg f a -> a -> Term f
apo RCoalg f a
f = a -> Cxt NoHole f ()
run
where run :: a -> Cxt NoHole f ()
run = forall (b :: * -> *) a c. b (Cxt a b c) -> Cxt a b c
Term forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Either (Cxt NoHole f ()) a -> Cxt NoHole f ()
run' forall b c a. (b -> c) -> (a -> b) -> a -> c
. RCoalg f a
f
run' :: Either (Cxt NoHole f ()) a -> Cxt NoHole f ()
run' (Left Cxt NoHole f ()
t) = Cxt NoHole f ()
t
run' (Right a
a) = a -> Cxt NoHole f ()
run a
a
type RCoalgM m f a = a -> m (f (Either (Term f) a))
apoM :: (Traversable f, Monad m) =>
RCoalgM m f a -> a -> m (Term f)
apoM :: forall (f :: * -> *) (m :: * -> *) a.
(Traversable f, Monad m) =>
RCoalgM m f a -> a -> m (Term f)
apoM RCoalgM m f a
f = a -> m (Cxt NoHole f ())
run
where run :: a -> m (Cxt NoHole f ())
run a
a = do
f (Either (Cxt NoHole f ()) a)
t <- RCoalgM m f a
f a
a
f (Cxt NoHole f ())
t' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Either (Cxt NoHole f ()) a -> m (Cxt NoHole f ())
run' f (Either (Cxt NoHole f ()) a)
t
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (b :: * -> *) a c. b (Cxt a b c) -> Cxt a b c
Term f (Cxt NoHole f ())
t'
run' :: Either (Cxt NoHole f ()) a -> m (Cxt NoHole f ())
run' (Left Cxt NoHole f ()
t) = forall (m :: * -> *) a. Monad m => a -> m a
return Cxt NoHole f ()
t
run' (Right a
a) = a -> m (Cxt NoHole f ())
run a
a
type CVAlg f a f' = f (Term f') -> a
projectTip :: (DistAnn f a f') => Term f' -> (f (Term f'), a)
projectTip :: forall (f :: * -> *) a (f' :: * -> *).
DistAnn f a f' =>
Term f' -> (f (Term f'), a)
projectTip (Term f' (Cxt NoHole f' ())
v) = forall {k} (s :: k -> *) p (s' :: k -> *) (a :: k).
DistAnn s p s' =>
s' a -> (s a, p)
projectA f' (Cxt NoHole f' ())
v
histo :: (Functor f,DistAnn f a f') => CVAlg f a f' -> Term f -> a
histo :: forall (f :: * -> *) a (f' :: * -> *).
(Functor f, DistAnn f a f') =>
CVAlg f a f' -> Term f -> a
histo CVAlg f a f'
alg = forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a (f' :: * -> *).
DistAnn f a f' =>
Term f' -> (f (Term f'), a)
projectTip forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. Functor f => Alg f a -> Term f -> a
cata f (Term f') -> Term f'
run
where run :: f (Term f') -> Term f'
run f (Term f')
v = forall (b :: * -> *) a c. b (Cxt a b c) -> Cxt a b c
Term forall a b. (a -> b) -> a -> b
$ forall {k} (s :: k -> *) p (s' :: k -> *) (a :: k).
DistAnn s p s' =>
p -> s a -> s' a
injectA (CVAlg f a f'
alg f (Term f')
v) f (Term f')
v
type CVAlgM m f a f' = f (Term f') -> m a
histoM :: (Traversable f, Monad m, DistAnn f a f') =>
CVAlgM m f a f' -> Term f -> m a
histoM :: forall (f :: * -> *) (m :: * -> *) a (f' :: * -> *).
(Traversable f, Monad m, DistAnn f a f') =>
CVAlgM m f a f' -> Term f -> m a
histoM CVAlgM m f a f'
alg = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a (f' :: * -> *).
DistAnn f a f' =>
Term f' -> (f (Term f'), a)
projectTip) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) (m :: * -> *) a.
(Traversable f, Monad m) =>
AlgM m f a -> Term f -> m a
cataM f (Term f') -> m (Term f')
run
where run :: f (Term f') -> m (Term f')
run f (Term f')
v = do a
r <- CVAlgM m f a f'
alg f (Term f')
v
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (b :: * -> *) a c. b (Cxt a b c) -> Cxt a b c
Term forall a b. (a -> b) -> a -> b
$ forall {k} (s :: k -> *) p (s' :: k -> *) (a :: k).
DistAnn s p s' =>
p -> s a -> s' a
injectA a
r f (Term f')
v
type CVCoalg f a = a -> f (Context f a)
futu :: forall f a . Functor f => CVCoalg f a -> a -> Term f
futu :: forall (f :: * -> *) a. Functor f => CVCoalg f a -> a -> Term f
futu CVCoalg f a
coa = forall a (f :: * -> *). Functor f => Coalg f a -> a -> Term f
ana Coalg f (Context f a)
run forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c (b :: * -> *). c -> Cxt Hole b c
Hole
where run :: Coalg f (Context f a)
run :: Coalg f (Context f a)
run (Hole a
x) = CVCoalg f a
coa a
x
run (Term f (Context f a)
t) = f (Context f a)
t
type CVCoalgM m f a = a -> m (f (Context f a))
futuM :: forall f a m . (Traversable f, Monad m) =>
CVCoalgM m f a -> a -> m (Term f)
futuM :: forall (f :: * -> *) a (m :: * -> *).
(Traversable f, Monad m) =>
CVCoalgM m f a -> a -> m (Term f)
futuM CVCoalgM m f a
coa = forall a (m :: * -> *) (f :: * -> *).
(Traversable f, Monad m) =>
CoalgM m f a -> a -> m (Term f)
anaM CoalgM m f (Context f a)
run forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c (b :: * -> *). c -> Cxt Hole b c
Hole
where run :: CoalgM m f (Context f a)
run :: CoalgM m f (Context f a)
run (Hole a
x) = CVCoalgM m f a
coa a
x
run (Term f (Context f a)
t) = forall (m :: * -> *) a. Monad m => a -> m a
return f (Context f a)
t
type CVCoalg' f a = a -> Context f a
futu' :: forall f a . Functor f => CVCoalg' f a -> a -> Term f
futu' :: forall (f :: * -> *) a. Functor f => CVCoalg' f a -> a -> Term f
futu' CVCoalg' f a
coa = a -> Term f
run
where run :: a -> Term f
run :: a -> Term f
run a
x = forall (f :: * -> *) h a.
Functor f =>
Context f (Cxt h f a) -> Cxt h f a
appCxt forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Term f
run (CVCoalg' f a
coa a
x)
appAlgHom :: forall f g d . (Functor g) => Alg g d -> Hom f g -> Term f -> d
{-# NOINLINE [1] appAlgHom #-}
appAlgHom :: forall (f :: * -> *) (g :: * -> *) d.
Functor g =>
Alg g d -> Hom f g -> Term f -> d
appAlgHom Alg g d
alg Hom f g
hom = Term f -> d
run where
run :: Term f -> d
run :: Term f -> d
run (Term f (Term f)
t) = Context g (Term f) -> d
run' forall a b. (a -> b) -> a -> b
$ Hom f g
hom f (Term f)
t
run' :: Context g (Term f) -> d
run' :: Context g (Term f) -> d
run' (Term g (Context g (Term f))
t) = Alg g d
alg forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Context g (Term f) -> d
run' g (Context g (Term f))
t
run' (Hole Term f
x) = Term f -> d
run Term f
x
appSigFunHom :: forall f g h. (Functor g)
=> SigFun g h -> Hom f g -> CxtFun f h
{-# NOINLINE [1] appSigFunHom #-}
appSigFunHom :: forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
Functor g =>
SigFun g h -> Hom f g -> CxtFun f h
appSigFunHom SigFun g h
f Hom f g
g = CxtFun f h
run where
run :: CxtFun f h
run :: CxtFun f h
run (Term f (Cxt h f a)
t) = forall h' b. Context g (Cxt h' f b) -> Cxt h' h b
run' forall a b. (a -> b) -> a -> b
$ Hom f g
g f (Cxt h f a)
t
run (Hole a
h) = forall c (b :: * -> *). c -> Cxt Hole b c
Hole a
h
run' :: Context g (Cxt h' f b) -> Cxt h' h b
run' :: forall h' b. Context g (Cxt h' f b) -> Cxt h' h b
run' (Term g (Cxt Hole g (Cxt h' f b))
t) = forall (b :: * -> *) a c. b (Cxt a b c) -> Cxt a b c
Term forall a b. (a -> b) -> a -> b
$ SigFun g h
f forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall h' b. Context g (Cxt h' f b) -> Cxt h' h b
run' g (Cxt Hole g (Cxt h' f b))
t
run' (Hole Cxt h' f b
h) = CxtFun f h
run Cxt h' f b
h
appAlgHomM :: forall m f g a. (Traversable g, Monad m)
=> AlgM m g a -> HomM m f g -> Term f -> m a
{-# NOINLINE [1] appAlgHomM #-}
appAlgHomM :: forall (m :: * -> *) (f :: * -> *) (g :: * -> *) a.
(Traversable g, Monad m) =>
AlgM m g a -> HomM m f g -> Term f -> m a
appAlgHomM AlgM m g a
alg HomM m f g
hom = Term f -> m a
run
where run :: Term f -> m a
run :: Term f -> m a
run (Term f (Term f)
t) = HomM m f g
hom f (Term f)
t forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Term f -> m a
run forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Cxt Hole g a -> m a
run'
run' :: Context g a -> m a
run' :: Cxt Hole g a -> m a
run' (Term g (Cxt Hole g a)
t) = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Cxt Hole g a -> m a
run' g (Cxt Hole g a)
t forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= AlgM m g a
alg
run' (Hole a
x) = forall (m :: * -> *) a. Monad m => a -> m a
return a
x
appHomHomM :: forall m f g h . (Monad m, Traversable g, Functor h)
=> HomM m g h -> HomM m f g -> CxtFunM m f h
appHomHomM :: forall (m :: * -> *) (f :: * -> *) (g :: * -> *) (h :: * -> *).
(Monad m, Traversable g, Functor h) =>
HomM m g h -> HomM m f g -> CxtFunM m f h
appHomHomM HomM m g h
f HomM m f g
g = CxtFunM m f h
run where
run :: CxtFunM m f h
run :: CxtFunM m f h
run (Term f (Cxt h f a)
t) = forall h' b. Context g (Cxt h' f b) -> m (Cxt h' h b)
run' forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< HomM m f g
g f (Cxt h f a)
t
run (Hole a
h) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall c (b :: * -> *). c -> Cxt Hole b c
Hole a
h
run' :: Context g (Cxt h' f b) -> m (Cxt h' h b)
run' :: forall h' b. Context g (Cxt h' f b) -> m (Cxt h' h b)
run' (Term g (Cxt Hole g (Cxt h' f b))
t) = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall (f :: * -> *) h a.
Functor f =>
Context f (Cxt h f a) -> Cxt h f a
appCxt forall a b. (a -> b) -> a -> b
$ HomM m g h
f forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall h' b. Context g (Cxt h' f b) -> m (Cxt h' h b)
run' g (Cxt Hole g (Cxt h' f b))
t
run' (Hole Cxt h' f b
h) = CxtFunM m f h
run Cxt h' f b
h
appSigFunHomM :: forall m f g h . (Traversable g, Monad m)
=> SigFunM m g h -> HomM m f g -> CxtFunM m f h
appSigFunHomM :: forall (m :: * -> *) (f :: * -> *) (g :: * -> *) (h :: * -> *).
(Traversable g, Monad m) =>
SigFunM m g h -> HomM m f g -> CxtFunM m f h
appSigFunHomM SigFunM m g h
f HomM m f g
g = CxtFunM m f h
run where
run :: CxtFunM m f h
run :: CxtFunM m f h
run (Term f (Cxt h f a)
t) = forall h' b. Context g (Cxt h' f b) -> m (Cxt h' h b)
run' forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< HomM m f g
g f (Cxt h f a)
t
run (Hole a
h) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall c (b :: * -> *). c -> Cxt Hole b c
Hole a
h
run' :: Context g (Cxt h' f b) -> m (Cxt h' h b)
run' :: forall h' b. Context g (Cxt h' f b) -> m (Cxt h' h b)
run' (Term g (Cxt Hole g (Cxt h' f b))
t) = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall (b :: * -> *) a c. b (Cxt a b c) -> Cxt a b c
Term forall a b. (a -> b) -> a -> b
$ SigFunM m g h
f forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall h' b. Context g (Cxt h' f b) -> m (Cxt h' h b)
run' g (Cxt Hole g (Cxt h' f b))
t
run' (Hole Cxt h' f b
h) = CxtFunM m f h
run Cxt h' f b
h
#ifndef NO_RULES
{-# RULES
"cata/appHom" forall (a :: Alg g d) (h :: Hom f g) x.
cata a (appHom h x) = cata (compAlg a h) x;
"cata/appHom'" forall (a :: Alg g d) (h :: Hom f g) x.
cata a (appHom' h x) = appAlgHom a h x;
"cata/appSigFun" forall (a :: Alg g d) (h :: SigFun f g) x.
cata a (appSigFun h x) = cata (compAlgSigFun a h) x;
"cata/appSigFun'" forall (a :: Alg g d) (h :: SigFun f g) x.
cata a (appSigFun' h x) = appAlgHom a (hom h) x;
"cata/appSigFunHom" forall (f :: Alg f3 d) (g :: SigFun f2 f3)
(h :: Hom f1 f2) x.
cata f (appSigFunHom g h x) = appAlgHom (compAlgSigFun f g) h x;
"appAlgHom/appHom" forall (a :: Alg h d) (f :: Hom f g) (h :: Hom g h) x.
appAlgHom a h (appHom f x) = cata (compAlg a (compHom h f)) x;
"appAlgHom/appHom'" forall (a :: Alg h d) (f :: Hom f g) (h :: Hom g h) x.
appAlgHom a h (appHom' f x) = appAlgHom a (compHom h f) x;
"appAlgHom/appSigFun" forall (a :: Alg h d) (f :: SigFun f g) (h :: Hom g h) x.
appAlgHom a h (appSigFun f x) = cata (compAlg a (compHomSigFun h f)) x;
"appAlgHom/appSigFun'" forall (a :: Alg h d) (f :: SigFun f g) (h :: Hom g h) x.
appAlgHom a h (appSigFun' f x) = appAlgHom a (compHomSigFun h f) x;
"appAlgHom/appSigFunHom" forall (a :: Alg i d) (f :: Hom f g) (g :: SigFun g h)
(h :: Hom h i) x.
appAlgHom a h (appSigFunHom g f x)
= appAlgHom a (compHom (compHomSigFun h g) f) x;
"appHom/appHom" forall (a :: Hom g h) (h :: Hom f g) x.
appHom a (appHom h x) = appHom (compHom a h) x;
"appHom'/appHom'" forall (a :: Hom g h) (h :: Hom f g) x.
appHom' a (appHom' h x) = appHom' (compHom a h) x;
"appHom'/appHom" forall (a :: Hom g h) (h :: Hom f g) x.
appHom' a (appHom h x) = appHom (compHom a h) x;
"appHom/appHom'" forall (a :: Hom g h) (h :: Hom f g) x.
appHom a (appHom' h x) = appHom' (compHom a h) x;
"appSigFun/appSigFun" forall (f :: SigFun g h) (g :: SigFun f g) x.
appSigFun f (appSigFun g x) = appSigFun (compSigFun f g) x;
"appSigFun'/appSigFun'" forall (f :: SigFun g h) (g :: SigFun f g) x.
appSigFun' f (appSigFun' g x) = appSigFun' (compSigFun f g) x;
"appSigFun/appSigFun'" forall (f :: SigFun g h) (g :: SigFun f g) x.
appSigFun f (appSigFun' g x) = appSigFunHom f (hom g) x;
"appSigFun'/appSigFun" forall (f :: SigFun g h) (g :: SigFun f g) x.
appSigFun' f (appSigFun g x) = appSigFun (compSigFun f g) x;
"appHom/appSigFun" forall (f :: Hom g h) (g :: SigFun f g) x.
appHom f (appSigFun g x) = appHom (compHomSigFun f g) x;
"appHom/appSigFun'" forall (f :: Hom g h) (g :: SigFun f g) x.
appHom f (appSigFun' g x) = appHom' (compHomSigFun f g) x;
"appHom'/appSigFun'" forall (f :: Hom g h) (g :: SigFun f g) x.
appHom' f (appSigFun' g x) = appHom' (compHomSigFun f g) x;
"appHom'/appSigFun" forall (f :: Hom g h) (g :: SigFun f g) x.
appHom' f (appSigFun g x) = appHom (compHomSigFun f g) x;
"appSigFun/appHom" forall (f :: SigFun g h) (g :: Hom f g) x.
appSigFun f (appHom g x) = appSigFunHom f g x;
"appSigFun'/appHom'" forall (f :: SigFun g h) (g :: Hom f g) x.
appSigFun' f (appHom' g x) = appHom' (compSigFunHom f g) x;
"appSigFun/appHom'" forall (f :: SigFun g h) (g :: Hom f g) x.
appSigFun f (appHom' g x) = appSigFunHom f g x;
"appSigFun'/appHom" forall (f :: SigFun g h) (g :: Hom f g) x.
appSigFun' f (appHom g x) = appHom (compSigFunHom f g) x;
"appSigFunHom/appSigFun" forall (f :: SigFun f3 f4) (g :: Hom f2 f3)
(h :: SigFun f1 f2) x.
appSigFunHom f g (appSigFun h x)
= appSigFunHom f (compHomSigFun g h) x;
"appSigFunHom/appSigFun'" forall (f :: SigFun f3 f4) (g :: Hom f2 f3)
(h :: SigFun f1 f2) x.
appSigFunHom f g (appSigFun' h x)
= appSigFunHom f (compHomSigFun g h) x;
"appSigFunHom/appHom" forall (f :: SigFun f3 f4) (g :: Hom f2 f3)
(h :: Hom f1 f2) x.
appSigFunHom f g (appHom h x)
= appSigFunHom f (compHom g h) x;
"appSigFunHom/appHom'" forall (f :: SigFun f3 f4) (g :: Hom f2 f3)
(h :: Hom f1 f2) x.
appSigFunHom f g (appHom' h x)
= appSigFunHom f (compHom g h) x;
"appSigFun/appSigFunHom" forall (f :: SigFun f3 f4) (g :: SigFun f2 f3)
(h :: Hom f1 f2) x.
appSigFun f (appSigFunHom g h x) = appSigFunHom (compSigFun f g) h x;
"appSigFun'/appSigFunHom" forall (f :: SigFun f3 f4) (g :: SigFun f2 f3)
(h :: Hom f1 f2) x.
appSigFun' f (appSigFunHom g h x) = appSigFunHom (compSigFun f g) h x;
"appHom/appSigFunHom" forall (f :: Hom f3 f4) (g :: SigFun f2 f3)
(h :: Hom f1 f2) x.
appHom f (appSigFunHom g h x) = appHom' (compHom (compHomSigFun f g) h) x;
"appHom'/appSigFunHom" forall (f :: Hom f3 f4) (g :: SigFun f2 f3)
(h :: Hom f1 f2) x.
appHom' f (appSigFunHom g h x) = appHom' (compHom (compHomSigFun f g) h) x;
"appSigFunHom/appSigFunHom" forall (f1 :: SigFun f4 f5) (f2 :: Hom f3 f4)
(f3 :: SigFun f2 f3) (f4 :: Hom f1 f2) x.
appSigFunHom f1 f2 (appSigFunHom f3 f4 x)
= appSigFunHom f1 (compHom (compHomSigFun f2 f3) f4) x; #-}
{-# RULES
"cataM/appHomM" forall (a :: AlgM Maybe g d) (h :: HomM Maybe f g) x.
appHomM h x >>= cataM a = appAlgHomM a h x;
"cataM/appHomM'" forall (a :: AlgM Maybe g d) (h :: HomM Maybe f g) x.
appHomM' h x >>= cataM a = appAlgHomM a h x;
"cataM/appSigFunM" forall (a :: AlgM Maybe g d) (h :: SigFunM Maybe f g) x.
appSigFunM h x >>= cataM a = appAlgHomM a (homM h) x;
"cataM/appSigFunM'" forall (a :: AlgM Maybe g d) (h :: SigFunM Maybe f g) x.
appSigFunM' h x >>= cataM a = appAlgHomM a (homM h) x;
"cataM/appHom" forall (a :: AlgM m g d) (h :: Hom f g) x.
cataM a (appHom h x) = appAlgHomM a (sigFunM h) x;
"cataM/appHom'" forall (a :: AlgM m g d) (h :: Hom f g) x.
cataM a (appHom' h x) = appAlgHomM a (sigFunM h) x;
"cataM/appSigFun" forall (a :: AlgM m g d) (h :: SigFun f g) x.
cataM a (appSigFun h x) = appAlgHomM a (sigFunM $ hom h) x;
"cataM/appSigFun'" forall (a :: AlgM m g d) (h :: SigFun f g) x.
cataM a (appSigFun' h x) = appAlgHomM a (sigFunM $ hom h) x;
"cataM/appSigFun" forall (a :: AlgM m g d) (h :: SigFun f g) x.
cataM a (appSigFun h x) = appAlgHomM a (sigFunM $ hom h) x;
"cataM/appSigFunHom" forall (a :: AlgM m h d) (g :: SigFun g h) (f :: Hom f g) x.
cataM a (appSigFunHom g f x) = appAlgHomM a (sigFunM $ compSigFunHom g f) x;
"appHomM/appHomM" forall (a :: HomM Maybe g h) (h :: HomM Maybe f g) x.
appHomM h x >>= appHomM a = appHomM (compHomM a h) x;
"appHomM/appSigFunM" forall (a :: HomM Maybe g h) (h :: SigFunM Maybe f g) x.
appSigFunM h x >>= appHomM a = appHomM (compHomSigFunM a h) x;
"appHomM/appHomM'" forall (a :: HomM Maybe g h) (h :: HomM Maybe f g) x.
appHomM' h x >>= appHomM a = appHomHomM a h x;
"appHomM/appSigFunM'" forall (a :: HomM Maybe g h) (h :: SigFunM Maybe f g) x.
appSigFunM' h x >>= appHomM a = appHomHomM a (homM h) x;
"appHomM'/appHomM" forall (a :: HomM Maybe g h) (h :: HomM Maybe f g) x.
appHomM h x >>= appHomM' a = appHomM' (compHomM' a h) x;
"appHomM'/appSigFunM" forall (a :: HomM Maybe g h) (h :: SigFunM Maybe f g) x.
appSigFunM h x >>= appHomM' a = appHomM' (compHomSigFunM a h) x;
"appHomM'/appHomM'" forall (a :: HomM Maybe g h) (h :: HomM Maybe f g) x.
appHomM' h x >>= appHomM' a = appHomM' (compHomM' a h) x;
"appHomM'/appSigFunM'" forall (a :: HomM Maybe g h) (h :: SigFunM Maybe f g) x.
appSigFunM' h x >>= appHomM' a = appHomM' (compHomSigFunM a h) x;
"appHomM/appHom" forall (a :: HomM m g h) (h :: Hom f g) x.
appHomM a (appHom h x) = appHomHomM a (sigFunM h) x;
"appHomM/appSigFun" forall (a :: HomM m g h) (h :: SigFun f g) x.
appHomM a (appSigFun h x) = appHomHomM a (sigFunM $ hom h) x;
"appHomM'/appHom" forall (a :: HomM m g h) (h :: Hom f g) x.
appHomM' a (appHom h x) = appHomM' (compHomM' a (sigFunM h)) x;
"appHomM'/appSigFun" forall (a :: HomM m g h) (h :: SigFun f g) x.
appHomM' a (appSigFun h x) = appHomM' (compHomSigFunM a (sigFunM h)) x;
"appHomM/appHom'" forall (a :: HomM m g h) (h :: Hom f g) x.
appHomM a (appHom' h x) = appHomHomM a (sigFunM h) x;
"appHomM/appSigFun'" forall (a :: HomM m g h) (h :: SigFun f g) x.
appHomM a (appSigFun' h x) = appHomHomM a (sigFunM $ hom h) x;
"appHomM'/appHom'" forall (a :: HomM m g h) (h :: Hom f g) x.
appHomM' a (appHom' h x) = appHomM' (compHomM' a (sigFunM h)) x;
"appHomM'/appSigFun'" forall (a :: HomM m g h) (h :: SigFun f g) x.
appHomM' a (appSigFun' h x) = appHomM' (compHomSigFunM a (sigFunM h)) x;
"appSigFunM/appHomM" forall (a :: SigFunM Maybe g h) (h :: HomM Maybe f g) x.
appHomM h x >>= appSigFunM a = appSigFunHomM a h x;
"appSigFunHomM/appSigFunM" forall (a :: SigFunM Maybe g h) (h :: SigFunM Maybe f g) x.
appSigFunM h x >>= appSigFunM a = appSigFunM (compSigFunM a h) x;
"appSigFunM/appHomM'" forall (a :: SigFunM Maybe g h) (h :: HomM Maybe f g) x.
appHomM' h x >>= appSigFunM a = appSigFunHomM a h x;
"appSigFunM/appSigFunM'" forall (a :: SigFunM Maybe g h) (h :: SigFunM Maybe f g) x.
appSigFunM' h x >>= appSigFunM a = appSigFunHomM a (homM h) x;
"appSigFunM'/appHomM" forall (a :: SigFunM Maybe g h) (h :: HomM Maybe f g) x.
appHomM h x >>= appSigFunM' a = appHomM' (compSigFunHomM' a h) x;
"appSigFunM'/appSigFunM" forall (a :: SigFunM Maybe g h) (h :: SigFunM Maybe f g) x.
appSigFunM h x >>= appSigFunM' a = appSigFunM' (compSigFunM a h) x;
"appSigFunM'/appHomM'" forall (a :: SigFunM Maybe g h) (h :: HomM Maybe f g) x.
appHomM' h x >>= appSigFunM' a = appHomM' (compSigFunHomM' a h) x;
"appSigFunM'/appSigFunM'" forall (a :: SigFunM Maybe g h) (h :: SigFunM Maybe f g) x.
appSigFunM' h x >>= appSigFunM' a = appSigFunM' (compSigFunM a h) x;
"appSigFunM/appHom" forall (a :: SigFunM m g h) (h :: Hom f g) x.
appSigFunM a (appHom h x) = appSigFunHomM a (sigFunM h) x;
"appSigFunM/appSigFun" forall (a :: SigFunM m g h) (h :: SigFun f g) x.
appSigFunM a (appSigFun h x) = appSigFunHomM a (sigFunM $ hom h) x;
"appSigFunM'/appHom" forall (a :: SigFunM m g h) (h :: Hom f g) x.
appSigFunM' a (appHom h x) = appHomM' (compSigFunHomM' a (sigFunM h)) x;
"appSigFunM'/appSigFun" forall (a :: SigFunM m g h) (h :: SigFun f g) x.
appSigFunM' a (appSigFun h x) = appSigFunM' (compSigFunM a (sigFunM h)) x;
"appSigFunM/appHom'" forall (a :: SigFunM m g h) (h :: Hom f g) x.
appSigFunM a (appHom' h x) = appSigFunHomM a (sigFunM h) x;
"appSigFunM/appSigFun'" forall (a :: SigFunM m g h) (h :: SigFun f g) x.
appSigFunM a (appSigFun' h x) = appSigFunHomM a (sigFunM $ hom h) x;
"appSigFunM'/appHom'" forall (a :: SigFunM m g h) (h :: Hom f g) x.
appSigFunM' a (appHom' h x) = appHomM' (compSigFunHomM' a (sigFunM h)) x;
"appSigFunM'/appSigFun'" forall (a :: SigFunM m g h) (h :: SigFun f g) x.
appSigFunM' a (appSigFun' h x) = appSigFunM' (compSigFunM a (sigFunM h)) x;
#-}
{-# RULES
"cata/build" forall alg (g :: forall a . Alg f a -> a) .
cata alg (build g) = g alg #-}
#endif