fix: do not use nullKind for group combinator

We use `nullKind` for the `group` parser combinator.
When pattern matching `nullKind` nodes, we check their arities.
So, error recovery often fails for parsers that use the `group`
combinator.
For example, we have the parser
```
def whereDecls := leading_parser "where " >> many1Indent (group (letRecDecl >> optional ";"))
```
If there is syntax error at `letRecDecl`, the node corresponding to
```
group (letRecDecl >> optional ";")
```
will contain only one child, and the pattern matching at
```
def expandWhereDecls (whereDecls : Syntax) (body : Syntax) : MacroM Syntax :=
  match whereDecls with
  | `(whereDecls|where $[$decls:letRecDecl $[;]?]*) => `(let rec $decls:letRecDecl,*; $body)
  | _ => Macro.throwUnsupported
```
fails, and we can't elaborate the partial syntax tree for
`letRecDecl`, and auto-completion will not work there.

We address this issue by using a new kind for the `group` combinator.
The idea is to pattern match `group` as we pattern match `node`s with
proper syntax node kinds. This change is consistent with the way we
use `group` where it mainly a convenience for saving us the trouble of
defining a new parser definition that is used only once.
This commit is contained in:
Leonardo de Moura 2021-04-07 20:16:10 -07:00
parent 2b9df7d8b9
commit 578b3b822f
3 changed files with 3 additions and 2 deletions

View file

@ -1673,6 +1673,7 @@ instance : Inhabited Syntax where
/- Builtin kinds -/
def choiceKind : SyntaxNodeKind := `choice
def nullKind : SyntaxNodeKind := `null
def groupKind : SyntaxNodeKind := `group
def identKind : SyntaxNodeKind := `ident
def strLitKind : SyntaxNodeKind := `strLit
def charLitKind : SyntaxNodeKind := `charLit

View file

@ -283,7 +283,7 @@ private def toFieldLHS (stx : Syntax) : Except String FieldLHS :=
return FieldLHS.modifyOp stx stx[1]
else
-- Note that the representation of the first field is different.
let stx := if stx.getKind == nullKind then stx[1] else stx
let stx := if stx.getKind == groupKind then stx[1] else stx
if stx.isIdent then
return FieldLHS.fieldName stx stx.getId.eraseMacroScopes
else match stx.isFieldIdx? with

View file

@ -49,7 +49,7 @@ attribute [runBuiltinParserAttributeHooks]
withAntiquot (mkAntiquot "nameLit" nameLitKind) nameLitNoAntiquot
@[runBuiltinParserAttributeHooks, inline] def group (p : Parser) : Parser :=
node nullKind p
node groupKind p
@[runBuiltinParserAttributeHooks, inline] def many1Indent (p : Parser) : Parser :=
withPosition $ many1 (checkColGe "irrelevant" >> p)