module Data.Comp.MultiParam.Show
(
PShow(..),
ShowHD(..)
) where
import Data.Comp.MultiParam.Term
import Data.Comp.MultiParam.HDifunctor
import Data.Comp.MultiParam.Ops
import Data.Comp.MultiParam.Derive
import Data.Comp.MultiParam.FreshM
instance Show a => PShow (K a) where
pshow = return . show . unK
$(derive [liftSum] [''ShowHD])
instance PShow Var where
pshow = return . varShow
instance (ShowHD f, PShow a) => PShow (Cxt h f Var a) where
pshow (Term t) = showHD t
pshow (Hole h) = pshow h
pshow (Place p) = pshow p
instance (HDifunctor f, ShowHD f) => Show (Term f i) where
show = evalFreshM . pshow .
(coerceCxt :: Term f i -> Trm f Var i)
instance (ShowHD f, PShow (K p)) => ShowHD (f :&: p) where
showHD (x :&: p) = do sx <- showHD x
sp <- pshow $ K p
return $ sx ++ " :&: " ++ sp