diff options
Diffstat (limited to '')
| -rw-r--r-- | bin/main.ml | 80 | ||||
| -rw-r--r-- | docs/tooling.org | 16 | ||||
| -rw-r--r-- | editors/emacs/sol-mode.el | 31 | ||||
| -rw-r--r-- | examples/integrity.sol | 1 |
4 files changed, 101 insertions, 27 deletions
diff --git a/bin/main.ml b/bin/main.ml index eb212d2..26375da 100644 --- a/bin/main.ml +++ b/bin/main.ml @@ -44,30 +44,78 @@ let run_file path = | Ok statements -> ( match run_statements statements with Ok () -> () | Error () -> exit 1) +let declarations statements = + List.filter + (function Sol.Ast.Directive ("Query", _) -> false | _ -> true) + statements + +(* Feeding statements into the session: declarations accumulate, + queries answer immediately, and a failure changes nothing, so the + session only ever holds an admitted program. *) +let feed history statements = + match run_statements (history @ statements) with + | Ok () -> history @ declarations statements + | Error () -> history + +let strip_quotes s = + let n = String.length s in + if n >= 2 && s.[0] = '"' && s.[n - 1] = '"' then String.sub s 1 (n - 2) + else s + +let load_file history argument = + let path = strip_quotes argument in + match In_channel.with_open_text path In_channel.input_all with + | exception Sys_error message -> + prerr_endline message; + history + | contents -> ( + match Sol.Front.parse_string contents with + | Error message -> + prerr_endline (path ^ ": " ^ message); + history + | Ok statements -> + let next = feed history statements in + if next != history then + Printf.printf "loaded %s: %d declarations, %d queries run.\n" path + (List.length (declarations statements)) + (List.length statements - List.length (declarations statements)); + next) + let repl () = - print_endline "Sol. Statements accumulate; Query expression: ... runs."; + print_endline + "Sol. Statements accumulate; Query expression: ... runs; :help for commands."; 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 | Some line -> ( - match Sol.Front.parse_string line with - | Error message -> - prerr_endline message; + let line = String.trim line in + match String.index_opt line ' ' with + | _ when line = "" -> loop history + | _ when line = ":quit" -> () + | _ when line = ":reset" -> + print_endline "session cleared."; + loop [] + | _ when line = ":help" -> + print_endline + ":load FILE bring a program into the session (atomic: a rejected file changes nothing)\n\ + :reset clear the session\n\ + :quit leave"; + loop history + | Some i when String.sub line 0 i = ":load" -> + loop + (load_file history + (String.trim (String.sub line i (String.length line - i)))) + | _ when String.length line > 0 && line.[0] = ':' -> + prerr_endline "unknown command; :help lists them."; loop history - | Ok statements -> ( - let declarations = - List.filter - (function - | Sol.Ast.Directive ("Query", _) -> false - | _ -> true) - statements - in - match run_statements (history @ statements) with - | Ok () -> loop (history @ declarations) - | Error () -> loop history)) + | _ -> ( + match Sol.Front.parse_string line with + | Error message -> + prerr_endline message; + loop history + | Ok statements -> loop (feed history statements))) in loop [] diff --git a/docs/tooling.org b/docs/tooling.org index e09917e..2fe4860 100644 --- a/docs/tooling.org +++ b/docs/tooling.org @@ -66,5 +66,17 @@ Install by adding the directory to =load-path= and requiring =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. +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. diff --git a/editors/emacs/sol-mode.el b/editors/emacs/sol-mode.el index f46c0dd..0b9579d 100644 --- a/editors/emacs/sol-mode.el +++ b/editors/emacs/sol-mode.el @@ -15,8 +15,10 @@ ;; 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. +;; - 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. ;; @@ -246,15 +248,25 @@ With ARG, repeat that many times. Returns non-nil on success." (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) - (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)))) + (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." @@ -279,7 +291,8 @@ With ARG, repeat that many times. Returns non-nil on success." (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-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) diff --git a/examples/integrity.sol b/examples/integrity.sol index 2729f4b..ec23b26 100644 --- a/examples/integrity.sol +++ b/examples/integrity.sol @@ -33,3 +33,4 @@ Query expression: % reject the whole program. % [Employee name: "Ghost" dept: 9 score: 50] % [Employee name: "Over" dept: 1 score: 101] + |