path: root/editors/emacs/sol-mode.el

;;; 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