{-# 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 :: NatM Maybe (Cxt h f a) (g (Cxt h f a))
project (Hole a i
_) = Maybe (g (Cxt h f a) i)
forall a. Maybe a
Nothing
project (Term f (Cxt h f a) i
t) = f (Cxt h f a) i -> Maybe (g (Cxt h f a) i)
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 :: CxtFunM Maybe f g
deepProject = SigFunM Maybe f g -> CxtFunM Maybe f g
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
       (m :: * -> *).
(HTraversable g, Monad m) =>
SigFunM m f g -> CxtFunM m f g
appSigFunM' SigFunM Maybe f g
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 :: g (Cxt h f a) :-> Cxt h f a
inject = f (Cxt h f a) i -> Cxt h f a i
forall (f :: (* -> *) -> * -> *) h (a :: * -> *) i.
f (Cxt h f a) i -> Cxt h f a i
Term (f (Cxt h f a) i -> Cxt h f a i)
-> (g (Cxt h f a) i -> f (Cxt h f a) i)
-> g (Cxt h f a) i
-> Cxt h f a i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. g (Cxt h f a) i -> f (Cxt h f a) i
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 :: CxtFun g f
deepInject = SigFun g f -> CxtFun g f
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *).
HFunctor f =>
SigFun f g -> CxtFun f g
appSigFun SigFun g f
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 :: (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) = (f1 (Term f) :-> a) -> (f2 (Term f) :-> a) -> f (Term f) i -> a i
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 :: Cxt h' g (Cxt h f a) :-> Cxt h f a
injectCxt = Alg g (Cxt h f a) -> Cxt h' g (Cxt h f a) :-> Cxt h f a
forall (f :: (* -> *) -> * -> *) (e :: * -> *) h.
HFunctor f =>
Alg f e -> Cxt h f e :-> e
cata' Alg g (Cxt h f a)
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 :: g a :-> Context f a
liftCxt g a i
g = f a i -> Context f a i
forall (f :: (* -> *) -> * -> *) (a :: * -> *) i.
HFunctor f =>
f a i -> Context f a i
simpCxt (f a i -> Context f a i) -> f a i -> Context f a i
forall a b. (a -> b) -> a -> b
$ g a i -> f a i
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 :: (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 = Cxt h' f (Cxt h g a) i -> Cxt h g a i
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h' h
       (a :: * -> *).
(HFunctor g, g :<: f) =>
Cxt h' g (Cxt h f a) :-> Cxt h f a
injectCxt (Cxt h' f (Cxt h g a) i -> Cxt h g a i)
-> Cxt h' f (Cxt h g a) i -> Cxt h g a i
forall a b. (a -> b) -> a -> b
$ (v :-> Cxt h g a) -> Cxt h' f v i -> Cxt h' f (Cxt h g a) i
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 :: Const g :-> Cxt h f a
injectConst = g (Cxt h f a) i -> Cxt h f a i
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject (g (Cxt h f a) i -> Cxt h f a i)
-> (g (K ()) i -> g (Cxt h f a) i) -> g (K ()) i -> Cxt h f a i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (K () :-> Cxt h f a) -> Const g :-> g (Cxt h f a)
forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap (Cxt h f a i -> K () i -> Cxt h f a i
forall a b. a -> b -> a
const Cxt h f a i
forall a. HasCallStack => a
undefined)

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