branch: elpa/idris-mode
commit 248926852dd5e1ffacb4050f5e474bcfd2a04aa1
Author: Marek L <nospam.ke...@gmail.com>
Commit: Marek L <nospam.ke...@gmail.com>
Update `idris-make-lemma` to insert lemma above
doc string of current function.
Why:
Previously if function had a doc string the lemma
was inserted before signature but after the doc string
requiring user to further adjust the position.
Before:
```idris
||| Useful doc for foo
foo_rhs : String -> String
foo : String -> String
foo str = foo_rhs str
```
After:
```idris
foo_rhs : String -> String
||| Useful doc for foo
foo : String -> String
foo str = foo_rhs str
```
---
idris-commands.el | 28 +++++++++--
test/idris-commands-test.el | 113 ++++++++++++++++++++++++++++++++++++++++++++
2 files changed, 138 insertions(+), 3 deletions(-)
diff --git a/idris-commands.el b/idris-commands.el
index 95975e1aab..f8fd61c8df 100644
--- a/idris-commands.el
+++ b/idris-commands.el
@@ -653,12 +653,33 @@ Otherwise, case split as a pattern variable."
(re-search-backward (if (idris-lidr-p)
"^\\(>\\s-*\\)\\(([^)]+)\\|[a-zA-Z_0-9]+\\)\\s-*:"
"^\\(\\s-*\\)\\(([^)]+)\\|[a-zA-Z_0-9]+\\)\\s-*:"))
- (let ((indentation (match-string 1)) end-point)
+ (let ((indentation (match-string 1))
+ end-point)
(beginning-of-line)
+
+ ;; make sure we are above the documentation string
+ (forward-line -1)
+ (while (and (not (looking-at-p "^\\s-*$"))
+ (not (equal (point) (point-min)))
+ (or (looking-at-p "^|||") (looking-at-p "^--")))
+ (forward-line -1))
+
+ ;; if we reached beginning of file
+ ;; add new line between the type signature and the lemma
+ (if (equal (point) (point-min))
+ (progn
+ (newline 1)
+ (forward-line -1))
+ ;; otherwise find first non empty line
+ (forward-line -1)
+ (when (looking-at-p "^.*\\S-.*$")
+ (forward-line 1)
+ (newline 1)))
+
(insert indentation)
(setq end-point (point))
(insert type-decl)
- (newline 2)
+ (newline 1)
;; make sure point ends up ready to start a new pattern
match
(goto-char end-point))))
((equal lemma-type :provisional-definition-lemma)
@@ -669,7 +690,8 @@ Otherwise, case split as a pattern variable."
(let ((next-defn-point
(re-search-forward (if (idris-lidr-p)
"^\\(>\\s-*\\)\\(([^)]+)\\|\\w+\\)\\s-*:"
-
"^\\(\\s-*\\)\\(([^)]+)\\|\\w+\\)\\s-*:") nil t)))
+
"^\\(\\s-*\\)\\(([^)]+)\\|\\w+\\)\\s-*:")
+ nil t)))
(if next-defn-point ;; if we found a definition
(let ((indentation (match-string 1)) end-point)
(goto-char next-defn-point)
diff --git a/test/idris-commands-test.el b/test/idris-commands-test.el
index 4d1f95e49a..e37bb72f13 100644
--- a/test/idris-commands-test.el
+++ b/test/idris-commands-test.el
@@ -313,6 +313,119 @@ myReverse xs = revAcc [] xs where
(delete-directory mock-directory-name t)
(idris-quit))))
+(ert-deftest idris-test-idris-make-lemma ()
+ "Test `idris-make-lemma' replacing a hole with a metavariable lemma."
+ (cl-flet ((idris-load-file-sync-stub () nil)
+ (idris-eval-stub (&optional &rest args)
+ '((:metavariable-lemma
+ (:replace-metavariable "closeDistance_rhs s1 s2")
+ (:definition-type "closeDistance_rhs : String -> String -> IO
Bool")))))
+ (advice-add 'idris-load-file-sync :override #'idris-load-file-sync-stub)
+ (advice-add 'idris-eval :override #'idris-eval-stub)
+ (unwind-protect
+ (progn
+ (with-temp-buffer
+ (insert "closeDistance : String -> String -> IO Bool
+closeDistance s1 s2 = ?closeDistance_rhs")
+ (goto-char (point-min))
+ (re-search-forward "closeDistance_rh")
+ (funcall-interactively 'idris-make-lemma)
+ (should (string= "closeDistance_rhs : String -> String -> IO Bool
+
+closeDistance : String -> String -> IO Bool
+closeDistance s1 s2 = closeDistance_rhs s1 s2"
+ (buffer-substring-no-properties (point-min)
(point-max)))))
+
+ (with-temp-buffer
+ (insert "something_else
+
+closeDistance : String -> String -> IO Bool
+closeDistance s1 s2 = ?closeDistance_rhs")
+ (goto-char (point-min))
+ (re-search-forward "closeDistance_rh")
+ (funcall-interactively 'idris-make-lemma)
+ (should (string= "something_else
+
+closeDistance_rhs : String -> String -> IO Bool
+
+closeDistance : String -> String -> IO Bool
+closeDistance s1 s2 = closeDistance_rhs s1 s2"
+ (buffer-substring-no-properties (point-min)
(point-max)))))
+
+ (with-temp-buffer
+ (insert "something_else
+
+closeDistance : String -> String -> IO Bool
+closeDistance s1 s2 = ?closeDistance_rhs")
+ (goto-char (point-min))
+ (re-search-forward "closeDistance_rh")
+ (funcall-interactively 'idris-make-lemma)
+ (should (string= "something_else
+
+closeDistance_rhs : String -> String -> IO Bool
+
+closeDistance : String -> String -> IO Bool
+closeDistance s1 s2 = closeDistance_rhs s1 s2"
+ (buffer-substring-no-properties (point-min)
(point-max)))))
+
+ (with-temp-buffer
+ (insert "||| Check if two strings are close enough to be similar,
+||| using the namespace distance criteria.
+closeDistance : String -> String -> IO Bool
+closeDistance s1 s2 = ?closeDistance_rhs")
+ (goto-char (point-min))
+ (re-search-forward "closeDistance_rh")
+ (funcall-interactively 'idris-make-lemma)
+ (should (string= "closeDistance_rhs : String -> String -> IO Bool
+
+||| Check if two strings are close enough to be similar,
+||| using the namespace distance criteria.
+closeDistance : String -> String -> IO Bool
+closeDistance s1 s2 = closeDistance_rhs s1 s2"
+ (buffer-substring-no-properties (point-min)
(point-max)))))
+
+ (with-temp-buffer
+ (insert "something_else
+
+||| Check if two strings are close enough to be similar,
+||| using the namespace distance criteria.
+closeDistance : String -> String -> IO Bool
+closeDistance s1 s2 = ?closeDistance_rhs")
+ (goto-char (point-min))
+ (re-search-forward "closeDistance_rh")
+ (funcall-interactively 'idris-make-lemma)
+ ;; (message "%s" (buffer-substring-no-properties (point-min)
(point-max)))
+ (should (string= "something_else
+
+closeDistance_rhs : String -> String -> IO Bool
+
+||| Check if two strings are close enough to be similar,
+||| using the namespace distance criteria.
+closeDistance : String -> String -> IO Bool
+closeDistance s1 s2 = closeDistance_rhs s1 s2"
+ (buffer-substring-no-properties (point-min)
(point-max)))))
+
+ (with-temp-buffer
+ (insert "something else
+
+-- some inline comment
+closeDistance : String -> String -> IO Bool
+closeDistance s1 s2 = ?closeDistance_rhs")
+ (goto-char (point-min))
+ (re-search-forward "closeDistance_rh")
+ (funcall-interactively 'idris-make-lemma)
+ (should (string= "something else
+
+closeDistance_rhs : String -> String -> IO Bool
+
+-- some inline comment
+closeDistance : String -> String -> IO Bool
+closeDistance s1 s2 = closeDistance_rhs s1 s2"
+ (buffer-substring-no-properties (point-min)
(point-max))))))
+
+ (advice-remove 'idris-load-file-sync #'idris-load-file-sync-stub)
+ (advice-remove 'idris-eval #'idris-eval-stub))))
+
;; Tests by Yasuhiko Watanabe
;; https://github.com/idris-hackers/idris-mode/pull/537/files
(idris-ert-command-action "test-data/CaseSplit.idr" idris-case-split
idris-test-eq-buffer)
