39 lines
1.5 KiB
Haskell
39 lines
1.5 KiB
Haskell
module Errors where
|
|
|
|
import Expr
|
|
import Prettyprinter
|
|
import Prettyprinter.Render.Text
|
|
import Prelude hiding (group)
|
|
|
|
data Error
|
|
= UnboundVariable Text
|
|
| NotASort Expr
|
|
| ExpectedPiType Expr Expr
|
|
| ExpectedSigmaType Expr Expr
|
|
| NotEquivalent Expr Expr Expr
|
|
| PNMissingType Text
|
|
| DuplicateDefinition Text
|
|
deriving (Eq, Ord)
|
|
|
|
instance Pretty Error where
|
|
pretty (UnboundVariable x) = "Unbound variable: '" <> pretty x <> "'"
|
|
pretty (NotASort x) = group $ hang 4 ("Term:" <> line <> pretty x) <> line <> "is not a type"
|
|
pretty (ExpectedPiType x t) = group $ hang 4 ("Term:" <> line <> pretty x) <> line <> hang 4 ("is not a function, instead is type" <> line <> pretty t)
|
|
pretty (ExpectedSigmaType x t) = group $ hang 4 ("Term:" <> line <> pretty x) <> line <> hang 4 ("is not a pair, instead is type" <> line <> pretty t)
|
|
pretty (NotEquivalent a a' e) =
|
|
group $
|
|
hang 4 ("Cannot unify" <> line <> pretty a)
|
|
<> line
|
|
<> hang 4 ("with" <> line <> pretty a')
|
|
<> line
|
|
<> hang 4 ("when evaluating" <> line <> pretty e)
|
|
pretty (PNMissingType x) = "Axiom '" <> pretty x <> "' missing type ascription"
|
|
pretty (DuplicateDefinition n) = "'" <> pretty n <> "' already defined"
|
|
|
|
instance ToText Error where
|
|
toText = renderStrict . layoutSmart (LayoutOptions (AvailablePerLine 100 1.0)) . pretty
|
|
|
|
instance ToString Error where
|
|
toString = toString . toText
|
|
|
|
type Result = Either Error
|