{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Rank2Types            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE TypeSynonymInstances  #-}
--------------------------------------------------------------------------------
-- |
-- Module      :  Data.Comp.Sum
-- Copyright   :  (c) 2010-2011 Patrick Bahr, Tom Hvitved
-- License     :  BSD3
-- Maintainer  :  Patrick Bahr <paba@diku.dk>
-- Stability   :  experimental
-- Portability :  non-portable (GHC Extensions)
--
-- This module provides the infrastructure to extend signatures.
--
--------------------------------------------------------------------------------

module Data.Comp.Sum
    (
     (:<:),
     (:=:),
     (:+:),
     caseF,

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

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

     split,

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

import Data.Comp.Algebra
import Data.Comp.Ops
import Data.Comp.Term

import Control.Monad hiding (mapM, sequence)
import Prelude hiding (mapM, sequence)

import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe


-- |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) => Cxt h f a -> Maybe (g (Cxt h f a))
project :: forall (g :: * -> *) (f :: * -> *) h a.
(g :<: f) =>
Cxt h f a -> Maybe (g (Cxt h f a))
project = forall (f :: * -> *) (g :: * -> *) h a.
SigFunM Maybe f g -> Cxt h f a -> Maybe (g (Cxt h f a))
project_ forall (f :: * -> *) (g :: * -> *) a.
(f :<: g) =>
g a -> Maybe (f a)
proj

-- |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_ :: SigFunM Maybe f g -> Cxt h f a -> Maybe (g (Cxt h f a))
project_ :: forall (f :: * -> *) (g :: * -> *) h a.
SigFunM Maybe f g -> Cxt h f a -> Maybe (g (Cxt h f a))
project_ SigFunM Maybe f g
_ (Hole a
_) = forall a. Maybe a
Nothing
project_ SigFunM Maybe f g
f (Term f (Cxt h f a)
t) = SigFunM Maybe f g
f f (Cxt h f a)
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 :: (Traversable g, g :<: f) => CxtFunM Maybe f g
{-# INLINE deepProject #-}
deepProject :: forall (g :: * -> *) (f :: * -> *).
(Traversable g, g :<: f) =>
CxtFunM Maybe f g
deepProject = forall (g :: * -> *) (m :: * -> *) (f :: * -> *).
(Traversable g, Monad m) =>
SigFunM m f g -> CxtFunM m f g
appSigFunM' forall (f :: * -> *) (g :: * -> *) a.
(f :<: g) =>
g a -> Maybe (f a)
proj

-- | 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_ :: (Traversable g) => (SigFunM Maybe f g) -> CxtFunM Maybe f g
{-# INLINE deepProject_ #-}
deepProject_ :: forall (g :: * -> *) (f :: * -> *).
Traversable g =>
SigFunM Maybe f g -> CxtFunM Maybe f g
deepProject_ = forall (g :: * -> *) (m :: * -> *) (f :: * -> *).
(Traversable g, Monad m) =>
SigFunM m f g -> CxtFunM m f g
appSigFunM'


-- |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 (g :: * -> *) (f :: * -> *) h a.
SigFun g f -> g (Cxt h f a) -> Cxt h f a
inject_ forall (f :: * -> *) (g :: * -> *) a. (f :<: g) => f a -> g a
inj

-- |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_ :: SigFun g f -> g (Cxt h f a) -> Cxt h f a
inject_ :: forall (g :: * -> *) (f :: * -> *) h a.
SigFun g f -> g (Cxt h f a) -> Cxt h f a
inject_ SigFun g f
f = forall (b :: * -> *) a c. b (Cxt a b c) -> Cxt a b c
Term forall b c a. (b -> c) -> (a -> b) -> a -> c
. SigFun g f
f


-- |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 :: (Functor g, g :<: f) => CxtFun g f
{-# INLINE deepInject #-}
deepInject :: forall (g :: * -> *) (f :: * -> *).
(Functor g, g :<: f) =>
CxtFun g f
deepInject = forall (g :: * -> *) (f :: * -> *).
Functor g =>
SigFun g f -> CxtFun g f
deepInject_ 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_ :: (Functor g) => SigFun g f -> CxtFun g f
{-# INLINE deepInject_ #-}
deepInject_ :: forall (g :: * -> *) (f :: * -> *).
Functor g =>
SigFun g f -> CxtFun g f
deepInject_ = forall (g :: * -> *) (f :: * -> *).
Functor g =>
SigFun g f -> CxtFun g f
appSigFun


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)
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)
t

injectConst :: (Functor g, g :<: f) => Const g -> Cxt h f a
injectConst :: forall (g :: * -> *) (f :: * -> *) h a.
(Functor 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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. a -> b -> a
const forall a. HasCallStack => a
undefined)


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

{-| This function injects a whole context into another context. -}
injectCxt :: (Functor g, g :<: f) => Cxt h' g (Cxt h f a) -> Cxt h f a
injectCxt :: forall (g :: * -> *) (f :: * -> *) h' h a.
(Functor g, g :<: f) =>
Cxt h' g (Cxt h f a) -> Cxt h f a
injectCxt = forall (f :: * -> *) a h. Functor f => Alg f a -> Cxt h f a -> a
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 :: (Functor f, g :<: f) => g a -> Context f a
liftCxt :: forall (f :: * -> *) (g :: * -> *) a.
(Functor f, g :<: f) =>
g a -> Context f a
liftCxt g a
g = forall (f :: * -> *) a. Functor f => f a -> Context f a
simpCxt forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) (g :: * -> *) a. (f :<: g) => f a -> g a
inj g a
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 :: (Functor f, Functor g, f :<: g) => Cxt h' f v -> (v -> Cxt h g a) -> Cxt h g a
substHoles :: forall (f :: * -> *) (g :: * -> *) h' v h a.
(Functor f, Functor g, f :<: g) =>
Cxt h' f v -> (v -> Cxt h g a) -> Cxt h g a
substHoles Cxt h' f v
c v -> Cxt h g a
f = forall (g :: * -> *) (f :: * -> *) h' h a.
(Functor g, g :<: f) =>
Cxt h' g (Cxt h f a) -> Cxt h f a
injectCxt forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap v -> Cxt h g a
f Cxt h' f v
c

substHoles' :: (Functor f, Functor g, f :<: g, Ord v) => Cxt h' f v -> Map v (Cxt h g a) -> Cxt h g a
substHoles' :: forall (f :: * -> *) (g :: * -> *) v h' h a.
(Functor f, Functor g, f :<: g, Ord v) =>
Cxt h' f v -> Map v (Cxt h g a) -> Cxt h g a
substHoles' Cxt h' f v
c Map v (Cxt h g a)
m = forall (f :: * -> *) (g :: * -> *) h' v h a.
(Functor f, Functor g, f :<: g) =>
Cxt h' f v -> (v -> Cxt h g a) -> Cxt h g a
substHoles Cxt h' f v
c (forall a. HasCallStack => Maybe a -> a
fromJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall k a. Ord k => k -> Map k a -> Maybe a
`Map.lookup`  Map v (Cxt h g a)
m))


instance (Show (f a), Show (g a)) => Show ((f :+: g) a) where
    show :: (:+:) f g a -> String
show (Inl f a
v) = forall a. Show a => a -> String
show f a
v
    show (Inr g a
v) = forall a. Show a => a -> String
show g a
v


instance (Ord (f a), Ord (g a)) => Ord ((f :+: g) a) where
    compare :: (:+:) f g a -> (:+:) f g a -> Ordering
compare (Inl f a
_) (Inr g a
_) = Ordering
LT
    compare (Inr g a
_) (Inl f a
_) = Ordering
GT
    compare (Inl f a
x) (Inl f a
y) = forall a. Ord a => a -> a -> Ordering
compare f a
x f a
y
    compare (Inr g a
x) (Inr g a
y) = forall a. Ord a => a -> a -> Ordering
compare g a
x g a
y


instance (Eq (f a), Eq (g a)) => Eq ((f :+: g) a) where
    (Inl f a
x) == :: (:+:) f g a -> (:+:) f g a -> Bool
== (Inl f a
y) = f a
x forall a. Eq a => a -> a -> Bool
== f a
y
    (Inr g a
x) == (Inr g a
y) = g a
x forall a. Eq a => a -> a -> Bool
== g a
y
    (:+:) f g a
_ == (:+:) f g a
_ = Bool
False