module Errors where

import Expr

data Error
    = UnboundVariable Text
    | NotASort Expr Expr
    | ExpectedPiType Expr Expr
    | NotEquivalent Expr Expr Expr
    | PNMissingType Text
    | DuplicateDefinition Text
    | EmptySection Text
    deriving (Eq, Ord)

instance ToText Error where
    toText (UnboundVariable x) = "Unbound variable: '" <> x <> "'"
    toText (NotASort x t) = "Expected '" <> pretty x <> "' to have type * or □, instead found '" <> pretty t <> "'"
    toText (ExpectedPiType x t) = "'" <> pretty x <> "' : '" <> pretty t <> "' is not a function"
    toText (NotEquivalent a a' e) = "Cannot unify '" <> pretty a <> "' with '" <> pretty a' <> "' when evaluating '" <> pretty e <> "'"
    toText (PNMissingType x) = "Axiom '" <> x <> "' missing type ascription"
    toText (DuplicateDefinition n) = "'" <> n <> "' already defined"
    toText (EmptySection var) = "Tried to declare variable " <> var <> " without a section"

instance ToString Error where
    toString = toString . toText

type Result = Either Error