From ab36ed477e1ab985e7b5eb0bfed03ec9789b5de5 Mon Sep 17 00:00:00 2001 From: Leni Aniva <107011294+vleni@users.noreply.github.com> Date: Fri, 17 Nov 2023 04:31:41 -0800 Subject: [PATCH] feat: allow trailing comma in tuples, lists, and tactics (#2643) --- src/Init/Data/List/Basic.lean | 39 ++++++++++++++++++++++ src/Init/Notation.lean | 34 ------------------- src/Init/Tactics.lean | 6 ++-- src/Lean/Parser/Term.lean | 4 +-- tests/compiler/tuple.lean | 6 ++++ tests/compiler/tuple.lean.expected.out | 1 + tests/lean/StxQuot.lean | 2 +- tests/lean/trailingComma.lean | 17 ++++++++++ tests/lean/trailingComma.lean.expected.out | 4 +++ 9 files changed, 73 insertions(+), 40 deletions(-) create mode 100644 tests/compiler/tuple.lean create mode 100644 tests/compiler/tuple.lean.expected.out create mode 100644 tests/lean/trailingComma.lean create mode 100644 tests/lean/trailingComma.lean.expected.out diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean index bfbb0db0ff..f7ed064025 100644 --- a/src/Init/Data/List/Basic.lean +++ b/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} diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index d8b8734549..e74a543faf 100644 --- a/src/Init/Notation.lean +++ b/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. diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index cc4272d203..5e836be033 100644 --- a/src/Init/Tactics.lean +++ b/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`, .... diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index c0f4f56ce5..1d79f4ab1b 100644 --- a/src/Lean/Parser/Term.lean +++ b/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 diff --git a/tests/compiler/tuple.lean b/tests/compiler/tuple.lean new file mode 100644 index 0000000000..5fd0be76a6 --- /dev/null +++ b/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,)) diff --git a/tests/compiler/tuple.lean.expected.out b/tests/compiler/tuple.lean.expected.out new file mode 100644 index 0000000000..1e8b314962 --- /dev/null +++ b/tests/compiler/tuple.lean.expected.out @@ -0,0 +1 @@ +6 diff --git a/tests/lean/StxQuot.lean b/tests/lean/StxQuot.lean index 747c282871..a8aa5ca3b5 100644 --- a/tests/lean/StxQuot.lean +++ b/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) diff --git a/tests/lean/trailingComma.lean b/tests/lean/trailingComma.lean new file mode 100644 index 0000000000..380b244eed --- /dev/null +++ b/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,] diff --git a/tests/lean/trailingComma.lean.expected.out b/tests/lean/trailingComma.lean.expected.out new file mode 100644 index 0000000000..99655e8904 --- /dev/null +++ b/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 ')'