Set/Change Command Syntax Category?

Stream: lean4

[Mac]

Is possible / is it planned to be possible to set the syntax category used to parse commands? This would be a nice feature when writing files that are entirely written in a DSL. Is it also seems somewhat feasible given that way parsing works. The goal would be to do something like this:

declare_syntax_cat command2
macro "#" cmd:command : command2 => `($cmd)

-- ... define various other DSL commands ..

set_command_cat command2

-- ... do stuff with DSL commands ...

# def  foo := -- ....

-- ... do more stuff with DSL commands ..

[Sebastian Ullrich]

There was some talk about supporting something like Racket's #lang that would allow you to completely replace the default frontend, but nothing specific so far. This would allows for frontends that work completely different from the default one; we didn't think about special cases for ones that work like the default one, just with a different set of commands, yet.

[Mac]

Sebastian Ullrich said:

There was some talk about supporting something like Racket's #lang that would allow you to completely replace the default frontend, but nothing specific so far.

That also sounds really cool! I was suggesting this most as it seemed the simplest step in that direction since it mostly just requires topLevelCommandParserFn ((in particular, the category it uses) to be passed on some parameter in the context, which seems quite feasible. However, being able to overwrite runFrontend (and, in particular, the header processing) as well would be even cooler.

I think Lean's metaprogramming framework provides a very good general base for exploring all kinds of interesting DSLs and other programming language idioms, so I will really love to be able to manipulate the entire syntax of a file (with something like #lang). Still though, custom commands would get pretty close to that already -- it really only misses the header.