Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update idris-make-lemma to insert lemma above doc string of current function. #637

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Update idris-make-lemma to insert lemma above doc string of current function. #637

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
28 changes: 25 additions & 3 deletions idris-commands.el
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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)
Expand Down
113 changes: 113 additions & 0 deletions test/idris-commands-test.el
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
Loading