feat(emacs/lean-option): provide candidates and validation for lean-set-option

Close #106

src/emacs/lean-cmd.el

@@ -76,6 +76,10 @@ set using the command set_option in a ‘.lean’ file is supported."
 It has the effect of evaluating a command in the end of the current file"
   `(EVAL ,lean-cmd))
 
+(defun lean-cmd-options ()
+  "Display all configuration options available in Lean."
+  `(OPTIONS))
+
 ;; Type
 ;; ====
 (defun lean-cmd-type (cmd)
@@ -192,6 +196,9 @@ It has the effect of evaluating a command in the end of the current file"
 (defun lean-cmd-eval-to-string (cmd)
   "Convert Eval command to string"
   (format "EVAL\n%s" (lean-cmd-eval-get-lean-cmd cmd)))
+(defun lean-cmd-options-to-string (cmd)
+  "Convert Options command to string"
+  (format "OPTIONS"))
 
 (defun lean-cmd-to-string (cmd)
   "Convert command to string"
@@ -204,7 +211,8 @@ It has the effect of evaluating a command in the end of the current file"
     ('INFO    (lean-cmd-info-to-string    cmd))
     ('CHECK   (lean-cmd-check-to-string   cmd))
     ('SET     (lean-cmd-set-to-string     cmd))
-    ('EVAL    (lean-cmd-eval-to-string    cmd))))
+    ('EVAL    (lean-cmd-eval-to-string    cmd))
+    ('OPTIONS (lean-cmd-options-to-string cmd))))
 
 ;; -- Test
 (cl-assert (string= (lean-cmd-to-string (lean-cmd-load "~/work/lean/basic.lean"))

src/emacs/lean-mode.el

@@ -23,6 +23,7 @@
 (require 'lean-input)
 (require 'lean-type)
 (require 'lean-tags)
+(require 'lean-option)
 (require 'lean-syntax)
 
 (defun lean-compile-string (exe-name args file-name)

src/emacs/lean-option.el

@@ -0,0 +1,175 @@
+(require 'dash)
+(require 'dash-functional)
+
+(defun lean-set-parse-string (str)
+  "Parse the output of eval command."
+  (let ((str-list (split-string str "\n")))
+    ;; Drop the first line "-- BEGINSET" and
+    ;; the last line "-- ENDSET"
+    (setq str-list
+          (-take (- (length str-list) 2)
+                 (-drop 1 str-list)))
+    (string-join str-list "\n")))
+
+(defun lean-set-option ()
+  "Set Lean option."
+  (interactive)
+  (lean-get-options)
+  (let* ((key-list (-map 'car lean-global-option-record-alist))
+         (option-name
+          (completing-read "Option name: "
+                           key-list
+                           nil t "" nil (car key-list)))
+         (option (cdr (assoc option-name lean-global-option-record-alist)))
+         (option-value (lean-option-read option)))
+    (lean-server-send-cmd (lean-cmd-set option-name option-value))
+    (while (not lean-global-server-message-to-process)
+      (accept-process-output (lean-server-get-process) 0 50 t))
+    (pcase lean-global-server-message-to-process
+      (`(SET ,pre ,body)
+       (lean-server-log "The following pre-message will be thrown away:")
+       (lean-server-log "%s" pre)
+       (setq lean-global-server-message-to-process nil)
+       (lean-server-log "We have the following response from lean-server")
+       (message "%s" (lean-set-parse-string body)))
+      (`(,type ,pre , body)
+       (lean-server-log "The following pre-message will be thrown away:")
+       (lean-server-log "%s" pre)
+       (lean-server-log "Something other than SET detected: %S" type)
+       (setq lean-global-server-message-to-process nil)))))
+
+(defun lean-option-read-bool (prompt)
+  (interactive)
+  (completing-read prompt'(("true" 1) ("false" 2)) nil t "" nil "true"))
+
+(defun lean-option-read-int (prompt)
+  (interactive)
+  (let* ((str (read-string prompt))
+         (val (string-to-int str))
+         tmp-str)
+    (setq tmp-str (int-to-string val))
+    (if (and (integerp val)
+             (stringp tmp-str)
+             (string= tmp-str str))
+        val
+        (error "%s is not an int value" str))))
+
+(defun lean-option-read-uint (prompt)
+  (interactive)
+  (let* ((str (read-string prompt))
+         (val (string-to-int str))
+         tmp-str)
+    (setq tmp-str (int-to-string val))
+    (if (and (integerp val)
+             (>= val 0)
+             (stringp tmp-str)
+             (string= tmp-str str))
+        val
+      (error "%s is not an unsigned int value" str))))
+
+(defun lean-option-read-double (prompt)
+  (interactive)
+  (let* ((str (read-string prompt))
+         (val (string-to-number str))
+         tmp-str)
+    (setq tmp-str (number-to-string val))
+    (if (and (numberp val)
+             (>= val 0)
+             (stringp tmp-str)
+             (string= tmp-str str))
+        (string-to-number str)
+      (error "%s is not a double value" str))))
+
+(defun lean-option-read-string (prompt)
+  (interactive)
+  (read-string prompt))
+
+(defun lean-option-read-sexp (prompt)
+  (interactive)
+  (let* ((str (read-string prompt))
+         (sexp (ignore-errors (read str))))
+    (if (ignore-errors
+          (string= (prin1-to-string sexp) str))
+        sexp
+      (error "%s is not a well-formed S-Expression"))))
+
+(defun lean-option-type (option)
+  (let ((type-str (lean-option-record-type option)))
+    (cond ((string= "Bool" type-str)          'Bool)
+          ((string= "Int" type-str)           'Int)
+          ((string= "Unsigned Int" type-str)  'UInt)
+          ((string= "Double" type-str)        'Double)
+          ((string= "String" type-str)        'String)
+          ((string= "S-Expressions" type-str) 'SEXP)
+          (t (error "lean-option-string-to-type: %s is not supported lean-option type."
+                    type-str)))))
+
+(defun lean-option-read (option)
+  (let* ((option-type-str (lean-option-record-type option))
+         (option-name (lean-option-record-name option))
+         (option-desc (lean-option-record-desc option))
+         (prompt (format "%s [%s] : %s = "
+                         option-name
+                         option-desc
+                         option-type-str)))
+    (pcase (lean-option-type option)
+      (`Bool   (lean-option-read-bool prompt))
+      (`Int    (lean-option-read-int prompt))
+      (`UInt   (lean-option-read-uint prompt))
+      (`Double (lean-option-read-double prompt))
+      (`String (lean-option-read-string prompt))
+      (`SEXP   (lean-option-read-sexp prompt)))))
+
+(cl-defstruct lean-option-record name type default-value desc)
+(defun lean-option-parse-string (line)
+  "Parse a line to lean-option-record"
+  (let* ((str-list             (split-string line "|"))
+         (option-name          (substring-no-properties (cl-first str-list) 3))
+         (option-type          (cl-second str-list))
+         (option-default-value (cl-third str-list))
+         (option-desc          (cl-fourth str-list)))
+    (make-lean-option-record :name option-name
+                             :type option-type
+                             :default-value option-default-value
+                             :desc option-desc)))
+
+(defun lean-options-parse-string (str)
+  "Parse lines of option string into an entry of alist of lean-option-records
+
+(NAME . OPTION-RECORD)."
+  (let ((str-list (split-string str "\n"))
+        str-str-list
+        option-list)
+    ;; Drop the first line "-- BEGINOPTIONS" and
+    ;;      the last line  "-- ENDOPTIONS"
+    (setq str-list
+          (-take (- (length str-list) 2)
+                 (-drop 1 str-list)))
+    (-map (lambda (line)
+            (let ((option-record (lean-option-parse-string line)))
+              `(,(lean-option-record-name option-record) . ,option-record)))
+          str-list)))
+
+(defun lean-get-options ()
+  "Get Lean option."
+  (interactive)
+  (unless lean-global-option-record-alist
+    (lean-server-send-cmd (lean-cmd-options))
+    (while (not lean-global-server-message-to-process)
+      (accept-process-output (lean-server-get-process) 0 50 t))
+    (pcase lean-global-server-message-to-process
+      (`(OPTIONS ,pre ,body)
+       (lean-server-log "The following pre-message will be thrown away:")
+       (lean-server-log "%s" pre)
+       (setq lean-global-server-message-to-process nil)
+       (lean-server-log "We have the following response from lean-server")
+       (setq lean-global-option-record-alist
+             (lean-options-parse-string body)))
+      (`(,type ,pre , body)
+       (lean-server-log "The following pre-message will be thrown away:")
+       (lean-server-log "%s" pre)
+       (lean-server-log "Something other than SET detected: %S" type)
+       (setq lean-global-server-message-to-process nil))))
+  lean-global-option-record-alist)
+
+(provide 'lean-option)

src/emacs/lean-server.el

@@ -46,7 +46,9 @@
     (SET  ,(rx line-start "-- BEGINSET"  line-end)
           ,(rx line-start (group "-- ENDSET")  line-end))
     (EVAL ,(rx line-start "-- BEGINEVAL"  line-end)
-          ,(rx line-start (group "-- ENDEVAL")  line-end))
+          ,(rx line-start (group "-- ENDEVAL") line-end))
+    (OPTIONS ,(rx line-start "-- BEGINOPTIONS" line-end)
+          ,(rx line-start (group "-- ENDOPTIONS") line-end))
     (ERROR ,(rx line-start "-- " (0+ not-newline) line-end)
            ,(rx line-start (group "-- ERROR" (0+ not-newline)) line-end)))
   "Regular expression pattern for lean-server message syntax")
@@ -93,6 +95,8 @@
   "Handle signals for lean-server-process"
   (cond
    ((string-prefix-p "hangup" event)
+    (lean-server-initialize-global-vars))
+   ((string-prefix-p "killed" event)
     (lean-server-initialize-global-vars))))
 
 ;; How to create an async process
@@ -104,6 +108,7 @@
   (setq lean-global-server-current-file-name nil)
   (setq lean-global-server-message-to-process nil)
   (setq lean-global-server-last-time-sent nil)
+  (setq lean-global-option-record-alist nil)
   (when (timerp lean-global-nay-retry-timer)
     (cancel-timer lean-global-nay-retry-timer))
   (setq lean-global-nay-retry-timer nil))
@@ -195,9 +200,10 @@ If it's not the same with file-name (default: buffer-file-name), send VISIT cmd.
     ('INSERT  (lean-server-check-current-file))
     ('REMOVE  (lean-server-check-current-file))
     ('INFO    (lean-flush-changed-lines))
-    ('CHECK   )
+    ('CHECK   ())
     ('SET     ())
-    ('EVAL    (lean-server-check-current-file))))
+    ('EVAL    (lean-server-check-current-file))
+    ('OPTIONS ())))
 
 (defun lean-server-after-send-cmd (cmd)
   "Operations to perform after sending a command."
@@ -210,7 +216,8 @@ If it's not the same with file-name (default: buffer-file-name), send VISIT cmd.
     ('INFO    ())
     ('CHECK   ())
     ('SET     ())
-    ('EVAL    ())))
+    ('EVAL    ())
+    ('OPTIONS ())))
 
 (defun lean-server-send-cmd (cmd)
   "Send string to lean-server."

src/emacs/lean-type.el

@@ -14,7 +14,6 @@
 (require 'lean-debug)
 (require 'flymake)
 
-
 (defun lean-fill-placeholder ()
   "Fill the placeholder with a synthesized expression by Lean."
   (interactive)
@@ -51,39 +50,6 @@
       (when info-string
         (message "%s" info-string))))))
 
-;; =======================================================
-;; set option
-;; =======================================================
-
-(defun lean-set-parse-string (str)
-  "Parse the output of eval command."
-  (let ((str-list (split-string str "\n")))
-    ;; Drop the first line "-- BEGINSET" and
-    ;; the last line "-- ENDSET"
-    (setq str-list
-          (-take (- (length str-list) 2)
-                 (-drop 1 str-list)))
-    (string-join str-list "\n")))
-
-(defun lean-set-option (option-name option-value)
-  "Set Lean option."
-  (interactive "sOption Name: \nsOption Value: ")
-  (lean-server-send-cmd (lean-cmd-set option-name option-value))
-  (while (not lean-global-server-message-to-process)
-    (accept-process-output (lean-server-get-process) 0 50 t))
-  (pcase lean-global-server-message-to-process
-    (`(SET ,pre ,body)
-     (lean-server-log "The following pre-message will be thrown away:")
-     (lean-server-log "%s" pre)
-     (setq lean-global-server-message-to-process nil)
-     (lean-server-log "We have the following response from lean-server")
-     (message "%s" (lean-set-parse-string body)))
-    (`(,type ,pre , body)
-     (lean-server-log "The following pre-message will be thrown away:")
-     (lean-server-log "%s" pre)
-     (lean-server-log "Something other than SET detected: %S" type)
-     (setq lean-global-server-message-to-process nil))))
-
 ;; =======================================================
 ;; eval
 ;; =======================================================

src/emacs/lean-variable.el

@@ -11,10 +11,13 @@
   "A shared variable contains a received message to process.
 
 A message is in the form of (TYPE PRE BODY)
-where TYPE := INFO | SET | EVAL | ERROR,
+where TYPE := INFO | SET | EVAL | OPTIONS | ERROR,
       PRE is a server message comes before the message
       BODY is a body of the received message.")
 
+(defvar lean-global-option-record-alist nil
+  "lean option-record alist")
+
 (defvar lean-global-server-process nil
   "lean server process")