1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
|
#+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, so the session only ever holds an
admitted program. The prompt flushes eagerly so the REPL works under
comint and pipes.
Commands:
- =:load FILE= brings a program into the session. The file's queries
run once, its declarations stay. The load is atomic: a file that
fails parsing or admission changes nothing.
- =:reset= clears the session.
- =:quit= leaves; =:help= lists the commands.
From Emacs, =C-c C-l= saves and loads the current file into the
REPL, =C-c C-e= sends the statement at point.
|
