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

module Data.Comp.Multi.Sum
    (
     (:<:),
     (:+:),
     caseH,

     -- * Projections for Signatures and Terms
     proj,
     project,
     deepProject,

     -- * Injections for Signatures and Terms
     inj,
     inject,
     deepInject,

     split,

     -- * Injections and Projections for Constants
     injectConst,
     projectConst,
     injectCxt,
     liftCxt,
     substHoles,
--     substHoles'
    ) where

import Data.Comp.Multi.Algebra
import Data.Comp.Multi.HFunctor
import Data.Comp.Multi.HTraversable
import Data.Comp.Multi.Ops
import Data.Comp.Multi.Term


-- |Project the outermost layer of a term to a sub signature. If the signature
-- @g@ is compound of /n/ atomic signatures, use @project@/n/ instead.
project :: (g :<: f) => NatM Maybe (Cxt h f a) (g (Cxt h f a))
project :: forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project (Hole a i
_) = forall a. Maybe a
Nothing
project (Term f (Cxt h f a) i
t) = forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
       (a :: * -> *).
(f :<: g) =>
NatM Maybe (g a) (f a)
proj f (Cxt h f a) i
t


-- | Tries to coerce a term/context to a term/context over a sub-signature. If
-- the signature @g@ is compound of /n/ atomic signatures, use
-- @deepProject@/n/ instead.
deepProject :: (HTraversable g, g :<: f)  => CxtFunM Maybe f g
{-# INLINE deepProject #-}
deepProject :: forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *).
(HTraversable g, g :<: f) =>
CxtFunM Maybe f g
deepProject = forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
       (m :: * -> *).
(HTraversable g, Monad m) =>
SigFunM m f g -> CxtFunM m f g
appSigFunM' forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
       (a :: * -> *).
(f :<: g) =>
NatM Maybe (g a) (f a)
proj


-- |Inject a term where the outermost layer is a sub signature. If the signature
-- @g@ is compound of /n/ atomic signatures, use @inject@/n/ instead.
inject :: (g :<: f) => g (Cxt h f a) :-> Cxt h f a
inject :: forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject = forall (f :: (* -> *) -> * -> *) h (a :: * -> *) i.
f (Cxt h f a) i -> Cxt h f a i
Term forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
       (a :: * -> *).
(f :<: g) =>
f a :-> g a
inj


-- |Inject a term over a sub signature to a term over larger signature. If the
-- signature @g@ is compound of /n/ atomic signatures, use @deepInject@/n/
-- instead.
deepInject :: (HFunctor g, g :<: f) => CxtFun g f
{-# INLINE deepInject #-}
deepInject :: forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *).
(HFunctor g, g :<: f) =>
CxtFun g f
deepInject = forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *).
HFunctor f =>
SigFun f g -> CxtFun f g
appSigFun forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
       (a :: * -> *).
(f :<: g) =>
f a :-> g a
inj


split :: (f :=: f1 :+: f2) => (f1 (Term f) :-> a) -> (f2 (Term f) :-> a) -> Term f :-> a
split :: forall (f :: (* -> *) -> * -> *) (f1 :: (* -> *) -> * -> *)
       (f2 :: (* -> *) -> * -> *) (a :: * -> *).
(f :=: (f1 :+: f2)) =>
(f1 (Term f) :-> a) -> (f2 (Term f) :-> a) -> Term f :-> a
split f1 (Term f) :-> a
f1 f2 (Term f) :-> a
f2 (Term f (Term f) i
t) = forall (f :: (* -> *) -> * -> *) (f1 :: (* -> *) -> * -> *)
       (f2 :: (* -> *) -> * -> *) (a :: * -> *) (b :: * -> *).
(f :=: (f1 :+: f2)) =>
(f1 a :-> b) -> (f2 a :-> b) -> f a :-> b
spl f1 (Term f) :-> a
f1 f2 (Term f) :-> a
f2 f (Term f) i
t


-- | This function injects a whole context into another context.
injectCxt :: (HFunctor g, g :<: f) => Cxt h' g (Cxt h f a) :-> Cxt h f a
injectCxt :: forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h' h
       (a :: * -> *).
(HFunctor g, g :<: f) =>
Cxt h' g (Cxt h f a) :-> Cxt h f a
injectCxt = forall (f :: (* -> *) -> * -> *) (e :: * -> *) h.
HFunctor f =>
Alg f e -> Cxt h f e :-> e
cata' forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject

-- | This function lifts the given functor to a context.
liftCxt :: (HFunctor f, g :<: f) => g a :-> Context f a
liftCxt :: forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
       (a :: * -> *).
(HFunctor f, g :<: f) =>
g a :-> Context f a
liftCxt g a i
g = forall (f :: (* -> *) -> * -> *) (a :: * -> *) i.
HFunctor f =>
f a i -> Context f a i
simpCxt forall a b. (a -> b) -> a -> b
$ forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
       (a :: * -> *).
(f :<: g) =>
f a :-> g a
inj g a i
g

-- | This function applies the given context with hole type @a@ to a
-- family @f@ of contexts (possibly terms) indexed by @a@. That is,
-- each hole @h@ is replaced by the context @f h@.

substHoles :: (HFunctor f, HFunctor g, f :<: g)
           => (v :-> Cxt h g a) -> Cxt h' f v :-> Cxt h g a
substHoles :: forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
       (v :: * -> *) h (a :: * -> *) h'.
(HFunctor f, HFunctor g, f :<: g) =>
(v :-> Cxt h g a) -> Cxt h' f v :-> Cxt h g a
substHoles v :-> Cxt h g a
f Cxt h' f v i
c = forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h' h
       (a :: * -> *).
(HFunctor g, g :<: f) =>
Cxt h' g (Cxt h f a) :-> Cxt h f a
injectCxt forall a b. (a -> b) -> a -> b
$ forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap v :-> Cxt h g a
f Cxt h' f v i
c

injectConst :: (HFunctor g, g :<: f) => Const g :-> Cxt h f a
injectConst :: forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(HFunctor g, g :<: f) =>
Const g :-> Cxt h f a
injectConst = forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap (forall a b. a -> b -> a
const forall a. HasCallStack => a
undefined)

projectConst :: (HFunctor g, g :<: f) => NatM Maybe (Cxt h f a) (Const g)
projectConst :: forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(HFunctor g, g :<: f) =>
NatM Maybe (Cxt h f a) (Const g)
projectConst = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap (forall a b. a -> b -> a
const (forall a i. a -> K a i
K ()))) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project