feat: dot auto-completion for identifiers outside of terms

src/Init/Meta.lean

@@ -1095,6 +1095,10 @@ partial def findAux (p : Syntax → Bool) : Syntax → Option Syntax
 def find? (stx : Syntax) (p : Syntax → Bool) : Option Syntax :=
   findAux p stx
 
+def hasDanglingDot : Syntax → Bool
+  | .ident _ raw _ _ => raw.toString.endsWith "."
+  | _ => false
+
 end Syntax
 
 namespace TSyntax

src/Init/Notation.lean

@@ -462,7 +462,7 @@ namespace Lean
 `binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding
 position, where `_` means that the value should be left unnamed and inaccessible.
 -/
-syntax binderIdent := ident <|> hole
+syntax binderIdent := ident <|> hole -- TODO after stage0 update: use `identBeforeDot`
 
 namespace Parser.Tactic
 

src/Lean/Elab/Print.lean

@@ -180,7 +180,7 @@ private def printIdCore (id : Name) : CommandElabM Unit := do
   | none => throwUnknownId id
 
 private def printId (id : Syntax) : CommandElabM Unit := do
-  addCompletionInfo <| CompletionInfo.id id id.getId (danglingDot := false) {} none
+  addCompletionInfo <| CompletionInfo.id id id.getId id.hasDanglingDot {} none
   let cs ← liftCoreM <| realizeGlobalConstWithInfos id
   cs.forM printIdCore
 

src/Lean/Elab/Term.lean

@@ -1955,7 +1955,7 @@ private def mkConsts (candidates : List (Name × List String)) (explicitLevels :
     return (const, projs) :: result
 
 def resolveName (stx : Syntax) (n : Name) (preresolved : List Syntax.Preresolved) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (List (Expr × List String)) := do
-  addCompletionInfo <| CompletionInfo.id stx stx.getId (danglingDot := false) (← getLCtx) expectedType?
+  addCompletionInfo <| CompletionInfo.id stx stx.getId stx.hasDanglingDot (← getLCtx) expectedType?
   if let some (e, projs) ← resolveLocalName n then
     unless explicitLevels.isEmpty do
       throwError "invalid use of explicit universe parameters, '{e}' is a local variable"

src/Lean/Parser.lean

@@ -30,6 +30,7 @@ builtin_initialize
   register_parser_alias (kind := nameLitKind) "name" nameLit
   register_parser_alias (kind := scientificLitKind) "scientific" scientificLit
   register_parser_alias (kind := identKind) ident
+  register_parser_alias (kind := identKind) "identBeforeDot" identBeforeDot
   register_parser_alias (kind := hygieneInfoKind) hygieneInfo
   register_parser_alias "colGt" checkColGt { stackSz? := some 0 }
   register_parser_alias "colGe" checkColGe { stackSz? := some 0 }

src/Lean/Parser/Basic.lean

@@ -951,7 +951,7 @@ def mkIdResult (startPos : String.Pos) (tk : Option Token) (val : Name) : Parser
     mkTokenAndFixPos startPos tk c s
   else
     let input           := c.input
-    let rawVal          := { str := input, startPos := startPos, stopPos := stopPos  : Substring }
+    let rawVal          := { str := input, startPos := startPos, stopPos := stopPos : Substring }
     let s               := whitespace c s
     let trailingStopPos := s.pos
     let leading         := mkEmptySubstringAt input startPos
@@ -1274,7 +1274,26 @@ def nameLitNoAntiquot : Parser := {
   info := mkAtomicInfo "name"
 }
 
-def identFn : ParserFn := expectTokenFn identKind "identifier"
+def identBeforeDotFn : ParserFn := expectTokenFn identKind "identifier"
+
+def identBeforeDotNoAntiquot : Parser := {
+  fn   := identBeforeDotFn
+  info := mkAtomicInfo "ident"
+}
+
+def identFn : ParserFn := fun c s =>
+  let s := expectTokenFn identKind "identifier" c s
+  match s.stxStack.back with
+  | .ident (.original l p _ p') { str, startPos, stopPos } nm pre =>
+    if c.input.get p' == '.' then
+      let endPos := stopPos + '.'
+      let s := whitespace c { s with pos := endPos }
+      let stx' : Syntax := .ident (.original l p { str, startPos := endPos, stopPos := s.pos } endPos)
+        { str, startPos, stopPos := endPos } nm pre
+      (s.popSyntax.pushSyntax stx').mkUnexpectedError "incomplete identifier"
+    else
+      s
+  | _ => s
 
 def identNoAntiquot : Parser := {
   fn   := identFn
@@ -1752,7 +1771,7 @@ def pushNone : Parser := {
 
 -- We support three kinds of antiquotations: `$id`, `$_`, and `$(t)`, where `id` is a term identifier and `t` is a term.
 def antiquotNestedExpr : Parser := node `antiquotNestedExpr (symbolNoAntiquot "(" >> decQuotDepth termParser >> symbolNoAntiquot ")")
-def antiquotExpr : Parser       := identNoAntiquot <|> symbolNoAntiquot "_" <|> antiquotNestedExpr
+def antiquotExpr : Parser       := identBeforeDotNoAntiquot <|> symbolNoAntiquot "_" <|> antiquotNestedExpr
 
 def tokenAntiquotFn : ParserFn := fun c s => Id.run do
   if s.hasError then

src/Lean/Parser/Command.lean

@@ -88,7 +88,7 @@ such as inductive constructors, structure projections, and `let rec` / `where` d
 /-- `declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names -/
 -- @[builtin_doc] -- FIXME: suppress the hover
 def declId := leading_parser
-  ident >> optional (".{" >> sepBy1 (recover ident (skipUntil (fun c => c.isWhitespace || c ∈ [',', '}']))) ", " >> "}")
+  identBeforeDot >> optional (".{" >> sepBy1 (recover ident (skipUntil (fun c => c.isWhitespace || c ∈ [',', '}']))) ", " >> "}")
 /-- `declSig` matches the signature of a declaration with required type: a list of binders and then `: type` -/
 -- @[builtin_doc] -- FIXME: suppress the hover
 def declSig := leading_parser

src/Lean/Parser/Extra.lean

@@ -73,12 +73,15 @@ You can use `TSyntax.getId` to extract the name from the resulting syntax object
 @[run_builtin_parser_attribute_hooks, builtin_doc] def ident : Parser :=
   withAntiquot (mkAntiquot "ident" identKind) identNoAntiquot
 
+@[run_builtin_parser_attribute_hooks, builtin_doc] def identBeforeDot : Parser :=
+  withAntiquot (mkAntiquot "ident" identKind) identBeforeDotNoAntiquot
+
 -- `optional (checkNoWsBefore >> "." >> checkNoWsBefore >> ident)`
 -- can never fully succeed but ensures that the identifier
 -- produces a partial syntax that contains the dot.
 -- The partial syntax is sometimes useful for dot-auto-completion.
 @[run_builtin_parser_attribute_hooks, builtin_doc] def identWithPartialTrailingDot :=
-  ident >> optional (checkNoWsBefore >> "." >> checkNoWsBefore >> ident)
+  identBeforeDot >> optional (checkNoWsBefore >> "." >> checkNoWsBefore >> identBeforeDot)
 
 -- `ident` and `rawIdent` produce the same syntax tree, so we reuse the antiquotation kind name
 @[run_builtin_parser_attribute_hooks, builtin_doc] def rawIdent : Parser :=

src/Lean/Parser/Term.lean

@@ -123,7 +123,7 @@ def optSemicolon (p : Parser) : Parser :=
 
 -- `checkPrec` necessary for the pretty printer
 @[builtin_term_parser] def ident :=
-  checkPrec maxPrec >> Parser.ident
+  checkPrec maxPrec >> Parser.identBeforeDot
 @[builtin_term_parser] def num : Parser :=
   checkPrec maxPrec >> numLit
 @[builtin_term_parser] def scientific : Parser :=
@@ -206,7 +206,7 @@ The delayed assigned metavariables themselves can be pretty printed using `set_o
 For more information, see the "Gruesome details" module docstrings in `Lean.MetavarContext`.
 -/
 @[builtin_term_parser] def syntheticHole := leading_parser
-  "?" >> (ident <|> "_")
+  "?" >> (identBeforeDot <|> "_")
 /--
 The `⋯` term denotes a term that was omitted by the pretty printer.
 The presence of `⋯` in pretty printer output is controlled by the `pp.deepTerms` and `pp.proofs` options,
@@ -217,7 +217,7 @@ However, in case it is copied and pasted from the Infoview, `⋯` logs a warning
 -/
 @[builtin_term_parser] def omission := leading_parser
   "⋯"
-def binderIdent : Parser  := ident <|> hole
+def binderIdent : Parser := identBeforeDot <|> hole
 /--
 The `sorry` term is a temporary placeholder for a missing proof or value.
 
@@ -267,7 +267,7 @@ Can also be used for creating simple functions when combined with `·`. Here are
   - `(h (· + 1) ·)` is shorthand for `fun x => h (fun y => y + 1) x`
   - also applies to other parentheses-like notations such as `(·, 1)`
 -/
-@[builtin_term_parser] def paren := leading_parser
+@[builtin_term_parser high] def paren := leading_parser
   "(" >> withoutPosition (withoutForbidden (ppDedentIfGrouped termParser)) >> ")"
 /--
 The *anonymous constructor* `⟨e, ...⟩` is equivalent to `c e ...` if the

src/Lean/PrettyPrinter/Formatter.lean

@@ -428,7 +428,7 @@ def unicodeSymbolNoAntiquot.formatter (sym asciiSym : String) : Formatter := do
     pushToken info asciiSym false
   goLeft
 
-@[combinator_formatter identNoAntiquot]
+@[combinator_formatter identNoAntiquot, combinator_formatter identBeforeDotNoAntiquot]
 def identNoAntiquot.formatter : Formatter := do
   checkKind identKind
   let stx@(Syntax.ident info _ id _) ← getCur

src/Lean/PrettyPrinter/Parenthesizer.lean

@@ -456,6 +456,7 @@ def trailingNode.parenthesizer (k : SyntaxNodeKind) (prec lhsPrec : Nat) (p : Pa
 @[combinator_parenthesizer unicodeSymbolNoAntiquot] def unicodeSymbolNoAntiquot.parenthesizer (_sym _asciiSym : String) := visitToken
 
 @[combinator_parenthesizer identNoAntiquot] def identNoAntiquot.parenthesizer := do checkKind identKind; visitToken
+@[combinator_parenthesizer identBeforeDotNoAntiquot] def identBeforeDotNoAntiquot.parenthesizer := do checkKind identKind; visitToken
 @[combinator_parenthesizer rawIdentNoAntiquot] def rawIdentNoAntiquot.parenthesizer := visitToken
 @[combinator_parenthesizer identEq] def identEq.parenthesizer (_id : Name) := visitToken
 @[combinator_parenthesizer nonReservedSymbolNoAntiquot] def nonReservedSymbolNoAntiquot.parenthesizer (_sym : String) (_includeIdent : Bool) := visitToken

src/Lean/Server/Completion/SyntheticCompletion.lean

@@ -88,7 +88,7 @@ private def findSyntheticIdentifierCompletion?
     none
   let some (id, danglingDot) :=
       match stx with
-      | `($id:ident) => some (id.getId, false)
+      | `($id:ident) => some (id.getId, id.raw.hasDanglingDot)
       | `($id:ident.) => some (id.getId, true)
       | _ => none
     | none

tests/lean/1781.lean

@@ -1,5 +1,5 @@
 import Lean.Elab.ElabRules
-syntax "kdef " ident (".{" ident,+ "}")? " : " term " := " term : command
+syntax "kdef " identBeforeDot (".{" ident,+ "}")? " : " term " := " term : command
 
 open Lean Elab Command Term in
 elab_rules : command | `(kdef $name $[.{ $levelParams?,* }]? : $type := $value) => do

tests/lean/interactive/completionAtPrint.lean

@@ -2,3 +2,6 @@ def f.gg := 0
 
 #print f.g
         --^ textDocument/completion
+
+#print f.
+       --^ textDocument/completion

tests/lean/interactive/completionAtPrint.lean.expected.out

@@ -10,3 +10,15 @@
     "id": {"const": {"declName": "f.gg"}},
     "cPos": 0}}],
  "isIncomplete": false}
+{"textDocument": {"uri": "file:///completionAtPrint.lean"},
+ "position": {"line": 5, "character": 9}}
+{"items":
+ [{"label": "gg",
+   "kind": 21,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionAtPrint.lean"},
+     "position": {"line": 5, "character": 9}},
+    "id": {"const": {"declName": "f.gg"}},
+    "cPos": 0}}],
+ "isIncomplete": false}

tests/lean/interactive/incrementalTactic.lean.expected.out

@@ -34,7 +34,7 @@ t 2
    "severity": 1,
    "range":
    {"start": {"line": 1, "character": 38}, "end": {"line": 4, "character": 3}},
-   "message": "unexpected token '/-!'; expected ')', '_', identifier or term",
+   "message": "unexpected token '/-!'; expected term",
    "fullRange":
    {"start": {"line": 1, "character": 38},
     "end": {"line": 4, "character": 3}}}]}

tests/lean/parserRecovery.lean.expected.out

@@ -36,7 +36,7 @@ parserRecovery.lean:49:30-49:36: error: unexpected token; expected identifier
 parserRecovery.lean:50:9-50:11: error: unexpected token ')'; expected term
 parserRecovery.lean:69:16-69:17: error: unexpected token ']'; expected '|}'
 parserRecovery.lean:69:20: error: unexpected token at this precedence level; consider parenthesizing the term
-parserRecovery.lean:72:15-72:16: error: unexpected token ']'; expected ')', ',' or ':'
+parserRecovery.lean:72:15-72:16: error: unexpected token ']'; expected ')'
 parserRecovery.lean:100:3-101:1: error: unexpected token; expected identifier
 parserRecovery.lean:103:1-104:3: error: unexpected token 'def'; expected identifier
 parserRecovery.lean:105:0-105:1: error: unexpected token; expected identifier