Formatter - initial basic implementation

[aabounegm]

This implements a very basic formatter that scans the lexical tokens for some known patterns and applies text edits to have them adhere to the style guide. The code is still in an early stage and can definitely be improved a lot, so a code review would be tremendously helpful.

Also, an issue was discovered with LSP's VFS wherein it includes carriage return (\r) character on Windows, causing issues with the parser. A workaround has been added (filter (/= '\r')), but can probably be improved.

Notable features

• Adds a space after the opening parenthesis to help with the code tree structure
• Puts the definition conclusion (type, starting with :) and construction (body, starting with :=) on new lines
• Adds a space after the \ of a lambda term and around binary operators (like ,)
• Moves binary operators to the beginning of the next line if they appear at the end of the previous one.
• Replaces common ASCII sequences with their Unicode equivalent
• A CLI subcommand (rzk format) with --check and --write options

Known limitations

• The 80 character line limit is currently not enforced due to the difficulty of determining where to add line breaks (for reference, check out this post by a Dart fmt engineer)
• Fixing indentation is not yet implemented due to the need for more semantics than the lexer provides to determine indentation level.
• Moving binary operators from the end of the line to the beginning of the next is not yet implemented. Edit: Implemented for , and ->. What other binary operators are needed?
• No commands other than #define (and its alias #def) are handled yet.
• There are rare edge cases in which applying the formatter twice would result in additional edits that were not detected the first time.

I will open separate issues to work on these in the future.

Possible inconsistencies in the style guide

These may not be inconsistencies as much as a lack of understand on my side, but I'd like to understand either way:

• About the spaces after opening parenthesis, it seems that 2 styles have been used when it comes to nested parentheses. One example has ( ( a-term-of-a-type) ...) (with a space after the inner paren), while another is written as ( (x : A) ...) (without a space before the x)
• Regarding the same recommendation about space in opening parentheses, it seems that it only applies when that open paren is the first character in its line. For example, it appears as : (x = z) in the type. However, in the sHoTT repo itself, a definition has : ( concat A w x z p ...) with a space after the paren. Which one should it be? (mostly clarified in Auto-format all files sHoTT#142 (comment) and partially implemented)

Planned improvements

• Formatting configuration settings (preferably in rzk.yaml, but possible also .vscode/settings.json) for controlling options like auto-replacement of ASCII sequences, line width, ...

A pull request to the sHoTT repo (and others) will follow after more work is done into stabilizing the formatter and implementing more rules.