{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Comp.Annotation
(
(:&:) (..),
(:*:) (..),
DistAnn (..),
RemA (..),
liftA,
liftA',
stripA,
propAnn,
propAnnM,
ann,
project'
) where
import Control.Monad
import Data.Comp.Algebra
import Data.Comp.Ops
import Data.Comp.Term
liftA :: (RemA s s') => (s' a -> t) -> s a -> t
liftA :: forall (s :: * -> *) (s' :: * -> *) a t.
RemA s s' =>
(s' a -> t) -> s a -> t
liftA s' a -> t
f s a
v = s' a -> t
f (forall {k} (s :: k -> *) (s' :: k -> *) (a :: k).
RemA s s' =>
s a -> s' a
remA s a
v)
liftA' :: (DistAnn s' p s, Functor s')
=> (s' a -> Cxt h s' a) -> s a -> Cxt h s a
liftA' :: forall (s' :: * -> *) p (s :: * -> *) a h.
(DistAnn s' p s, Functor s') =>
(s' a -> Cxt h s' a) -> s a -> Cxt h s a
liftA' s' a -> Cxt h s' a
f s a
v = let (s' a
v',p
p) = forall {k} (s :: k -> *) p (s' :: k -> *) (a :: k).
DistAnn s p s' =>
s' a -> (s a, p)
projectA s a
v
in forall (f :: * -> *) p (g :: * -> *).
(DistAnn f p g, Functor f) =>
p -> CxtFun f g
ann p
p (s' a -> Cxt h s' a
f s' a
v')
stripA :: (RemA g f, Functor g) => CxtFun g f
stripA :: forall (g :: * -> *) (f :: * -> *).
(RemA g f, Functor g) =>
CxtFun g f
stripA = forall (f :: * -> *) (g :: * -> *).
Functor f =>
SigFun f g -> CxtFun f g
appSigFun forall {k} (s :: k -> *) (s' :: k -> *) (a :: k).
RemA s s' =>
s a -> s' a
remA
propAnn :: (DistAnn f p f', DistAnn g p g', Functor g)
=> Hom f g -> Hom f' g'
propAnn :: forall (f :: * -> *) p (f' :: * -> *) (g :: * -> *) (g' :: * -> *).
(DistAnn f p f', DistAnn g p g', Functor g) =>
Hom f g -> Hom f' g'
propAnn Hom f g
hom f' a
f' = forall (f :: * -> *) p (g :: * -> *).
(DistAnn f p g, Functor f) =>
p -> CxtFun f g
ann p
p (Hom f g
hom f a
f)
where (f a
f,p
p) = forall {k} (s :: k -> *) p (s' :: k -> *) (a :: k).
DistAnn s p s' =>
s' a -> (s a, p)
projectA f' a
f'
propAnnM :: (DistAnn f p f', DistAnn g p g', Functor g, Monad m)
=> HomM m f g -> HomM m f' g'
propAnnM :: forall (f :: * -> *) p (f' :: * -> *) (g :: * -> *) (g' :: * -> *)
(m :: * -> *).
(DistAnn f p f', DistAnn g p g', Functor g, Monad m) =>
HomM m f g -> HomM m f' g'
propAnnM HomM m f g
hom f' a
f' = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (forall (f :: * -> *) p (g :: * -> *).
(DistAnn f p g, Functor f) =>
p -> CxtFun f g
ann p
p) (HomM m f g
hom f a
f)
where (f a
f,p
p) = forall {k} (s :: k -> *) p (s' :: k -> *) (a :: k).
DistAnn s p s' =>
s' a -> (s a, p)
projectA f' a
f'
ann :: (DistAnn f p g, Functor f) => p -> CxtFun f g
ann :: forall (f :: * -> *) p (g :: * -> *).
(DistAnn f p g, Functor f) =>
p -> CxtFun f g
ann p
c = forall (f :: * -> *) (g :: * -> *).
Functor f =>
SigFun f g -> CxtFun f g
appSigFun (forall {k} (s :: k -> *) p (s' :: k -> *) (a :: k).
DistAnn s p s' =>
p -> s a -> s' a
injectA p
c)
project' :: (RemA f f', s :<: f') => Cxt h f a -> Maybe (s (Cxt h f a))
project' :: forall (f :: * -> *) (f' :: * -> *) (s :: * -> *) h a.
(RemA f f', s :<: f') =>
Cxt h f a -> Maybe (s (Cxt h f a))
project' (Term f (Cxt h f a)
x) = forall (f :: * -> *) (g :: * -> *) a.
(f :<: g) =>
g a -> Maybe (f a)
proj forall a b. (a -> b) -> a -> b
$ forall {k} (s :: k -> *) (s' :: k -> *) (a :: k).
RemA s s' =>
s a -> s' a
remA f (Cxt h f a)
x
project' Cxt h f a
_ = forall a. Maybe a
Nothing