content: {-# LANGUAGE AllowAmbiguousTypes   #-} -- For isNode'
  {-# LANGUAGE ConstraintKinds       #-}
  {-# LANGUAGE DataKinds             #-}
  {-# LANGUAGE FlexibleContexts      #-}
  {-# LANGUAGE FlexibleInstances     #-}
  {-# LANGUAGE GADTs                 #-}
  {-# LANGUAGE KindSignatures        #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE PatternSynonyms       #-}
  {-# LANGUAGE Rank2Types            #-}
  {-# LANGUAGE ScopedTypeVariables   #-}
  {-# LANGUAGE TypeApplications      #-}
  {-# LANGUAGE TypeFamilies          #-}
  {-# LANGUAGE TypeOperators         #-}
  {-# LANGUAGE UndecidableInstances  #-}
  {-# LANGUAGE ViewPatterns          #-}
  --------------------------------------------------------------------------------
  -- |
  -- 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
      (
       AnnTerm,
       AnnHFix,
       (:&:) (..),
       RemA (..),
       liftA,
       ann,
       liftA',
       stripA,
       propAnn,
       project',
       pattern (::&::),
       isNode',
       inj',
       inject',
       injectOpt,
       caseH',
       caseCxt',
       caseCxt'',
       DistAnn,
       AnnCxt,
       AnnCxtS
      ) where
  
  import Data.Comp.Dict
  import Data.Comp.Elem
  import Data.Comp.Multi.Algebra
  import Data.Comp.Multi.HFunctor
  import Data.Comp.Multi.Kinds
  import Data.Comp.Multi.Ops
  import Data.Comp.Multi.Sum
  import Data.Comp.Multi.Term
  
  type AnnHFix a f = HFix (f :&: a)
  type AnnTerm a fs = HFix (Sum fs :&: a)
  
  type AnnCxt p h f a = Cxt h (f :&: p) a
  -- type AnnContext p f a = AnnCxt p Hole f a
  
  type AnnCxtS p h fs a = AnnCxt p h (Sum fs) a
  -- type AnnContextS p fs a = AnnContext p (Sum fs) a
  
  -- | 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 f v = f (remA v)
  
  -- | This function annotates each sub term of the given term with the
  -- given value (of type a).
  
  ann :: (HFunctor f) => p -> CxtFun f (f :&: p)
  ann c = appSigFun (:&: 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' :: (HFunctor s)
         => (s a :-> Cxt h s a) -> (s :&: p) a :-> Cxt h (s :&: p) a
  liftA' f (v' :&: p) = ann p (f v')
  
  {-| This function strips the annotations from a term over a
  functor with annotations. -}
  
  stripA :: (RemA g f, HFunctor g) => CxtFun g f
  stripA = appSigFun remA
  
  
  propAnn :: (HFunctor g) => Hom f g -> Hom (f :&: p) (g :&: p)
  propAnn alg (f :&: p) = ann p (alg 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' (Term x) = proj $ remA x
  project' _ = Nothing
  
  pattern (::&::) :: (g :-<: fs) => g (Cxt h (Sum fs :&: x) a) l -> x -> Cxt h (Sum fs :&: x) a l
  pattern (::&::) t x <- Term ((proj -> Just t) :&: x) where
    (::&::) t x = Term (inj t :&: x)
  
  isNode' :: forall f g g' h a l. (HFunctor g, RemA g g', f :<: g') => Cxt h g a l -> Bool
  isNode' t = isNode @f $ stripA t
  
  inj' :: (f :<: g) => (f :&: p) e l -> (g :&: p) e l
  inj' (x :&: p) = (inj x) :&: p
  
  inject' :: (f :<: g) => (f :&: p) (Cxt h (g :&: p) a) :-> Cxt h (g :&: p) a
  inject' = Term . inj'
  
  injectOpt :: (f :<: g) => f (AnnHFix (Maybe p) g) l -> AnnHFix (Maybe p) g l
  injectOpt t = inject' (t :&: Nothing)
  
  caseH' :: forall fs a e l t. Alts (DistAnn fs a) e l t -> (Sum fs :&: a) e l -> t
  caseH' alts = caseH alts . distAnn
  
  caseCxt' :: forall cxt fs a e l t. (All cxt fs) => (forall f. (cxt f) => (f :&: a) e l -> t) -> (Sum fs :&: a) e l -> t
  caseCxt' f (Sum wit v :&: a) =
    f (v :&: a) \\ dictFor @cxt wit
  
  caseCxt'' :: forall cxt fs a e l t. (All cxt (DistAnn fs a)) => (forall f. (cxt (f :&: a)) => (f :&: a) e l -> t) -> (Sum fs :&: a) e l -> t
  caseCxt'' f (Sum wit v :&: a) =
    f (v :&: a) \\ dictFor @cxt (annWit wit)
  
    where annWit :: Elem f fs -> Elem (f :&: a) (DistAnn fs a)
          annWit = unsafeElem
  
  
  type family DistAnn (fs :: Signature) (a :: *) :: Signature where
    DistAnn (f ': fs) a = f :&: a ': DistAnn fs a
    DistAnn '[]       _ = '[]
  
  distAnn :: (Sum fs :&: a) e :-> Sum (DistAnn fs a) e
  distAnn (Sum wit v :&: a) =
    unsafeMapSum wit v (:&: a)
  