Formatter for Quint source code

[romac]

It would be nice to have a quint format command that would format any source file given to it, much like rustfmt for Rust or prettier for JavaScript/TypesScript.

As far as I can tell, Quint can already pretty print Quint values for the REPL, but it lacks formatting capabilities for the whole of the syntax. Also, we may want to format things differently for the REPL and for source code.

I see a few ways of going at this:

a) Write a formatter that works at the level of lexical tokens (not sure if high-level enough to properly format all Quint expressions) b) Write a formatter that works at the level of the parsed AST (might need to track comments in there if not done yet) c) Write a Tree Sitter grammar for Quint and implement the formatter using Topiary

What do you think?

[bugarela]

I actually wrote a (partial) tree-sitter grammar for Quint in my pi-week! https://github.com/informalsystems/quint/tree/gabriela/tree-sitter-quint/tree-sitter-quint

And I agree, we really need a formatter. My current intention is to write a prettier plugin and use their infrastructure. Regarding your ideas:

• I'm not sure about (a), as I don't really have a reference for how to do that. I'll look it up when I pick this issue up
• For (b), we'd need to take not only comments, but also some more information that is currently lost after parsing - i.e. foo.in(bar) and in(foo, bar) are parsed as the same thing.
  • iirc, we'd also need to do this for writing a prettier plugin, because I think it takes some form of AST as input.
• As for (c), I was a bit demotivated from using the tree-sitter grammar after seeing VSCode doesn't have proper support for it yet. So I think this would be like a secondary solution, for people using tools with proper tree-sitter support. I haven't heard about Topiary before tho, it might be able to solve this issue!

[bugarela]

Trying Topiary seems fairly easy, according to https://github.com/tweag/topiary/issues/630

[romac]

I'm not sure about (a)

I included it because I too wonder if it's possible to do proper formatting from lexemes, instead of from the parse tree. I would need to research this a bit.

For (b), we'd need to take not only comments, but also some more information that is currently lost after parsing - i.e. foo.in(bar) and in(foo, bar) are parsed as the same thing.

Ah yes, perhaps we'd need to split the AST into a parse tree and an actual abstract syntax tree. Or maybe that's too much and adding back the distinction into the AST is enough, but that might make working with the AST more cumbersome for later phases.

I was a bit demotivated from using the tree-sitter grammar after seeing VSCode doesn't have proper support for it yet

Ah that's a bummer! Works really well in Neovim though, together with the Quint LSP :)