feat: dot auto-completion for most occurrences of global identifiers

src/Init/Grind/Tactics.lean

@@ -15,19 +15,19 @@ Reset all `grind` attributes. This command is intended for testing purposes only
 syntax (name := resetGrindAttrs) "reset_grind_attrs%" : command
 
 namespace Attr
-syntax grindEq     := "= "
-syntax grindEqBoth := atomic("_" "=" "_ ")
-syntax grindEqRhs  := atomic("=" "_ ")
-syntax grindEqBwd  := atomic("←" "= ") <|> atomic("<-" "= ")
-syntax grindBwd    := "← " <|> "-> "
-syntax grindFwd    := "→ " <|> "<- "
-syntax grindRL     := "⇐ " <|> "<= "
-syntax grindLR     := "⇒ " <|> "=> "
-syntax grindUsr    := &"usr "
-syntax grindCases  := &"cases "
-syntax grindCasesEager := atomic(&"cases" &"eager ")
-syntax grindIntro  := &"intro "
-syntax grindExt    := &"ext "
+syntax grindEq     := "="
+syntax grindEqBoth := atomic("_" "=" "_")
+syntax grindEqRhs  := atomic("=" "_")
+syntax grindEqBwd  := atomic("←" "=") <|> atomic("<-" "=")
+syntax grindBwd    := "← " <|> "<-" -- TODO after stage0 update: fix whitespace
+syntax grindFwd    := "→ " <|> "->"
+syntax grindRL     := "⇐ " <|> "<="
+syntax grindLR     := "⇒ " <|> "=>"
+syntax grindUsr    := &"usr"
+syntax grindCases  := &"cases"
+syntax grindCasesEager := atomic(&"cases " &"eager")
+syntax grindIntro  := &"intro"
+syntax grindExt    := &"ext"
 syntax grindMod := grindEqBoth <|> grindEqRhs <|> grindEq <|> grindEqBwd <|> grindBwd <|> grindFwd <|> grindRL <|> grindLR <|> grindUsr <|> grindCasesEager <|> grindCases <|> grindIntro <|> grindExt
 syntax (name := grind) "grind" (grindMod)? : attr
 end Attr
@@ -140,19 +140,19 @@ namespace Lean.Parser.Tactic
 `grind` tactic and related tactics.
 -/
 
-syntax grindErase := "-" ident
-syntax grindLemma := (Attr.grindMod)? ident
+syntax grindErase := "-" ident -- TODO after stage0 update: identWithOptDot
+syntax grindLemma := (Attr.grindMod ppSpace)? ident -- TODO after stage0 update: identWithOptDot
 syntax grindParam := grindErase <|> grindLemma
 
 syntax (name := grind)
   "grind" optConfig (&" only")?
   (" [" withoutPosition(grindParam,*) "]")?
-  ("on_failure " term)? : tactic
+  (&" on_failure " term)? : tactic
 
 
 syntax (name := grindTrace)
   "grind?" optConfig (&" only")?
   (" [" withoutPosition(grindParam,*) "]")?
-  ("on_failure " term)? : tactic
+  (&" on_failure " term)? : tactic
 
 end Lean.Parser.Tactic

src/Init/Meta.lean

@@ -1083,9 +1083,12 @@ def isNone (stx : Syntax) : Bool :=
   | Syntax.missing     => true
   | _                  => false
 
+def getIdOrIdWithOptDot (stx : Syntax) : Name :=
+  if let .ident _ _ n _ := stx then n else stx[0].getId
+
 def getOptionalIdent? (stx : Syntax) : Option Name :=
   match stx.getOptional? with
-  | some stx => some stx.getId
+  | some stx => some stx.getIdOrIdWithOptDot
   | none     => none
 
 partial def findAux (p : Syntax → Bool) : Syntax → Option Syntax
@@ -1115,6 +1118,14 @@ Returns `Name.anonymous` if the syntax is malformed.
 def getId (s : Ident) : Name :=
   s.raw.getId
 
+/--
+Extracts the parsed name from the syntax of an `identWithOptDot`.
+
+Returns `Name.anonymous` if the syntax is malformed.
+-/
+def getIdWithOptDot (s : TSyntax ``identWithOptDot) : Name :=
+  s.raw[0].getId
+
 /--
 Extracts the components of a scientific numeric literal.
 
@@ -1275,7 +1286,7 @@ macro "eval_prio " p:prio:max : term => return quote (k := `term) (← evalPrio
 
 def evalOptPrio : Option (TSyntax `prio) → MacroM Nat
   | some prio => evalPrio prio
-  | none      => return 1000 -- TODO: FIX back eval_prio default
+  | none      => return eval_prio default
 
 end Lean
 
@@ -1373,6 +1384,9 @@ instance : CoeOut (TSyntaxArray k) (Array Syntax) where
 instance : Coe Ident (TSyntax `Lean.Parser.Command.declId) where
   coe id := mkNode _ #[id, mkNullNode #[]]
 
+instance : CoeOut (TSyntax ``identWithOptDot) Ident where
+  coe id := ⟨id.raw[0]⟩
+
 instance : Coe (Lean.Term) (Lean.TSyntax `Lean.Parser.Term.funBinder) where
   coe stx := ⟨stx⟩
 

src/Init/Notation.lean

@@ -18,7 +18,7 @@ namespace Lean
 Auxiliary type used to represent syntax categories. We mainly use auxiliary
 definitions with this type to attach doc strings to syntax categories.
 -/
-structure Parser.Category
+structure Parser.Category where
 
 namespace Parser.Category
 
@@ -422,6 +422,12 @@ recommended_spelling "seqRight" for "*>" in [SeqRight.seqRight, «term_*>_»]
 
 namespace Lean
 
+/--
+`indentWithOptDot` is similar to `ident` except it creates a partial syntax for identifiers with a
+trailing dot which can be used for auto-completion.
+-/
+syntax identWithOptDot := ident (noWs "." noWs ident)? -- TODO: improve error message
+
 /--
 `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.
@@ -558,6 +564,7 @@ scoped syntax (name := withAnnotateTerm) "with_annotate_term " rawStx ppSpace te
 /-- Normalize casts in an expression using the same method as the `norm_cast` tactic. -/
 syntax (name := modCast) "mod_cast " term : term
 
+-- TODO after stage0 update: identWithOptDot
 /--
 The attribute `@[deprecated]` on a declaration indicates that the declaration
 is discouraged for use in new code, and/or should be migrated away from in
@@ -577,6 +584,7 @@ applications of this function as `↑` when printing expressions.
 -/
 syntax (name := Attr.coe) "coe" : attr
 
+-- TODO after stage0 update: identWithOptDot
 /--
 This attribute marks a code action, which is used to suggest new tactics or replace existing ones.
 
@@ -591,6 +599,7 @@ This attribute marks a code action, which is used to suggest new tactics or repl
 -/
 syntax (name := command_code_action) "command_code_action" (ppSpace ident)* : attr
 
+-- TODO after stage0 update: identWithOptDot
 /--
 Builtin command code action. See `command_code_action`.
 -/
@@ -842,6 +851,7 @@ syntax (name := discrTreeKeyCmd) "#discr_tree_key " term : command
 @[inherit_doc discrTreeKeyCmd]
 syntax (name := discrTreeSimpKeyCmd) "#discr_tree_simp_key" term : command
 
+-- TODO after stage0 update: identWithOptDot
 /--
 The `seal foo` command ensures that the definition of `foo` is sealed, meaning it is marked as `[irreducible]`.
 This command is particularly useful in contexts where you want to prevent the reduction of `foo` in proofs.
@@ -852,6 +862,7 @@ which helps in maintaining the desired abstraction level without affecting globa
 -/
 syntax "seal " (ppSpace ident)+ : command
 
+-- TODO after stage0 update: identWithOptDot
 /--
 The `unseal foo` command ensures that the definition of `foo` is unsealed, meaning it is marked as `[semireducible]`, the
 default reducibility setting. This command is useful when you need to allow some level of reduction of `foo` in proofs.
@@ -861,8 +872,4 @@ Applying this attribute makes `foo` semireducible only within the local scope.
 -/
 syntax "unseal " (ppSpace ident)+ : command
 
-macro_rules
-  | `(seal $fs:ident*) => `(attribute [local irreducible] $fs:ident*)
-  | `(unseal $fs:ident*) => `(attribute [local semireducible] $fs:ident*)
-
 end Parser

src/Init/NotationExtra.lean

@@ -328,6 +328,11 @@ macro_rules
   | `(letI $x:ident $bs* := $val; $body) => `(letI $x $bs* : _ := $val; $body)
   | `(letI $_:ident $_* : $_ := $_; $_) => Lean.Macro.throwUnsupported -- handled by elab
 
+-- TODO after stage0 update: move these back to `Init.Notation`
+macro_rules
+  | `(seal $fs:ident*) => `(attribute [local irreducible] $[$fs]*)
+  | `(unseal $fs:ident*) => `(attribute [local semireducible] $[$fs]*)
+
 
 namespace Lean
 syntax cdotTk := patternIgnore("· " <|> ". ")

src/Init/Simproc.lean

@@ -71,11 +71,13 @@ A builtin defeq simplification procedure declaration.
 -/
 syntax (docComment)? "builtin_dsimproc_decl " ident " (" term ")" " := " term : command
 
+-- TODO after stage0 update: identWithOptDot
 /--
 Auxiliary command for associating a pattern with a simplification procedure.
 -/
 syntax (name := simprocPattern) "simproc_pattern% " term " => " ident : command
 
+-- TODO after stage0 update: identWithOptDot
 /--
 Auxiliary command for associating a pattern with a builtin simplification procedure.
 -/

src/Init/Tactics.lean

@@ -737,13 +737,15 @@ syntax (name := simpa) "simpa" "?"? "!"? simpaArgsRest : tactic
 @[inherit_doc simpa] macro "simpa?!" rest:simpaArgsRest : tactic =>
   `(tactic| simpa ?! $rest:simpaArgsRest)
 
+-- TODO after stage0 update: identWithOptDot
 /--
 `delta id1 id2 ...` delta-expands the definitions `id1`, `id2`, ....
 This is a low-level tactic, it will expose how recursive definitions have been
 compiled by Lean.
 -/
 syntax (name := delta) "delta" (ppSpace colGt ident)+ (location)? : tactic
 
+-- TODO after stage0 update: identWithOptDot
 /--
 * `unfold id` unfolds all occurrences of definition `id` in the target.
 * `unfold id1 id2 ...` is equivalent to `unfold id1; unfold id2; ...`.
@@ -843,7 +845,7 @@ macro "refine_lift' " e:term : tactic => `(tactic| focus (refine' no_implicit_la
 /-- Similar to `have`, but using `refine'` -/
 macro "have' " d:haveDecl : tactic => `(tactic| refine_lift' have $d:haveDecl; ?_)
 set_option linter.missingDocs false in -- OK, because `tactic_alt` causes inheritance of docs
-macro (priority := high) "have'" x:ident " := " p:term : tactic => `(tactic| have' $x:ident : _ := $p)
+macro (priority := high) "have' " x:ident " := " p:term : tactic => `(tactic| have' $x:ident : _ := $p)
 attribute [tactic_alt tacticHave'_] «tacticHave'_:=_»
 /-- Similar to `let`, but using `refine'` -/
 macro "let' " d:letDecl : tactic => `(tactic| refine_lift' let $d:letDecl; ?_)
@@ -1484,10 +1486,11 @@ See also `norm_cast`.
 syntax (name := pushCast) "push_cast" optConfig (discharger)? (&" only")?
   (" [" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic
 
+-- TODO after stage0 update: identWithOptDot
 /--
 `norm_cast_add_elim foo` registers `foo` as an elim-lemma in `norm_cast`.
 -/
-syntax (name := normCastAddElim) "norm_cast_add_elim" ident : command
+syntax (name := normCastAddElim) "norm_cast_add_elim " ident : command
 
 /--
 `ac_nf` normalizes equalities up to application of an associative and commutative operator.
@@ -1648,7 +1651,7 @@ syntax (name := apply?) "apply?" (" using " (colGt term),+)? : tactic
 /--
 Syntax for excluding some names, e.g. `[-my_lemma, -my_theorem]`.
 -/
-syntax rewrites_forbidden := " [" (("-" ident),*,?) "]"
+syntax rewrites_forbidden := " [" (("-" ident),*,?) "]" -- TODO after stage0 update: identWithOptDot
 
 /--
 `rw?` tries to find a lemma which can rewrite the goal.

src/Lean/Elab/BuiltinCommand.lean

@@ -79,9 +79,8 @@ private def checkEndHeader : Name → List Scope → Option Name
   | _, _ => some .anonymous -- should not happen
 
 @[builtin_command_elab «namespace»] def elabNamespace : CommandElab := fun stx =>
-  match stx with
-  | `(namespace $n) => addNamespace n.getId
-  | _               => throwUnsupportedSyntax
+  -- TODO after stage0 update: back to syntax `match`
+  addNamespace stx[1].getIdOrIdWithOptDot
 
 @[builtin_command_elab «section»] def elabSection : CommandElab := fun stx => do
   match stx with
@@ -98,7 +97,7 @@ private def checkEndHeader : Name → List Scope → Option Name
   | _                        => throwUnsupportedSyntax
 
 @[builtin_command_elab «end»] def elabEnd : CommandElab := fun stx => do
-  let header? := (stx.getArg 1).getOptionalIdent?;
+  let header? := (stx.getArg 1).getOptionalIdent?
   let endSize := match header? with
     | none   => 1
     | some n => n.getNumParts
@@ -138,13 +137,13 @@ private partial def elabChoiceAux (cmds : Array Syntax) (i : Nat) : CommandElabM
   liftCoreM <| addDecl Declaration.quotDecl
 
 @[builtin_command_elab «export»] def elabExport : CommandElab := fun stx => do
-  let `(export $ns ($ids*)) := stx | throwUnsupportedSyntax
+  let `(export $ns ($ids:identWithOptDot*)) := stx | throwUnsupportedSyntax
   let nss ← resolveNamespace ns
   let currNamespace ← getCurrNamespace
   if nss == [currNamespace] then throwError "invalid 'export', self export"
   let mut aliases := #[]
   for idStx in ids do
-    let id := idStx.getId
+    let id := idStx.getIdWithOptDot
     let declName ← resolveNameUsingNamespaces nss idStx
     if (← getInfoState).enabled then
       addConstInfo idStx declName
@@ -354,7 +353,7 @@ def failIfSucceeds (x : CommandElabM Unit) : CommandElabM Unit := do
     pure ()
 
 @[builtin_command_elab «set_option»] def elabSetOption : CommandElab := fun stx => do
-  let options ← Elab.elabSetOption stx[1] stx[3]
+  let options ← Elab.elabSetOption stx[1][0] stx[2]
   modify fun s => { s with maxRecDepth := maxRecDepth.get options }
   modifyScope fun scope => { scope with opts := options }
 
@@ -498,7 +497,7 @@ where
       if simple.isEmpty then
         return (lines, simple)
       else
-        return (lines.push <| ← `(command| open $(simple.map mkIdent)*), #[])
+        return (lines.push <| ← `(command| open $[$(simple.map mkIdent)]*), #[])
     for d in ds do
       match d with
       | .explicit id decl =>

src/Lean/Elab/BuiltinTerm.lean

@@ -316,12 +316,12 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
     popScope
 
 @[builtin_term_elab «set_option»] def elabSetOption : TermElab := fun stx expectedType? => do
-  let options ← Elab.elabSetOption stx[1] stx[3]
+  let options ← Elab.elabSetOption stx[1][0] stx[2]
   withOptions (fun _ => options) do
     try
-      elabTerm stx[5] expectedType?
+      elabTerm stx[4] expectedType?
     finally
-      if stx[1].getId == `diagnostics then
+      if stx[1][0].getId == `diagnostics then
         reportDiag
 
 @[builtin_term_elab withAnnotateTerm] def elabWithAnnotateTerm : TermElab := fun stx expectedType? => do

src/Lean/Elab/Command.lean

@@ -871,13 +871,12 @@ Given a command elaborator `cmd`, returns a new command elaborator that
 first evaluates any local `set_option ... in ...` clauses and then invokes `cmd` on what remains.
 -/
 partial def withSetOptionIn (cmd : CommandElab) : CommandElab := fun stx => do
-  if stx.getKind == ``Lean.Parser.Command.in &&
-     stx[0].getKind == ``Lean.Parser.Command.set_option then
-      let opts ← Elab.elabSetOption stx[0][1] stx[0][3]
-      Command.withScope (fun scope => { scope with opts }) do
-        withSetOptionIn cmd stx[2]
-  else
-    cmd stx
+  match stx with
+  | `(command| set_option $i:identWithOptDot $v in $c) =>
+    let opts ← Elab.elabSetOption (i : Ident) v
+    Command.withScope (fun scope => { scope with opts }) do
+      withSetOptionIn cmd c
+  | _ => cmd stx
 
 export Elab.Command (Linter addLinter)
 

src/Lean/Elab/Declaration.lean

@@ -307,7 +307,7 @@ def elabMutual : CommandElab := fun stx => do
       try
         realizeGlobalConstWithInfos ident
       catch _ =>
-        let name := ident.getId.eraseMacroScopes
+        let name := ident.getIdOrIdWithOptDot.eraseMacroScopes
         if (← Simp.isBuiltinSimproc name) then
           pure [name]
         else

src/Lean/Elab/Deriving/Basic.lean

@@ -97,7 +97,7 @@ private def tryApplyDefHandler (className : Name) (declName : Name) : CommandEla
     Term.processDefDeriving className declName
 
 @[builtin_command_elab «deriving»] def elabDeriving : CommandElab
-  | `(deriving instance $[$classes],* for $[$declNames],*) => do
+  | `(deriving instance $[$classes],* for $[$declNames:identWithOptDot],*) => do
      let declNames ← liftCoreM <| declNames.mapM realizeGlobalConstNoOverloadWithInfo
      for cls in classes do
        try