{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Rank2Types            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UndecidableInstances  #-}
--------------------------------------------------------------------------------
-- |
-- Module      :  Data.Comp.Multi.Annotation
-- Copyright   :  (c) 2011 Patrick Bahr
-- License     :  BSD3
-- Maintainer  :  Patrick Bahr <paba@diku.dk>
-- Stability   :  experimental
-- Portability :  non-portable (GHC Extensions)
--
-- This module defines annotations on signatures. All definitions are
-- generalised versions of those in "Data.Comp.Annotation".
--
--------------------------------------------------------------------------------

module Data.Comp.Multi.Annotation
    (
     (:&:) (..),
     DistAnn (..),
     RemA (..),
     liftA,
     ann,
     liftA',
     stripA,
     propAnn,
     project'
    ) where

import Data.Comp.Multi.Algebra
import Data.Comp.Multi.HFunctor
import Data.Comp.Multi.Ops
import Data.Comp.Multi.Term
import qualified Data.Comp.Ops as O

-- | This function transforms 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 i
v = s' a i -> t i
s' a :-> t
f (s a i -> s' a i
forall (s :: (* -> *) -> * -> *) (s' :: (* -> *) -> * -> *)
       (a :: * -> *).
RemA s s' =>
s a :-> s' a
remA s a i
v)


-- | This function annotates each sub term of the given term with the
-- given value (of type a).

ann :: (DistAnn f p g, HFunctor f) => p -> CxtFun f g
ann :: p -> CxtFun f g
ann p
c = SigFun f g -> CxtFun f g
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *).
HFunctor f =>
SigFun f g -> CxtFun f g
appSigFun (p -> f a :-> g a
forall (s :: (* -> *) -> * -> *) p (s' :: (* -> *) -> * -> *)
       (a :: * -> *).
DistAnn s p s' =>
p -> s a :-> s' a
injectA p
c)

-- | This function transforms 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, HFunctor 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 i
v = let (s' a i
v' O.:&: p
p) = s a i -> (:&:) (s' a) p i
forall (s :: (* -> *) -> * -> *) p (s' :: (* -> *) -> * -> *)
       (a :: * -> *).
DistAnn s p s' =>
s' a :-> (s a :&: p)
projectA s a i
v
             in p -> Cxt h s' a i -> Cxt h s a i
forall (f :: (* -> *) -> * -> *) p (g :: (* -> *) -> * -> *).
(DistAnn f p g, HFunctor f) =>
p -> CxtFun f g
ann p
p (s' a i -> Cxt h s' a i
s' a :-> Cxt h s' a
f s' a i
v')

{-| This function strips the annotations from a term over a
functor with annotations. -}

stripA :: (RemA g f, HFunctor g) => CxtFun g f
stripA :: CxtFun g f
stripA = SigFun g f -> CxtFun g f
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *).
HFunctor f =>
SigFun f g -> CxtFun f g
appSigFun SigFun g f
forall (s :: (* -> *) -> * -> *) (s' :: (* -> *) -> * -> *)
       (a :: * -> *).
RemA s s' =>
s a :-> s' a
remA


propAnn :: (DistAnn f p f', DistAnn g p g', HFunctor g)
               => Hom f g -> Hom f' g'
propAnn :: Hom f g -> Hom f' g'
propAnn Hom f g
alg f' a i
f' = p -> Cxt Hole g a i -> Cxt Hole g' a i
forall (f :: (* -> *) -> * -> *) p (g :: (* -> *) -> * -> *).
(DistAnn f p g, HFunctor f) =>
p -> CxtFun f g
ann p
p (f a i -> Cxt Hole g a i
Hom f g
alg f a i
f)
    where (f a i
f O.:&: p
p) = f' a i -> (:&:) (f a) p i
forall (s :: (* -> *) -> * -> *) p (s' :: (* -> *) -> * -> *)
       (a :: * -> *).
DistAnn s p s' =>
s' a :-> (s a :&: p)
projectA f' a i
f'

-- | 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 i -> Maybe (s (Cxt h f a) i)
project' :: Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' (Term f (Cxt h f a) i
x) = f' (Cxt h f a) i -> Maybe (s (Cxt h f a) i)
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
       (a :: * -> *).
(f :<: g) =>
NatM Maybe (g a) (f a)
proj (f' (Cxt h f a) i -> Maybe (s (Cxt h f a) i))
-> f' (Cxt h f a) i -> Maybe (s (Cxt h f a) i)
forall a b. (a -> b) -> a -> b
$ f (Cxt h f a) i -> f' (Cxt h f a) i
forall (s :: (* -> *) -> * -> *) (s' :: (* -> *) -> * -> *)
       (a :: * -> *).
RemA s s' =>
s a :-> s' a
remA f (Cxt h f a) i
x
project' Cxt h f a i
_ = Maybe (s (Cxt h f a) i)
forall a. Maybe a
Nothing