Quotation for list of list of string

Stream: lean4

[Adam Topaz]

I'm trying to write an elaborator that takes takes some syntax which is a list, separated by ;, of lists of strings, separated by ,, but I'm having a hard time figuring out how to write the necessary quotation... Can someone point me in the right direction?

import Lean
open Lean

syntax "foo%" ((str,*) ";")* : term

open Lean Elab Term
elab_rules : term
  | `(foo%) => sorry
  | `(foo% $xs;) => sorry -- xs : TSyntax `str ???
  -- recursive step???

In the exapmle above, the single case gives me a string literal for xs, where I would have expected an array of string literals. And I don't even know how to start writing the recursive step which considers more than one list of string literals.

[Kyle Miller]

Maybe look at docs#Matrix.matrixNotation for inspiration? It's a little more complicated than what you need, since it's handling the case of 0 x n and m x 0 matrices.

[Adam Topaz]

Thanks Kyle! Yes I should have thought of that -- this is essentially exactly the same sort of parsing I'm trying to do

[Kyle Miller]

Then again, here you go:

syntax "foo%" sepBy((str,*),";") : term

open Lean Elab Term

elab_rules : term
  | `(foo% $[$[$xss],*];*) => sorry -- xss : Array (Array (TSyntax `str))

[Kyle Miller]

(Untested beyond not seeing any errors!)

[Adam Topaz]

Amazing! Thanks! I always seem to have a hard time remembering where to put the [,] and $ :)

[Patrick Massot]

Adam, you're not alone...

[Adam Topaz]

We really need some cheatsheet with very many examples of this sort!

[Johan Commelin]

It somehow makes me think of Perl...

[Adam Topaz]

Is that a good or bad thing?

[Patrick Massot]

I think it's meant to make you think of racket.

[Sebastian Ullrich]

Rust, actually