parsing keyword followed by number without whitespace

Stream: lean4

[Michael Sammler]

Hi, I would like to define a syntax such that it can parse numbers of the form bv1, bv2, ... as 1, 2, ... However, Lean always parses bv1 as an identifier instead of bv followed by the number 1, even for a syntax category where there are no identifiers allowed. Is there a way around this?

The following illustrates the problem

import Lean

open Lean Elab Meta

declare_syntax_cat test
syntax "bv" noWs num : test

def elabTest : Syntax → MetaM Expr
  | `(test| bv$n) => do
    return mkNatLit n.getNat
  | _ => throwUnsupportedSyntax

elab "test_elab " e:test : term => elabTest e

#check test_elab bv2
-- fails with unexpected identifier; expected test
-- should print 2 : Nat

[Aaron Liu]

You can try #bv1, which I don't think is a legel identifier

[Michael Sammler]

Indeed, using '#bv1` would probably work. The problem is that I have an existing format that I would like to parse, so I would be interested if there are ways to do this without changing the format.

[Sebastian Ullrich]

You can always accept any identifiers and then parse/reject them when elaborating the syntax tree

[Michael Sammler]

This sounds like it would be what I need. Do you have a pointer where I can see / learn how I can parse during elaboration?
So far, I have based my code on Metaprogramming in Lean, but I do not think this book explains how to call the parser from the elaborator.

[Sebastian Ullrich]

Oh I would parse that tiny remaining grammar manually, calling back into the Lean parser isn't necessary there

[Michael Sammler]

I see, that is probably the easiest indeed. This approach seems to work! :tada: Thank you for your help!

import Lean

open Lean Elab Meta

declare_syntax_cat test
syntax ident : test

def elabTest : Syntax → MetaM Expr
  | `(test| $i:ident) => do
    let s := i.getId.toString
    unless s.startsWith "bv" do
      throwUnsupportedSyntax
    let s' := s.drop 2
    let .some n := s'.toNat? | throwUnsupportedSyntax
    return mkNatLit n
  | _ => throwUnsupportedSyntax

elab "test_elab " e:test : term => elabTest e

#check test_elab bv2