{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeSynonymInstances #-}
module Data.Comp.Sum
(
(:<:),
(:=:),
(:+:),
caseF,
proj,
project,
deepProject,
project_,
deepProject_,
inj,
inject,
deepInject,
inject_,
deepInject_,
split,
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 :: (g :<: f) => Cxt h f a -> Maybe (g (Cxt h f a))
project = project_ proj
project_ :: SigFunM Maybe f g -> Cxt h f a -> Maybe (g (Cxt h f a))
project_ _ (Hole _) = Nothing
project_ f (Term t) = f t
deepProject :: (Traversable g, g :<: f) => CxtFunM Maybe f g
{-# INLINE deepProject #-}
deepProject = appSigFunM' proj
deepProject_ :: (Traversable g) => (SigFunM Maybe f g) -> CxtFunM Maybe f g
{-# INLINE deepProject_ #-}
deepProject_ = appSigFunM'
inject :: (g :<: f) => g (Cxt h f a) -> Cxt h f a
inject = inject_ inj
inject_ :: SigFun g f -> g (Cxt h f a) -> Cxt h f a
inject_ f = Term . f
deepInject :: (Functor g, g :<: f) => CxtFun g f
{-# INLINE deepInject #-}
deepInject = deepInject_ inj
deepInject_ :: (Functor g) => SigFun g f -> CxtFun g f
{-# INLINE deepInject_ #-}
deepInject_ = appSigFun
split :: (f :=: f1 :+: f2) => (f1 (Term f) -> a) -> (f2 (Term f) -> a) -> Term f -> a
split f1 f2 (Term t) = spl f1 f2 t
injectConst :: (Functor g, g :<: f) => Const g -> Cxt h f a
injectConst = inject . fmap (const undefined)
projectConst :: (Functor g, g :<: f) => Cxt h f a -> Maybe (Const g)
projectConst = fmap (fmap (const ())) . project
injectCxt :: (Functor g, g :<: f) => Cxt h' g (Cxt h f a) -> Cxt h f a
injectCxt = cata' inject
liftCxt :: (Functor f, g :<: f) => g a -> Context f a
liftCxt g = simpCxt $ inj g
substHoles :: (Functor f, Functor g, f :<: g) => Cxt h' f v -> (v -> Cxt h g a) -> Cxt h g a
substHoles c f = injectCxt $ fmap f 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' c m = substHoles c (fromJust . (`Map.lookup` m))
instance (Show (f a), Show (g a)) => Show ((f :+: g) a) where
show (Inl v) = show v
show (Inr v) = show v
instance (Ord (f a), Ord (g a)) => Ord ((f :+: g) a) where
compare (Inl _) (Inr _) = LT
compare (Inr _) (Inl _) = GT
compare (Inl x) (Inl y) = compare x y
compare (Inr x) (Inr y) = compare x y
instance (Eq (f a), Eq (g a)) => Eq ((f :+: g) a) where
(Inl x) == (Inl y) = x == y
(Inr x) == (Inr y) = x == y
_ == _ = False