{-# LANGUAGE EmptyDataDecls, GADTs, KindSignatures, Rank2Types,
MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
module Data.Comp.Param.Term
(
Cxt(..),
Hole,
NoHole,
Term(..),
Trm,
Context,
simpCxt,
toCxt,
cxtMap,
ParamFunctor(..)
) where
import Prelude hiding (mapM, sequence, foldl, foldl1, foldr, foldr1)
import Data.Comp.Param.Difunctor
import Unsafe.Coerce (unsafeCoerce)
import Data.Maybe (fromJust)
data Cxt :: * -> (* -> * -> *) -> * -> * -> * where
In :: f a (Cxt h f a b) -> Cxt h f a b
Hole :: b -> Cxt Hole f a b
Var :: a -> Cxt h f a b
data Hole
data NoHole
type Context = Cxt Hole
type Trm f a = Cxt NoHole f a ()
newtype Term f = Term{unTerm :: forall a. Trm f a}
simpCxt :: Difunctor f => f a b -> Cxt Hole f a b
{-# INLINE simpCxt #-}
simpCxt = In . difmap Hole
toCxt :: Difunctor f => Trm f a -> Cxt h f a b
{-# INLINE toCxt #-}
toCxt = unsafeCoerce
cxtMap :: Difunctor f => (b -> c) -> Context f a b -> Context f a c
cxtMap f (Hole x) = Hole (f x)
cxtMap _ (Var x) = Var x
cxtMap f (In t) = In (dimap id (cxtMap f) t)
class ParamFunctor m where
termM :: (forall a. m (Trm f a)) -> m (Term f)
coerceTermM :: ParamFunctor m => (forall a. m (Trm f a)) -> m (Term f)
{-# INLINE coerceTermM #-}
coerceTermM t = unsafeCoerce t
{-# RULES
"termM/coerce" termM = coerceTermM
#-}
instance ParamFunctor Maybe where
{-# NOINLINE [1] termM #-}
termM Nothing = Nothing
termM x = Just (Term $ fromJust x)
instance ParamFunctor (Either a) where
{-# NOINLINE [1] termM #-}
termM (Left x) = Left x
termM x = Right (Term $ fromRight x)
where fromRight :: Either a b -> b
fromRight (Right x) = x
fromRight _ = error "fromRight: Left"
instance ParamFunctor [] where
{-# NOINLINE [1] termM #-}
termM [] = []
termM l = Term (head l) : termM (tail l)