#+TITLE: Tooling

* About

This document describes the developer tooling around Sol: the
language server, the Emacs mode, and the REPL. The tooling reuses
the pipeline instead of imitating it; the checker the editor runs is
the checker the runtime runs.

* The language server

=sol lsp= speaks the Language Server Protocol over stdio. Four
capabilities:

- diagnostics :: on every open and change the document goes through
  the same parse and the same admission the loader performs, so a
  recursive rule without a decrease witness, a fact violating its
  schema, an unknown relation or a failed membership criterion
  appears in the editor at typing time, with the runtime's own
  message. Parse errors carry line and column; admission errors
  anchor at the top of the file until the loader learns source
  locations.
- hover :: a builtin shows its signature and operational meaning
  (what solves backward, what residuates, what generates); a
  declared relation shows its defining source lines, verbatim,
  which is the honest notion of type in a language where types are
  relations.
- definition :: jumping from a use site to the Relation directive
  or the rule heads that define the name.
- completion :: declared relations, builtins and quantifier forms,
  every label spelled in the document, directives, and the
  combinators, triggered on =[=, =#= and =:=.

Hover, definition and completion work from a per-line symbol scan of
the stored text, deliberately not from the parsed program, so they
keep working while the buffer is broken mid edit.

The server is hand rolled JSON-RPC on yojson, in =bin/lsp.ml=. It
answers =initialize=, tracks documents through full-content sync,
publishes diagnostics, clears them on close, and answers unsupported
requests with method-not-found instead of silence.

* The Emacs mode

=editors/emacs/sol-mode.el= provides:

- highlighting per token category under the delimiter law:
  directives, combinators, structural and generic labels, relation
  heads, variables, references (=#Name=), literals;
- =%= line comments, bracket pairing for =[]= ={}= =()=, prettify
  of =:and= =:or= =:not= into their logical glyphs;
- imenu over Relations, Rules and Queries, and defun navigation
  across top level forms;
- =run-sol= (C-c C-z), an inferior REPL through comint;
  =sol-send-line= (C-c C-l) sends the statement at point;
  =sol-run-buffer= (C-c C-k) runs the file and shows answers in a
  compilation buffer;
- eglot wiring: with eglot enabled, =sol lsp= starts automatically
  for =sol-mode= buffers.

Install by adding the directory to =load-path= and requiring
=sol-mode=; =.sol= files open in the mode automatically.

* The REPL

=sol= with no arguments reads one statement per line. Declarations
and facts accumulate; =Query expression: ...= runs against
everything accumulated so far. A rejected statement reports its
error and changes nothing. The prompt flushes eagerly so the REPL
works under comint and pipes.