diff --git a/idris-commands.el b/idris-commands.el index 95975e1..f8fd61c 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 4d1f95e..e37bb72 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)