feat(emacs/lean-cmd): add FINDP cmd

src/emacs/lean-cmd.el

@@ -92,6 +92,11 @@ It has the effect of evaluating a command in the end of the current file"
   "Display valid/invalid lines. Invalid lines are the one we need to refresh type information"
   `(VALID))
 
+(defun lean-cmd-findp (line-number prefix)
+  "Find All auto-complete candidates matched with prefix at line-number"
+  `(FINDP ,line-number ,prefix))
+
+
 ;; Type
 ;; ====
 (defun lean-cmd-type (cmd)
@@ -125,6 +130,10 @@ It has the effect of evaluating a command in the end of the current file"
   (cl-third set-cmd))
 (defun lean-cmd-eval-get-lean-cmd (eval-cmd)
   (cl-second eval-cmd))
+(defun lean-cmd-findp-get-line-number (findp-cmd)
+  (cl-second findp-cmd))
+(defun lean-cmd-findp-get-prefix (findp-cmd)
+  (cl-third findp-cmd))
 
 ;; -- Test
 (cl-assert (string= (lean-cmd-load-get-file-name (lean-cmd-load "nat.lean"))
@@ -174,6 +183,12 @@ It has the effect of evaluating a command in the end of the current file"
 (cl-assert (string= (lean-cmd-eval-get-lean-cmd
                      (lean-cmd-eval "print 3"))
                     "print 3"))
+(cl-assert (= (lean-cmd-findp-get-line-number
+               (lean-cmd-findp 10 "iff_"))
+              10))
+(cl-assert (string= (lean-cmd-findp-get-prefix
+                     (lean-cmd-findp 10 "iff_"))
+                    "iff_"))
 
 ;; to-string functions
 ;; ===================
@@ -220,6 +235,11 @@ It has the effect of evaluating a command in the end of the current file"
 (defun lean-cmd-valid-to-string (cmd)
   "Convert valid command to string"
   (format "VALID"))
+(defun lean-cmd-findp-to-string (cmd)
+  "Convert valid command to string"
+  (format "FINDP %d\n%s"
+          (lean-cmd-findp-get-line-number cmd)
+          (lean-cmd-findp-get-prefix cmd)))
 
 (defun lean-cmd-to-string (cmd)
   "Convert command to string"
@@ -236,7 +256,8 @@ It has the effect of evaluating a command in the end of the current file"
     ('OPTIONS     (lean-cmd-options-to-string     cmd))
     ('CLEAR-CACHE (lean-cmd-clear-cache-to-string cmd))
     ('SHOW        (lean-cmd-show-to-string        cmd))
-    ('VALID       (lean-cmd-valid-to-string       cmd))))
+    ('VALID       (lean-cmd-valid-to-string       cmd))
+    ('FINDP       (lean-cmd-findp-to-string       cmd))))
 
 ;; -- Test
 (cl-assert (string= (lean-cmd-to-string (lean-cmd-load "~/work/lean/basic.lean"))
@@ -253,5 +274,7 @@ It has the effect of evaluating a command in the end of the current file"
                     (concat "INFO 42")))
 (cl-assert (string= (lean-cmd-to-string (lean-cmd-check 42 "∀ (n : nat), ne (succ n) zero"))
                     (concat "CHECK 42" "\n" "∀ (n : nat), ne (succ n) zero")))
+(cl-assert (string= (lean-cmd-to-string (lean-cmd-findp 42 "iff_"))
+                    (concat "FINDP 42" "\n" "iff_")))
 ;; ----------------
 (provide 'lean-cmd)

src/emacs/lean-server.el

@@ -52,6 +52,8 @@
              ,(rx line-start (group "-- ENDOPTIONS") line-end))
     (SHOW    ,(rx line-start "-- BEGINSHOW" line-end)
              ,(rx line-start (group "-- ENDSHOW") line-end))
+    (FINDP   ,(rx line-start "-- BEGINFINDP" (* not-newline) line-end)
+             ,(rx line-start (group "-- ENDFINDP") 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")
@@ -198,8 +200,9 @@ If it's not the same with file-name (default: buffer-file-name), send VISIT cmd.
     ('SET     ())
     ('EVAL    (lean-server-check-current-file))
     ('OPTIONS ())
-    ('SHOW    ())
+    ('SHOW    (lean-server-check-current-file))
-    ('VALID   ())))
+    ('VALID   (lean-server-check-current-file))
+    ('FINDP   (lean-server-check-current-file))))
 
 (defun lean-server-after-send-cmd (cmd)
   "Operations to perform after sending a command."
@@ -215,7 +218,8 @@ If it's not the same with file-name (default: buffer-file-name), send VISIT cmd.
     ('EVAL    ())
     ('OPTIONS ())
     ('SHOW    ())
-    ('VALID   ())))
+    ('VALID   ())
+    ('FINDP   ())))
 
 (defun lean-server-send-cmd (cmd &optional cont)
   "Send string to lean-server."
@@ -247,6 +251,18 @@ If it's not the same with file-name (default: buffer-file-name), send VISIT cmd.
                  (-drop 1 str-list)))
     (string-join str-list "\n")))
 
+(defun lean-findp-parse-string (str)
+  "Parse the output of findp command."
+  (let ((str-list (split-string str "\n")))
+    ;; Drop the first line "-- BEGINFINDP" and
+    ;; the last line "-- ENDFINDP"
+    (setq str-list
+          (-take (- (length str-list) 2)
+                 (-drop 1 str-list)))
+    (--map
+     (let ((items (split-string it "|")))
+       `(,(cl-first items) . ,(cl-second items))) str-list)))
+
 (defun lean-server-show ()
   (interactive)
   (lean-server-send-cmd (lean-cmd-show) 'message))

src/emacs/lean-variable.el

@@ -11,7 +11,7 @@
   "A shared variable contains a received message to process.
 
 A message is in the form of (TYPE PRE BODY)
-where TYPE := INFO | SET | EVAL | OPTIONS | SHOW | ERROR,
+where TYPE := INFO | SET | EVAL | OPTIONS | SHOW | FINDP | ERROR,
       PRE is a server message comes before the message
       BODY is a body of the received message.")