From c67686132aba98b87cdb85f62ec2d53c9d575103 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 8 Aug 2023 14:00:08 +0200
Subject: [PATCH] feat: include unexpected token in error message

---
 src/Lean/Parser/Module.lean                        |  4 +++-
 src/Lean/Parser/Types.lean                         |  6 +++++-
 tests/lean/1606.lean.expected.out                  |  6 +++---
 tests/lean/1705.lean.expected.out                  |  2 +-
 tests/lean/1707.lean.expected.out                  |  2 +-
 tests/lean/1760.lean.expected.out                  |  2 +-
 tests/lean/1971.lean                               |  4 ++++
 tests/lean/1971.lean.expected.out                  | 11 ++++++-----
 tests/lean/348.lean.expected.out                   |  2 +-
 tests/lean/361.lean.expected.out                   |  2 +-
 tests/lean/689.lean.expected.out                   |  2 +-
 tests/lean/StxQuot.lean.expected.out               |  4 ++--
 tests/lean/antiquotRecovery.lean.expected.out      |  2 +-
 tests/lean/byStrictIndent.lean.expected.out        |  4 ++--
 tests/lean/commandPrefix.lean.expected.out         |  2 +-
 tests/lean/exitAfterParseError.lean.expected.out   |  2 +-
 tests/lean/have.lean.expected.out                  |  2 +-
 tests/lean/letArrowOutsideDo.lean.expected.out     |  2 +-
 tests/lean/linterUnusedVariables.lean.expected.out |  2 +-
 tests/lean/nonReserved.lean.expected.out           |  2 +-
 tests/lean/partialVariable.lean.expected.out       |  2 +-
 tests/lean/precissues.lean.expected.out            |  6 +++---
 tests/lean/scientific.lean.expected.out            |  6 +++---
 tests/lean/semicolonOrLinebreak.lean.expected.out  |  4 ++--
 tests/lean/syntaxPrec.lean.expected.out            |  2 +-
 25 files changed, 48 insertions(+), 37 deletions(-)

diff --git a/src/Lean/Parser/Module.lean b/src/Lean/Parser/Module.lean
index 5d1ad14929..34ecb46c58 100644
--- a/src/Lean/Parser/Module.lean
+++ b/src/Lean/Parser/Module.lean
@@ -34,7 +34,9 @@ structure ModuleParserState where
 
 private def mkErrorMessage (c : InputContext) (s : ParserState) (e : Parser.Error) : Message := Id.run do
   let mut pos := c.fileMap.toPosition s.pos
-  if e.stopPos?.isSome then
+  -- if there is an unexpected token, include preceding whitespace as well as the expected token could
+  -- be inserted at any of these places to fix the error; see tests/lean/1971.lean
+  if !e.unexpected.isEmpty && e.stopPos?.isSome then
     if let .original (trailing := trailing) .. := s.stxStack.back.getTailInfo then
       if trailing.stopPos == s.pos then
         pos := c.fileMap.toPosition trailing.startPos
diff --git a/src/Lean/Parser/Types.lean b/src/Lean/Parser/Types.lean
index 5484f007a3..f3d15f9843 100644
--- a/src/Lean/Parser/Types.lean
+++ b/src/Lean/Parser/Types.lean
@@ -293,7 +293,11 @@ def mkErrorAt (s : ParserState) (msg : String) (pos : String.Pos) (initStackSz?
 def mkUnexpectedTokenErrors (s : ParserState) (ex : List String) : ParserState :=
   let tk := s.stxStack.back
   let s := s.setPos tk.getPos?.get!
-  let s := s.setError { stopPos? := tk.getTailPos?, expected := ex }
+  let unexpected := match tk with
+    | .ident .. => "unexpected identifier"
+    | .atom _ v => s!"unexpected token '{v}'"
+    | _         => "unexpected token"  -- TODO: categorize (custom?) literals as well?
+  let s := s.setError { stopPos? := tk.getTailPos?, expected := ex, unexpected }
   s.popSyntax.pushSyntax .missing
 
 /--
diff --git a/tests/lean/1606.lean.expected.out b/tests/lean/1606.lean.expected.out
index a56bccaee0..bfa73dfc55 100644
--- a/tests/lean/1606.lean.expected.out
+++ b/tests/lean/1606.lean.expected.out
@@ -1,9 +1,9 @@
 1606.lean:1:18-2:6: error: unsolved goals
 ⊢ True
-1606.lean:3:4: error: expected command
+1606.lean:3:4-3:8: error: unexpected identifier; expected command
 1606.lean:8:18-10:8: error: unsolved goals
 ⊢ True
-1606.lean:11:4: error: expected command
+1606.lean:11:4-11:14: error: unexpected identifier; expected command
 1606.lean:19:18-21:14: error: unsolved goals
 ⊢ True
-1606.lean:22:4: error: expected command
+1606.lean:22:4-22:14: error: unexpected identifier; expected command
diff --git a/tests/lean/1705.lean.expected.out b/tests/lean/1705.lean.expected.out
index e3e946eeba..3f3dd8b54d 100644
--- a/tests/lean/1705.lean.expected.out
+++ b/tests/lean/1705.lean.expected.out
@@ -2,4 +2,4 @@
   T
 term has type
   ?m
-1705.lean:1:18: error: expected command
+1705.lean:1:18-1:19: error: unexpected identifier; expected command
diff --git a/tests/lean/1707.lean.expected.out b/tests/lean/1707.lean.expected.out
index 09f980e684..c47071f7ba 100644
--- a/tests/lean/1707.lean.expected.out
+++ b/tests/lean/1707.lean.expected.out
@@ -1,2 +1,2 @@
 1707.lean:1:9-1:12: error: invalid field index
-1707.lean:1:12: error: expected command
+1707.lean:1:12-1:13: error: unexpected identifier; expected command
diff --git a/tests/lean/1760.lean.expected.out b/tests/lean/1760.lean.expected.out
index 0472ebebd0..7b711fdba2 100644
--- a/tests/lean/1760.lean.expected.out
+++ b/tests/lean/1760.lean.expected.out
@@ -1,2 +1,2 @@
-1760.lean:3:0: error: expected ':', ']' or term
+1760.lean:2:31-3:6: error: unexpected token '#check'; expected ':', ']' or term
 () : Unit
diff --git a/tests/lean/1971.lean b/tests/lean/1971.lean
index d716b08cb2..5b473db350 100644
--- a/tests/lean/1971.lean
+++ b/tests/lean/1971.lean
@@ -39,3 +39,7 @@ example := 0
 set_option pp.all
 
 example := 0
+
+/-! Do not shift other kinds of errors. -/
+
+example := "a
diff --git a/tests/lean/1971.lean.expected.out b/tests/lean/1971.lean.expected.out
index 3f93841972..c383f7f5e6 100644
--- a/tests/lean/1971.lean.expected.out
+++ b/tests/lean/1971.lean.expected.out
@@ -1,5 +1,6 @@
-1971.lean:14:7-16:7: error: expected term
-1971.lean:22:6-24:3: error: expected ':=', 'where' or '|'
-1971.lean:30:9-30:13: error: expected term
-1971.lean:34:9-36:7: error: expected identifier
-1971.lean:39:17-41:7: error: expected 'false', 'true', numeral or string literal
+1971.lean:14:7-16:7: error: unexpected token 'theorem'; expected term
+1971.lean:22:6-24:3: error: unexpected token 'def'; expected ':=', 'where' or '|'
+1971.lean:30:9-30:13: error: unexpected token 'def'; expected term
+1971.lean:34:9-36:7: error: unexpected token 'example'; expected identifier
+1971.lean:39:17-41:7: error: unexpected token 'example'; expected 'false', 'true', numeral or string literal
+1971.lean:45:11: error: unterminated string literal
diff --git a/tests/lean/348.lean.expected.out b/tests/lean/348.lean.expected.out
index 4abed64a94..cc7ea95c77 100644
--- a/tests/lean/348.lean.expected.out
+++ b/tests/lean/348.lean.expected.out
@@ -1 +1 @@
-348.lean:3:24: error: expected ')'
+348.lean:3:24-3:25: error: unexpected token '⟩'; expected ')'
diff --git a/tests/lean/361.lean.expected.out b/tests/lean/361.lean.expected.out
index 18ab15f98c..136be26e5a 100644
--- a/tests/lean/361.lean.expected.out
+++ b/tests/lean/361.lean.expected.out
@@ -1,4 +1,4 @@
-361.lean:3:0: error: expected '{' or tactic
+361.lean:1:62-3:7: error: unexpected token 'theorem'; expected '{' or tactic
 361.lean:1:60-1:62: error: unsolved goals
 p q r : Prop
 h1 : p ∨ q
diff --git a/tests/lean/689.lean.expected.out b/tests/lean/689.lean.expected.out
index f6d662944f..21e4095d3f 100644
--- a/tests/lean/689.lean.expected.out
+++ b/tests/lean/689.lean.expected.out
@@ -1,2 +1,2 @@
-689.lean:4:0: error: expected '|'
+689.lean:2:14-4:7: error: unexpected token 'section'; expected '|'
 689.lean:9:0: error: unexpected end of input; expected '{'
diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out
index 73d8f660ac..eccd273053 100644
--- a/tests/lean/StxQuot.lean.expected.out
+++ b/tests/lean/StxQuot.lean.expected.out
@@ -1,4 +1,4 @@
-StxQuot.lean:8:12: error: expected identifier or term
+StxQuot.lean:8:12-8:13: error: unexpected token ')'; expected identifier or term
 "`Nat.one._@.UnhygienicMain._hyg.1"
 "<missing>"
 "<missing>"
@@ -6,7 +6,7 @@ StxQuot.lean:8:12: error: expected identifier or term
 "(«term_+_» <missing> \"+\" (num \"1\"))"
 "(«term_+_» <missing> \"+\" (num \"1\"))"
 "(«term_+_» (num \"1\") \"+\" (num \"1\"))"
-StxQuot.lean:19:15: error: expected term
+StxQuot.lean:19:15-19:16: error: unexpected token ']'; expected term
 "(Term.fun \"fun\" (Term.basicFun [`a._@.UnhygienicMain._hyg.1] [] \"=>\" `a._@.UnhygienicMain._hyg.1))"
 "(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n  \"def\"\n  (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n  (Command.optDeclSig [] [])\n  (Command.declValSimple \":=\" (num \"1\") [])\n  []\n  []\n  []))"
 "[(Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (num \"1\") [])\n   []\n   []\n   []))\n (Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (num \"2\") [])\n   []\n   []\n   []))]"
diff --git a/tests/lean/antiquotRecovery.lean.expected.out b/tests/lean/antiquotRecovery.lean.expected.out
index e336434091..d810f5d945 100644
--- a/tests/lean/antiquotRecovery.lean.expected.out
+++ b/tests/lean/antiquotRecovery.lean.expected.out
@@ -1 +1 @@
-antiquotRecovery.lean:5:18: error: expected ')'
+antiquotRecovery.lean:5:17-5:19: error: unexpected token '$'; expected ')'
diff --git a/tests/lean/byStrictIndent.lean.expected.out b/tests/lean/byStrictIndent.lean.expected.out
index 6765b63fc3..5c57943f85 100644
--- a/tests/lean/byStrictIndent.lean.expected.out
+++ b/tests/lean/byStrictIndent.lean.expected.out
@@ -15,10 +15,10 @@ n : Nat
 h : n > 0
 helper : n > 1
 ⊢ n > 1
-byStrictIndent.lean:19:3: error: expected command
+byStrictIndent.lean:19:3-19:8: error: unexpected token 'sorry'; expected command
 byStrictIndent.lean:22:54-24:9: error: unsolved goals
 n : Nat
 h : n > 0
 helper : n > 1
 ⊢ n > 1
-byStrictIndent.lean:25:6: error: expected command
+byStrictIndent.lean:25:6-25:11: error: unexpected token 'sorry'; expected command
diff --git a/tests/lean/commandPrefix.lean.expected.out b/tests/lean/commandPrefix.lean.expected.out
index 980ce9984b..b9a65fc994 100644
--- a/tests/lean/commandPrefix.lean.expected.out
+++ b/tests/lean/commandPrefix.lean.expected.out
@@ -1,3 +1,3 @@
 let_fun this := ();
 this : Id Unit
-commandPrefix.lean:3:0: error: expected command
+commandPrefix.lean:3:0-3:4: error: unexpected identifier; expected command
diff --git a/tests/lean/exitAfterParseError.lean.expected.out b/tests/lean/exitAfterParseError.lean.expected.out
index 3a659731bf..619c1e8c62 100644
--- a/tests/lean/exitAfterParseError.lean.expected.out
+++ b/tests/lean/exitAfterParseError.lean.expected.out
@@ -1,2 +1,2 @@
-exitAfterParseError.lean:5:0: error: expected ':=', 'where' or '|'
+exitAfterParseError.lean:3:7-5:5: error: unexpected token '#exit'; expected ':=', 'where' or '|'
 exitAfterParseError.lean:5:0-5:5: warning: using 'exit' to interrupt Lean
diff --git a/tests/lean/have.lean.expected.out b/tests/lean/have.lean.expected.out
index 2265fae1b7..bf1f9f98a4 100644
--- a/tests/lean/have.lean.expected.out
+++ b/tests/lean/have.lean.expected.out
@@ -1,4 +1,4 @@
-have.lean:4:0: error: expected term
+have.lean:2:19-4:7: error: unexpected token 'example'; expected term
 have.lean:2:18-2:19: error: don't know how to synthesize placeholder
 context:
 ⊢ False
diff --git a/tests/lean/letArrowOutsideDo.lean.expected.out b/tests/lean/letArrowOutsideDo.lean.expected.out
index 12d0a1aafa..9e9450b355 100644
--- a/tests/lean/letArrowOutsideDo.lean.expected.out
+++ b/tests/lean/letArrowOutsideDo.lean.expected.out
@@ -1 +1 @@
-letArrowOutsideDo.lean:2:8: error: expected ':=' or '|'
+letArrowOutsideDo.lean:2:7-2:9: error: unexpected token '←'; expected ':=' or '|'
diff --git a/tests/lean/linterUnusedVariables.lean.expected.out b/tests/lean/linterUnusedVariables.lean.expected.out
index b55d1ad6a2..b36b23ebfa 100644
--- a/tests/lean/linterUnusedVariables.lean.expected.out
+++ b/tests/lean/linterUnusedVariables.lean.expected.out
@@ -38,7 +38,7 @@ a : Nat
 ⊢ Nat
 linterUnusedVariables.lean:227:0-227:7: warning: declaration uses 'sorry'
 linterUnusedVariables.lean:228:0-228:7: warning: declaration uses 'sorry'
-linterUnusedVariables.lean:231:0: error: expected '{' or tactic
+linterUnusedVariables.lean:229:29-231:7: error: unexpected token 'theorem'; expected '{' or tactic
 linterUnusedVariables.lean:229:27-229:29: error: unsolved goals
 bar : ?m
 bar' : Nat → Nat
diff --git a/tests/lean/nonReserved.lean.expected.out b/tests/lean/nonReserved.lean.expected.out
index 1469fad61e..95536ab6bb 100644
--- a/tests/lean/nonReserved.lean.expected.out
+++ b/tests/lean/nonReserved.lean.expected.out
@@ -1,2 +1,2 @@
 10 : Nat
-nonReserved.lean:11:11: error: expected 'bla'
+nonReserved.lean:11:10-11:14: error: unexpected identifier; expected 'bla'
diff --git a/tests/lean/partialVariable.lean.expected.out b/tests/lean/partialVariable.lean.expected.out
index ef9db114f9..9c5d039376 100644
--- a/tests/lean/partialVariable.lean.expected.out
+++ b/tests/lean/partialVariable.lean.expected.out
@@ -1 +1 @@
-partialVariable.lean:1:9: error: expected '(', '[', '{' or '⦃'
+partialVariable.lean:1:8-1:10: error: unexpected token ':'; expected '(', '[', '{' or '⦃'
diff --git a/tests/lean/precissues.lean.expected.out b/tests/lean/precissues.lean.expected.out
index 3dd4b22ee6..f36d0ce034 100644
--- a/tests/lean/precissues.lean.expected.out
+++ b/tests/lean/precissues.lean.expected.out
@@ -4,9 +4,9 @@ f 1 fun x => x : Nat
 0 : Nat
 f 1 fun x => x : Nat
 id.{u} {α : Sort u} (a : α) : α
-precissues.lean:15:10: error: expected command
+precissues.lean:15:10-15:14: error: unexpected token 'have'; expected command
 id.{u} {α : Sort u} (a : α) : α
-precissues.lean:17:10: error: expected command
+precissues.lean:17:10-17:13: error: unexpected token 'let'; expected command
 1 : Nat
 id
   (let_fun this := True.intro;
@@ -27,4 +27,4 @@ p ∧ ¬q : Prop
 id ¬p : Prop
 Nat → ∀ (a : Nat), a = a : Prop
 id.{u} {α : Sort u} (a : α) : α
-precissues.lean:41:10: error: expected command
+precissues.lean:41:10-41:14: error: unexpected token 'foo!'; expected command
diff --git a/tests/lean/scientific.lean.expected.out b/tests/lean/scientific.lean.expected.out
index 28b77df7e3..2f1396f521 100644
--- a/tests/lean/scientific.lean.expected.out
+++ b/tests/lean/scientific.lean.expected.out
@@ -9,11 +9,11 @@
 123000.000000
 -8.534000
 scientific.lean:14:6-14:7: error: invalid occurrence of `·` notation, it must be surrounded by parentheses (e.g. `(· + 1)`)
-scientific.lean:14:7: error: expected command
+scientific.lean:14:7-14:10: error: unexpected token; expected command
 scientific.lean:15:6-15:7: error: invalid occurrence of `·` notation, it must be surrounded by parentheses (e.g. `(· + 1)`)
-scientific.lean:15:7: error: expected command
+scientific.lean:15:7-15:12: error: unexpected token; expected command
 scientific.lean:16:6-16:7: error: invalid occurrence of `·` notation, it must be surrounded by parentheses (e.g. `(· + 1)`)
-scientific.lean:16:7: error: expected command
+scientific.lean:16:7-16:16: error: unexpected token; expected command
 scientific.lean:19:6-19:7: error: unknown identifier 'e'
 scientific.lean:19:0-19:9: error: cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors
 scientific.lean:20:9: error: missing exponent digits in scientific literal
diff --git a/tests/lean/semicolonOrLinebreak.lean.expected.out b/tests/lean/semicolonOrLinebreak.lean.expected.out
index 441cf6f5ba..0f49c49dae 100644
--- a/tests/lean/semicolonOrLinebreak.lean.expected.out
+++ b/tests/lean/semicolonOrLinebreak.lean.expected.out
@@ -1,4 +1,4 @@
 semicolonOrLinebreak.lean:2:12: error: expected ';' or line break
 semicolonOrLinebreak.lean:9:31-10:8: error: fields missing: 'y'
-semicolonOrLinebreak.lean:10:8: error: expected command
-semicolonOrLinebreak.lean:20:8: error: expected ':'
+semicolonOrLinebreak.lean:10:8-10:9: error: unexpected identifier; expected command
+semicolonOrLinebreak.lean:20:7-20:9: error: unexpected token '}'; expected ':'
diff --git a/tests/lean/syntaxPrec.lean.expected.out b/tests/lean/syntaxPrec.lean.expected.out
index 3e738002ff..d5bc121d47 100644
--- a/tests/lean/syntaxPrec.lean.expected.out
+++ b/tests/lean/syntaxPrec.lean.expected.out
@@ -1,4 +1,4 @@
-syntaxPrec.lean:1:18: error: expected ':'
+syntaxPrec.lean:1:17-1:21: error: unexpected token '<|>'; expected ':'
 [Elab.command] syntax "foo" ("*" <|> term,+) : term
   [Elab.command] @[term_parser 1000]
       def «termFoo*_» : Lean.ParserDescr✝ :=