From 52c7709cb34ef37b65f158610d6501ac33922e4b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 8 Jun 2020 14:34:50 -0700
Subject: [PATCH] fix: `longestMatch` at trailing parsers

Before this commit, if we execut `longestMatch [p1, p2]` in a
trailing parser where both `p1` and `p2` succeed, then an incorrect
syntax tree is generated by `p2`. The issue is that before executing
`p2`, the trailing stack is of the form
`#[..., left, syntax-by-p1]`
Then, the trailing parser `p2` incorrectly assumes that `syntax-by-p1`
was the "left" syntax node.
This commit fix this issue by storing the `left` node at the
`ParserContext` at `trailingLoop`

@Kha This bug was introduced when we unified leading and trailing
parsers. I think this is the simplest solution.
We can observe the bug before this commit by using
```
set_option syntaxMaxDepth 1000
set_option trace.Elab true
```
at `choiceMacroRules.lean`.

It is funny the correct result was produced even with the bug.
It was working because the `macro_rules` was matching the
buggy syntax with the nested `syntax-by-p1` there :)
---
 src/Lean/Parser/Parser.lean | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Parser/Parser.lean b/src/Lean/Parser/Parser.lean
index 2e0b17b7c2..4b540bdb4d 100644
--- a/src/Lean/Parser/Parser.lean
+++ b/src/Lean/Parser/Parser.lean
@@ -145,6 +145,7 @@ instance InputContext.inhabited : Inhabited InputContext :=
 
 structure ParserContext extends InputContext :=
 (rbp      : Nat)
+(left     : Syntax := Syntax.missing)
 (env      : Environment)
 (tokens   : TokenTable)
 
@@ -236,10 +237,10 @@ match s with
     let stack   := stack.push newNode;
     ⟨stack, pos, cache, err⟩
 
-def mkTrailingNode (s : ParserState) (k : SyntaxNodeKind) (iniStackSz : Nat) : ParserState :=
+def mkTrailingNode (s : ParserState) (k : SyntaxNodeKind) (left : Syntax) (iniStackSz : Nat) : ParserState :=
 match s with
 | ⟨stack, pos, cache, err⟩ =>
-  let newNode := Syntax.node k (stack.extract (iniStackSz - 1) stack.size);
+  let newNode := Syntax.node k (#[left] ++ stack.extract iniStackSz stack.size);
   let stack   := stack.shrink iniStackSz;
   let stack   := stack.push newNode;
   ⟨stack, pos, cache, err⟩
@@ -363,7 +364,7 @@ instance hasAndthen : HasAndthen Parser :=
 | c, s =>
   let iniSz := s.stackSize;
   let s     := p c s;
-  s.mkTrailingNode n iniSz
+  s.mkTrailingNode n c.left iniSz
 
 @[noinline] def nodeInfo (n : SyntaxNodeKind) (p : ParserInfo) : ParserInfo :=
 { collectTokens := p.collectTokens,
@@ -1601,6 +1602,7 @@ partial def trailingLoop (tables : PrattParsingTables) (c : ParserContext) : Par
   let (s, lbp) := currLbp left c s;
   if c.rbp ≥ lbp then s
   else
+    let c             := { c with left := s.stxStack.back };
     let iniSz         := s.stackSize;
     let identAsSymbol := false;
     let (s, ps)       := indexed tables.trailingTable c s identAsSymbol;