From cf85080e7a97496ac6dd7da1867f93ccbe53985d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 17 Sep 2020 12:20:57 -0700
Subject: [PATCH] feat: proper support for `nullKind` at `evalTactic`

@Kha When we write command macros, we can easily expand a command
into multiple ones by using `mkNullNode [cmd_1, ... cmd_n]`. Before
this commit, a tactic macro that expands into a sequence of tactics
had to produce `mkNullNode [tac_1, "; ", ..., "; ", tac_n]`.
I forgot the ";" a few times, and it produces very counterintuitive
behavior. This commit is the last step for fixing this issue.
The previous commits add the `withResultOf p f` combinator that allows
us to implement variants of the `unboxSingleton` trick. Now,
```
`(tactic| t)
```
Produces just `t` as before, but
```
`(tactic| t_1; t_2)
```
produces
```
Syntax.node `Tactic.seq [[t_1, "; ", t_2]]
```
instead of
```
Syntax.node `null [t_1, "; ", t_2]
```
---
 src/Lean/Elab/Tactic/Basic.lean | 5 ++---
 src/Lean/Elab/Tactic/Match.lean | 5 +----
 2 files changed, 3 insertions(+), 7 deletions(-)

diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index aeddcf1206..7bff2ae1ae 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -152,9 +152,8 @@ partial def evalTactic : Syntax → TacticM Unit
 | stx => withRef stx $ withIncRecDepth $ withFreshMacroScope $ match stx with
   | Syntax.node k args =>
     if k == nullKind then
-      -- list of tactics separated by `;` => evaluate in order
-      -- Syntax quotations can return multiple ones
-      stx.forSepArgsM evalTactic
+      -- Macro writers create a sequence of tactics `t₁ ... tₙ` using `mkNullNode #[t₁, ..., tₙ]`
+      stx.getArgs.forM evalTactic
     else do
       trace `Elab.step fun _ => stx;
       env ← getEnv;
diff --git a/src/Lean/Elab/Tactic/Match.lean b/src/Lean/Elab/Tactic/Match.lean
index 766b24319c..6000c94197 100644
--- a/src/Lean/Elab/Tactic/Match.lean
+++ b/src/Lean/Elab/Tactic/Match.lean
@@ -44,15 +44,12 @@ private def mkAuxiliaryMatchTerm (parentTag : Name) (matchTac : Syntax) : MacroM
 (matchTerm, s) ← (mkAuxiliaryMatchTermAux parentTag matchTac).run {};
 pure (matchTerm, s.cases)
 
-def mkTacticSeq (ref : Syntax) (tacs : Array Syntax) : Syntax :=
-mkSepStx tacs (mkAtomFrom ref "; ")
-
 @[builtinTactic Lean.Parser.Tactic.match] def evalMatch : Tactic :=
 fun stx => do
   tag ← getMainTag;
   (matchTerm, cases) ← liftMacroM $ mkAuxiliaryMatchTerm tag stx;
   refineMatchTerm ← `(tactic| refine $matchTerm);
-  let stxNew := mkTacticSeq stx (#[refineMatchTerm] ++ cases);
+  let stxNew := mkNullNode (#[refineMatchTerm] ++ cases);
   withMacroExpansion stx stxNew $ evalTactic stxNew
 
 end Tactic