Defining syntax then using it within a single command

Stream: general

[Matthew Toohey]

I'm trying to create a Lean library that does something similar to ott by using Lean's metaprogramming features to embed an ott-like DSL. I've managed to create commands for defining metavariables and non-terminals (with elaborations to inductive datatypes and syntax definitions), and I'm currently trying to figure out how to create something similar to the defns/defn syntax from ott, which defines judgements through inference rules.

The issue is that a defn-like command will need to allow the user to define syntax for the judgement (for example the syntax G " |- " e " : " t could be used for a simple typing judgement, where G, e, and t are non-terminals for environment, expression, and type that have already been defined) and then make use of that syntax within the same command, since the conclusion of each inference rule should use the judgement's syntax. Does anyone have recommendations about how I should do this? My current thought is that I'd need to define a custom ParserFn which parses things dynamically based on its interpretation of the user-provided judgement syntax, but this seems less than ideal since I'd have to duplicate a lot of the code that already exists inside toParserDescr (since that function returns a term for a ParserDescr or TrailingParserDescr instead of a ParserFn value that can be used immediately).

The one easier (but less elegant) alternative that I've considered is having two separate commands, one which defines the syntax for the judgement, then a second which specifies the inference rule. Then I could just use toParserDescr when elaborating the first command and I wouldn't have this problem, but it would be much nicer to be able to make them a single command, since then you wouldn't have to repeat any information in both to link the two.

Let me know if anything I've said needs clarification! Thanks for any help/suggestions!

[Sebastian Ullrich]

I think your evaluation of the status quo is exactly right. How I want to solve this for inductive (and Verso) is by allowing commands to do their own additional parsing, but currently they can neither read nor write the parser state

[Matthew Toohey]

That's unfortunate, thanks for confirming though! Maybe I'll go with the easier approach for now, and if what you've suggested becomes possible at some point I can switch things to use that then.