{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE TypeSynonymInstances #-}
module Data.Comp.Term
(Cxt (..),
Hole,
NoHole,
Context,
Term,
PTerm,
Const,
unTerm,
simpCxt,
toCxt,
constTerm
) where
import Control.Applicative hiding (Const)
import Control.Monad hiding (mapM, sequence)
import Data.Foldable
import Data.Traversable
import Unsafe.Coerce
import Prelude hiding (foldl, foldl1, foldr, foldr1, mapM, sequence)
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
{-# INLINE simpCxt #-}
simpCxt = Term . fmap Hole
toCxt :: Functor f => Term f -> Cxt h f a
{-# INLINE toCxt #-}
toCxt = unsafeCoerce
type Term f = Cxt NoHole f ()
type PTerm f = forall h a . Cxt h f a
instance Functor f => Functor (Cxt h f) where
fmap f = run
where run (Hole v) = Hole (f v)
run (Term t) = Term (fmap run t)
instance Functor f => Applicative (Context f) where
pure = Hole
(<*>) = ap
instance (Functor f) => Monad (Context f) where
return = Hole
m >>= f = run m
where run (Hole v) = f v
run (Term t) = Term (fmap run t)
instance (Foldable f) => Foldable (Cxt h f) where
foldr op c a = run a c
where run (Hole a) e = a `op` e
run (Term t) e = foldr run e t
foldl op = run
where run e (Hole a) = e `op` a
run e (Term t) = foldl run e t
fold (Hole a) = a
fold (Term t) = foldMap fold t
foldMap f = run
where run (Hole a) = f a
run (Term t) = foldMap run t
instance (Traversable f) => Traversable (Cxt h f) where
traverse f = run
where run (Hole a) = Hole <$> f a
run (Term t) = Term <$> traverse run t
sequenceA (Hole a) = Hole <$> a
sequenceA (Term t) = Term <$> traverse sequenceA t
mapM f = run
where run (Hole a) = liftM Hole $ f a
run (Term t) = liftM Term $ mapM run 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)
{-# INLINE unTerm #-}
unTerm (Term t) = t