{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
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
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 i
v = s' a :-> t
f (forall (s :: (* -> *) -> * -> *) (s' :: (* -> *) -> * -> *)
(a :: * -> *).
RemA s s' =>
s a :-> s' a
remA s a i
v)
ann :: (DistAnn f p g, HFunctor f) => p -> CxtFun f g
ann :: forall (f :: (* -> *) -> * -> *) p (g :: (* -> *) -> * -> *).
(DistAnn f p g, HFunctor f) =>
p -> CxtFun f g
ann p
c = forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *).
HFunctor f =>
SigFun f g -> CxtFun f g
appSigFun (forall (s :: (* -> *) -> * -> *) p (s' :: (* -> *) -> * -> *)
(a :: * -> *).
DistAnn s p s' =>
p -> s a :-> s' a
injectA p
c)
liftA' :: (DistAnn s' p s, HFunctor s')
=> (s' a :-> Cxt h s' a) -> s a :-> Cxt h s a
liftA' :: forall (s' :: (* -> *) -> * -> *) p (s :: (* -> *) -> * -> *)
(a :: * -> *) h.
(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
f s a i
v = let (s' a i
v' O.:&: p
p) = forall (s :: (* -> *) -> * -> *) p (s' :: (* -> *) -> * -> *)
(a :: * -> *).
DistAnn s p s' =>
s' a :-> (s a :&: p)
projectA s a i
v
in forall (f :: (* -> *) -> * -> *) p (g :: (* -> *) -> * -> *).
(DistAnn f p g, HFunctor f) =>
p -> CxtFun f g
ann p
p (s' a :-> Cxt h s' a
f s' a i
v')
stripA :: (RemA g f, HFunctor g) => CxtFun g f
stripA :: forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *).
(RemA g f, HFunctor g) =>
CxtFun g f
stripA = forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *).
HFunctor f =>
SigFun f g -> CxtFun f g
appSigFun 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 :: forall (f :: (* -> *) -> * -> *) p (f' :: (* -> *) -> * -> *)
(g :: (* -> *) -> * -> *) (g' :: (* -> *) -> * -> *).
(DistAnn f p f', DistAnn g p g', HFunctor g) =>
Hom f g -> Hom f' g'
propAnn Hom f g
alg f' a i
f' = forall (f :: (* -> *) -> * -> *) p (g :: (* -> *) -> * -> *).
(DistAnn f p g, HFunctor f) =>
p -> CxtFun f g
ann p
p (Hom f g
alg f a i
f)
where (f a i
f O.:&: p
p) = forall (s :: (* -> *) -> * -> *) p (s' :: (* -> *) -> * -> *)
(a :: * -> *).
DistAnn s p s' =>
s' a :-> (s a :&: p)
projectA f' a i
f'
project' :: (RemA f f', s :<: f') => Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' :: forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
(s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' (Term f (Cxt h f a) i
x) = forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
(a :: * -> *).
(f :<: g) =>
NatM Maybe (g a) (f a)
proj forall a b. (a -> b) -> a -> b
$ 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
_ = forall a. Maybe a
Nothing