search

rzk-lang / vscode-rzk

Visual Studio Code Extension(s) for Rzk proof assistant.
https://marketplace.visualstudio.com/items?itemName=NikolaiKudasovfizruk.rzk-1-experimental-highlighting
Other
8 stars 1 forks source link

Add fallback semantic highlighting #55

Open deemp opened 11 months ago

deemp commented 11 months ago

vscode-rzk supports semantic highlighting via LSP. However, happy seems to fail on incorrect output.

On the other hand, lezer has error-recovery mechanism that lets it parse incorrect input, at least partially. This allows CodeMirror highlight partially incorrect code.

The parser package is here. The parser file will be generated upon installing the package.

aabounegm commented 11 months ago

Unfortunately, all the parsing is done in the Haskell side rather than JavaScript. One idea would be to use Lezer only for displaying parse errors and ask Haskell to typecheck after Lezer parses successfully, but that would mean maintaining the grammar in 2 places and also parsing twice.

However, one middle-ground solution for the playground specifically (not the extension) is if we can export a function from Haskell that accepts a parsed module in the format returned by Lezer, but that seems like it can become more work than it's worth.

deemp commented 11 months ago

Lezer is fast enough to parse on each keystroke. However, I believe its parse tree can't be reused in Haskell. So, no need to send it to Haskell. Therefore, a module can be parsed by Haskell and Lezer in parallel.

Lezer produces highlighting until Haskell can parse.

The Lezer grammar should be maintained anyway until you drop support for the online playground.

I derived the Lezer grammar from the BNFC grammar in the rzk repo. The Lezer grammar file has a bit different layout than the BNFC grammar file, but token and node names and transformation rules are the same. Overall, I expect low maintainance burden.

aabounegm commented 11 months ago

Hmm, I still do not see too much value in re-implementing part of the Language Server in the VS Code wrapper, especially since we already have fallback syntax highlighting with TextMate grammar. Generating semantic tokens again requires repeating some work, and the only benefit would be that the extension wrapper loads a little bit faster than LSP. But then the question would be where do we draw the line on what to implement in TypeScript (and hence only for VS Code) vs. what to implement in LSP