88 lines
2.6 KiB
Idris
88 lines
2.6 KiB
Idris
module Quox.Parser.FromParser.Error
|
|
|
|
import Quox.Parser.Parser
|
|
import Quox.Typing
|
|
import System.File
|
|
|
|
import Quox.Pretty
|
|
|
|
|
|
public export
|
|
TypeError, LexError, ParseError : Type
|
|
TypeError = Typing.Error
|
|
LexError = Lexer.Error
|
|
ParseError = Parser.Error
|
|
%hide Typing.Error
|
|
%hide Lexer.Error
|
|
%hide Parser.Error
|
|
|
|
public export
|
|
data Error =
|
|
AnnotationNeeded (NameContexts d n) (Term d n)
|
|
| DuplicatesInEnum (List TagVal)
|
|
| TermNotInScope Name
|
|
| DimNotInScope PBaseName
|
|
| QtyNotGlobal Qty
|
|
| DimNameInTerm PBaseName
|
|
| WrapTypeError TypeError
|
|
| LoadError String FileError
|
|
| WrapParseError String ParseError
|
|
|
|
|
|
parameters (unicode, showContext : Bool)
|
|
export
|
|
prettyBounds : String -> Bounds -> Doc HL
|
|
prettyBounds file (MkBounds l1 c1 l2 c2) =
|
|
hcat [hl Free $ pretty file, hl Delim ":",
|
|
hl TVar $ pretty l1, hl Delim ":",
|
|
hl DVar $ pretty c1, hl Delim "-",
|
|
hl TVar $ pretty l2, hl Delim ":",
|
|
hl DVar $ pretty c2]
|
|
|
|
export
|
|
prettyParseError1 : String -> ParsingError _ -> Doc HL
|
|
prettyParseError1 file (Error msg Nothing) =
|
|
pretty msg
|
|
prettyParseError1 file (Error msg (Just bounds)) =
|
|
asep [prettyBounds file bounds <+> hl Delim ":", pretty msg]
|
|
|
|
export
|
|
prettyParseError : String -> ParseError -> Doc HL
|
|
prettyParseError file (LexError err) =
|
|
vsep ["lexical error:", nest 2 $ pretty $ show err]
|
|
prettyParseError file (ParseError errs) =
|
|
vsep $ "parse error:" ::
|
|
map (("-" <++>) . prettyParseError1 file) (toList errs)
|
|
|
|
export
|
|
prettyError : Error -> Doc HL
|
|
prettyError (AnnotationNeeded ctx tm) =
|
|
sep ["the term", prettyTerm unicode ctx.dnames ctx.tnames tm,
|
|
"needs a type annotation"]
|
|
-- [todo] print the original PTerm instead
|
|
|
|
prettyError (DuplicatesInEnum tags) =
|
|
sep ["duplicate tags in enum type", braces $ fillSep $ map pretty tags]
|
|
|
|
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"]
|
|
|
|
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 (WrapTypeError err) =
|
|
Typing.prettyError unicode showContext $ trimContext 2 err
|
|
|
|
prettyError (LoadError str err) =
|
|
vsep [hsep ["couldn't load file", pretty str], fromString $ show err]
|
|
|
|
prettyError (WrapParseError file err) =
|
|
prettyParseError file err
|