Separators for variadic syntax patterns

Stream: metaprogramming / tactics

[Paul Biberstein]

I'm trying to write macros that match on syntax with */+ quantifiers and space as the separator, but am receiving parsing errors when trying to write the syntax patterns. Why is it that this macro is allowed

syntax "Test0" "(" term,* ")" : term
macro_rules
| `(Test0($args:term,*)) => `([$args,*])
#eval Test0(1, 2) -- expecting [1, 2]

But this one is not (note that the only change is the comma separator has been removed in the syntax declaration and the LHS of the macro)

syntax "Test1" "(" term* ")" : term
macro_rules
| `(Test1($args:term*)) => `([$args,*])
#eval Test1(1 2) -- expecting [1, 2]

[Kyle Miller]

The issue is precedence: 1 2 is a perfectly valid term.

Try term:max* instead

[Paul Biberstein]

Ahh I understand thank you. As a follow up, what is the proper way to create syntax that includes a pattern that can be included in a match expression, while also providing element-wise access to the terms in the pattern. For examples, a matches macro like below that can remove some elements of the pattern to match on:

declare_syntax_cat elem
syntax "Foo" : elem
syntax term:max : elem
syntax "Matches" "(" elem+ ")" : term
macro_rules
| `(Matches($pattern:elem*)) =>
  let newPattern := pattern.filter (fun x => match x with
  | `(Foo) => false
  | _ => true)
  `(fun x => match x with
    | $newPattern* => true
    | _ => false)
#guard Matches(List.cons h Foo t Foo) [1,2] -- allowed to have `Foo` wherever in the pattern, it will be removed

[Kyle Miller]

Application syntax isn't just a list of zero or more terms; you need a function followed by arguments. They also need to be Terms, not elems. Maybe this will help:

open Lean
declare_syntax_cat elem
syntax "Foo" : elem
syntax term:max : elem
syntax "Matches" "(" elem+ ")" : term
macro_rules
| `(Matches($pattern:elem*)) => do
  let newPattern : Array Term ← pattern.filterMapM (fun x => match x with
    | `(elem| Foo) => pure none
    | `(elem| $t:term) => pure t
    | _ => Lean.Macro.throwUnsupported)
  let some f := newPattern[0]? | Lean.Macro.throwError "Nothing left after filtering Foo"
  let args := newPattern[1...*]
  `(fun x => match x with
      | $f $args* => true
      | _ => false)
#check Matches(List.cons h Foo t Foo) [1,2]
/-
(fun x =>
    match x with
    | h :: t => true
    | x => false)
  [1, 2] : Bool
-/

[Eric Wieser]

Just to check, :max is more correct than :arg here?