Parser for a custom identifier

Stream: lean4

[Yuri de Wit]

I am creating a syntax for a simple DSL and I would like to reuse the ident parser.

inductive HTerm : Type
...
| ctr (name : String) (args : Array HTerm)

syntax num : rw_term
syntax ident : rw_term
syntax "(" ident rw_term* ")" : rw_term

macro_rules
...
| `(`[rw| ($name $args*) ]) => `(HTerm.ctr (toString $name) #[])

However, this is what I get:

#eval `[rw| 4] -- HTerm.num 4
#eval `[rw| n] -- error: unknown identifier 'n'
#eval `[rw| (Double n)] -- error: unknown identifier 'Double'

What am I missing here? Is there a different ident-like parser I can use to reuse the lexical rules? (Note that str is too open ended and requires quotes around it.

[Sebastian Ullrich]

You are constructing the term toString Double, which is not what you want I assume

[Andrés Goens]

to expand upon that, where you call (toString $name) in your macro rules, you are just interpreting the identifier as a variable name and letting Lean expand that. For what you want, you probably want to construct a string literal out of your identifier, which you could do with something like $(Lean.quote name.getId.toString) instead

[Andrés Goens]

the metaprogramming book might also be quite helpful to read up on this stuff

[Yuri de Wit]

This works now, thanks.

macro_rules
| `(`[rw|$numb:num]) => `(HTerm.num $numb)
| `(`[rw|$name:ident]) => `(HTerm.var $(Lean.quote name.getId.toString))
| `(`[rw|($name $[$arg]*)]) => `(HTerm.ctr $(Lean.quote name.getId.toString) #[])

#eval `[rw| n] -- HTerm.var "n"

[Yuri de Wit]

This was a stupid error: not being careful with what you end up putting inside `() without anti-quoting it. I will sure do this a few more times ... :-)

One thing that makes this harder is that there is a disconnect between the surface syntax "`[rw| n]" and the final syntax that causes the compilation error. Is there a way to dump this final syntax that Lean is using to elaborate?