feat: use new structInstFields parser to tag structure instance fields

src/Lean/Elab/StructInst.lean

@@ -144,7 +144,7 @@ private def getStructSource (structStx : Syntax) : TermElabM Source :=
   ```
 -/
 private def isModifyOp? (stx : Syntax) : TermElabM (Option Syntax) := do
-  let s? ← stx[2].getSepArgs.foldlM (init := none) fun s? arg => do
+  let s? ← stx[2][0].getSepArgs.foldlM (init := none) fun s? arg => do
     /- arg is of the form `structInstFieldAbbrev <|> structInstField` -/
     if arg.getKind == ``Lean.Parser.Term.structInstField then
       /- Remark: the syntax for `structInstField` is
@@ -359,15 +359,15 @@ private def mkStructView (stx : Syntax) (structName : Name) (source : Source) :
   /- Recall that `stx` is of the form
      ```
      leading_parser "{" >> optional (atomic (sepBy1 termParser ", " >> " with "))
-                 >> sepByIndent (structInstFieldAbbrev <|> structInstField) ...
+                 >> structInstFields (sepByIndent (structInstFieldAbbrev <|> structInstField) ...)
                  >> optional ".."
                  >> optional (" : " >> termParser)
                  >> " }"
      ```
 
      This method assumes that `structInstFieldAbbrev` had already been expanded.
   -/
-  let fields ← stx[2].getSepArgs.toList.mapM fun fieldStx => do
+  let fields ← stx[2][0].getSepArgs.toList.mapM fun fieldStx => do
     let val      := fieldStx[2]
     let first    ← toFieldLHS fieldStx[0][0]
     let rest     ← fieldStx[0][1].getArgs.toList.mapM toFieldLHS
@@ -511,7 +511,9 @@ mutual
             let valStx := s.ref -- construct substructure syntax using s.ref as template
             let valStx := valStx.setArg 4 mkNullNode -- erase optional expected type
             let args   := substructFields.toArray.map (·.toSyntax)
-            let valStx := valStx.setArg 2 (mkNullNode <| mkSepArray args (mkAtom ","))
+            let fieldsStx := mkNode Parser.Term.structInstFieldsKind
+              #[mkNullNode <| mkSepArray args (mkAtom ",")]
+            let valStx := valStx.setArg 2 fieldsStx
             let valStx ← updateSource valStx
             return { field with lhs := [field.lhs.head!], val := FieldVal.term valStx }
   /--

src/Lean/Parser/Command.lean

@@ -137,7 +137,7 @@ def declValEqns      := leading_parser
 def whereStructField := leading_parser
   Term.letDecl
 def whereStructInst  := leading_parser
-  ppIndent ppSpace >> "where" >> sepByIndent (ppGroup whereStructField) "; " (allowTrailingSep := true) >>
+  ppIndent ppSpace >> "where" >> Term.structInstFields (sepByIndent (ppGroup whereStructField) "; " (allowTrailingSep := true)) >>
   optional Term.whereDecls
 /-- `declVal` matches the right-hand side of a declaration, one of:
 * `:= expr` (a "simple declaration")

src/Lean/Parser/Term.lean

@@ -281,6 +281,8 @@ def structInstFieldAbbrev := leading_parser
   atomic (ident >> notFollowedBy ("." <|> ":=" <|> symbol "[") "invalid field abbreviation")
 def optEllipsis      := leading_parser
   optional " .."
+def structInstFieldsKind : SyntaxNodeKind := `Lean.Parser.Term.structInstFields
+def structInstFields (p : Parser) : Parser := node structInstFieldsKind p
 /--
 Structure instance. `{ x := e, ... }` assigns `e` to field `x`, which may be
 inherited. If `e` is itself a variable called `x`, it can be elided:
@@ -292,7 +294,7 @@ The structure type can be specified if not inferable:
 -/
 @[builtin_term_parser] def structInst := leading_parser
   "{ " >> withoutPosition (optional (atomic (sepBy1 termParser ", " >> " with "))
-    >> sepByIndent (structInstFieldAbbrev <|> structInstField) ", " (allowTrailingSep := true)
+    >> structInstFields (sepByIndent (structInstFieldAbbrev <|> structInstField) ", " (allowTrailingSep := true))
     >> optEllipsis
     >> optional (" : " >> termParser)) >> " }"
 def typeSpec := leading_parser " : " >> termParser
@@ -984,6 +986,7 @@ builtin_initialize
   register_parser_alias bracketedBinder
   register_parser_alias attrKind
   register_parser_alias optSemicolon
+  register_parser_alias structInstFields
 
 end Parser
 end Lean

src/Lean/Server/Completion/SyntheticCompletion.lean

@@ -268,138 +268,111 @@ private def findExpectedTypeAt (infoTree : InfoTree) (hoverPos : String.Pos) : O
     | none
   (ctx, i.expectedType?.get!)
 
-private structure HoverData where
-  fileMap                    : FileMap
-  hoverPos                   : String.Pos
-  hoverFilePos               : Position
-  hoverLineIndentation       : Nat
-  isCursorOnWhitespace       : Bool
-  isCursorInProperWhitespace : Bool
+private partial def foldWithLeadingToken [Inhabited α]
+    (f    : α → Option Syntax → Syntax → α)
+    (init : α)
+    (stx  : Syntax)
+    : α :=
+  let (_, r) := go none init stx
+  r
+where
+  go [Inhabited α] (leadingToken? : Option Syntax) (acc : α) (stx : Syntax) : Option Syntax × α :=
+    let acc := f acc leadingToken? stx
+    match stx with
+    | .missing  => (none, acc)
+    | .atom ..  => (stx, acc)
+    | .ident .. => (stx, acc)
+    | .node _ _ args => Id.run do
+      let mut acc := acc
+      let mut lastToken? := none
+      for arg in args do
+        let (lastToken'?, acc') := go (lastToken? <|> leadingToken?) acc arg
+        lastToken? := lastToken'? <|> lastToken?
+        acc := acc'
+      return (lastToken?, acc)
+
+private def findWithLeadingToken?
+    (p : Option Syntax → Syntax → Bool)
+    (stx : Syntax)
+    : Option Syntax :=
+  foldWithLeadingToken (stx := stx) (init := none) fun foundStx? leadingToken? stx =>
+    match foundStx? with
+    | some foundStx => foundStx
+    | none =>
+      if p leadingToken? stx then
+        some stx
+      else
+        none
 
-private def HoverData.ofPosInFile
+private def isSyntheticStructFieldCompletion
     (fileMap  : FileMap)
     (hoverPos : String.Pos)
-    : HoverData := Id.run do
+    (cmdStx   : Syntax)
+    : Bool := Id.run do
+  let isCursorOnWhitespace := isCursorOnWhitespace fileMap hoverPos
+  let isCursorInProperWhitespace := isCursorInProperWhitespace fileMap hoverPos
+  if ! isCursorOnWhitespace then
+    return false
+
   let hoverFilePos := fileMap.toPosition hoverPos
   let mut hoverLineIndentation := getIndentationAmount fileMap hoverFilePos.line
   if hoverFilePos.column < hoverLineIndentation then
     -- Ignore trailing whitespace after the cursor
     hoverLineIndentation := hoverFilePos.column
-  let isCursorOnWhitespace := Completion.isCursorOnWhitespace fileMap hoverPos
-  let isCursorInProperWhitespace := Completion.isCursorInProperWhitespace fileMap hoverPos
-  return {
-    fileMap,
-    hoverPos,
-    hoverFilePos,
-    hoverLineIndentation
-    isCursorOnWhitespace,
-    isCursorInProperWhitespace
-  }
 
-private structure SepBy1Data (ks : SyntaxNodeKinds) (sep : String) where
-  sepBy1Stx   : Syntax.TSepArray ks sep
-  outerBounds : String.Range
-
-private def isCompletionInSepBy1
-    {ks  : SyntaxNodeKinds}
-    {sep : String}
-    (hd  : HoverData)
-    (sd  : SepBy1Data ks sep)
-    : Bool := Id.run do
-  if ! hd.isCursorOnWhitespace then
-    return false
-
-  let isCompletionInEmptyBlock :=
-    sd.sepBy1Stx.elemsAndSeps.isEmpty && sd.outerBounds.contains hd.hoverPos (includeStop := true)
-  if isCompletionInEmptyBlock then
-    return true
-
-  let isCompletionAfterSep := sd.sepBy1Stx.elemsAndSeps.any fun fieldOrSep => Id.run do
-    if ! fieldOrSep.isToken sep then
-      return false
-    let some sepTailPos := fieldOrSep.getTailPos?
+  return Option.isSome <| findWithLeadingToken? (stx := cmdStx) fun leadingToken? stx => Id.run do
+    let some leadingToken := leadingToken?
       | return false
-    return sepTailPos <= hd.hoverPos
-      && hd.hoverPos.byteIdx <= sepTailPos.byteIdx + fieldOrSep.getTrailingSize
-  if isCompletionAfterSep then
-    return true
 
-  let isCompletionOnIndentation := Id.run do
-    if ! hd.isCursorInProperWhitespace then
+    if stx.getKind != Parser.Term.structInstFieldsKind then
       return false
-    let isCursorInIndentation := hd.hoverFilePos.column <= hd.hoverLineIndentation
-    if ! isCursorInIndentation then
-      return false
-    let some firstFieldPos := sd.sepBy1Stx.elemsAndSeps[0]?.getD Syntax.missing |>.getPos?
-      | return false
-    let firstFieldLine := hd.fileMap.toPosition firstFieldPos |>.line
-    let firstFieldIndentation := getIndentationAmount hd.fileMap firstFieldLine
-    let isCursorInBlock := hd.hoverLineIndentation == firstFieldIndentation
-    return isCursorInBlock
-  return isCompletionOnIndentation
 
-private def isSyntheticWhereBlockFieldCompletion
-  (fileMap  : FileMap)
-  (hoverPos : String.Pos)
-  (cmdStx   : Syntax)
-  : Bool :=
-  let hd := HoverData.ofPosInFile fileMap hoverPos
-  Option.isSome <| cmdStx.find? fun stx => Id.run do
-    let `(Parser.Command.whereStructInst|where $structFields:whereStructField;* $[$_:whereDecls]?) :=
-        stx
+    let fieldsAndSeps := stx[0].getArgs
+    let some outerBoundsStart := leadingToken.getTailPos? (canonicalOnly := true)
       | return false
-    let some outerBoundStart := stx[0].getTailPos? (canonicalOnly := true)
+    let some outerBoundsStop :=
+        stx.getTrailingTailPos? (canonicalOnly := true)
+          <|> leadingToken.getTrailingTailPos? (canonicalOnly := true)
       | return false
-    let some outerBoundStop :=
-        stx[2].getPos? (canonicalOnly := true)
-        <|> stx[1].getTrailingTailPos? (canonicalOnly := true)
-        <|> stx[0].getTrailingTailPos? (canonicalOnly := true)
-      | return false
-    let sd : SepBy1Data _ _ := {
-      sepBy1Stx   := structFields
-      outerBounds := {
-        start := outerBoundStart
-        stop  := outerBoundStop
-      }
-    }
-    return isCompletionInSepBy1 hd sd
+    let outerBounds : String.Range := ⟨outerBoundsStart, outerBoundsStop⟩
 
-private def isSyntheticStructInstFieldCompletion
-  (fileMap  : FileMap)
-  (hoverPos : String.Pos)
-  (cmdStx   : Syntax)
-  : Bool :=
-  let hd := HoverData.ofPosInFile fileMap hoverPos
-  Option.isSome <| cmdStx.find? fun stx => Id.run do
-    let `(Lean.Parser.Term.structInst| { $[$srcs,* with]? $fields,* $[..%$ell]? $[: $ty]? }) :=
-        stx
-      | return false
-    let some outerBoundStart :=
-        stx[1].getTailPos? (canonicalOnly := true)
-        <|> stx[0].getTailPos? (canonicalOnly := true)
-      | return false
-    let some outerBoundStop :=
-        stx[3].getPos? (canonicalOnly := true)
-        <|> stx[4].getPos? (canonicalOnly := true)
-        <|> stx[5].getPos? (canonicalOnly := true)
-      | return false
-    let sd : SepBy1Data _ _ := {
-      sepBy1Stx   := fields
-      outerBounds := {
-        start := outerBoundStart
-        stop  := outerBoundStop
-      }
-    }
-    return isCompletionInSepBy1 hd sd
+    let isCompletionInEmptyBlock :=
+      fieldsAndSeps.isEmpty && outerBounds.contains hoverPos (includeStop := true)
+    if isCompletionInEmptyBlock then
+      return true
+
+    let isCompletionAfterSep := fieldsAndSeps.zipWithIndex.any fun (fieldOrSep, i) => Id.run do
+      if i % 2 == 0 || !fieldOrSep.isAtom then
+        return false
+      let sep := fieldOrSep
+      let some sepTailPos := sep.getTailPos?
+        | return false
+      return sepTailPos <= hoverPos
+        && hoverPos.byteIdx <= sepTailPos.byteIdx + sep.getTrailingSize
+    if isCompletionAfterSep then
+      return true
+
+    let isCompletionOnIndentation := Id.run do
+      if ! isCursorInProperWhitespace then
+        return false
+      let isCursorInIndentation := hoverFilePos.column <= hoverLineIndentation
+      if ! isCursorInIndentation then
+        return false
+      let some firstFieldPos := stx.getPos?
+        | return false
+      let firstFieldLine := fileMap.toPosition firstFieldPos |>.line
+      let firstFieldIndentation := getIndentationAmount fileMap firstFieldLine
+      let isCursorInBlock := hoverLineIndentation == firstFieldIndentation
+      return isCursorInBlock
+    return isCompletionOnIndentation
 
 private def findSyntheticFieldCompletion?
   (fileMap  : FileMap)
   (hoverPos : String.Pos)
   (cmdStx   : Syntax)
   (infoTree : InfoTree)
   : Option ContextualizedCompletionInfo := do
-  if ! isSyntheticWhereBlockFieldCompletion fileMap hoverPos cmdStx
-      && ! isSyntheticStructInstFieldCompletion fileMap hoverPos cmdStx then
+  if ! isSyntheticStructFieldCompletion fileMap hoverPos cmdStx then
     none
   let (ctx, expectedType) ← findExpectedTypeAt infoTree hoverPos
   let .const typeName _ := expectedType.getAppFn