feat: forbid non-reserved identifiers via withForbidden (#14432)

This PR makes `withForbidden` stop a term at a non-reserved word used as
an identifier, not just at a registered token. A parser like
`withForbidden "invariant" termParser` now ends the term when it reaches
a bare `invariant`, while `invariant` remains usable as an identifier
everywhere else.

`identFn` rejects an identifier whose text is in `forbiddenTks`,
mirroring the forbidden-token check in `mkTokenAndFixPos`. The check is
guarded by `forbiddenTks.isEmpty`, so the common identifier path is
unchanged.
We considered putting a unified check in `tokenFn` or `mkIdResult`, but
decided against that. The former would move the check outside the cache
and regress some benchmarks by ~1%. The latter forces a flag on
`mkIdResult` and `identFnAux` because `nameLitAux` and `rawLitFn` must
not forbid any tokens.

Author: sgraf812

src/Lean/Parser/Basic.lean

@@ -1295,7 +1295,20 @@ def nameLitNoAntiquot : Parser := {
   info := mkAtomicInfo "name"
 }
 
-def identFn : ParserFn := expectTokenFn identKind "identifier"
+def identFn : ParserFn := fun c s =>
+  if c.forbiddenTks.isEmpty then
+    expectTokenFn identKind "identifier" c s
+  else
+    -- A forbidden token used as an identifier (e.g. a non-reserved clause keyword like
+    -- `invariant`) stops the enclosing term, mirroring `mkTokenAndFixPos`.
+    let iniSz  := s.stackSize
+    let iniPos := s.pos
+    let s := expectTokenFn identKind "identifier" c s
+    if s.hasError then s
+    else match s.stxStack.back with
+      | .ident _ rawVal _ _ =>
+        if c.forbiddenTks.contains rawVal.toString then s.mkErrorAt "forbidden token" iniPos iniSz else s
+      | _ => s
 
 def identNoAntiquot : Parser := {
   fn   := identFn

tests/elab/forbiddenIdentifiers.lean

@@ -0,0 +1,30 @@
+import Lean
+/-!
+`withForbidden` stops a term at a non-reserved word used as a bare identifier, while the word
+stays usable as an identifier (escaped, projected, or a plain declaration name).
+-/
+open Lean Elab Command Parser
+
+namespace ForbiddenIdentTest
+
+-- `#collect e sep e'` parses `e` with the non-reserved word `sep` forbidden, so a bare `sep`
+-- ends `e` without `sep` being a reserved keyword.
+@[command_parser]
+def collectCmd : Parser := leading_parser
+  "#collect " >> withForbidden "sep" termParser >> nonReservedSymbol "sep" >> ppSpace >> termParser
+
+@[command_elab collectCmd]
+def elabCollect : CommandElab := fun _ => pure ()
+
+-- A bare `sep` ends the first term (requires the forbidding; else `a sep` is an application).
+#collect a sep b
+-- A multi-token first term still stops at the bare `sep`.
+#collect f a sep b
+-- Escaped `«sep»` is not forbidden: it is consumed as the first term.
+#collect «sep» sep b
+-- A projection `.sep` (rawIdent path) is not forbidden.
+#collect (id x).sep sep b
+-- The word remains usable as an ordinary identifier.
+def sep : Nat := 0
+
+end ForbiddenIdentTest