character prefix to int in macro

Stream: lean4

[Siddharth Bhat]

I want to parse numbers such as i32 within a macro. Here's what I have so far:

declare_syntax_cat inum
syntax "i"num : inum

syntax "inum% " inum : term
macro_rules
| `(inum% i$x:numLit) => `($x + 42)

-- def fooNoSpace : Int := (inum% i10)
def fooSpace : Int := (inum% i 10)
#print foo

fooSpace does work and prints 10 + 42. fooNoSpace errors out with:

crash.lean:8:31: error: expected inum

How should I change the macro to allow definitions like i32 or i10?

[Mac]

@Siddharth Bhat as i32 is already an ident, you need a custom parser. I wrote one already for my LLVM IR DSL. The code I used to do so is here: https://github.com/tydeu/lean4-papyrus/blob/master/Papyrus/Script/IntegerType.lean

[Siddharth Bhat]

@Mac Thanks a lot for the pointer. I'm trying to understand how everything fits together. What invokes the decodeIntTypeLit? function? I find zero uses of this function, so I imagine this has to be invoked by some sort of hook?

[Mac]

@Siddharth Bhat oops, nope. I think that is just a leftover from an earlier version of the code.

[Siddharth Bhat]

@Mac is there another example I could take a look at, in that case?

[Mac]

@Siddharth Bhat what do you mean (i.e., what kind of example would you like)?

After then macro at the end of that file the syntaxi32 will expand to integerType 32. If you wanted to change that to, for example. foo 32 you would by changing expandInTypeLitAsType to, for example, an expandIntTypeLitAsFoo which is defined like so:

def expandIntTypeLitAsFoo (stx : Syntax) : MacroM Syntax := do
  mkCAppFrom stx `foo #[← expandIntTypeLitAsNatLit stx]

scoped macro:max (priority := high) x:intTypeLit : term => expandIntTypeLitAsFoo x