[Draft] Deeper integration with Agda: foundational work

[nvarner]

Draft PR for #35. Currently likely to break on all but simple files.

Most of the big changes are behind-the-scenes work to enable future development.

• Data model, which tracks the server's knowledge of AgdaFiles and AgdaLibs
• Indexer, which turns an Agda AST into an AgdaFile
• LSP handler infrastructure, which gives handler implementations access to the relevant AgdaFile
• Document symbol handler implementation for demonstration, which turns an AgdaFile into the "Outline" tab in VS Code

TODO:

• Rebase
• Major errors to identify and iron out (i.e. shouldn't break on agda-stdlib)
• Control via configuration/disable by default?

[L-TChen]

@banacorn, do you know why CI failed for Agda 2.6.4.3?

[banacorn]

@banacorn, do you know why CI failed for Agda 2.6.4.3?

@L-TChen Just type errors really, not some nasty Stack/Cabal dependency errors.

[banacorn]

Looks great, thank you!!

Question: would the data model also keep track of edits made to the file, that hasn't been saved to the file system 👀

[nvarner]

@banacorn in principle it could, but it will take work and may not be worth it yet.

Filesystem access is baked into Agda, including resolving imports and searching for .agda-lib files. We'd have to work around each potential filesystem access and feed Agda the unsaved versions of everything instead. This is probably also a requirement for WASM support, but I'm not quite sure how WASM Agda handles filesystem access in the first place.

Also, Agda is known to slow down on large files and complex types. I suspect that Agda and my code are too slow to constantly reanalyze a file while someone edits it live. Instead, I've set it up to rerun analysis on save, a lot like reloading on C-c C-l. Since this means analysis is always happening right after the current file is saved, there isn't as much benefit to keeping Agda from reading things off the filesystem.

In the future, I want to experiment with an incremental model, like what the Haskell and Rust language servers use today. It might be fast enough for live reanalysis, at the cost of major refactoring and complexity.