{-# 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 f v = f (remA v)
liftA' :: (DistAnn s' p s, Functor s')
=> (s' a -> Cxt h s' a) -> s a -> Cxt h s a
liftA' f v = let (v',p) = projectA v
in ann p (f v')
stripA :: (RemA g f, Functor g) => CxtFun g f
stripA = appSigFun remA
propAnn :: (DistAnn f p f', DistAnn g p g', Functor g)
=> Hom f g -> Hom f' g'
propAnn hom f' = ann p (hom f)
where (f,p) = projectA f'
propAnnM :: (DistAnn f p f', DistAnn g p g', Functor g, Monad m)
=> HomM m f g -> HomM m f' g'
propAnnM hom f' = liftM (ann p) (hom f)
where (f,p) = projectA f'
ann :: (DistAnn f p g, Functor f) => p -> CxtFun f g
ann c = appSigFun (injectA c)
project' :: (RemA f f', s :<: f') => Cxt h f a -> Maybe (s (Cxt h f a))
project' (Term x) = proj $ remA x
project' _ = Nothing