From b1a9c58d43f6afeeea9aeeb2736f7d8f0c72d42e Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 30 Jun 2022 11:22:01 +0200
Subject: [PATCH] feat: relax eager antiquotation parsing

---
 src/Lean/Parser/Basic.lean | 43 +++++++++++++++++++++++++-------------
 1 file changed, 29 insertions(+), 14 deletions(-)

diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index 26a491ca80..233f38d64f 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -485,9 +485,14 @@ def mergeOrElseErrors (s : ParserState) (error1 : Error) (iniPos : String.Pos) (
     else s
   | other => other
 
--- When `mergeAntiquots` is true, if `p` parses an antiquotation, we try `q` as well and return a choice node if they
--- both return antiquotations
-def orelseFnCore (p q : ParserFn) (mergeAntiquots : Bool) : ParserFn := fun c s => Id.run do
+-- When `p` in `p <|> q` parses exactly one antiquotation, ...
+inductive OrElseOnAntiquotBehavior where
+  | acceptLhs    -- return it
+  | takeLongest  -- return result of `q` instead if it made more progress
+  | merge        -- ... and create choice node if both made the same progress
+  deriving BEq
+
+def orelseFnCore (p q : ParserFn) (antiquotBehavior := OrElseOnAntiquotBehavior.merge) : ParserFn := fun c s => Id.run do
   let s0     := s
   let iniSz  := s.stackSize
   let iniPos := s.pos
@@ -500,17 +505,24 @@ def orelseFnCore (p q : ParserFn) (mergeAntiquots : Bool) : ParserFn := fun c s
       s
   | none =>
     let back := s.stxStack.back
-    if mergeAntiquots && back.isAntiquots then
+    if antiquotBehavior != .acceptLhs && s.stackSize == iniSz + 1 && back.isAntiquots then
       let s' := q c s0
-      if !s'.hasError && s'.stxStack.back.isAntiquot then
-        if back.isOfKind choiceKind then
-          s := { s with stxStack := s.stxStack.pop ++ back.getArgs }
-        s := s.pushSyntax s'.stxStack.back
-        s := s.mkNode choiceKind iniSz
+      if !s'.hasError then
+        -- If `q` made more progress than `p`, we prefer its result.
+        -- Thus `(structInstField| $id := $val) is interpreted as
+        -- `(structInstField| $id:ident := $val:term), not
+        -- `(structInstField| $id:structInstField <ERROR: expected ')'>.
+        if s'.pos > s.pos then
+          return s'
+        else if antiquotBehavior == .merge && s'.stackSize == iniSz + 1 && s'.stxStack.back.isAntiquot then
+          if back.isOfKind choiceKind then
+            s := { s with stxStack := s.stxStack.pop ++ back.getArgs }
+          s := s.pushSyntax s'.stxStack.back
+          s := s.mkNode choiceKind iniSz
     s
 
 @[inline] def orelseFn (p q : ParserFn) : ParserFn :=
-  orelseFnCore (mergeAntiquots := true) p q
+  orelseFnCore p q
 
 @[noinline] def orelseInfo (p q : ParserInfo) : ParserInfo := {
   collectTokens := p.collectTokens ∘ q.collectTokens,
@@ -1740,11 +1752,14 @@ def mkAntiquot (name : String) (kind : SyntaxNodeKind) (anonymous := true) (isPs
     checkNoWsBefore "no space before spliced term" >> antiquotExpr >>
     nameP
 
-@[inline] def withAntiquotFn (antiquotP p : ParserFn) : ParserFn := fun c s =>
+@[inline] def withAntiquotFn (antiquotP p : ParserFn) (isCatAntiquot := false) : ParserFn := fun c s =>
   -- fast check that is false in most cases
   if c.input.get s.pos == '$' then
-    -- do not allow antiquotation choice nodes here as `antiquotP` is the strictly more general antiquotation than any in `p`
-    orelseFnCore (mergeAntiquots := false) antiquotP p c s
+    -- Do not allow antiquotation choice nodes here as `antiquotP` is the strictly more general
+    -- antiquotation than any in `p`.
+    -- If it is a category antiquotation, do not backtrack into the category at all as that would
+    -- run *all* parsers of the category, and trailing parsers will later be applied anyway.
+    orelseFnCore (antiquotBehavior := if isCatAntiquot then .acceptLhs else .takeLongest) antiquotP p c s
   else
     p c s
 
@@ -1833,7 +1848,7 @@ def leadingParserAux (kind : Name) (tables : PrattParsingTables) (behavior : Lea
   mkResult s iniSz
 
 @[inline] def leadingParser (kind : Name) (tables : PrattParsingTables) (behavior : LeadingIdentBehavior) (antiquotParser : ParserFn) : ParserFn :=
-  withAntiquotFn antiquotParser (leadingParserAux kind tables behavior)
+  withAntiquotFn (isCatAntiquot := true) antiquotParser (leadingParserAux kind tables behavior)
 
 def trailingLoopStep (tables : PrattParsingTables) (left : Syntax) (ps : List (Parser × Nat)) : ParserFn := fun c s =>
   longestMatchFn left (ps ++ tables.trailingParsers) c s