language server over stdio, emacs mode with repl and eglot wiring

1 files changed, 319 insertions, 0 deletions

diff --git a/editors/emacs/sol-mode.el b/editors/emacs/sol-mode.el
new file mode 100644
index 0000000..f46c0dd
--- /dev/null
+++ b/editors/emacs/sol-mode.el
@@ -0,0 +1,319 @@
+;;; sol-mode.el --- Major mode for the Sol relational language -*- lexical-binding: t; -*-
+
+;; Author: Marcos Magueta
+;; Keywords: languages, logic, relational
+;; Version: 0.2.0
+;; Package-Requires: ((emacs "26.1"))
+
+;;; Commentary:
+
+;; A major mode for Sol, a total relational language with Smalltalk-like
+;; message syntax.  It provides:
+;;
+;;   - Syntax highlighting, one face per token category: directives,
+;;     logical combinators, reserved labels, generic labels, relation
+;;     heads, variables, references (#Name), literals, delimiters.
+;;   - Navigation: imenu over Relations, Rules and Queries;
+;;     beginning/end-of-defun over top-level forms.
+;;   - An inferior Sol REPL (`run-sol') and `sol-run-buffer' to execute
+;;     the current file.
+;;   - Eglot wiring: `sol lsp' serves diagnostics, so admission errors
+;;     (totality, schemas, integrity) appear while typing.
+;;
+;; Installation:
+;;
+;;   (add-to-list 'load-path "/path/to/sol2/editors/emacs")
+;;   (require 'sol-mode)
+;;
+;; Files ending in .sol open in `sol-mode' automatically.
+
+;;; Code:
+
+(require 'comint)
+
+(defgroup sol nil
+  "Major mode for the Sol relational language."
+  :group 'languages
+  :prefix "sol-")
+
+(defcustom sol-indent-offset 2
+  "Number of columns to indent per bracket nesting level."
+  :type 'integer
+  :group 'sol)
+
+(defcustom sol-program "sol"
+  "Path to the sol executable, used by the REPL, the runner and eglot."
+  :type 'string
+  :group 'sol)
+
+;;; ----------------------------------------------------------------------
+;;; Faces -- one colour per token category.
+;;; ----------------------------------------------------------------------
+
+(defface sol-keyword-face
+  '((((background dark))  (:foreground "#c678dd" :weight bold))
+    (((background light)) (:foreground "#a626a4" :weight bold)))
+  "Face for top-level directives: Relation, Rule, Query."
+  :group 'sol)
+
+(defface sol-combinator-face
+  '((((background dark))  (:foreground "#56b6c2" :weight bold))
+    (((background light)) (:foreground "#0184bc" :weight bold)))
+  "Face for the logical combinators :and, :or and :not."
+  :group 'sol)
+
+(defface sol-builtin-label-face
+  '((((background dark))  (:foreground "#e5c07b"))
+    (((background light)) (:foreground "#b07d00")))
+  "Face for structural labels: named:, schema:, head:, body:, and kin."
+  :group 'sol)
+
+(defface sol-label-face
+  '((((background dark))  (:foreground "#61afef"))
+    (((background light)) (:foreground "#4078f2")))
+  "Face for generic attribute labels, e.g. value:, left:, age:."
+  :group 'sol)
+
+(defface sol-relation-face
+  '((((background dark))  (:foreground "#98c379" :weight bold))
+    (((background light)) (:foreground "#50a14f" :weight bold)))
+  "Face for relation heads -- the first name after `['."
+  :group 'sol)
+
+(defface sol-variable-face
+  '((((background dark))  (:foreground "#e06c75"))
+    (((background light)) (:foreground "#e45649")))
+  "Face for logical variables -- capitalised identifiers in term position."
+  :group 'sol)
+
+(defface sol-reference-face
+  '((((background dark))  (:foreground "#d19a66" :weight bold))
+    (((background light)) (:foreground "#986801" :weight bold)))
+  "Face for relation references, #Name."
+  :group 'sol)
+
+(defface sol-number-face
+  '((((background dark))  (:foreground "#ff79c6"))
+    (((background light)) (:foreground "#c41a8d")))
+  "Face for integer and rational literals."
+  :group 'sol)
+
+(defface sol-bracket-face
+  '((((background dark))  (:foreground "#828997"))
+    (((background light)) (:foreground "#9ca0a4")))
+  "Face for delimiters and the cons bar |."
+  :group 'sol)
+
+;;; ----------------------------------------------------------------------
+;;; Syntax table.
+;;; ----------------------------------------------------------------------
+
+(defvar sol-mode-syntax-table
+  (let ((table (make-syntax-table)))
+    ;; Line comments start with % and run to end of line.
+    (modify-syntax-entry ?% "<" table)
+    (modify-syntax-entry ?\n ">" table)
+    ;; Strings.
+    (modify-syntax-entry ?\" "\"" table)
+    (modify-syntax-entry ?\\ "\\" table)
+    ;; The delimiter law: [] propositions, {} records, () grouping,
+    ;; #( ... ) sequences.  All pair for navigation.
+    (modify-syntax-entry ?\[ "(]" table)
+    (modify-syntax-entry ?\] ")[" table)
+    (modify-syntax-entry ?\{ "(}" table)
+    (modify-syntax-entry ?\} "){" table)
+    (modify-syntax-entry ?\( "()" table)
+    (modify-syntax-entry ?\) ")(" table)
+    ;; # prefixes references and sequences.
+    (modify-syntax-entry ?# "'" table)
+    ;; Identifier constituents.
+    (modify-syntax-entry ?_ "_" table)
+    ;; Punctuation used as token glue.
+    (modify-syntax-entry ?: "." table)
+    (modify-syntax-entry ?| "." table)
+    (modify-syntax-entry ?/ "." table)
+    table)
+  "Syntax table for `sol-mode'.")
+
+;;; ----------------------------------------------------------------------
+;;; Font lock.  Order matters: earlier entries win.
+;;; ----------------------------------------------------------------------
+
+(defconst sol-font-lock-keywords
+  (list
+   ;; 1. Top-level directives.
+   '("^[[:space:]]*\\(Relation\\|Rule\\|Query\\)\\_>" 1 'sol-keyword-face)
+   ;; 2. Logical combinators.
+   '("\\(:and\\|:or\\|:not\\)\\_>" 1 'sol-combinator-face)
+   ;; 3. Relation references, #Name.
+   '("\\(#[A-Za-z][A-Za-z0-9_]*\\)" 1 'sol-reference-face)
+   ;; 4. Structural labels.
+   '("\\_<\\(named\\|schema\\|name\\|head\\|body\\|expression\\|domain\\|variable\\|quantifier\\):"
+     1 'sol-builtin-label-face)
+   ;; 5. Relation head: the first name after `['.
+   '("\\[[[:space:]]*\\([A-Za-z][A-Za-z0-9_]*\\)" 1 'sol-relation-face)
+   ;; 6. Generic attribute labels.
+   '("\\_<\\([A-Za-z_][A-Za-z0-9_]*\\):" 1 'sol-label-face)
+   ;; 7. Logical variables: capitalised identifiers in term position.
+   '("\\_<\\([A-Z][A-Za-z0-9_]*\\)\\_>" 1 'sol-variable-face)
+   ;; 8. Numeric literals: integers and rationals.
+   '("\\_<-?[0-9]+\\(?:/[0-9]+\\)?\\_>" 0 'sol-number-face)
+   ;; 9. Delimiters.
+   '("[][}{|]" 0 'sol-bracket-face))
+  "Font-lock highlighting for `sol-mode'.")
+
+(defvar sol-prettify-symbols-alist
+  '((":and" . ?∧)
+    (":or"  . ?∨)
+    (":not" . ?¬))
+  "Symbol prettification for `sol-mode'.")
+
+;;; ----------------------------------------------------------------------
+;;; Navigation.
+;;; ----------------------------------------------------------------------
+
+(defconst sol-defun-regexp
+  "^[[:space:]]*\\(?:Relation\\|Rule\\|Query\\)\\_>\\|^[[:space:]]*\\["
+  "Regexp matching the start of a top-level Sol form: a directive or a fact.")
+
+(defvar sol-imenu-generic-expression
+  (list
+   (list "Relation"
+         "\\_<Relation\\_>[[:space:]]+named:[[:space:]]*\\([A-Za-z][A-Za-z0-9_]*\\)" 1)
+   (list "Rule"
+         "\\_<Rule\\_>[[:space:]]+name:[[:space:]]*\"\\([^\"]+\\)\"" 1)
+   (list "Query"
+         "\\_<Query\\_>[[:space:]]+expression:[[:space:]]*\\(?:(\\|\\[\\)[[:space:]]*\\([A-Za-z][A-Za-z0-9_]*\\)" 1))
+  "Imenu configuration for `sol-mode'.")
+
+(defun sol-beginning-of-defun (&optional arg)
+  "Move backward to the start of a top-level Sol form.
+With ARG, repeat that many times.  Returns non-nil on success."
+  (setq arg (or arg 1))
+  (let ((found nil))
+    (while (> arg 0)
+      (setq found (re-search-backward sol-defun-regexp nil t))
+      (setq arg (1- arg)))
+    (when found
+      (goto-char (match-beginning 0))
+      (back-to-indentation))
+    found))
+
+(defun sol-end-of-defun ()
+  "Move to the end of the current top-level Sol form."
+  (when (looking-at-p sol-defun-regexp)
+    (forward-char 1))
+  (if (re-search-forward sol-defun-regexp nil 'move)
+      (progn
+        (goto-char (match-beginning 0))
+        (skip-chars-backward " \t\n"))
+    (goto-char (point-max))))
+
+;;; ----------------------------------------------------------------------
+;;; Indentation: bracket-depth based, conservative.
+;;; ----------------------------------------------------------------------
+
+(defun sol-indent-line ()
+  "Indent the current line by its bracket nesting depth."
+  (let* ((bol   (line-beginning-position))
+         (depth (car (syntax-ppss bol))))
+    (save-excursion
+      (back-to-indentation)
+      (when (and (> depth 0) (looking-at-p "[])}]"))
+        (setq depth (1- depth))))
+    (if (> depth 0)
+        (indent-line-to (* depth sol-indent-offset))
+      'noindent)))
+
+;;; ----------------------------------------------------------------------
+;;; Inferior Sol: the REPL, through comint.
+;;; ----------------------------------------------------------------------
+
+(defvar inferior-sol-buffer "*sol*"
+  "Buffer name of the inferior Sol process.")
+
+(define-derived-mode inferior-sol-mode comint-mode "Inferior Sol"
+  "Major mode for the Sol REPL."
+  (setq comint-prompt-regexp "^sol> ")
+  (setq comint-prompt-read-only t))
+
+;;;###autoload
+(defun run-sol ()
+  "Start the Sol REPL, or pop to it if it is already running."
+  (interactive)
+  (unless (comint-check-proc inferior-sol-buffer)
+    (with-current-buffer (make-comint "sol" sol-program)
+      (inferior-sol-mode)))
+  (pop-to-buffer inferior-sol-buffer))
+
+(defun sol-send-line ()
+  "Send the current line (one statement) to the REPL."
+  (interactive)
+  (let ((statement (string-trim (or (thing-at-point 'line t) ""))))
+    (run-sol)
+    (with-current-buffer inferior-sol-buffer
+      (goto-char (point-max))
+      (insert statement)
+      (comint-send-input))))
+
+(defun sol-run-buffer ()
+  "Run the current file with sol, showing answers in a compilation buffer."
+  (interactive)
+  (when (buffer-modified-p) (save-buffer))
+  (compile (format "%s %s" sol-program (shell-quote-argument buffer-file-name))))
+
+;;; ----------------------------------------------------------------------
+;;; Eglot: diagnostics from `sol lsp'.
+;;; ----------------------------------------------------------------------
+
+(defvar eglot-server-programs)
+
+(with-eval-after-load 'eglot
+  (add-to-list 'eglot-server-programs
+               `(sol-mode . (,sol-program "lsp"))))
+
+;;; ----------------------------------------------------------------------
+;;; Keymap.
+;;; ----------------------------------------------------------------------
+
+(defvar sol-mode-map
+  (let ((map (make-sparse-keymap)))
+    (define-key map (kbd "C-c C-z") #'run-sol)
+    (define-key map (kbd "C-c C-l") #'sol-send-line)
+    (define-key map (kbd "C-c C-k") #'sol-run-buffer)
+    (define-key map (kbd "C-c C-j") #'imenu)
+    map)
+  "Keymap for `sol-mode'.")
+
+;;; ----------------------------------------------------------------------
+;;; Mode definition.
+;;; ----------------------------------------------------------------------
+
+;;;###autoload
+(define-derived-mode sol-mode prog-mode "Sol"
+  "Major mode for editing Sol relational programs.
+
+\\{sol-mode-map}"
+  :syntax-table sol-mode-syntax-table
+  (setq-local font-lock-defaults '(sol-font-lock-keywords))
+  ;; Comments.
+  (setq-local comment-start "% ")
+  (setq-local comment-end "")
+  (setq-local comment-start-skip "%+[ \t]*")
+  ;; Navigation.
+  (setq-local beginning-of-defun-function #'sol-beginning-of-defun)
+  (setq-local end-of-defun-function #'sol-end-of-defun)
+  (setq-local imenu-generic-expression sol-imenu-generic-expression)
+  (setq-local imenu-case-fold-search nil)
+  ;; Indentation.
+  (setq-local indent-line-function #'sol-indent-line)
+  (setq-local indent-tabs-mode nil)
+  ;; Eye-candy.
+  (setq-local prettify-symbols-alist sol-prettify-symbols-alist))
+
+;;;###autoload
+(add-to-list 'auto-mode-alist '("\\.sol\\'" . sol-mode))
+
+(provide 'sol-mode)
+
+;;; sol-mode.el ends here