Structure

The server is written as a asynchronous tokio application. The following list shows the different subsystems of the server:

• LSP lifecycle
  • main.rs - LSP json-rpc interface with tower, system initialization etc.
  • core/cache.rs - Find files control what files need to be relinked
  • core/document.rs - File update logic
  • core/pipeline.rs - Pipeline: multi-stage compiler, it provides access to files in various compilation stages. Constists of multiple subsystems like: green tree parsing, linking, error reporting, smt checking etc.
  • core/semantic.rs - Contains a central struct RootGraph. This struct includes the latest linked uvl and config files, it can be thought of as a snapshot of all related documents. It can be accessed through the pipeline.
• Basic UVL language support
  • green tree parsing (tree-sitter):
    • core/parse.rs
    • core/query.rs
  • green tree to red tree(AST ECS) transformer
    • core/ast/def.rs - Common AST types.
    • core/ast/transform.rs - The transformer implementation
    • core/ast/visitor.rs - Util functions and traits for the transformer
    • core/ast.rs - AstDocument: main interface to the AST ECS.
  • name resolution and type checking
    • core/resolve.rs - resolve_file: Type resolving for an AstDocument, resolve_*: nameresultion under various conditions.
• SMT
  • core/module.rs: Module is a uvl instance containing all sub instances of an arbitrary root file.
  • smt/parse.rs: Turn smt-lib strings to rust.
  • smt/smt_lib.rs: SMTModule: A smt-lib module equivalent to some UVL source module. uvl2smt: Turn some uvl module into a SMTModule.
  • smt/smt.rs: SmtSolver: Z3 process interface(over stdio). check_handler: Runs smt-analysis on new files when the Rootgraph changes. web_view_handler runs smt-analysis on configurations.
• Configuration:
  • core/config.rs: Common config parsing and lifecycle utils.
  • webview.rs: Config Webview "backend" (both backend and frontend run on the server have a look at)
  • webview/frontend: Config Webview "frontend".
• IDE features like completion etc. are all in the ide module.