From 7bb3d100147f1dbfc00b977846ffa66ff62e104e Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 1 Apr 2021 17:22:42 +0200 Subject: [PATCH] chore: ensure that a failing `node` parser creates at least one `missing` --- src/Lean/Parser/Basic.lean | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean index f5b39b05c3..d3d4ba8b86 100644 --- a/src/Lean/Parser/Basic.lean +++ b/src/Lean/Parser/Basic.lean @@ -221,8 +221,15 @@ def mkNode (s : ParserState) (k : SyntaxNodeKind) (iniStackSz : Nat) : ParserSta match s with | ⟨stack, lhsPrec, pos, cache, err⟩ => if err != none && stack.size == iniStackSz then - -- If there is an error but there are no new nodes on the stack, we just return `s` - s + -- If there is an error but there are no new nodes on the stack, use `missing` instead. + -- Thus we ensure the property that an syntax tree contains (at least) one `missing` node + -- if (and only if) there was a parse error. + -- We should not create an actual node of kind `k` in this case because it would mean we + -- choose an "arbitrary" node (in practice the last one) in an alternative of the form + -- `node k1 p1 <|> ... <|> node kn pn` when all parsers fail. With the code below we + -- instead return a less misleading single `missing` node without randomly selecting any `ki`. + let stack := stack.push Syntax.missing + ⟨stack, lhsPrec, pos, cache, err⟩ else let newNode := Syntax.node k (stack.extract iniStackSz stack.size) let stack := stack.shrink iniStackSz