feat: introduce SepArray and use it for sepBy antiquotation splices

src/Init/Meta.lean

@@ -267,6 +267,12 @@ namespace Syntax
 def mkSep (a : Array Syntax) (sep : Syntax) : Syntax :=
   mkNullNode <| mkSepArray a sep
 
+def SepArray.ofElems {sep} (elems : Array Syntax) : SepArray sep :=
+⟨mkSepArray elems (mkAtom sep)⟩
+
+instance (sep) : Coe (Array Syntax) (SepArray sep) :=
+⟨SepArray.ofElems⟩
+
 /-- Create syntax representing a Lean term application, but avoid degenerate empty applications. -/
 def mkApp (fn : Syntax) : (args : Array Syntax) → Syntax
   | #[]  => fn
@@ -675,6 +681,16 @@ def mapSepElems (a : Array Syntax) (f : Syntax → Syntax) : Array Syntax :=
 
 end Array
 
+namespace Lean.Syntax.SepArray
+
+def getElems {sep} (sa : SepArray sep) : Array Syntax :=
+sa.elemsAndSeps.getSepElems
+
+instance (sep) : Coe (SepArray sep) (Array Syntax) :=
+⟨getElems⟩
+
+end Lean.Syntax.SepArray
+
 /--
   Gadget for automatic parameter support. This is similar to the `optParam` gadget, but it uses
   the given tactic.

src/Init/Prelude.lean

@@ -1689,6 +1689,12 @@ def getPos (stx : Syntax) : Option String.Pos :=
   | some info => info.pos
   | _         => none
 
+/--
+  An array of syntax elements interspersed with separators. Can be coerced to/from `Array Syntax` to automatically
+  remove/insert the separators. -/
+structure SepArray (sep : String) :=
+(elemsAndSeps : Array Syntax)
+
 end Syntax
 
 def mkAtomFrom (src : Syntax) (val : String) : Syntax :=

src/Lean/Elab/Quotation.lean

@@ -29,6 +29,10 @@ private partial def floatOutAntiquotTerms : Syntax → StateT (Syntax → TermEl
     Syntax.node k (← args.mapM floatOutAntiquotTerms)
   | stx => pure stx
 
+private def getSepFromSplice (splice : Syntax) : Syntax := do
+  let Syntax.atom _ sep ← getAntiquotSpliceSuffix splice | unreachable!
+  Syntax.mkStrLit (sep.dropRight 1)
+
 -- Elaborate the content of a syntax quotation term
 private partial def quoteSyntax : Syntax → TermElabM Syntax
   | Syntax.ident info rawVal val preresolved => do
@@ -52,7 +56,7 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax
       let empty ← `(Array.empty);
       -- if escaped antiquotation, decrement by one escape level
       let stx := unescapeAntiquot stx
-      let args ← stx.getArgs.foldlM (fun args arg =>
+      let args ← stx.getArgs.foldlM (fun args arg => do
         if k == nullKind && isAntiquotSuffixSplice arg then
           let antiquot := getAntiquotSuffixSpliceInner arg
           match antiquotSuffixSplice? arg with
@@ -60,12 +64,9 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax
             | some x => Array.empty.push x
             | none   => Array.empty))
           | `many     => `(Array.appendCore $args $(getAntiquotTerm antiquot))
-          | `sepBy    => do
-            let Syntax.atom _ sep ← getAntiquotSuffixSpliceSuffix arg | unreachable!
-            let sep := Syntax.mkStrLit (sep.dropRight 1)
-            `(Array.appendCore $args (mkSepArray $(getAntiquotTerm antiquot) (mkAtom $sep)))
+          | `sepBy    => `(Array.appendCore $args (@SepArray.elemsAndSeps $(getSepFromSplice arg) $(getAntiquotTerm antiquot)))
           | k         => throwErrorAt! arg "invalid antiquotation suffix splice kind '{k}'"
-        else if k == nullKind && isAntiquotScope arg then do
+        else if k == nullKind && isAntiquotScope arg then
           let k := antiquotScopeKind? arg
           let (arg, bindLets) ← floatOutAntiquotTerms arg |>.run pure
           let inner ← (getAntiquotScopeContents arg).mapM quoteSyntax
@@ -84,8 +85,7 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax
             | _ => throwErrorAt stx "too many antiquotations in antiquotation scope; don't be greedy"
           let arr ←
             if k == `sepBy then
-              let Syntax.atom _ sep ← getAntiquotScopeSuffix arg | unreachable!
-              `(mkSepArray $arr (mkAtom $(Syntax.mkStrLit (sep.dropRight 1))))
+              `(mkSepArray $arr (mkAtom $(getSepFromSplice arg)))
             else arr
           let arr ← bindLets arr
           `(Array.appendCore $args $arr)
@@ -213,7 +213,7 @@ private def getHeadInfo (alt : Alt) : HeadInfo :=
       unconditional fun rhs => match antiquotSuffixSplice? quoted[0] with
         | `optional => `(let $anti := Syntax.getOptional? discr; $rhs)
         | `many     => `(let $anti := Syntax.getArgs discr; $rhs)
-        | `sepBy    => `(let $anti := Array.getSepElems (Syntax.getArgs discr); $rhs)
+        | `sepBy    => `(let $anti := @SepArray.mk $(getSepFromSplice quoted[0]) (Syntax.getArgs discr); $rhs)
         | k         => throwErrorAt! quoted "invalid antiquotation suffix splice kind '{k}'"
       -- TODO: support for more complex antiquotation splices
     else if quoted.getArgs.size == 1 && isAntiquotScope quoted[0] then

src/Lean/Syntax.lean

@@ -395,8 +395,12 @@ def isAntiquotScope (stx : Syntax) : Bool :=
 def getAntiquotScopeContents (stx : Syntax) : Array Syntax :=
   stx[3].getArgs
 
-def getAntiquotScopeSuffix (stx : Syntax) : Syntax :=
-  stx[5]
+-- `$[..],*` or `$x,*` ~> `,*`
+def getAntiquotSpliceSuffix (stx : Syntax) : Syntax :=
+  if stx.isAntiquotScope then
+    stx[5]
+  else
+    stx[1]
 
 -- `$x,*` etc.
 def antiquotSuffixSplice? : Syntax → Option SyntaxNodeKind
@@ -410,9 +414,5 @@ def isAntiquotSuffixSplice (stx : Syntax) : Bool :=
 def getAntiquotSuffixSpliceInner (stx : Syntax) : Syntax :=
   stx[0]
 
--- `",*"` in the example above
-def getAntiquotSuffixSpliceSuffix (stx : Syntax) : Syntax :=
-  stx[1]
-
 end Syntax
 end Lean

tests/lean/StxQuot.lean

@@ -37,7 +37,7 @@ end Lean.Syntax
 #eval run $ do let a ← `(∀ _, c); match a with `(∀ $a, $e) => pure a | _ => pure a
 #eval run $ do let a ← `(a); match a with `($id:ident) => pure id | _ => pure a
 #eval run $ do let a ← `(a.{0}); match a with `($id:ident) => pure id | _ => pure a
-#eval run $ do let a ← `(match a with | a => 1 | _ => 2); match a with `(match $e with $[|]? $eqns:matchAlt|*) => pure eqns | _ => pure #[]
+#eval run $ do let a ← `(match a with | a => 1 | _ => 2); match a with `(match $e with $[|]? $eqns:matchAlt|*) => pure eqns.elemsAndSeps | _ => pure #[]
 
 def f (stx : Syntax) : Unhygienic Syntax := match stx with
   | `({ a := a $[: $a]?}) => `({ a := a $[: $(id a)]?})

tests/lean/StxQuot.lean.expected.out

@@ -26,7 +26,7 @@
 "(Term.simpleBinder [(Term.hole \"_\")] [])"
 "`a._@.UnhygienicMain._hyg.1"
 "(Term.explicitUniv `a._@.UnhygienicMain._hyg.1 \".{\" [(numLit \"0\")] \"}\")"
-"#[(Term.matchAlt [`a._@.UnhygienicMain._hyg.1] \"=>\" (numLit \"1\")), (Term.matchAlt [(Term.hole \"_\")] \"=>\" (numLit \"2\"))]"
+"#[(Term.matchAlt [`a._@.UnhygienicMain._hyg.1] \"=>\" (numLit \"1\")), \"|\", (Term.matchAlt [(Term.hole \"_\")] \"=>\" (numLit \"2\"))]"
 "(Term.structInst\n \"{\"\n []\n [[(Term.structInstField (Term.structInstLVal `a._@.UnhygienicMain._hyg.1 []) \":=\" `a._@.UnhygienicMain._hyg.1) []]]\n (Term.optEllipsis [])\n [\":\" `a._@.UnhygienicMain._hyg.1]\n \"}\")"
 "(Term.structInst\n \"{\"\n []\n [[(Term.structInstField (Term.structInstLVal `a._@.UnhygienicMain._hyg.1 []) \":=\" `a._@.UnhygienicMain._hyg.1) []]]\n (Term.optEllipsis [])\n []\n \"}\")"
 "(Command.section \"section\" [])"