[nongnu] elpa/idris-mode 744f773bb4 18/18: Merge pull request #578 from keram/backport-pr-21-intro

[ELPA Syncer]

branch: elpa/idris-mode
commit 744f773bb4ea5f4e2b325c34b6ebce0d129c490c
Merge: 063a63b770 5b3c88dc1d
Author: Jan de Muijnck-Hughes <jfdm@users.noreply.github.com>
Commit: GitHub <noreply@github.com>

    Merge pull request #578 from keram/backport-pr-21-intro
    
    [ new ] intro command - backport from idris2-mode
---
 idris-commands.el    | 35 +++++++++++++++++++++++------------
 idris-keys.el        |  3 ++-
 idris-tests.el       | 25 +++++++++++++++++++++++++
 test-data/Refine.idr |  4 ----
 4 files changed, 50 insertions(+), 17 deletions(-)

diff --git a/idris-commands.el b/idris-commands.el
index f69909c5f5..73df5d1b8c 100644
--- a/idris-commands.el
+++ b/idris-commands.el
@@ -735,6 +735,15 @@ Otherwise, case split as a pattern variable."
         (idris-repl-eval-string (format ":exec %s" name) 0))
     (idris-eval '(:interpret ":exec"))))
 
+(defun idris-replace-hole-with (expr)
+  "Replace the hole under the cursor by some EXPR."
+  (save-excursion
+    (let ((start (progn (search-backward "?") (point)))
+          (end (progn (forward-char) (search-forward-regexp "[^a-zA-Z0-9_']")
+                      (backward-char) (point))))
+      (delete-region start end))
+    (insert expr)))
+
 (defvar-local proof-region-start nil
   "The start position of the last proof region.")
 (defvar-local proof-region-end nil
@@ -766,13 +775,7 @@ prefix argument sets the recursion depth directly."
                            ))))
         (if (string= result "")
             (error "Nothing found")
-          (save-excursion
-            (let ((start (progn (search-backward "?") (point)))
-                  (end (progn (forward-char) (search-forward-regexp 
"[^a-zA-Z0-9_']") (backward-char) (point))))
-              (delete-region start end))
-            (setq proof-region-start (point))
-            (insert result)
-            (setq proof-region-end (point))))))))
+          (idris-replace-hole-with result))))))
 
 (defun idris-proof-search-next ()
   "Replace the previous proof search result with the next one, if it exists.
@@ -848,6 +851,18 @@ Idris 2 only."
           (insert result)
           (setq def-region-end (point)))))))
 
+(defun idris-intro ()
+  "Introduce the unambiguous constructor to use in this hole."
+  (interactive)
+  (let ((what (idris-thing-at-point)))
+    (unless (car what)
+      (error "Could not find a hole at point to refine by"))
+    (save-excursion (idris-load-file-sync))
+    (let ((results (car (idris-eval `(:intro ,(cdr what) ,(car what))))))
+      (pcase results
+        (`(,result) (idris-replace-hole-with result))
+        (_ (idris-replace-hole-with (ido-completing-read "I'm hesitating 
between: " results)))))))
+
 (defun idris-refine (name)
   "Refine by some NAME, without recursive proof search."
   (interactive "MRefine by: ")
@@ -856,11 +871,7 @@ Idris 2 only."
       (error "Could not find a hole at point to refine by"))
     (save-excursion (idris-load-file-sync))
     (let ((result (car (idris-eval `(:refine ,(cdr what) ,(car what) ,name)))))
-      (save-excursion
-        (let ((start (progn (search-backward "?") (point)))
-              (end (progn (forward-char) (search-forward-regexp 
"[^a-zA-Z0-9_']") (backward-char) (point))))
-          (delete-region start end))
-        (insert result)))))
+      (idris-replace-hole-with result))))
 
 (defun idris-identifier-backwards-from-point ()
   (let (identifier-start
diff --git a/idris-keys.el b/idris-keys.el
index ca0e568fbd..7dc5b97027 100644
--- a/idris-keys.el
+++ b/idris-keys.el
@@ -64,7 +64,8 @@
   (define-key map (kbd "C-c C-g") 'idris-generate-def)
   (define-key map (kbd "C-c C-S-g") 'idris-generate-def-next)
 
-  (define-key map (kbd "C-c C-r") 'idris-refine)
+  (define-key map (kbd "C-c C-r") 'idris-intro)
+  (define-key map (kbd "C-c C-S-r") 'idris-refine)
   (define-key map (kbd "RET") 'idris-newline-and-indent)
   ;; Not using `kbd' due to oddness about backspace and delete
   (define-key map [delete] 'idris-delete-forward-char)
diff --git a/idris-tests.el b/idris-tests.el
index a042a5d61d..5bc9d5153f 100644
--- a/idris-tests.el
+++ b/idris-tests.el
@@ -203,6 +203,31 @@ remain."
       (kill-buffer))
     (idris-quit)))
 
+(ert-deftest idris-test-idris-refine ()
+  "Test that `idris-refine' works as expected."
+  (let* ((buffer (find-file "test-data/Refine.idr"))
+         (buffer-content (buffer-substring-no-properties (point-min) 
(point-max))))
+    (goto-char (point-min))
+    (search-forward "test : T")
+    (beginning-of-line)
+    (funcall-interactively 'idris-add-clause nil)
+    (should (looking-at-p "test \\w+ = \\?test_rhs"))
+    (idris-delete-ibc t)
+    (search-forward "?test")
+    (funcall-interactively 'idris-refine "x")
+    (should (looking-at-p
+             (if (>=-protocol-version 2 1)
+                 "x"
+               "?test_rhs1")))
+    (idris-delete-ibc t)
+    ;; Cleanup
+    ;; (sit-for 3) ;; usefull for manual inspection before restore
+    (erase-buffer)
+    (insert buffer-content)
+    (save-buffer)
+    (kill-buffer)
+    (idris-quit)))
+
 (ert-deftest idris-backard-toplevel-navigation-test-2pTac9 ()
   "Test idris-backard-toplevel navigation command."
   (idris-test-with-temp-buffer
diff --git a/test-data/Refine.idr b/test-data/Refine.idr
index 7f90b68517..1a2b830821 100644
--- a/test-data/Refine.idr
+++ b/test-data/Refine.idr
@@ -8,7 +8,3 @@ f : Test -> Test
 f = const A
 
 test : Test -> Test
-
-
-
-