diff --git a/src/Core/Core.idr b/src/Core/Core.idr index 853ad088a..b8c9001b9 100644 --- a/src/Core/Core.idr +++ b/src/Core/Core.idr @@ -133,8 +133,10 @@ data Error : Type where GenericMsg : FC -> String -> Error TTCError : TTCErrorMsg -> Error FileErr : String -> FileError -> Error + LitFail : FC -> Error + LexFail : FC -> String -> Error ParseFail : (Show token, Pretty token) => - FC -> ParseError token -> Error + FC -> String -> List token -> Error ModuleNotFound : FC -> ModuleIdent -> Error CyclicImports : List ModuleIdent -> Error ForceNeeded : Error @@ -295,7 +297,9 @@ Show Error where show (GenericMsg fc str) = show fc ++ ":" ++ str show (TTCError msg) = "Error in TTC file: " ++ show msg show (FileErr fname err) = "File error (" ++ fname ++ "): " ++ show err - show (ParseFail fc err) = "Parse error (" ++ show err ++ ")" + show (LitFail fc) = show fc ++ ":Can't parse literate" + show (LexFail fc err) = show fc ++ ":Lexer error (" ++ show err ++ ")" + show (ParseFail fc err toks) = "Parse error (" ++ show err ++ "): " ++ show toks show (ModuleNotFound fc ns) = show fc ++ ":" ++ show ns ++ " not found" show (CyclicImports ns) @@ -373,7 +377,9 @@ getErrorLoc (BadRunElab loc _ _) = Just loc getErrorLoc (GenericMsg loc _) = Just loc getErrorLoc (TTCError _) = Nothing getErrorLoc (FileErr _ _) = Nothing -getErrorLoc (ParseFail loc _) = Just loc +getErrorLoc (LitFail loc) = Just loc +getErrorLoc (LexFail loc _) = Just loc +getErrorLoc (ParseFail loc _ _) = Just loc getErrorLoc (ModuleNotFound loc _) = Just loc getErrorLoc (CyclicImports _) = Nothing getErrorLoc ForceNeeded = Nothing diff --git a/src/Idris/Error.idr b/src/Idris/Error.idr index 694064f00..2344d70be 100644 --- a/src/Idris/Error.idr +++ b/src/Idris/Error.idr @@ -407,8 +407,12 @@ perror (TTCError msg) <++> parens (pretty "the most likely case is that the ./build directory in your current project contains files from a previous build of idris2 or the idris2 executable is from a different build than the installed .ttc files") perror (FileErr fname err) = pure $ errorDesc (reflow "File error in" <++> pretty fname <++> colon) <++> pretty (show err) -perror (ParseFail _ err) - = pure $ pretty err +perror (LitFail fc) + = pure $ errorDesc (reflow "Can't parse literate.") <+> line <+> !(ploc fc) +perror (LexFail fc msg) + = pure $ errorDesc (pretty msg) <+> line <+> !(ploc fc) +perror (ParseFail fc msg toks) + = pure $ errorDesc (pretty msg) <+> line <+> !(ploc fc) perror (ModuleNotFound fc ns) = pure $ errorDesc ("Module" <++> annotate FileCtxt (pretty ns) <++> reflow "not found") <+> line <+> !(ploc fc) perror (CyclicImports ns) diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr index b950d0101..3daf15585 100644 --- a/src/Idris/Package.idr +++ b/src/Idris/Package.idr @@ -507,8 +507,7 @@ parsePkgFile file = do (do desc <- parsePkgDesc file eoi pure desc) - | Left (FileFail err) => throw (FileErr file err) - | Left err => throw (ParseFail (getParseErrorLoc file err) err) + | Left err => throw (fromParseError file err) addFields fs (initPkgDesc pname) processPackage : {auto c : Ref Ctxt Defs} -> @@ -526,8 +525,7 @@ processPackage cmd file opts (do desc <- parsePkgDesc file eoi pure desc) - | Left (FileFail err) => throw (FileErr file err) - | Left err => throw (ParseFail (getParseErrorLoc file err) err) + | Left err => throw (fromParseError file err) pkg <- addFields fs (initPkgDesc pname) maybe (pure ()) setBuildDir (builddir pkg) setOutputDir (outputdir pkg) @@ -629,8 +627,7 @@ findIpkg fname (do desc <- parsePkgDesc ipkgn eoi pure desc) - | Left (FileFail err) => throw (FileErr ipkgn err) - | Left err => throw (ParseFail (getParseErrorLoc ipkgn err) err) + | Left err => throw (fromParseError ipkgn err) pkg <- addFields fs (initPkgDesc pname) maybe (pure ()) setBuildDir (builddir pkg) setOutputDir (outputdir pkg) diff --git a/src/Idris/ProcessIdr.idr b/src/Idris/ProcessIdr.idr index 466b09c14..ee9615b63 100644 --- a/src/Idris/ProcessIdr.idr +++ b/src/Idris/ProcessIdr.idr @@ -4,6 +4,7 @@ import Compiler.Inline import Core.Binary import Core.Context +import Core.Core import Core.Context.Log import Core.Directory import Core.Env @@ -187,11 +188,13 @@ modTime fname pure (cast t) export -getParseErrorLoc : String -> ParseError Token -> FC -getParseErrorLoc fname (ParseFail _ (Just pos) _) = MkFC fname pos pos -getParseErrorLoc fname (LexFail (_, l, c, _)) = MkFC fname (l, c) (l, c) -getParseErrorLoc fname (LitFail (MkLitErr l c _)) = MkFC fname (l, 0) (l, 0) -getParseErrorLoc fname _ = replFC +fromParseError : (Show token, Pretty token) => String -> ParseError token -> Error +fromParseError fname (FileFail err) = FileErr fname err +fromParseError fname (LitFail (MkLitErr l c _)) = LitFail (MkFC fname (l, c) (l, c + 1)) +fromParseError fname (LexFail (ComposeNotClosing begin end, _, _, _)) = LexFail (MkFC fname begin end) "Bracket is not properly closed." +fromParseError fname (LexFail (_, l, c, _)) = LexFail (MkFC fname (l, c) (l, c + 1)) "Can't recognoise token." +fromParseError fname (ParseFail msg (Just (l, c)) toks) = ParseFail (MkFC fname (l, c) (l, c + 1)) msg toks +fromParseError fname (ParseFail msg Nothing toks) = ParseFail replFC msg toks export readHeader : {auto c : Ref Ctxt Defs} -> @@ -202,7 +205,7 @@ readHeader path -- Stop at the first :, that's definitely not part of the header, to -- save lexing the whole file unnecessarily case runParserTo (isLitFile path) (is ':') res (progHdr path) of - Left err => throw (ParseFail (getParseErrorLoc path err) err) + Left err => throw (fromParseError path err) Right mod => pure mod %foreign "scheme:collect" @@ -265,7 +268,7 @@ processMod srcf ttcf msg sourcecode do iputStrLn msg Right mod <- logTime ("++ Parsing " ++ srcf) $ pure (runParser (isLitFile srcf) sourcecode (do p <- prog srcf; eoi; pure p)) - | Left err => pure (Just [ParseFail (getParseErrorLoc srcf err) err]) + | Left err => pure (Just [fromParseError srcf err]) initHash traverse addPublicHash (sort hs) resetNextVar diff --git a/tests/idris2/perf005/expected b/tests/idris2/perf005/expected index cc8d65ceb..d32e1ced6 100644 --- a/tests/idris2/perf005/expected +++ b/tests/idris2/perf005/expected @@ -12,11 +12,26 @@ Lambda.idr:62:3--88:9 67 | (Func 1/1: Building Bad1 (Bad1.idr) -Error: Parse error at line 3:1: -Couldn't parse declaration (next tokens: [data, identifier Bad, symbol =, identifier BadDCon, symbol (, identifier x, symbol :, identifier Nat, symbol ), end of input]) +Error: Couldn't parse declaration + +Bad1.idr:3:1--3:2 + | + 3 | data Bad = BadDCon (x : Nat) + | ^ + 1/1: Building Bad2 (Bad2.idr) -Error: Parse error at line 3:13: -Expected 'case', 'if', 'do', application or operator expression (next tokens: [symbol (, identifier whatever, symbol :, identifier Int, symbol ), end of input]) +Error: Expected 'case', 'if', 'do', application or operator expression + +Bad2.idr:3:13--3:14 + | + 3 | badReturn : (whatever : Int) + | ^ + 1/1: Building Bad3 (Bad3.idr) -Error: Parse error at line 4:1: -Couldn't parse declaration (next tokens: [identifier badExpr, symbol (, identifier whatever, symbol :, symbol (, symbol ), symbol ), end of input]) +Error: Couldn't parse declaration + +Bad3.idr:4:1--4:2 + | + 4 | badExpr (whatever : ()) + | ^ + diff --git a/tests/idris2/perror001/expected b/tests/idris2/perror001/expected index 4436dbe4f..9bac3551b 100644 --- a/tests/idris2/perror001/expected +++ b/tests/idris2/perror001/expected @@ -1,6 +1,8 @@ 1/1: Building PError (PError.idr) -Error: Lex error ComposeNotClosing (3, 6) (3, 7) at (3, 6) input: (Int -> Int -bar x = let y = 42 in y + x +Error: Bracket is not properly closed. + +PError.idr:4:7--4:8 + | + 4 | bar : (Int -> Int + | ^ -baz : Int -> Int -baz x = x diff --git a/tests/idris2/perror002/expected b/tests/idris2/perror002/expected index 32fededac..87a7c6e9d 100644 --- a/tests/idris2/perror002/expected +++ b/tests/idris2/perror002/expected @@ -1,5 +1,8 @@ 1/1: Building PError (PError.idr) -Error: Lex error ComposeNotClosing (4, 22) (4, 23) at (4, 22) input: (y + x +Error: Bracket is not properly closed. + +PError.idr:5:23--5:24 + | + 5 | bar x = let y = 42 in (y + x + | ^ -baz : Int -> Int -baz x = x diff --git a/tests/idris2/perror003/expected b/tests/idris2/perror003/expected index 0d3bae97d..fe41cd68a 100644 --- a/tests/idris2/perror003/expected +++ b/tests/idris2/perror003/expected @@ -1,10 +1,16 @@ 1/1: Building PError (PError.idr) -Error: Lex error ComposeNotClosing (4, 16) (4, 17) at (4, 16) input: (42 in y + x +Error: Bracket is not properly closed. + +PError.idr:5:17--5:18 + | + 5 | bar x = let y = (42 in y + x + | ^ -baz : Int -> Int -baz x = x 1/1: Building PError2 (PError2.idr) -Error: Lex error ComposeNotClosing (4, 17) (4, 18) at (4, 17) input: (42 in y + x +Error: Bracket is not properly closed. + +PError2.idr:5:18--5:19 + | + 5 | bar x = let y := (42 in y + x + | ^ -baz : Int -> Int -baz x = x diff --git a/tests/idris2/perror004/expected b/tests/idris2/perror004/expected index 26b909a21..e1cc5bbbf 100644 --- a/tests/idris2/perror004/expected +++ b/tests/idris2/perror004/expected @@ -1,3 +1,8 @@ 1/1: Building PError (PError.idr) -Error: Parse error at line 4:33: -Wrong number of 'with' arguments (next tokens: [symbol =, identifier x, identifier foo, identifier x, identifier y, symbol |, identifier True, symbol |, identifier True, symbol =]) +Error: Wrong number of 'with' arguments + +PError.idr:4:33--4:34 + | + 4 | foo x y | True | False | 10 = x + | ^ + diff --git a/tests/idris2/perror005/expected b/tests/idris2/perror005/expected index 68f034a5e..6c74070d4 100644 --- a/tests/idris2/perror005/expected +++ b/tests/idris2/perror005/expected @@ -1,3 +1,8 @@ 1/1: Building PError (PError.idr) -Error: Parse error at line 7:1: -Expected 'in' (next tokens: [identifier baz, symbol :, identifier Int, symbol ->, identifier Int, identifier baz, identifier x, symbol =, identifier x, end of input]) +Error: Expected 'in' + +PError.idr:7:1--7:2 + | + 7 | baz : Int -> Int + | ^ + diff --git a/tests/idris2/perror006/expected b/tests/idris2/perror006/expected index 5ecee7ed3..346576437 100644 --- a/tests/idris2/perror006/expected +++ b/tests/idris2/perror006/expected @@ -1,3 +1,8 @@ 1/1: Building PError (PError.idr) -Error: Parse error at line 7:1: -Expected 'else' (next tokens: [identifier baz, symbol :, identifier Int, symbol ->, identifier Int, identifier baz, identifier x, symbol =, identifier x, end of input]) +Error: Expected 'else' + +PError.idr:7:1--7:2 + | + 7 | baz : Int -> Int + | ^ +