how to match on this syntax?

Stream: lean4

[Arthur Paulino]

I have the following syntax category:

declare_syntax_cat             atom_
...
scoped syntax num noWs "u64" : atom_

Now I'm trying to implement a def elabAtom : TSyntax `atom_ → TermElabM Lean.Expr, but how can I specify the match case for that u64?

I'm trying to parse things like 2u64

[Arthur Paulino]

I've tried some nonsense stuff like | `(atom_| $[$n:num]u64) => ... but I don't know what I'm doing at this point

[Sebastian Ullrich]

Yikes, that may not be possible currently using quotations

[Arthur Paulino]

Aw. Okay then. I'll stick with scoped syntax num noWs "|u64" : atom_ then. | `(atom_| $n:num|u64) works

[Arthur Paulino]

Sebastian Ullrich said:

Yikes, that may not be possible currently using quotations

Oh wait, how can I do it without quotations?

[Sebastian Ullrich]

In the end it's just an inductive data type. See Syntax.getArg. set_option pp.raw might be helpful for visualizing the internal structure.

[Arthur Paulino]

Sorry, I'm a bit lost here. How can I use pp.raw to help me?

[Sebastian Ullrich]

If you have an example command that uses the notation, you can for example combine the option with trace.Elab.input to see the structure. But really there is not much guesswork needed in this case, stx.raw[0].toNat should give you the num's value.

[Sebastian Ullrich]

Ah sorry, you still have to check the syntax kind (stx.getKind) to decide which atom kind you are looking at of course. You might want to use syntax (name := ...) so you don't have to rely on the generated name.

[Arthur Paulino]

scoped syntax (name := atom_u64) num noWs "u64" : atom_

  | stx =>
    if stx.raw.getKind == `atom_u64 then do
      mkAppM ``Atom.u64 #[← mkAppM ``UInt64.ofNat #[mkNatLit stx.raw[0].toNat]]
    else throwUnsupportedSyntax

[Arthur Paulino]

Thanks!!