{-# LANGUAGE AllowAmbiguousTypes   #-} -- For isNode
{-# 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.Comp.Multi.Algebra
import Data.Comp.Multi.HFunctor
import Data.Comp.Multi.HTraversable
import Data.Comp.Multi.Kinds
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 :: Fragment) (f :: Fragment) h (a :: * -> *).
(g :<: f) =>
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 (a :: * -> *). NatM Maybe (f a) (g a)
forall (f :: Fragment) (g :: Fragment) (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 :: Fragment) (f :: Fragment).
(HTraversable g, g :<: f) =>
CxtFunM Maybe f g
deepProject = SigFunM Maybe f g -> CxtFunM Maybe f g
forall (f :: Fragment) (g :: Fragment) (m :: * -> *).
(HTraversable g, Monad m) =>
SigFunM m f g -> CxtFunM m f g
appSigFunM' f a i -> Maybe (g a i)
SigFunM Maybe f g
forall (f :: Fragment) (g :: Fragment) (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 :: Fragment) (f :: Fragment) h (a :: * -> *).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject = f (Cxt h f a) i -> Cxt h f a i
forall (f :: Fragment) 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 (a :: * -> *). g a :-> f a
forall (f :: Fragment) (g :: Fragment) (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 :: Fragment) (f :: Fragment).
(HFunctor g, g :<: f) =>
CxtFun g f
deepInject = SigFun g f -> CxtFun g f
forall (f :: Fragment) (g :: Fragment).
HFunctor f =>
SigFun f g -> CxtFun f g
appSigFun g a i -> f a i
SigFun g f
forall (f :: Fragment) (g :: Fragment) (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 (f :: Fragment) (fs :: Signature) (a :: * -> *).
(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)
alts = (forall e l. Alts fs (HFix f) e (a l)) -> f (HFix f) :-> a
forall (f :: Fragment) (fs :: Signature) (a :: * -> *)
       (b :: * -> *).
(f :=: Sum fs) =>
(forall e l. Alts fs a e (b l)) -> f a :-> b
spl Alts fs (HFix f) e (a l)
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 :: Fragment) 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 :: forall (g :: Fragment) (f :: Fragment) h' h (a :: * -> *).
(HFunctor g, g :<: f) =>
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 :: Fragment) (e :: * -> *) h.
HFunctor f =>
Alg f e -> Cxt h f e :-> e
cata' g (Cxt h f a) i -> Cxt h f a i
Alg g (Cxt h f a)
forall (g :: Fragment) (f :: Fragment) 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 :: Fragment) (g :: Fragment) (a :: * -> *).
(HFunctor f, g :<: f) =>
g a :-> Context f a
liftCxt g a i
g = f a i -> Context f a i
forall (f :: Fragment) (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 (a :: * -> *). g a :-> f a
forall (f :: Fragment) (g :: Fragment) (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 :: Fragment) (g :: Fragment) (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 = Cxt h' f (Cxt h g a) i -> Cxt h g a i
Cxt h' f (Cxt h g a) :-> Cxt h g a
forall (g :: Fragment) (f :: Fragment) 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 :-> Cxt h' f (Cxt h g a)
forall (f :: * -> *) (g :: * -> *).
(f :-> g) -> Cxt h' f f :-> Cxt h' f g
forall (h :: Fragment) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap v i -> Cxt h g a i
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 :: Fragment) (f :: Fragment) h (a :: * -> *).
(HFunctor g, g :<: f) =>
Const g :-> Cxt h f a
injectConst = g (Cxt h f a) i -> Cxt h f a i
g (Cxt h f a) :-> Cxt h f a
forall (g :: Fragment) (f :: Fragment) 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)
-> (Const g i -> g (Cxt h f a) i) -> Const g i -> Cxt h f a i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (K () :-> Cxt h f a) -> g (K ()) :-> g (Cxt h f a)
forall (f :: * -> *) (g :: * -> *). (f :-> g) -> g f :-> g g
forall (h :: Fragment) (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 :: forall (g :: Fragment) (f :: Fragment) h (a :: * -> *).
(HFunctor g, g :<: f) =>
NatM Maybe (Cxt h f a) (Const g)
projectConst = (g (Cxt h f a) i -> Const g i)
-> Maybe (g (Cxt h f a) i) -> Maybe (Const g i)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Cxt h f a :-> K ()) -> g (Cxt h f a) :-> g (K ())
forall (f :: * -> *) (g :: * -> *). (f :-> g) -> g f :-> g g
forall (h :: Fragment) (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 (Const g i))
-> (Cxt h f a i -> Maybe (g (Cxt h f a) i))
-> Cxt h f a i
-> Maybe (Const g i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cxt h f a i -> Maybe (g (Cxt h f a) i)
NatM Maybe (Cxt h f a) (g (Cxt h f a))
forall (g :: Fragment) (f :: Fragment) 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 :: Node) :: Bool where
  IsSum (Sum fs) = True
  IsSum f        = False

type NotSum f = (IsSum f ~ False)


-- | Call like @isNode \@f x@
isNode :: forall f g h a l. (f :<: g) => Cxt h g a l -> Bool
isNode :: forall (f :: Fragment) (g :: Fragment) h (a :: * -> *) l.
(f :<: g) =>
Cxt h g a l -> Bool
isNode Cxt h g a l
t = case Cxt h g a l -> Maybe (f (Cxt h g a) l)
NatM Maybe (Cxt h g a) (f (Cxt h g a))
forall (g :: Fragment) (f :: Fragment) 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 f (Cxt h g a) l
_  -> Bool
True
             Maybe (f (Cxt h g a) l)
Nothing -> Bool
False