Is it possible to use "..." in syntax or macro definitions?

Stream: general

[samuela]

I would like to support numpy-esque syntax like arr[i, j, ...]. so far i have not managed to find a way to do this in lean4. is it possible or is this just a locked down symbol?

MWE

[Kenny Lau]

we definitely have something like that for range

[samuela]

@Kenny Lau Interesting, perhaps I'm missing something in my usage? What would the range thing look like?

[Kenny Lau]

@samuela i removed some spaces and it seem to work better:

macro:max "test" "[" indices:term,+ ",...]" : term =>
  `([$indices,*])

#check test[1, 2,...]

[Kenny Lau]

btw next time instead of posting a link it would be better to post the code in #backticks

[Kenny Lau]

it automatically generates a link on the top right corner of the box

[samuela]

ok figured this out:

inductive SliceTerm where
  | Singleton : Nat -> SliceTerm
  | Ellipsis : SliceTerm

instance : OfNat SliceTerm n where
  ofNat := SliceTerm.Singleton n

syntax "..." : term
macro_rules
  | `(...) => `(SliceTerm.Ellipsis)

syntax "test[" term,+ "]" : term
macro_rules
  | `(test[$indices,*]) => `([$indices,*])

#check test[1, 2, ...]

which i'm happy with now

[samuela]

actually this allows for arr[1, ..., 2, ..., 3] which i would like to avoid. it'd be nice to be able to write something to the effect of

syntax "test[" term,* "..." term,* "]" : term

would something like that possible? eg could one match on a specific type of term, esp non-"..." terms?

[Sebastian Ullrich]

If rejecting some syntax combinations during parsing is too hard, you can always do it in the macro/elaborator. That usually leads to better error messages anyway, e.g. "Cannot combine multiple ... in the same indexing operation"

[samuela]

Ah ok, thanks @Sebastian Ullrich ! I didn't realize you could handle that in elaboration