module Data.Comp.Term
(Cxt (..),
Hole,
NoHole,
Context,
Nothing,
Term,
PTerm,
Const,
unTerm,
simpCxt,
toCxt,
constTerm
) where
import Control.Applicative hiding (Const)
import Control.Monad hiding (mapM, sequence)
import Data.Traversable
import Data.Foldable
import Unsafe.Coerce
import Prelude hiding (mapM, sequence, foldl, foldl1, foldr, foldr1)
type Const f = f ()
constTerm :: (Functor f) => Const f -> Term f
constTerm = Term . fmap (const undefined)
data Cxt :: * -> (* -> *) -> * -> * where
Term :: f (Cxt h f a) -> Cxt h f a
Hole :: a -> Cxt Hole f a
data Hole
data NoHole
type Context = Cxt Hole
simpCxt :: (Functor f) => f a -> Context f a
simpCxt = Term . fmap Hole
toCxt :: Term f -> Cxt h f a
toCxt = unsafeCoerce
data Nothing
instance Eq Nothing where
instance Ord Nothing where
instance Show Nothing where
type Term f = Cxt NoHole f Nothing
type PTerm f = forall h a . Cxt h f a
instance Functor f => Functor (Cxt h f) where
fmap f (Hole v) = Hole (f v)
fmap f (Term t) = Term (fmap (fmap f) t)
instance (Foldable f) => Foldable (Cxt h f) where
foldr op e (Hole a) = a `op` e
foldr op e (Term t) = foldr op' e t
where op' c a = foldr op a c
foldl op e (Hole a) = e `op` a
foldl op e (Term t) = foldl op' e t
where op' = foldl op
fold (Hole a) = a
fold (Term t) = foldMap fold t
foldMap f (Hole a) = f a
foldMap f (Term t) = foldMap (foldMap f) t
instance (Traversable f) => Traversable (Cxt h f) where
traverse f (Hole a) = Hole <$> f a
traverse f (Term t) = Term <$> traverse (traverse f) t
sequenceA (Hole a) = Hole <$> a
sequenceA (Term t) = Term <$> traverse sequenceA t
mapM f (Hole a) = liftM Hole $ f a
mapM f (Term t) = liftM Term $ mapM (mapM f) t
sequence (Hole a) = liftM Hole a
sequence (Term t) = liftM Term $ mapM sequence t
unTerm :: Cxt NoHole f a -> f (Cxt NoHole f a)
unTerm (Term t) = t