From 54bdddb98f828e67a3ff11aa3b7eac66fe61bc02 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 30 Jan 2020 20:38:14 -0800
Subject: [PATCH] fix: `toParserDescrAux`

---
 src/Init/Lean/Elab/Syntax.lean | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

diff --git a/src/Init/Lean/Elab/Syntax.lean b/src/Init/Lean/Elab/Syntax.lean
index fc095c2c43..fca3382b3c 100644
--- a/src/Init/Lean/Elab/Syntax.lean
+++ b/src/Init/Lean/Elab/Syntax.lean
@@ -50,13 +50,12 @@ adaptReader (fun (ctx : ToParserDescrContext) => { first := false, .. ctx }) x
 adaptReader (fun (ctx : ToParserDescrContext) => { leftRec := false, .. ctx }) x
 
 def checkLeftRec (stx : Syntax) : ToParserDescrM Bool := do
-if stx.getKind == `Lean.Parser.Syntax.cat then do
+ctx ← read;
+if ctx.first && stx.getKind == `Lean.Parser.Syntax.cat then do
   let cat := (stx.getIdAt 0).eraseMacroScopes;
-  ctx ← read;
-  if ctx.first && cat == ctx.catName then do
+  if cat == ctx.catName then do
     let rbp? : Option Nat  := expandOptPrecedence (stx.getArg 1);
     unless rbp?.isNone $ liftM $ throwError (stx.getArg 1) ("invalid occurrence of ':<num>' modifier in head");
-    ctx ← read;
     unless ctx.leftRec $ liftM $
       throwError (stx.getArg 3) ("invalid occurrence of '" ++ cat ++ "', parser algorithm does not allow this form of left recursion");
     markAsTrailingParser; -- mark as trailing par
@@ -71,14 +70,14 @@ partial def toParserDescrAux : Syntax → ToParserDescrM Syntax
   let kind := stx.getKind;
   if kind == nullKind then do
     let args := stx.getArgs;
-    condM (checkLeftRec stx)
+    condM (checkLeftRec (stx.getArg 0))
       (do
         when (args.size == 1) $ liftM $ throwError stx "invalid atomic left recursive syntax";
         let args := args.eraseIdx 0;
-        args ← stx.getArgs.mapIdxM $ fun i arg => withNotFirst $ toParserDescrAux arg;
+        args ← args.mapIdxM $ fun i arg => withNotFirst $ toParserDescrAux arg;
         liftM $ mkParserSeq args)
       (do
-        args ← stx.getArgs.mapIdxM $ fun i arg => withNotFirst $ toParserDescrAux arg;
+        args ← args.mapIdxM $ fun i arg => withNotFirst $ toParserDescrAux arg;
         liftM $ mkParserSeq args)
   else if kind == choiceKind then do
     toParserDescrAux (stx.getArg 0)