quox/lib/Quox/Parser/FromParser/Error.idr

59 lines
1.6 KiB
Idris
Raw Normal View History

2023-03-31 13:27:38 -04:00
module Quox.Parser.FromParser.Error
import Quox.Parser.Parser
import Quox.Typing
import System.File
import Quox.Pretty
public export
data Error =
AnnotationNeeded (NameContexts d n) (Term d n)
2023-03-31 13:27:38 -04:00
| DuplicatesInEnum (List TagVal)
| TermNotInScope Name
2023-03-31 13:27:38 -04:00
| DimNotInScope PBaseName
2023-04-01 13:16:43 -04:00
| QtyNotGlobal Qty
2023-03-31 13:27:38 -04:00
| DimNameInTerm PBaseName
2023-04-01 13:16:43 -04:00
| TypeError Typing.Error
2023-03-31 13:27:38 -04:00
| LoadError String FileError
| ParseError Parser.Error
%hide Typing.Error
%hide Lexer.Error
%hide Parser.Error
parameters (unicode, showContext : Bool)
export
prettyError : Error -> Doc HL
prettyError (AnnotationNeeded ctx tm) =
sep ["the term", prettyTerm unicode ctx.dnames ctx.tnames tm,
2023-03-31 13:27:38 -04:00
"needs a type annotation"]
-- [todo] print the original PTerm instead
2023-03-31 13:27:38 -04:00
prettyError (DuplicatesInEnum tags) =
sep ["duplicate tags in enum type", braces $ fillSep $ map pretty tags]
2023-03-31 13:27:38 -04:00
prettyError (DimNotInScope i) =
sep ["dimension", pretty0 unicode $ DV $ fromString i, "not in scope"]
prettyError (TermNotInScope x) =
sep ["term variable", pretty0 unicode $ F x {d = 0, n = 0}, "not in scope"]
2023-03-31 13:27:38 -04:00
prettyError (QtyNotGlobal pi) =
sep ["quantity", pretty0 unicode pi,
"can't be used on a top level declaration"]
prettyError (DimNameInTerm i) =
sep ["dimension variable", pretty0 unicode $ DV $ fromString i,
"used in a term context"]
prettyError (TypeError err) =
Typing.prettyError unicode showContext $ trimContext 2 err
2023-03-31 13:27:38 -04:00
prettyError (LoadError str err) =
vsep [hsep ["couldn't load file", pretty str], fromString $ show err]
2023-03-31 13:27:38 -04:00
prettyError (ParseError err) =
pretty $ show err