module DDC.Core.Transform.Rewrite.Error
( Error (..)
, Side (..))
where
import DDC.Core.Exp
import DDC.Core.Check ()
import DDC.Type.Pretty
import qualified DDC.Core.Check as C
data Error a n
= ErrorTypeCheck
{
errorSide :: Side
, errorExp :: Exp a n
, errorCheckError :: C.Error a n }
| ErrorBadConstraint
{ errorConstraint :: Type n }
| ErrorTypeConflict
{ errorTypeLhs :: (Type n, Effect n, Closure n)
, errorTypeRhs :: (Type n, Effect n, Closure n) }
| ErrorNotFirstOrder
{ errorExp :: Exp a n }
| ErrorVarUnmentioned
| ErrorAnonymousBinder
{ errorBinder :: Bind n }
data Side
= Lhs | Rhs
instance Pretty Side where
ppr Lhs = text "lhs"
ppr Rhs = text "rhs"
instance (Show a, Pretty n, Show n, Eq n) => Pretty (Error a n) where
ppr err
= case err of
ErrorTypeCheck s x e
-> vcat [ text "Can't typecheck " <> ppr s <> text ": " <> ppr e
, text "While checking " <> ppr x ]
ErrorBadConstraint c
-> text "Bad constraint: " <> ppr c
ErrorTypeConflict (tl,el,cl) (tr,er,cr)
-> vcat [ text "LHS and RHS have different types:"
, text "Type L: " <> ppr tl
, text "Type R: " <> ppr tr
, text "Eff L: " <> ppr el
, text "Eff R: " <> ppr er
, text "Clo L: " <> ppr cl
, text "Clo R: " <> ppr cr ]
ErrorNotFirstOrder x
-> vcat [ text "No binders allowed in left-hand side."
, text "While checking " <> ppr x ]
ErrorVarUnmentioned
-> text "All variables in rule should be mentioned in left-hand side."
ErrorAnonymousBinder b
-> text "Anonymous binders, just give it a name: " <> ppr b