From f0ebf426b7da4e7049f78f1dea3a43bf458c5f91 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 11 Jun 2020 12:38:55 -0700
Subject: [PATCH] chore: `longestMatchFn` parsers must produce exactly one
 Syntax node

Before this commit, we were handling the following two abnormal cases:

1- `p` did not produce any `Syntax` node. `runLongestMatchParser`
would insert a `Syntax.missing`.

2- `p` produced more than one `Syntax` node on the
stack. `runLongestMatchParser` would combine all of them using a
`nullKind` node.

This feature was never used since we only use `longestMatchFn` to
process leading and trailing parsers. In both case, we create a node.
Moreover, if a bad parser is manually created, I think it is better to
fail than accept using `Syntax.missing` or a `nullKind` node. We would
only be postponing the problem since we don't have elaboration
functions for them.

cc @Kha
---
 src/Lean/Parser/Parser.lean | 31 +++++++++++--------------------
 1 file changed, 11 insertions(+), 20 deletions(-)

diff --git a/src/Lean/Parser/Parser.lean b/src/Lean/Parser/Parser.lean
index 154fbf5c31..230e50f989 100644
--- a/src/Lean/Parser/Parser.lean
+++ b/src/Lean/Parser/Parser.lean
@@ -1237,11 +1237,15 @@ s.keepLatest startStackSize
 
 end ParserState
 
+def invalidLongestMatchParser (s : ParserState) : ParserState :=
+s.mkError "longestMatch parsers must generate exactly one Syntax node"
+
 /--
  Auxiliary function used to execute parsers provided to `longestMatchFn`.
  Push `left?` into the stack if it is not `none`, and execute `p`.
- After executing `p`, remove `left` and combine `p` results.
+ After executing `p`, remove `left`.
 
+ Remark: `p` must produce exactly one syntax node.
  Remark: the `left?` is not none when we are processing trailing parsers. -/
 @[inline] def runLongestMatchParser (left? : Option Syntax) (p : ParserFn) : ParserFn :=
 fun c s =>
@@ -1251,37 +1255,24 @@ fun c s =>
     let s := p c s;
     if s.hasError then s
     else
-      -- stack contains `[..., result_1, ... result_n ]` we must combine the different result nodes
-      let currSize := s.stackSize;
-      if currSize == startSize + 1 then
-        -- `p` created one node
+      -- stack contains `[..., result ]`
+      if s.stackSize == startSize + 1 then
         s
       else
-        -- `p` created more than one node, we combine them into a single node
-        let r := Syntax.node nullKind (s.stxStack.extract startSize currSize);
-        let s := s.shrinkStack startSize;
-        s.pushSyntax r
+        invalidLongestMatchParser s
   | some left =>
     let s         := s.pushSyntax left;
     let s         := p c s;
     if s.hasError then s
     else
-      -- stack contains `[..., left, result_1, ... result_n ]` we must remove `left`, and combine the different result nodes
-      let currSize := s.stackSize;
-      if currSize == startSize + 1 then
-        -- `p` did not create any node, then we just remove `left` and add `Syntax.missing`
-        let s := s.shrinkStack startSize;
-        s.pushSyntax Syntax.missing
-      else if currSize == startSize + 2 then
+      -- stack contains `[..., left, result ]` we must remove `left`
+      if s.stackSize == startSize + 2 then
         -- `p` created one node, then we just remove `left` and keep it
         let r := s.stxStack.back;
         let s := s.shrinkStack startSize; -- remove `r` and `left`
         s.pushSyntax r -- add `r` back
       else
-        -- `p` created more than one node, we combine them into a single node
-        let r := Syntax.node nullKind (s.stxStack.extract (startSize+1) currSize);
-        let s := s.shrinkStack startSize;
-        s.pushSyntax r
+        invalidLongestMatchParser s
 
 def longestMatchStep (left? : Option Syntax) (startSize : Nat) (startPos : String.Pos) (p : ParserFn) : ParserFn :=
 fun c s =>