;;; 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'); `sol-load-file' (C-c C-l) loads
;; the current file into the session, `sol-send-line' (C-c C-e)
;; sends the statement at point, `sol-run-buffer' (C-c C-k) runs the
;; file in a compilation buffer.
;; - 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 (statement)
"Send STATEMENT to the REPL, starting it if needed."
(run-sol)
(with-current-buffer inferior-sol-buffer
(goto-char (point-max))
(insert statement)
(comint-send-input)))
(defun sol-send-line ()
"Send the current line (one statement) to the REPL."
(interactive)
(sol--send (string-trim (or (thing-at-point 'line t) ""))))
(defun sol-load-file ()
"Load the current file into the REPL session with :load.
The load is atomic: a rejected file changes nothing in the session."
(interactive)
(when (buffer-modified-p) (save-buffer))
(sol--send (format ":load %s" buffer-file-name)))
(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-load-file)
(define-key map (kbd "C-c C-e") #'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
