feat: allow trailing comma in tuples, lists, and tactics (#2643)

src/Init/Data/List/Basic.lean

@@ -6,9 +6,48 @@ Author: Leonardo de Moura
 prelude
 import Init.SimpLemmas
 import Init.Data.Nat.Basic
+import Init.Data.Nat.Div
 set_option linter.missingDocs true -- keep it documented
 open Decidable List
 
+/--
+The syntax `[a, b, c]` is shorthand for `a :: b :: c :: []`, or
+`List.cons a (List.cons b (List.cons c List.nil))`. It allows conveniently constructing
+list literals.
+
+For lists of length at least 64, an alternative desugaring strategy is used
+which uses let bindings as intermediates as in
+`let left := [d, e, f]; a :: b :: c :: left` to avoid creating very deep expressions.
+Note that this changes the order of evaluation, although it should not be observable
+unless you use side effecting operations like `dbg_trace`.
+-/
+syntax "[" withoutPosition(term,*,?) "]"  : term
+
+/--
+Auxiliary syntax for implementing `[$elem,*]` list literal syntax.
+The syntax `%[a,b,c|tail]` constructs a value equivalent to `a::b::c::tail`.
+It uses binary partitioning to construct a tree of intermediate let bindings as in
+`let left := [d, e, f]; a :: b :: c :: left` to avoid creating very deep expressions.
+-/
+syntax "%[" withoutPosition(term,*,? " | " term) "]" : term
+
+namespace Lean
+
+macro_rules
+  | `([ $elems,* ]) => do
+    -- NOTE: we do not have `TSepArray.getElems` yet at this point
+    let rec expandListLit (i : Nat) (skip : Bool) (result : TSyntax `term) : MacroM Syntax := do
+      match i, skip with
+      | 0,   _     => pure result
+      | i+1, true  => expandListLit i false result
+      | i+1, false => expandListLit i true  (← ``(List.cons $(⟨elems.elemsAndSeps.get! i⟩) $result))
+    let size := elems.elemsAndSeps.size
+    if size < 64 then
+      expandListLit size (size % 2 == 0) (← ``(List.nil))
+    else
+      `(%[ $elems,* | List.nil ])
+end Lean
+
 universe u v w
 
 variable {α : Type u} {β : Type v} {γ : Type w}

src/Init/Notation.lean

@@ -461,42 +461,8 @@ expected type is known. So, `without_expected_type` is not effective in this cas
 -/
 macro "without_expected_type " x:term : term => `(let aux := $x; aux)
 
-/--
-The syntax `[a, b, c]` is shorthand for `a :: b :: c :: []`, or
-`List.cons a (List.cons b (List.cons c List.nil))`. It allows conveniently constructing
-list literals.
-
-For lists of length at least 64, an alternative desugaring strategy is used
-which uses let bindings as intermediates as in
-`let left := [d, e, f]; a :: b :: c :: left` to avoid creating very deep expressions.
-Note that this changes the order of evaluation, although it should not be observable
-unless you use side effecting operations like `dbg_trace`.
--/
-syntax "[" withoutPosition(term,*) "]"  : term
-
-/--
-Auxiliary syntax for implementing `[$elem,*]` list literal syntax.
-The syntax `%[a,b,c|tail]` constructs a value equivalent to `a::b::c::tail`.
-It uses binary partitioning to construct a tree of intermediate let bindings as in
-`let left := [d, e, f]; a :: b :: c :: left` to avoid creating very deep expressions.
--/
-syntax "%[" withoutPosition(term,* " | " term) "]" : term
-
 namespace Lean
 
-macro_rules
-  | `([ $elems,* ]) => do
-    -- NOTE: we do not have `TSepArray.getElems` yet at this point
-    let rec expandListLit (i : Nat) (skip : Bool) (result : TSyntax `term) : MacroM Syntax := do
-      match i, skip with
-      | 0,   _     => pure result
-      | i+1, true  => expandListLit i false result
-      | i+1, false => expandListLit i true  (← ``(List.cons $(⟨elems.elemsAndSeps.get! i⟩) $result))
-    if elems.elemsAndSeps.size < 64 then
-      expandListLit elems.elemsAndSeps.size false (← ``(List.nil))
-    else
-      `(%[ $elems,* | List.nil ])
-
 /--
 Category for carrying raw syntax trees between macros; any content is printed as is by the pretty printer.
 The only accepted parser for this category is an antiquotation.

src/Init/Tactics.lean

@@ -435,14 +435,14 @@ non-dependent hypotheses. It has many variants:
   other hypotheses.
 -/
 syntax (name := simp) "simp" (config)? (discharger)? (&" only")?
-  (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*) "]")? (location)? : tactic
+  (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "]")? (location)? : tactic
 /--
 `simp_all` is a stronger version of `simp [*] at *` where the hypotheses and target
 are simplified multiple times until no simplification is applicable.
 Only non-dependent propositional hypotheses are considered.
 -/
 syntax (name := simpAll) "simp_all" (config)? (discharger)? (&" only")?
-  (" [" withoutPosition((simpErase <|> simpLemma),*) "]")? : tactic
+  (" [" withoutPosition((simpErase <|> simpLemma),*,?) "]")? : tactic
 
 /--
 The `dsimp` tactic is the definitional simplifier. It is similar to `simp` but only
@@ -450,7 +450,7 @@ applies theorems that hold by reflexivity. Thus, the result is guaranteed to be
 definitionally equal to the input.
 -/
 syntax (name := dsimp) "dsimp" (config)? (discharger)? (&" only")?
-  (" [" withoutPosition((simpErase <|> simpLemma),*) "]")? (location)? : tactic
+  (" [" withoutPosition((simpErase <|> simpLemma),*,?) "]")? (location)? : tactic
 
 /--
 `delta id1 id2 ...` delta-expands the definitions `id1`, `id2`, ....

src/Lean/Parser/Term.lean

@@ -164,7 +164,7 @@ do not yield the right result.
   "(" >> (withoutPosition (withoutForbidden (termParser >> " :" >> optional (ppSpace >> termParser)))) >> ")"
 /-- Tuple notation; `()` is short for `Unit.unit`, `(a, b, c)` for `Prod.mk a (Prod.mk b c)`, etc. -/
 @[builtin_term_parser] def tuple := leading_parser
-  "(" >> optional (withoutPosition (withoutForbidden (termParser >> ", " >> sepBy1 termParser ", "))) >> ")"
+  "(" >> optional (withoutPosition (withoutForbidden (termParser >> ", " >> sepBy1 termParser ", " (allowTrailingSep := true)))) >> ")"
 /--
 Parentheses, used for grouping expressions (e.g., `a * (b + c)`).
 Can also be used for creating simple functions when combined with `·`. Here are some examples:
@@ -184,7 +184,7 @@ are turned into a new anonymous constructor application. For example,
 `⟨a, b, c⟩ : α × (β × γ)` is equivalent to `⟨a, ⟨b, c⟩⟩`.
 -/
 @[builtin_term_parser] def anonymousCtor := leading_parser
-  "⟨" >> withoutPosition (withoutForbidden (sepBy termParser ", ")) >> "⟩"
+  "⟨" >> withoutPosition (withoutForbidden (sepBy termParser ", " (allowTrailingSep := true))) >> "⟩"
 def optIdent : Parser :=
   optional (atomic (ident >> " : "))
 def fromTerm   := leading_parser

tests/compiler/tuple.lean

@@ -0,0 +1,6 @@
+
+@[noinline] def f (a : Nat × Nat × Nat) : Nat:=
+  a.fst + a.snd.fst + a.snd.snd
+
+def main : IO Unit := do
+  IO.println (f (1, 2, 3,))

tests/compiler/tuple.lean.expected.out

@@ -0,0 +1 @@
+6

tests/lean/StxQuot.lean

@@ -16,7 +16,7 @@ namespace Lean.Syntax
 #eval run $ let id := miss; `($id + 1)
 end Lean.Syntax
 #eval run `(1 + 1)
-#eval run `([x,])
+#eval run `([x+])
 #eval run $ `(fun a => a) >>= pure
 #eval run $ `(def foo := 1)
 #eval run $ `(def foo := 1 def bar := 2)

tests/lean/trailingComma.lean

@@ -0,0 +1,17 @@
+import Lean
+open Lean
+
+#eval [1,2,3,]
+#eval (2,3,)
+#eval [1,2,3,,] -- Errors, double trailing comma
+#eval (4,5,,,) -- ditto
+
+axiom zeroAdd (x : Nat) : 0 + x = x
+theorem rewrite_comma (x y z: Nat) (h₁ : 0 + x = y) (h₂ : 0 + y = z) : x = z := by
+  rewrite [zeroAdd,] at *;
+  subst x;
+  subst y;
+  exact rfl
+
+theorem simp_comma (x: Nat) : x = x := by
+  simp [zeroAdd,]

tests/lean/trailingComma.lean.expected.out

@@ -0,0 +1,4 @@
+[1, 2, 3]
+(2, 3)
+trailingComma.lean:6:13-6:14: error: unexpected token ','; expected ']'
+trailingComma.lean:7:11-7:12: error: unexpected token ','; expected ')'