{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Rank2Types            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TemplateHaskell       #-}
{-# LANGUAGE TypeFamilies          #-}
{-# 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
    (
     (:<:),
     (:-<:),
     Sum,

     -- * 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'

     IsSum,
     NotSum,
     isNode
    ) where

import Data.Proxy ( Proxy )

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 _) = Maybe (g (Cxt h f a) i)
forall a. Maybe a
Nothing
project (Term t :: 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 :=: Sum fs) => (forall e l. Alts fs (HFix f) e (a l)) -> HFix f :-> a
split :: (forall e l. Alts fs (HFix f) e (a l)) -> HFix f :-> a
split alts :: forall e l. Alts fs (HFix f) e (a l)
alts = (forall e l. Alts fs (HFix f) e (a l)) -> f (HFix f) :-> a
forall (f :: (* -> *) -> * -> *) (fs :: [(* -> *) -> * -> *])
       (a :: * -> *) (b :: * -> *).
(f :=: Sum fs) =>
(forall e l. Alts fs a e (b l)) -> f a :-> b
spl forall e l. Alts fs (HFix f) e (a l)
alts (f (HFix f) i -> a i)
-> (HFix f i -> f (HFix f) i) -> HFix f i -> a i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HFix f i -> f (HFix f) i
forall (f :: (* -> *) -> * -> *) t. HFix f t -> f (HFix f) t
unTerm


-- | 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 :: 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 f :: v :-> Cxt h g a
f c :: 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

-- Used to prevent typechecker from applying the default cases when it shouldn't,
-- i.e.: it can't use the default case when it only has a type variable for the signature
type family IsSum (f :: (* -> *) -> * -> *) :: Bool where
  IsSum (Sum fs) = True
  IsSum f        = False

type NotSum f = (IsSum f ~ False)


isNode :: forall f g h a l. (f :<: g) => Proxy f -> Cxt h g a l -> Bool
isNode :: Proxy f -> Cxt h g a l -> Bool
isNode _ t :: Cxt h g a l
t = case Cxt h g a l -> Maybe (f (Cxt h g a) l)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project Cxt h g a l
t :: Maybe (f (Cxt h g a) l) of
               Just _  -> Bool
True
               Nothing -> Bool
False