Zulip Chat Archive

Stream: lean4

Topic: Parsing C-style octal number


Yasu Watanabe (Jun 24 2022 at 23:39):

I'm trying to be familiar with syntax extension method of Lean4. I gradually understand It's super flexible and really easy to implement new syntax in straight forward way from like EBNF.

I'm currently try to implement parsing mini language and have a problem parsing C-style octal number by the following code.

declare_syntax_cat oct  -- octal number
declare_syntax_cat oct1 -- leading 0 for octal number
declare_syntax_cat oct_digit -- octal digit one of [0,1,2,3,4,5,6,7]

syntax "0" : oct1
syntax "0" : oct_digit
syntax "1" : oct_digit
syntax "2" : oct_digit
syntax "3" : oct_digit
syntax "4" : oct_digit
syntax "5" : oct_digit
syntax "6" : oct_digit
syntax "7" : oct_digit
syntax "8" : oct_digit

syntax oct1 oct_digit+ : oct

Because 0 cannot be used as ident, I think the code above does not work.
Suggestion for this is very welcome.

Mac (Jun 25 2022 at 06:19):

Lean has a small set of core tokens (e.g., ident, num, char, str, scientific) that cannot be easily overwritten by user DSLs. To split them apart you must write a fully custom parser for the given piece of input. Alternatively, you could potentially just use the builtin num token as it supports octal numerals (in the form of 0o1234).


Last updated: Dec 20 2023 at 11:08 UTC