{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Rank2Types            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UndecidableInstances  #-}
--------------------------------------------------------------------------------
-- |
-- Module      :  Data.Comp.Annotation
-- Copyright   :  (c) 2010-2013 Patrick Bahr
-- License     :  BSD3
-- Maintainer  :  Patrick Bahr <paba@diku.dk>
-- Stability   :  experimental
-- Portability :  non-portable (GHC Extensions)
--
-- This module defines annotations on signatures.
--
--------------------------------------------------------------------------------

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


{-| Transform a function with a domain constructed from a functor to a function
 with a domain constructed with the same functor, but with an additional
 annotation. -}
liftA :: (RemA s s') => (s' a -> t) -> s a -> t
liftA :: (s' a -> t) -> s a -> t
liftA s' a -> t
f s a
v = s' a -> t
f (s a -> s' a
forall k (s :: k -> *) (s' :: k -> *) (a :: k).
RemA s s' =>
s a -> s' a
remA s a
v)

{-| Transform a function with a domain constructed from a functor to a function
  with a domain constructed with the same functor, but with an additional
  annotation. -}
liftA' :: (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) -> s a -> Cxt h s a
liftA' s' a -> Cxt h s' a
f s a
v = let (s' a
v',p
p) = s a -> (s' a, p)
forall k (s :: k -> *) p (s' :: k -> *) (a :: k).
DistAnn s p s' =>
s' a -> (s a, p)
projectA s a
v
             in p -> Cxt h s' a -> Cxt h s a
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')

{-| Strip the annotations from a term over a functor with annotations. -}
stripA :: (RemA g f, Functor g) => CxtFun g f
stripA :: CxtFun g f
stripA = SigFun g f -> CxtFun g f
forall (f :: * -> *) (g :: * -> *).
Functor f =>
SigFun f g -> CxtFun f g
appSigFun SigFun g f
forall k (s :: k -> *) (s' :: k -> *) (a :: k).
RemA s s' =>
s a -> s' a
remA

{-| Lift a term homomorphism over signatures @f@ and @g@ to a term homomorphism
 over the same signatures, but extended with annotations. -}
propAnn :: (DistAnn f p f', DistAnn g p g', Functor g)
        => Hom f g -> Hom f' g'
propAnn :: Hom f g -> Hom f' g'
propAnn Hom f g
hom f' a
f' = p -> Cxt Hole g a -> Cxt Hole g' a
forall (f :: * -> *) p (g :: * -> *).
(DistAnn f p g, Functor f) =>
p -> CxtFun f g
ann p
p (f a -> Cxt Hole g a
Hom f g
hom f a
f)
    where (f a
f,p
p) = f' a -> (f a, p)
forall k (s :: k -> *) p (s' :: k -> *) (a :: k).
DistAnn s p s' =>
s' a -> (s a, p)
projectA f' a
f'


{-| Lift a monadic term homomorphism over signatures @f@ and @g@ to a monadic
  term homomorphism over the same signatures, but extended with annotations. -}
propAnnM :: (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 -> HomM m f' g'
propAnnM HomM m f g
hom f' a
f' = (Cxt Hole g a -> Cxt Hole g' a)
-> m (Cxt Hole g a) -> m (Cxt Hole g' a)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (p -> CxtFun g g'
forall (f :: * -> *) p (g :: * -> *).
(DistAnn f p g, Functor f) =>
p -> CxtFun f g
ann p
p) (f a -> m (Cxt Hole g a)
HomM m f g
hom f a
f)
    where (f a
f,p
p) = f' a -> (f a, p)
forall k (s :: k -> *) p (s' :: k -> *) (a :: k).
DistAnn s p s' =>
s' a -> (s a, p)
projectA f' a
f'

{-| Annotate each node of a term with a constant value. -}
ann :: (DistAnn f p g, Functor f) => p -> CxtFun f g
ann :: p -> CxtFun f g
ann p
c = SigFun f g -> CxtFun f g
forall (f :: * -> *) (g :: * -> *).
Functor f =>
SigFun f g -> CxtFun f g
appSigFun (p -> f a -> g a
forall k (s :: k -> *) p (s' :: k -> *) (a :: k).
DistAnn s p s' =>
p -> s a -> s' a
injectA p
c)


{-| This function is similar to 'project' but applies to signatures
with an annotation which is then ignored. -}
project' :: (RemA f f', s :<: f') => Cxt h f a -> Maybe (s (Cxt h f a))
project' :: Cxt h f a -> Maybe (s (Cxt h f a))
project' (Term f (Cxt h f a)
x) = f' (Cxt h f a) -> Maybe (s (Cxt h f a))
forall (f :: * -> *) (g :: * -> *) a.
(f :<: g) =>
g a -> Maybe (f a)
proj (f' (Cxt h f a) -> Maybe (s (Cxt h f a)))
-> f' (Cxt h f a) -> Maybe (s (Cxt h f a))
forall a b. (a -> b) -> a -> b
$ f (Cxt h f a) -> f' (Cxt h f a)
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
_ = Maybe (s (Cxt h f a))
forall a. Maybe a
Nothing