Improve parse error report

Signed-off-by: Andy Lok <andylokandy@hotmail.com>

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

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)

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)

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

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 : ())
+   | ^
+

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

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

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

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
+   |                                 ^
+

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
+   | ^
+

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
+   | ^
+