Zulip Chat Archive
Stream: lean4
Topic: Basic question about recursive macros
Adam Topaz (Apr 27 2023 at 15:07):
It's common to define a function out of List X by pattern matching
-- pseudocode
def foo : List X -> Y
| [] => something
| (x::xs) => something else
Is it possible to do something similar in a macro that takes xs:term,*? I tried playing around with the following, which doesn't quite work:
syntax "a[" term,* "]" : term
macro_rules
| `(a[]) => `(List.nil)
| `(a[ $x, $xs:term,* ]) => `(List.cons $x `(a[$xs:term,*]))
Kyle Miller (Apr 27 2023 at 15:10):
I've found you usually need a 0, 1, and 2+ case due to commas to get these things to work
Adam Topaz (Apr 27 2023 at 15:11):
Hmmm...
macro_rules
| `(a[]) => `(List.nil)
| `(a[$x:term]) => `(List.cons $x List.nil)
| `(a[ $x, $xs:term,* ]) => `(List.cons $x `(a[$xs:term,*]))
#eval (a[1,2] : List Nat)
still gives me an error on the eval line.
Kyle Miller (Apr 27 2023 at 15:13):
Oh, I just noticed, you're quoting `(a[$xs:term,*]) in there. The value of a quote is a Syntax in a monad. You probably mean a[$xs,*] by itself.
Kyle Miller (Apr 27 2023 at 15:13):
syntax "a[" term,* "]" : term
macro_rules
| `(a[]) => `(List.nil)
| `(a[$x]) => `(List.cons $x List.nil)
| `(a[$x, $xs,*]) => `(List.cons $x a[$xs,*])
#check a[1,2,3]
Kyle Miller (Apr 27 2023 at 15:13):
This works, and you do need the length-1 case
Adam Topaz (Apr 27 2023 at 15:14):
Oh of course. Thanks!
Adam Topaz (Apr 27 2023 at 15:16):
I should have caught that -- while I was playing around earlier, I had
| `(a[$x,$xs:term,*]) => do
`(List.cons $x $(← `(a[$xs:term,*])))
at some point, but forgot to get rid of the quotation :)
Kyle Miller (Apr 27 2023 at 15:21):
If you want a non-recursive one, here's using Array.foldrM:
syntax "a[" term,* "]" : term
macro_rules
| `(a[$[$xs],*]) => TSyntax.raw <$> do xs.foldrM (fun (x l : Term) => ``(List.cons $x $l)) (← ``(List.nil))
#check a[1,2,3]
Kyle Miller (Apr 27 2023 at 15:22):
$[$xs],* gives you all the elements in the sequence without the commas.
Adam Topaz (Apr 27 2023 at 15:23):
Kyle Miller said:
$[$xs],*gives you all the elements in the sequence without the commas.
Oh, that's useful to know! I feel like we should have some cheatsheet for all these quotation tricks.
Kyle Miller (Apr 27 2023 at 15:23):
The double backquote Syntax quotations are sort of like double backquote Name literals, where here they check that the names List.nil and List.cons are what you think they are. (They report a tooltip and everything.)
Adam Topaz (Apr 27 2023 at 15:23):
Right, this is where I ended up:
macro_rules
| `(a[]) => ``(List.nil)
| `(a[$x:term]) => ``(List.cons $x List.nil)
| `(a[$x,$xs:term,*]) => ``(List.cons $x a[$xs:term,*])
Adam Topaz (Apr 27 2023 at 15:24):
I am surprised though that
macro_rules
| `(a[]) => ``(List.nil)
| `(a[$x:term]) => ``(List.cns $x List.nil)
| `(a[$x,$xs:term,*]) => ``(List.cons $x a[$xs:term,*])
doesn't register an error.
Kyle Miller (Apr 27 2023 at 15:26):
I suppose I don't really know what double backquote quotations do precisely...
Adam Topaz (Apr 27 2023 at 15:27):
OTOH, this does give an error:
macro_rules
| `(a[]) => ``(List.nil)
| `(a[$x:term]) => ``(Lst.cons $x List.nil)
| `(a[$x,$xs:term,*]) => ``(List.cons $x a[$xs:term,*])
Is something going on with dot notation?
Kyle Miller (Apr 27 2023 at 15:27):
Yeah, I think so. I did a similar test and was going to mention it.
Kyle Miller (Apr 27 2023 at 15:28):
(@Sebastian Ullrich Are double syntax quotations supposed to register an error here? In particular, with the List.cns example a few messages up.)
Adam Topaz (Apr 27 2023 at 15:42):
In case it helps, this does result in an error:
open List in
macro_rules
| `(a[]) => ``(nil)
| `(a[$x:term]) => ``(cns $x List.nil)
| `(a[$x,$xs:term,*]) => ``(cons $x a[$xs:term,*])
Sebastian Ullrich (Apr 27 2023 at 15:56):
Sebastian Ullrich (Apr 27 2023 at 20:01):
Kyle Miller said:
$[$xs],*gives you all the elements in the sequence without the commas.
I usually prefer $xs,* and then xs.getElems for what it's worth
Last updated: Dec 20 2023 at 11:08 UTC