Stream: lean4

Topic: Nested sepBy

Calvin Lee (Mar 18 2021 at 05:41):

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 (Mar 18 2021 at 05:42):

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

Calvin Lee (Mar 18 2021 at 05:43):

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 (Mar 18 2021 at 05:47):

hm, you're right. #mwe?

Calvin Lee (Mar 18 2021 at 05:47):

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

Calvin Lee (Mar 18 2021 at 05:53):

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 (Mar 18 2021 at 05:58):

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

Mario Carneiro (Mar 18 2021 at 06:01):

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 (Mar 18 2021 at 06:02):

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 (Mar 18 2021 at 06:02):

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 (Mar 18 2021 at 06:03):

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 (Mar 18 2021 at 06:04):

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 (Mar 18 2021 at 06:05):

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 (Mar 18 2021 at 06:06):

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

Mario Carneiro (Mar 18 2021 at 06:06):

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

Mario Carneiro (Mar 18 2021 at 06:09):

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 (Mar 18 2021 at 09:14):

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

Last updated: May 07 2021 at 13:21 UTC