{-# 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 :: Cxt h f a -> Maybe (g (Cxt h f a))
project = SigFunM Maybe f g -> Cxt h f a -> Maybe (g (Cxt h f a))
forall (f :: * -> *) (g :: * -> *) h a.
SigFunM Maybe f g -> Cxt h f a -> Maybe (g (Cxt h f a))
project_ SigFunM Maybe f g
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_ :: SigFunM Maybe f g -> Cxt h f a -> Maybe (g (Cxt h f a))
project_ SigFunM Maybe f g
_ (Hole a
_) = Maybe (g (Cxt h f a))
forall a. Maybe a
Nothing
project_ SigFunM Maybe f g
f (Term f (Cxt h f a)
t) = f (Cxt h f a) -> Maybe (g (Cxt h f a))
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 :: CxtFunM Maybe f g
deepProject = SigFunM Maybe f g -> CxtFunM Maybe f g
forall (g :: * -> *) (m :: * -> *) (f :: * -> *).
(Traversable g, Monad m) =>
SigFunM m f g -> CxtFunM m f g
appSigFunM' SigFunM Maybe f g
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_ :: SigFunM Maybe f g -> CxtFunM Maybe f g
deepProject_ = SigFunM Maybe f g -> Cxt h f a -> Maybe (Cxt h g a)
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 :: g (Cxt h f a) -> Cxt h f a
inject = SigFun g f -> g (Cxt h f a) -> Cxt h f a
forall (g :: * -> *) (f :: * -> *) h a.
SigFun g f -> g (Cxt h f a) -> Cxt h f a
inject_ SigFun g f
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_ :: SigFun g f -> g (Cxt h f a) -> Cxt h f a
inject_ SigFun g f
f = f (Cxt h f a) -> Cxt h f a
forall (f :: * -> *) h a. f (Cxt h f a) -> Cxt h f a
Term (f (Cxt h f a) -> Cxt h f a)
-> (g (Cxt h f a) -> f (Cxt h f a)) -> g (Cxt h f a) -> Cxt h f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. g (Cxt h f a) -> f (Cxt h f a)
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 :: CxtFun g f
deepInject = SigFun g f -> CxtFun g f
forall (g :: * -> *) (f :: * -> *).
Functor g =>
SigFun g f -> CxtFun g f
deepInject_ SigFun g f
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_ :: SigFun g f -> CxtFun g f
deepInject_ = SigFun g f -> Cxt h g a -> Cxt h f a
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 :: (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) = (f1 (Term f) -> a) -> (f2 (Term f) -> a) -> f (Term f) -> a
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 :: Const g -> Cxt h f a
injectConst = g (Cxt h f a) -> Cxt h f a
forall (g :: * -> *) (f :: * -> *) h a.
(g :<: f) =>
g (Cxt h f a) -> Cxt h f a
inject (g (Cxt h f a) -> Cxt h f a)
-> (Const g -> g (Cxt h f a)) -> Const g -> Cxt h f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (() -> Cxt h f a) -> Const g -> g (Cxt h f a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Cxt h f a -> () -> Cxt h f a
forall a b. a -> b -> a
const Cxt h f a
forall a. HasCallStack => a
undefined)


projectConst :: (Functor g, g :<: f) => Cxt h f a -> Maybe (Const g)
projectConst :: Cxt h f a -> Maybe (Const g)
projectConst = (g (Cxt h f a) -> Const g)
-> Maybe (g (Cxt h f a)) -> Maybe (Const g)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Cxt h f a -> ()) -> g (Cxt h f a) -> Const g
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (() -> Cxt h f a -> ()
forall a b. a -> b -> a
const ())) (Maybe (g (Cxt h f a)) -> Maybe (Const g))
-> (Cxt h f a -> Maybe (g (Cxt h f a)))
-> Cxt h f a
-> Maybe (Const g)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cxt h f a -> Maybe (g (Cxt h f a))
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 :: 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 :: * -> *) a h. Functor f => Alg f a -> Cxt h f a -> a
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 :: (Functor f, g :<: f) => g a -> Context f a
liftCxt :: g a -> Context f a
liftCxt g a
g = f a -> Context f a
forall (f :: * -> *) a. Functor f => f a -> Context f a
simpCxt (f a -> Context f a) -> f a -> Context f a
forall a b. (a -> b) -> a -> b
$ g a -> f a
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 :: 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 = Cxt h' f (Cxt h g a) -> Cxt h g a
forall (g :: * -> *) (f :: * -> *) h' h a.
(Functor g, g :<: f) =>
Cxt h' g (Cxt h f a) -> Cxt h f a
injectCxt (Cxt h' f (Cxt h g a) -> Cxt h g a)
-> Cxt h' f (Cxt h g a) -> Cxt h g a
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 :: * -> *) 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' :: 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 = Cxt h' f v -> (v -> Cxt h g a) -> Cxt h g a
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 (Maybe (Cxt h g a) -> Cxt h g a
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (Cxt h g a) -> Cxt h g a)
-> (v -> Maybe (Cxt h g a)) -> v -> Cxt h g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (v -> Map v (Cxt h g a) -> Maybe (Cxt h g a)
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) = f a -> String
forall a. Show a => a -> String
show f a
v
    show (Inr g a
v) = g a -> String
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) = f a -> f a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare f a
x f a
y
    compare (Inr g a
x) (Inr g a
y) = g a -> g a -> Ordering
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 f a -> f a -> Bool
forall a. Eq a => a -> a -> Bool
== f a
y
    (Inr g a
x) == (Inr g a
y) = g a
x g a -> g a -> Bool
forall a. Eq a => a -> a -> Bool
== g a
y
    (:+:) f g a
_ == (:+:) f g a
_ = Bool
False