Nested `sepBy`

Stream: lean4

[Calvin Lee]

Hi, I'm writing a macro that takes input like this: [[1,2,3],[4,5,6]]
I've tried writing "[" sepBy("[" sepBy(num, ", ") "]", ", ") "]" for the syntax this macro uses, but when I give it the input I desire it gives me the error expected ] on the second [

[Mario Carneiro]

It looks like you are using C-style function syntax, I don't think lean uses that anywhere

[Calvin Lee]

I'm writing this the same way as in https://github.com/leanprover/lean4/blob/master/src/Init/Data/Array/Basic.lean#L507

[Mario Carneiro]

hm, you're right. #mwe?

[Calvin Lee]

I'm currently using vectors, but I'll change it up so it uses arrays for one

[Calvin Lee]

Ok so this is what I'm doing (and it should work on its own) I can try to make this more minimal but I thought you might want to know my use case too. So the first macro generates a random multidimensional array and the second macro generates multiple terms that are all multidimensional arrays

syntax numArr := "[" sepBy(num, ", ") "]"

syntax "rand_multi_dim_arr_const%" numArr num num : term

macro_rules
  | `(rand_multi_dim_arr_const% [$nums,*] $s1 $s2) =>
    open Lean in do
      let nums : Array Syntax := nums
      if nums.size = 0 then
        let (val, _) : (Nat ×  StdGen) := randNat ⟨s1.toNat, s2.toNat⟩ 0 UInt64.size
        `($(quote val))
      else
        let (⟨s1, s2⟩,⟨s3, s4⟩) := stdSplit ⟨s1.toNat, s2.toNat⟩
        let n : Syntax := nums[0]
        match n.toNat with
          | 0 =>`(#[])
          | (Nat.succ n) =>
          `((rand_multi_dim_arr_const% [$(nums.set! 0 (quote n)),*] $(quote s1) $(quote s2)).push
            (rand_multi_dim_arr_const% [$(nums[1:]),*] $(quote s3) $(quote s4)))

/- Helper syntax for defining a bunch of random vecs. -/
syntax "gen_rand_arrs%" ident num numArr num num : command
/-
`gen_rand_arrs id [a,b,c] s` creates three random Vecs of dimension `a`, `b` and `c` respectively with
names `id_1`, `id_2` and `id_3` with random seed `s`.
-/
syntax numArrArr := "[" sepBy(numArr, ", ") "]"

macro_rules
  | `(gen_rand_arrs% $id $n [$elems,*] $s1 $s2) =>
    open Lean in --set_option trace.Meta.debug true in
      let elems : Array Syntax := elems
      if elems.size = 0 then
        return mkNullNode
      else
        let (⟨s1, s2⟩,⟨s3, s4⟩) := stdSplit ⟨s1.toNat, s2.toNat⟩
        let n := n.toNat
        let currId := id.getId.appendIndexAfter n
        `(def $(mkIdentFrom id currId) := rand_multi_dim_arr_const% $(elems[0]) $(quote s1) $(quote s2)
          gen_rand_vecs% $id $(quote (n+1)) [$(elems[1:]),*] $(quote s3) $(quote s4))

gen_rand_arrs% zobrist 1 [[5,5,5], [5,5,2]] 1 1

[Calvin Lee]

oooh wait I may have found my bug. In the meantime, any idea why sepBy has that syntax?

[Mario Carneiro]

I think numArrArr is not used in your code, you want this:

macro_rules
  | `(gen_rand_arrs% $id $n [$elems:numArr,*] $s1 $s2) =>
    open Lean in --set_option trace.Meta.debug true in
      let elems : Array Syntax := elems
      if elems.size = 0 then
        return mkNullNode
      else
        let (⟨s1, s2⟩,⟨s3, s4⟩) := stdSplit ⟨s1.toNat, s2.toNat⟩
        let n := n.toNat
        let currId := id.getId.appendIndexAfter n
        `(def $(mkIdentFrom id currId) := rand_multi_dim_arr_const% $(elems[0]) $(quote s1) $(quote s2)
          gen_rand_vecs% $id $(quote (n+1)) [$(elems[1:]),*] $(quote s3) $(quote s4))

gen_rand_arrs% zobrist 1 [[5,5,5], [5,5,2]] 1 1

[Calvin Lee]

yes indeed, I had it used in my macro but not its helper....
I can't believe I only realized after sending it to the chat :face_palm:

[Mario Carneiro]

If you want numArrArr to populate a global syntax class like term, you should write

syntax (name := numArrArr) "[" sepBy(numArr, ", ") "]" : term

(I think)

[Calvin Lee]

I don't think that's so necessary because I only need it to generate two large arrays of hashes, nice trick though

[Mario Carneiro]

I suspect you don't even need to declare a custom syntax for this, you can just use a regular term and evaluate it as a List (List Nat)

[Calvin Lee]

Really? I was trying to do something like parse syntax as a list in my code, but I wasn't able to do it since there isn't a toList like there is a toNat. The only option seemed to be "make everything SepArrays"

[Mario Carneiro]

in lean 3 there is eval_expr that will evaluate an expr into any type with a has_reflect instance

[Mario Carneiro]

It's basically equivalent to using #eval on the expression and passing the result to the tactic

[Mario Carneiro]

There is also Lean.Elab.Term.evalExpr but it is both unsafe and in TermElabM so it might be hard to use in a macro

[Sebastian Ullrich]

If you expect the term input of your macro to syntactically be a list of lists, you can just match against that syntax inside the macro