diff options
| -rw-r--r-- | .gitignore | 1 | ||||
| -rw-r--r-- | README.org | 5 | ||||
| -rw-r--r-- | bin/dune | 3 | ||||
| -rw-r--r-- | bin/lsp.ml | 166 | ||||
| -rw-r--r-- | bin/main.ml | 4 | ||||
| -rw-r--r-- | docs/tooling.org | 54 | ||||
| -rw-r--r-- | dune-project | 1 | ||||
| -rw-r--r-- | editors/emacs/sol-mode.el | 319 | ||||
| -rw-r--r-- | flake.nix | 2 | ||||
| -rw-r--r-- | lib/front.ml | 29 | ||||
| -rw-r--r-- | lib/front.mli | 15 | ||||
| -rw-r--r-- | sol.opam | 2 |
12 files changed, 589 insertions, 12 deletions
@@ -7,3 +7,4 @@ result *.vo *.glob *.aux +*.elc @@ -200,6 +200,11 @@ file.sol=. Worked examples live in =examples/= (see (structural and lexicographic decrease, extracted into admission; the interval characterizations behind propagation). +Tooling: =sol lsp= is a language server publishing admission +diagnostics (totality, schemas, integrity) as you type; +=editors/emacs/sol-mode.el= provides highlighting, navigation, an +inferior REPL and eglot wiring. See =docs/tooling.org=. + Machine checked proofs live in =theories/=: the admission checker's core claim, that strict containment decreases a well founded measure, is proven in Rocq and compiled as part of the default @@ -1,4 +1,5 @@ (executable (name main) (public_name sol) - (libraries sol)) + (modules main lsp) + (libraries sol yojson)) diff --git a/bin/lsp.ml b/bin/lsp.ml new file mode 100644 index 0000000..bfe2573 --- /dev/null +++ b/bin/lsp.ml @@ -0,0 +1,166 @@ +(* The Sol language server: JSON-RPC over stdio, hand rolled on + yojson. One capability, the load-bearing one: diagnostics. Every + edit runs the same admission the runtime runs, so a rule with no + decrease witness or a fact violating its schema is an error in + the editor, at typing time, with the same message the loader + gives. Parse errors carry positions; admission errors anchor at + the top of the file until the loader learns locations. *) + +let log_json json = Yojson.Safe.to_string json + +let send json = + let body = log_json json in + Printf.printf "Content-Length: %d\r\n\r\n%s" (String.length body) body; + flush stdout + +let read_message () = + let rec headers length = + match In_channel.input_line stdin with + | None -> None + | Some line -> ( + let line = String.trim line in + if line = "" then length + else + match String.index_opt line ':' with + | Some i + when String.lowercase_ascii (String.sub line 0 i) = "content-length" + -> + headers + (int_of_string_opt + (String.trim + (String.sub line (i + 1) (String.length line - i - 1)))) + | _ -> headers length) + in + match headers None with + | None -> None + | Some length -> ( + match really_input_string stdin length with + | body -> ( try Some (Yojson.Safe.from_string body) with _ -> None) + | exception End_of_file -> None) + +let member name json = + match json with + | `Assoc fields -> Option.value ~default:`Null (List.assoc_opt name fields) + | _ -> `Null + +let to_string_opt = function `String s -> Some s | _ -> None + +(* Everything the checker can say about a document, as LSP + diagnostics: (line, column, message), zero-based lines. *) +let diagnostics text = + match Sol.Front.parse text with + | Error { Sol.Front.line; column; message } -> + [ (max 0 (line - 1), max 0 column, message) ] + | Ok statements -> ( + match Sol.Program.load statements with + | Error error -> [ (0, 0, Format.asprintf "%a" Sol.Program.pp_error error) ] + | Ok _ -> []) + +let publish uri text = + let items = + List.map + (fun (line, column, message) -> + `Assoc + [ + ( "range", + `Assoc + [ + ( "start", + `Assoc [ ("line", `Int line); ("character", `Int column) ] + ); + ( "end", + `Assoc + [ ("line", `Int line); ("character", `Int (column + 1)) ] + ); + ] ); + ("severity", `Int 1); + ("source", `String "sol"); + ("message", `String message); + ]) + (diagnostics text) + in + send + (`Assoc + [ + ("jsonrpc", `String "2.0"); + ("method", `String "textDocument/publishDiagnostics"); + ("params", `Assoc [ ("uri", `String uri); ("diagnostics", `List items) ]); + ]) + +let respond id result = + send (`Assoc [ ("jsonrpc", `String "2.0"); ("id", id); ("result", result) ]) + +let check_notification params = + let uri = + to_string_opt (member "uri" (member "textDocument" params)) + in + let text = + match to_string_opt (member "text" (member "textDocument" params)) with + | Some text -> Some text + | None -> ( + (* didChange, full sync: the last full content change. *) + match member "contentChanges" params with + | `List changes -> ( + match List.rev changes with + | last :: _ -> to_string_opt (member "text" last) + | [] -> None) + | _ -> None) + in + match (uri, text) with Some uri, Some text -> publish uri text | _ -> () + +let run () = + set_binary_mode_in stdin true; + set_binary_mode_out stdout true; + let running = ref true in + while !running do + match read_message () with + | None -> running := false + | Some message -> ( + let id = member "id" message in + let params = member "params" message in + match to_string_opt (member "method" message) with + | Some "initialize" -> + respond id + (`Assoc + [ + ( "capabilities", + `Assoc [ ("textDocumentSync", `Int 1) ] ); + ( "serverInfo", + `Assoc + [ + ("name", `String "sol-lsp"); ("version", `String "0.1.0"); + ] ); + ]) + | Some "shutdown" -> respond id `Null + | Some "exit" -> running := false + | Some ("textDocument/didOpen" | "textDocument/didChange") -> + check_notification params + | Some "textDocument/didClose" -> ( + match to_string_opt (member "uri" (member "textDocument" params)) with + | Some uri -> + send + (`Assoc + [ + ("jsonrpc", `String "2.0"); + ("method", `String "textDocument/publishDiagnostics"); + ( "params", + `Assoc + [ ("uri", `String uri); ("diagnostics", `List []) ] ); + ]) + | None -> ()) + | Some _ when id <> `Null -> + (* An unsupported request deserves an answer, not silence. *) + send + (`Assoc + [ + ("jsonrpc", `String "2.0"); + ("id", id); + ( "error", + `Assoc + [ + ("code", `Int (-32601)); + ("message", `String "method not found"); + ] ); + ]) + | _ -> ()) + done diff --git a/bin/main.ml b/bin/main.ml index c5c329a..eb212d2 100644 --- a/bin/main.ml +++ b/bin/main.ml @@ -48,6 +48,7 @@ let repl () = print_endline "Sol. Statements accumulate; Query expression: ... runs."; let rec loop history = print_string "sol> "; + flush stdout; match In_channel.input_line stdin with | None -> () | Some line when String.trim line = "" -> loop history @@ -73,7 +74,8 @@ let repl () = let () = match Sys.argv with | [| _ |] -> repl () + | [| _; "lsp" |] -> Lsp.run () | [| _; path |] -> run_file path | _ -> - prerr_endline "usage: sol [file.sol]"; + prerr_endline "usage: sol [file.sol | lsp]"; exit 1 diff --git a/docs/tooling.org b/docs/tooling.org new file mode 100644 index 0000000..7fb0e8c --- /dev/null +++ b/docs/tooling.org @@ -0,0 +1,54 @@ +#+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. It has one +capability, the load bearing one: diagnostics. On every open and +every 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 same message the runtime would give. Parse errors +carry line and column; admission errors anchor at the top of the +file until the loader learns source locations. + +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. diff --git a/dune-project b/dune-project index d490405..50c0e42 100644 --- a/dune-project +++ b/dune-project @@ -21,6 +21,7 @@ (ocaml (>= 5.1)) zarith + yojson (menhir :build) (coq :build) (alcotest :with-test))) 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 @@ -38,6 +38,7 @@ ]; propagatedBuildInputs = [ ocamlPackages.zarith + ocamlPackages.yojson ]; checkInputs = [ ocamlPackages.alcotest ]; doCheck = true; @@ -63,6 +64,7 @@ ocamlPackages.utop ocamlPackages.odoc ocamlPackages.zarith + ocamlPackages.yojson ocamlPackages.alcotest ocamlPackages.menhir # Rocq, for the verified checkers and their extraction diff --git a/lib/front.ml b/lib/front.ml index 7cacc20..b728825 100644 --- a/lib/front.ml +++ b/lib/front.ml @@ -1,14 +1,27 @@ -let parse_string source = +type error = { line : int; column : int; message : string } + +let position lexbuf = + let p = lexbuf.Lexing.lex_curr_p in + (p.Lexing.pos_lnum, p.Lexing.pos_cnum - p.Lexing.pos_bol) + +let parse source = let lexbuf = Lexing.from_string source in match Parser.program Lexer.token lexbuf with | statements -> Ok statements | exception Lexer.Error message -> - let position = lexbuf.Lexing.lex_curr_p in - Error - (Printf.sprintf "lexical error at line %d: %s" - position.Lexing.pos_lnum message) + let line, column = position lexbuf in + Error { line; column; message } | exception Parser.Error -> - let position = lexbuf.Lexing.lex_curr_p in + let line, column = position lexbuf in Error - (Printf.sprintf "syntax error at line %d, before %S" - position.Lexing.pos_lnum (Lexing.lexeme lexbuf)) + { + line; + column; + message = Printf.sprintf "syntax error before %S" (Lexing.lexeme lexbuf); + } + +let parse_string source = + match parse source with + | Ok statements -> Ok statements + | Error { line; message; _ } -> + Error (Printf.sprintf "line %d: %s" line message) diff --git a/lib/front.mli b/lib/front.mli index 00fa65f..a4e91e6 100644 --- a/lib/front.mli +++ b/lib/front.mli @@ -1,7 +1,18 @@ (** Front door: text to statements. Wraps the generated lexer and parser so callers see one total - function from source text to syntax or a positioned message. - The REPL, the file runner, and the tests all enter here. *) + function from source text to syntax or a positioned error. The + REPL, the file runner, the LSP server, and the tests all enter + here. *) + +type error = { + line : int; (** 1-based, as editors count *) + column : int; (** 0-based character offset in the line *) + message : string; +} + +val parse : string -> (Ast.statement list, error) result val parse_string : string -> (Ast.statement list, string) result +(** [parse] with the position folded into the message, for callers + that only print. *) @@ -10,7 +10,9 @@ depends: [ "dune" {>= "3.17"} "ocaml" {>= "5.1"} "zarith" + "yojson" "menhir" {build} + "coq" {build} "alcotest" {with-test} "odoc" {with-doc} ] |