From 2dafdec000a7f612baba1eb49199776faa9523a9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 17 Sep 2020 12:12:12 -0700
Subject: [PATCH] feat: use `withResultOf` combinator instead of
 `unboxSingleton` parameter

---
 src/Lean/Parser/Basic.lean   | 33 ++++++++++++---------------------
 src/Lean/Parser/Command.lean |  2 +-
 src/Lean/Parser/Syntax.lean  |  4 ++--
 src/Lean/Parser/Tactic.lean  |  1 -
 src/Lean/Parser/Term.lean    | 12 ++++++++++--
 5 files changed, 25 insertions(+), 27 deletions(-)

diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index 66b377b6f3..25e024f818 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -510,21 +510,18 @@ fun c s =>
 { info := noFirstTokenInfo p.info,
   fn   := manyFn p.fn }
 
-@[inline] def many1Fn (p : ParserFn) (unboxSingleton : Bool) : ParserFn :=
+@[inline] def many1Fn (p : ParserFn) : ParserFn :=
 fun c s =>
   let iniSz  := s.stackSize;
   let s := andthenFn p (manyAux p) c s;
-  if s.stackSize - iniSz == 1 && unboxSingleton then
-    s
-  else
-    s.mkNode nullKind iniSz
+  s.mkNode nullKind iniSz
 
-@[inline] def many1 (p : Parser) (unboxSingleton := false) : Parser :=
+@[inline] def many1 (p : Parser) : Parser :=
 { info := p.info,
-  fn   := many1Fn p.fn unboxSingleton }
+  fn   := many1Fn p.fn }
 
 @[specialize] private partial def sepByFnAux (p : ParserFn) (sep : ParserFn) (allowTrailingSep : Bool)
-    (iniSz : Nat) (unboxSingleton : Bool)  : Bool → ParserFn
+    (iniSz : Nat) : Bool → ParserFn
 | pOpt, c, s =>
   let sz  := s.stackSize;
   let pos := s.pos;
@@ -533,10 +530,7 @@ fun c s =>
     if s.pos > pos then s
     else if pOpt then
       let s := s.restore sz pos;
-      if s.stackSize - iniSz == 2 && unboxSingleton then
-        s.popSyntax
-      else
-        s.mkNode nullKind iniSz
+      s.mkNode nullKind iniSz
     else
       -- append `Syntax.missing` to make clear that List is incomplete
       let s := s.pushSyntax Syntax.missing;
@@ -547,22 +541,19 @@ fun c s =>
     let s   := sep c s;
     if s.hasError then
       let s := s.restore sz pos;
-      if s.stackSize - iniSz == 1 && unboxSingleton then
-        s
-      else
-        s.mkNode nullKind iniSz
+      s.mkNode nullKind iniSz
     else
       sepByFnAux allowTrailingSep c s
 
 @[specialize] def sepByFn (allowTrailingSep : Bool) (p : ParserFn) (sep : ParserFn) : ParserFn
 | c, s =>
   let iniSz := s.stackSize;
-  sepByFnAux p sep allowTrailingSep iniSz false true c s
+  sepByFnAux p sep allowTrailingSep iniSz true c s
 
-@[specialize] def sepBy1Fn (allowTrailingSep : Bool) (p : ParserFn) (sep : ParserFn) (unboxSingleton : Bool) : ParserFn
+@[specialize] def sepBy1Fn (allowTrailingSep : Bool) (p : ParserFn) (sep : ParserFn) : ParserFn
 | c, s =>
   let iniSz := s.stackSize;
-  sepByFnAux p sep allowTrailingSep iniSz unboxSingleton false c s
+  sepByFnAux p sep allowTrailingSep iniSz false c s
 
 @[noinline] def sepByInfo (p sep : ParserInfo) : ParserInfo :=
 { collectTokens := p.collectTokens ∘ sep.collectTokens,
@@ -577,9 +568,9 @@ fun c s =>
 { info := sepByInfo p.info sep.info,
   fn   := sepByFn allowTrailingSep p.fn sep.fn }
 
-@[inline] def sepBy1 (p sep : Parser) (allowTrailingSep : Bool := false) (unboxSingleton := false) : Parser :=
+@[inline] def sepBy1 (p sep : Parser) (allowTrailingSep : Bool := false) : Parser :=
 { info := sepBy1Info p.info sep.info,
-  fn   := sepBy1Fn allowTrailingSep p.fn sep.fn unboxSingleton }
+  fn   := sepBy1Fn allowTrailingSep p.fn sep.fn }
 
 /- Apply `f` to the syntax object produced by `p` -/
 @[inline] def withResultOfFn (p : ParserFn) (f : Syntax → Syntax) : ParserFn :=
diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index b961814d06..0903d47332 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -23,7 +23,7 @@ categoryParser `command rbp
   Multiple command will be put in a `null node, but a single command will not (so that you can directly
   match against a quotation in a command kind's elaborator). -/
 -- TODO: use two separate quotation parsers with parser priorities instead
-@[builtinTermParser] def Term.quot := parser! "`(" >> toggleInsideQuot (termParser <|> many1 commandParser true) >> ")"
+@[builtinTermParser] def Term.quot := parser! "`(" >> toggleInsideQuot (termParser <|> unboxSingleton (many1 commandParser)) >> ")"
 
 namespace Command
 def commentBody : Parser :=
diff --git a/src/Lean/Parser/Syntax.lean b/src/Lean/Parser/Syntax.lean
index 8e61288b8c..fdd119e575 100644
--- a/src/Lean/Parser/Syntax.lean
+++ b/src/Lean/Parser/Syntax.lean
@@ -70,8 +70,8 @@ def notationItem := withAntiquot (mkAntiquot "notationItem" `Lean.Parser.Command
 def macroArgSimple := parser! ident >> checkNoWsBefore "no space before ':'" >> ":" >> syntaxParser maxPrec
 def macroArg  := try strLit <|> try macroArgSimple
 def macroHead := macroArg <|> try ident
-def macroTailTactic   : Parser := try (" : " >> identEq "tactic") >> darrow >> ("`(" >> sepBy1 tacticParser "; " true true >> ")" <|> termParser)
-def macroTailCommand  : Parser := try (" : " >> identEq "command") >> darrow >> ("`(" >> many1 commandParser true >> ")" <|> termParser)
+def macroTailTactic   : Parser := try (" : " >> identEq "tactic") >> darrow >> ("`(" >> Tactic.unboxSeq >> ")" <|> termParser)
+def macroTailCommand  : Parser := try (" : " >> identEq "command") >> darrow >> ("`(" >> unboxSingleton (many1 commandParser) >> ")" <|> termParser)
 def macroTailDefault  : Parser := try (" : " >> ident) >> darrow >> (("`(" >> categoryParserOfStack 2 >> ")") <|> termParser)
 def macroTail := macroTailTactic <|> macroTailCommand <|> macroTailDefault
 @[builtinCommandParser] def «macro»       := parser! "macro " >> optPrecedence >> macroHead >> many macroArg >> macroTail
diff --git a/src/Lean/Parser/Tactic.lean b/src/Lean/Parser/Tactic.lean
index 07336c512e..0faed81185 100644
--- a/src/Lean/Parser/Tactic.lean
+++ b/src/Lean/Parser/Tactic.lean
@@ -10,7 +10,6 @@ namespace Parser
 namespace Tactic
 
 def nonEmptySeq := node `Lean.Parser.Tactic.seq $ sepBy1 tacticParser "; " true
-def seq         := node `Lean.Parser.Tactic.seq $ sepBy tacticParser "; " true
 
 def underscoreFn : ParserFn :=
 fun c s =>
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 2d38ebd06b..af90f7cedf 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -254,8 +254,16 @@ stx.isAntiquot || stx.isIdent
 
 end Term
 
--- Use `unboxSingleton` trick similar to the one used at Command.lean for `Term.quot`
-@[builtinTermParser] def Tactic.quot : Parser := parser! "`(tactic|" >> toggleInsideQuot (sepBy1 tacticParser "; " true true) >> ")"
+def Tactic.seq := node `Lean.Parser.Tactic.seq $ sepBy tacticParser "; " true
+-- Similar to `unboxSingleton`, but for `Tactic.seq
+def Tactic.unboxSeq :=
+withResultOf Tactic.seq fun stx =>
+  if (stx.getArg 0).getNumArgs < 2 then
+    (stx.getArg 0).getArg 0
+  else
+    stx
+
+@[builtinTermParser] def Tactic.quot : Parser := parser! "`(tactic|" >> toggleInsideQuot Tactic.unboxSeq >> ")"
 @[builtinTermParser] def Level.quot  : Parser := parser! "`(level|" >> toggleInsideQuot levelParser >> ")"
 
 end Parser