feat: improve error messages for ambiguous 3.toDecmial syntax (#10488)

This PR changes the way that scientific numerals are parsed in order to
give better error messages for (invalid) syntax like `32.succ`.

Example:

```lean4
#check 32.succ
```

Before, the error message is:

```
unexpected identifier; expected command
```

This is because `32.` parses as a complete float, and `#check 32.`
parses as a complete command, so `succ` is being read as the start of a
new command.

With this change, the error message will move from the `succ` token to
the `32` token (which isn't totally ideal from my perspective) but gives
a less misleading error message and corresponding suggestion:

```
unexpected identifier after decimal point; consider parenthesizing the number
```

Author: robsimmons

src/Lean/Parser/Basic.lean

@@ -845,8 +845,8 @@ def decimalNumberFn (startPos : String.Pos) (includeWhitespace := true)
       mkNodeToken numLitKind startPos includeWhitespace c s
 where
   parseScientific s :=
-    let s := parseOptDot s
-    let s := parseOptExp s
+    let (s, hasBareDot) := parseOptDot s
+    let s := parseOptExp s hasBareDot
     mkNodeToken scientificLitKind startPos includeWhitespace c s
 
   parseOptDot s :=
@@ -856,25 +856,30 @@ where
       let i    := c.next i
       let curr := c.get i
       if curr.isDigit then
-        takeDigitsFn (fun c => c.isDigit) "decimal number" false c (s.setPos i)
+        (takeDigitsFn (fun c => c.isDigit) "decimal number" false c (s.setPos i), false)
       else
-        s.setPos i
+        (s.setPos i, true)
     else
-      s
+      (s, false)
 
-  parseOptExp s :=
-    let i     := s.pos
-    let curr  := c.get i
-    if curr == 'e' || curr == 'E' then
-      let i    := c.next i
-      let i    := if c.get i == '-' || c.get i == '+' then c.next i else i
-      let curr := c.get i
-      if curr.isDigit then
-        takeDigitsFn (fun c => c.isDigit) "decimal number" false c (s.setPos i)
-      else
-        s.mkUnexpectedError "missing exponent digits in scientific literal"
-    else
+  parseOptExp s hasBareDot :=
+    if h : c.atEnd s.pos then
       s
+    else
+      let i     := s.pos
+      let curr  := c.get' i h
+      if curr == 'e' || curr == 'E' then
+        let i    := c.next i
+        let i    := if c.get i == '-' || c.get i == '+' then c.next i else i
+        let curr := c.get i
+        if curr.isDigit then
+          takeDigitsFn (fun c => c.isDigit) "decimal number" false c (s.setPos i)
+        else
+          s.mkUnexpectedError "missing exponent digits in scientific literal"
+      else if hasBareDot && isIdFirst curr then
+          (s.setPos startPos).mkUnexpectedError s!"unexpected identifier after decimal point; consider parenthesizing the number"
+      else
+        s
 
 def binNumberFn (startPos : String.Pos) (includeWhitespace := true) : ParserFn := fun c s =>
   let s := takeDigitsFn (fun c => c == '0' || c == '1') "binary number" true c s

tests/lean/10488.lean

@@ -0,0 +1,53 @@
+#eval (1,(2,3)).2.fst
+
+#check 31.
+#check 31.0
+#eval 31.
+#eval 31.0
+
+#check 31.e
+#check 31.ee
+
+#check 31.f
+#check 31.ff
+
+#check 31.3e
+#check 31.3e2
+#check 31.3ee2
+
+#check 31.3f
+#check 31.3f2
+#check 31.3ff2
+
+#check 11.toDigits 13
+#check (11).toDigits 13
+#eval  (11).toDigits 13
+#check (11).toDigits(13)
+#check (11).toDigits (13)
+
+def succ (a: Nat) := a + 1
+def foo {A B} (_: A) (_: B) : Unit := ()
+#check foo 31.succ
+#check foo (31).succ
+#check foo 31(.succ)
+#check foo (31)(.succ)
+#check foo 31 .succ
+#check foo 31. succ
+
+#check 11succ
+#check 11.succ
+#check 11.12succ
+#check (11.succ)
+#check (11.12succ)
+
+
+-- This example (adapted from structInst4.lean) exercises the difference betwee
+-- term parsing and LVal parsing; the latter fails if we allow `2.snd` to parse
+-- as a scientificLit followed by an error token, so this test captures
+-- that we have to throw the error token right away, positioned before, rather
+-- than after the `2.`
+structure Foo where
+  (x : Nat × (Nat × Nat) := (2, (4, 5)))
+def bar : Foo := {}
+#check bar.x.2.snd
+#eval { bar with x.2.snd := 1 }

tests/lean/10488.lean.expected.out

@@ -0,0 +1,43 @@
+2
+31. : Float
+31.0 : Float
+31.000000
+31.000000
+10488.lean:8:10: error: missing exponent digits in scientific literal
+10488.lean:9:10: error: missing exponent digits in scientific literal
+10488.lean:11:7: error: unexpected identifier after decimal point; consider parenthesizing the number
+10488.lean:12:7: error: unexpected identifier after decimal point; consider parenthesizing the number
+10488.lean:14:11: error: missing exponent digits in scientific literal
+313e1 : Float
+10488.lean:16:11: error: missing exponent digits in scientific literal
+31.3 : Float
+10488.lean:18:11-18:12: error: unexpected identifier; expected command
+31.3 : Float
+10488.lean:19:11-19:13: error: unexpected identifier; expected command
+31.3 : Float
+10488.lean:20:11-20:14: error: unexpected identifier; expected command
+10488.lean:22:7: error: unexpected identifier after decimal point; consider parenthesizing the number
+Nat.toDigits 11 13 : List Char
+['1', '2']
+Nat.toDigits 11 : Nat → List Char
+10488.lean:25:20-25:21: error: unexpected token '('; expected command
+Nat.toDigits 11 13 : List Char
+foo.{u_1, u_2} {A : Sort u_1} {B : Sort u_2} : A → B → Unit
+10488.lean:30:11: error: unexpected identifier after decimal point; consider parenthesizing the number
+foo (Nat.succ 31) : ?m → Unit
+foo 31 : ?m → Unit
+10488.lean:32:13-32:14: error: unexpected token '('; expected command
+foo 31 : ?m → Unit
+10488.lean:33:15-33:16: error: unexpected token '('; expected command
+10488.lean:34:14-34:19: error(lean.invalidDottedIdent): Invalid dotted identifier notation: The expected type of `.succ` could not be determined
+foo 31 sorry : Unit
+foo 31. succ : Unit
+11 : Nat
+10488.lean:37:9-37:13: error: unexpected identifier; expected command
+10488.lean:38:7: error: unexpected identifier after decimal point; consider parenthesizing the number
+11.12 : Float
+10488.lean:39:12-39:16: error: unexpected identifier; expected command
+10488.lean:40:8: error: unexpected identifier after decimal point; consider parenthesizing the number
+10488.lean:41:13-41:17: error: unexpected identifier; expected ')', ',' or ':'
+bar.x.snd.snd : Nat
+{ x := (2, 4, 1) }

tests/lean/run/6199.lean

@@ -46,8 +46,8 @@ Scientific tests
 #guard_msgs in #term "100_000.0"
 /-- info: 0. : Float -/
 #guard_msgs in #term "0."
--- The decimal parser requires a digit at the start, so the `_` is left over:
-/-- error: <input>:1:4: expected end of input -/
+-- The decimal parser requires a digit at the start, so the `_` is left over and read as a distinct identifier:
+/-- error: <input>:1:0: unexpected identifier after decimal point; consider parenthesizing the number -/
 #guard_msgs in #term "100._"
 /-- info: 100.111111 : Float -/
 #guard_msgs in #term "100.111_111"