module Data.Comp.MultiParam.Term
(
Cxt(..),
Hole,
NoHole,
Term(..),
Trm,
Context,
simpCxt,
toCxt,
hfmapCxt,
hdimapMCxt,
ParamFunctor (..)
) where
import Prelude hiding (mapM, sequence, foldl, foldl1, foldr, foldr1)
import Data.Comp.MultiParam.HDifunctor
import Data.Comp.MultiParam.HDitraversable
import Control.Monad
import Unsafe.Coerce
import Data.Maybe (fromJust)
data Cxt :: * -> ((* -> *) -> (* -> *) -> * -> *) -> (* -> *) -> (* -> *) -> * -> * where
In :: f a (Cxt h f a b) i -> Cxt h f a b i
Hole :: b i -> Cxt Hole f a b i
Var :: a i -> Cxt h f a b i
data Hole
data NoHole
type Context = Cxt Hole
type Trm f a = Cxt NoHole f a (K ())
newtype Term f i = Term{unTerm :: forall a. Trm f a i}
simpCxt :: HDifunctor f => f a b :-> Cxt Hole f a b
simpCxt = In . hfmap Hole
toCxt :: HDifunctor f => Trm f a :-> Cxt h f a b
toCxt = unsafeCoerce
hfmapCxt :: forall h f a b b'. HDifunctor f
=> (b :-> b') -> Cxt h f a b :-> Cxt h f a b'
hfmapCxt f = run
where run :: Cxt h f a b :-> Cxt h f a b'
run (In t) = In $ hfmap run t
run (Var a) = Var a
run (Hole b) = Hole $ f b
hdimapMCxt :: forall h f a b b' m . (HDitraversable f, Monad m)
=> NatM m b b' -> NatM m (Cxt h f a b) (Cxt h f a b')
hdimapMCxt f = run
where run :: NatM m (Cxt h f a b) (Cxt h f a b')
run (In t) = liftM In $ hdimapM run t
run (Var a) = return $ Var a
run (Hole b) = liftM Hole (f b)
class ParamFunctor m where
termM :: (forall a. m (Trm f a i)) -> m (Term f i)
coerceTermM :: ParamFunctor m => (forall a. m (Trm f a i)) -> m (Term f i)
coerceTermM t = unsafeCoerce t
instance ParamFunctor Maybe where
termM Nothing = Nothing
termM x = Just (Term $ fromJust x)
instance ParamFunctor (Either a) where
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
termM [] = []
termM l = Term (head l) : termM (tail l)