repl session commands: load, reset, quit; emacs load-file binding

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]
+