diff --git a/Makefile b/Makefile index e7daf044..c80e51c4 100644 --- a/Makefile +++ b/Makefile @@ -37,6 +37,7 @@ OBJS = idris-commands.elc \ idris-syntax.elc \ idris-warnings.elc \ idris-warnings-tree.elc \ + idris-xref.elc \ inferior-idris.elc .el.elc: diff --git a/idris-mode.el b/idris-mode.el index 7d95895f..4d408897 100644 --- a/idris-mode.el +++ b/idris-mode.el @@ -29,7 +29,7 @@ (require 'idris-warnings) (require 'idris-common-utils) (require 'idris-ipkg-mode) - +(require 'idris-xref) (defun idris-mode-context-menu-items (plist) "Compute menu items from PLIST that are specific to editing text in `idris-mode'." @@ -162,7 +162,9 @@ Invokes `idris-mode-hook'." (when (idris-lidr-p) (run-hooks 'idris-mode-lidr-hook)) (set (make-local-variable 'prop-menu-item-functions) - '(idris-context-menu-items idris-mode-context-menu-items))) + '(idris-context-menu-items idris-mode-context-menu-items)) + + (add-hook 'xref-backend-functions #'idris-xref-backend nil 'local)) ;; Automatically use idris-mode for .idr and .lidr files. ;;;###autoload diff --git a/idris-repl.el b/idris-repl.el index 3a0d4578..7862a3dd 100644 --- a/idris-repl.el +++ b/idris-repl.el @@ -34,6 +34,7 @@ (require 'idris-common-utils) (require 'idris-prover) (require 'idris-highlight-input) +(require 'idris-xref) (eval-when-compile (require 'cl-lib)) @@ -229,7 +230,8 @@ Invokes `idris-repl-mode-hook'." (set (make-local-variable 'completion-at-point-functions) '(idris-repl-complete)) (setq mode-name `("Idris-REPL" (:eval (if idris-rex-continuations "!" "")))) (set (make-local-variable 'prop-menu-item-functions) - '(idris-context-menu-items))) + '(idris-context-menu-items)) + (add-hook 'xref-backend-functions #'idris-xref-backend nil 'local)) (defun idris-repl-remove-event-hook-function () (setq idris-prompt-string "Idris") diff --git a/idris-tests.el b/idris-tests.el index 2c3e9f5a..5f3476ab 100644 --- a/idris-tests.el +++ b/idris-tests.el @@ -189,7 +189,7 @@ remain." (with-current-buffer (get-buffer idris-info-buffer-name) (goto-char (point-min)) (should (re-search-forward "Zero" nil t))) - (idris-quit)) + (idris-quit)) (ert-deftest idris-test-ipkg-packages-with-underscores-and-dashes () "Test that loading an ipkg file can have dependencies on packages with _ or - in the name." @@ -322,7 +322,7 @@ myReverse xs = revAcc [] xs where "Some warning message")) ;; Cleanup (kill-buffer)))) - + (ert-deftest idris-backard-toplevel-navigation-test-2pTac9 () "Test idris-backard-toplevel navigation command." (idris-test-with-temp-buffer @@ -576,5 +576,6 @@ getData2 st failcount (should (looking-back "Store LoggedOut)]" (line-beginning-position))) )) +(load "idris-xref-test.el") (provide 'idris-tests) ;;; idris-tests.el ends here diff --git a/idris-xref-test.el b/idris-xref-test.el new file mode 100644 index 00000000..57d62cb6 --- /dev/null +++ b/idris-xref-test.el @@ -0,0 +1,328 @@ +;;; idris-xref-test.el --- Tests for Idris Xref backend -*- lexical-binding: t -*- +;; Copyright (C) 2022 Marek L. + +;; Author: Marek L +;; Keywords: languages, Idris, Xref, Ert + +;; This program is free software; you can redistribute it and/or modify +;; it under the terms of the GNU General Public License as published by +;; the Free Software Foundation, either version 3 of the License, or +;; (at your option) any later version. + +;; This program is distributed in the hope that it will be useful, +;; but WITHOUT ANY WARRANTY; without even the implied warranty of +;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +;; GNU General Public License for more details. + +;; You should have received a copy of the GNU General Public License +;; along with this program. If not, see . + +;;; Code: + +(require 'ert) +(require 'idris-xref) + +(ert-deftest idris-xref-backend-definitions--error-when-no-connection () + "Test that the file is loaded before making search for definition." + (let ((buffer (find-file-noselect "test-data/AddClause.idr")) + (inhibit-read-only t)) + (with-current-buffer "*Messages*" (erase-buffer)) + (with-current-buffer buffer + (goto-char (point-min)) + (search-forward ": Test") + (condition-case err + (funcall-interactively 'xref-find-definitions "Test") + (error (message "Error: %s" (error-message-string err))) + (user-error (message "User Error: %s" (error-message-string err))))) + + (with-current-buffer "*Messages*" + (should + (string-match-p "Buffer AddClause.idr has no process" + (buffer-substring-no-properties (point-min) (point-max))))) + + ;; Cleanup + (kill-buffer buffer))) + +(ert-deftest idris-xref-backend-definitions--not-supported-on-Idris-1 () + "Test that user error raised when invoking `xref-find-definitions' used on Idris1." + (let ((buffer (find-file-noselect "test-data/AddClause.idr")) + (err-msg "did not understand (synchronous Idris evaluation failed)") + (inhibit-read-only t)) + (with-current-buffer "*Messages*" (erase-buffer)) + (cl-flet ((idris-load-file-sync-stub () nil) + (idris-eval-stub (&optional &rest _args) + (user-error err-msg))) + (advice-add 'idris-load-file-sync :override #'idris-load-file-sync-stub) + (advice-add 'idris-eval :override #'idris-eval-stub) + + (unwind-protect + (with-current-buffer buffer + (goto-char (point-min)) + (search-forward ": Test") + + (condition-case err + (funcall-interactively 'xref-find-definitions "Test") + (error (message "%s" (error-message-string err))))) + + (advice-remove 'idris-load-file-sync #'idris-load-file-sync-stub) + (advice-remove 'idris-eval #'idris-eval-stub))) + + (with-current-buffer "*Messages*" + (should + (string-match-p err-msg (buffer-substring-no-properties (point-min) (point-max))))) + + ;; Cleanup + (kill-buffer buffer))) + +(ert-deftest idris-xref-backend-definitions--no-results () + "Test that an user error message is displayed when no definition found." + ;; Arrange + (let ((buffer (find-file-noselect "test-data/AddClause.idr")) + (idris-protocol-version 3) + (inhibit-read-only t)) + (with-current-buffer "*Messages*" (erase-buffer)) + (cl-flet ((idris-load-file-sync-stub () nil) + (idris-eval-stub (&optional &rest _args) '())) + (advice-add 'idris-load-file-sync :override #'idris-load-file-sync-stub) + (advice-add 'idris-eval :override #'idris-eval-stub) + + (unwind-protect + (with-current-buffer buffer + (goto-char (point-min)) + (search-forward ": Test") + ;; (with-demoted-errors "Error: %s" + ;; ;; Act + ;; (funcall-interactively 'xref-find-definitions "Test")) + (condition-case err + (funcall-interactively 'xref-find-definitions "Test") + (user-error (message "%s" (error-message-string err))))) + + (advice-remove 'idris-load-file-sync #'idris-load-file-sync-stub) + (advice-remove 'idris-eval #'idris-eval-stub))) + + (with-current-buffer "*Messages*" + ;; Assert + (should + (string-match-p "No definitions found for: Test" + (buffer-substring-no-properties (point-min) (point-max))))) + ;; Cleanup + (kill-buffer buffer))) + +(ert-deftest idris-xref-backend-definitions--one-existing-file-result () + "Test that point jumps to location in file from result." + (let* ((buffer (find-file-noselect "test-data/AddClause.idr")) + (idris-protocol-version 3) + (eval-result `((("AddClause.Test" + (:filename ,(buffer-file-name buffer)) + (:start 2 0) + (:end 2 17))))) + (inhibit-read-only t)) + (with-current-buffer "*Messages*" (erase-buffer)) + (cl-flet ((idris-load-file-sync-stub () nil) + (idris-eval-stub (&optional &rest _args) eval-result)) + (advice-add 'idris-load-file-sync :override #'idris-load-file-sync-stub) + (advice-add 'idris-eval :override #'idris-eval-stub) + + (unwind-protect + (with-current-buffer buffer + (goto-char (point-min)) + (search-forward ": Test") + (should (eq 6 (line-number-at-pos (point)))) + + (condition-case err + (funcall-interactively 'xref-find-definitions "Test") + (user-error (message "%s" (error-message-string err)))) + + (should (eq 3 (line-number-at-pos (point))))) + + (advice-remove 'idris-load-file-sync #'idris-load-file-sync-stub) + (advice-remove 'idris-eval #'idris-eval-stub))) + + ;; Cleanup + (kill-buffer buffer))) + +(ert-deftest idris-xref-backend-definitions--one-no-real-file-result () + "Test that the term and filename as message is displayed." + (let* ((buffer (find-file-noselect "test-data/AddClause.idr")) + (idris-protocol-version 3) + (eval-result `((("prim__lte_Bits64" + (:filename "(Interactive)") + (:start 0 0) + (:end 0 0))))) + (inhibit-read-only t)) + (with-current-buffer "*Messages*" (erase-buffer)) + (cl-flet ((idris-load-file-sync-stub () nil) + (idris-eval-stub (&optional &rest _args) eval-result)) + (advice-add 'idris-load-file-sync :override #'idris-load-file-sync-stub) + (advice-add 'idris-eval :override #'idris-eval-stub) + + (unwind-protect + (with-current-buffer buffer + (goto-char (point-min)) + (search-forward ": Test") + ;; (with-demoted-errors "Error: %s" + ;; ;; Act + ;; (funcall-interactively 'xref-find-definitions "Test")) + (condition-case err + (funcall-interactively 'xref-find-definitions "Test") + (user-error (message "%s" (error-message-string err))))) + + (advice-remove 'idris-load-file-sync #'idris-load-file-sync-stub) + (advice-remove 'idris-eval #'idris-eval-stub))) + + (with-current-buffer "*Messages*" + ;; Assert + (should + (string-match-p "prim__lte_Bits64 : (Interactive)" + (buffer-substring-no-properties (point-min) (point-max))))) + ;; Cleanup + (kill-buffer buffer))) + +(ert-deftest idris-xref-backend-definitions--multiple-results () + "Test that results are listed in *xref* buffer." + (let* ((buffer (find-file-noselect "test-data/AddClause.idr")) + (idris-protocol-version 3) + (eval-result `((("prim__lte_Bits64" + (:filename "(Interactive)") + (:start 0 0) + (:end 0 0)) + ("Prelude.Num.(-)" + (:filename "(File-Not-Found)") + (:start 30 2) + (:end 30 5)) + ("AddClause.(-)" + (:filename "AddClause.idr") + (:start 10 0) + (:end 10 9)))))) + (cl-flet ((idris-load-file-sync-stub () nil) + (idris-eval-stub (&optional &rest _args) eval-result)) + (advice-add 'idris-load-file-sync :override #'idris-load-file-sync-stub) + (advice-add 'idris-eval :override #'idris-eval-stub) + + (unwind-protect + (with-current-buffer buffer + (goto-char (point-min)) + (search-forward ": Test") + ;; (with-demoted-errors "Error: %s" + ;; ;; Act + ;; (funcall-interactively 'xref-find-definitions "Test")) + (condition-case err + (funcall-interactively 'xref-find-definitions "Test") + (user-error (message "%s" (error-message-string err))))) + + (advice-remove 'idris-load-file-sync #'idris-load-file-sync-stub) + (advice-remove 'idris-eval #'idris-eval-stub))) + + (with-current-buffer "*xref*" + ;; Assert + (let ((str (buffer-substring-no-properties (point-min) (point-max)))) + (should (string-match-p "11: AddClause.(-)" str)) + (should (string-match-p "AddClause.idr" str)) + (should (string-match-p "Prelude.Num.(-)" str)) + (should (string-match-p "prim__lte_Bits64" str))) + (kill-buffer)) + + ;; Cleanup + (kill-buffer buffer))) + +(ert-deftest idris-xref-normalise () + "Test normalisation of results from Idris compiler. +The updated candidate should have absolute path to file when possible +and coordinates indexed as expected by Emacs." + (let* ((buffer (find-file-noselect "test-data/AddClause.idr")) + (candidate `("AddClause.Test" + (:filename ,(buffer-file-name buffer)) + (:start 2 0) + (:end 2 17))) + (result (idris-xref-normalise candidate))) + + (pcase-let ((`(,_term (:filename ,fn) + (:start ,start-line ,start-col) + (:end ,_end-line ,_end-col)) + result)) + (should (string= fn (buffer-file-name buffer))) + (should (eq start-line 3)) + (should (eq start-col 1)))) + + ;; Test that the filepath is reconstructed from term + ;; and Idris process current working directory + (let* ((buffer (find-file-noselect "test-data/AddClause.idr")) + (candidate `("AddClause.Test" + (:filename "(File-Not-Found)") + (:start 2 0) + (:end 2 17))) + (idris-process-current-working-directory (file-name-directory (buffer-file-name buffer))) + (result (idris-xref-normalise candidate))) + + (pcase-let ((`(,_term (:filename ,fn) + (:start ,start-line ,start-col) + (:end ,_end-line ,_end-col)) + result)) + (should (string= fn (buffer-file-name buffer))) + (should (eq start-line 3)) + (should (eq start-col 1)))) + + ;; Test that the original filename returned if no success to + ;; reconstruct real absolute file path + (let* ((buffer (find-file-noselect "test-data/AddClause.idr")) + (candidate `("AddClause.Test" + (:filename "(File-Not-Found)") + (:start 2 0) + (:end 2 17))) + (idris-process-current-working-directory nil) + (result (idris-xref-normalise candidate))) + + (pcase-let ((`(,_term (:filename ,fn) + (:start ,start-line ,start-col) + (:end ,_end-line ,_end-col)) + result)) + (should (string= fn "(File-Not-Found)")) + (should (eq start-line 3)) + (should (eq start-col 1)))) + + ;; Test that the filepath is reconstructed from term + ;; and (idris-xref-idris-source-directories) + (let* ((buffer (find-file-noselect "test-data/AddClause.idr")) + (candidate `("AddClause.Test" + (:filename "(File-Not-Found)") + (:start 2 0) + (:end 2 17))) + (idris-process-current-working-directory nil)) + (cl-flet ((idris-xref-idris-source-directories-stub + () + (cons (file-name-directory (buffer-file-name buffer)) '()))) + (advice-add 'idris-xref-idris-source-directories + :override #'idris-xref-idris-source-directories-stub) + + (let ((result (idris-xref-normalise candidate))) + (pcase-let ((`(,_term (:filename ,fn) + (:start ,start-line ,start-col) + (:end ,_end-line ,_end-col)) + result)) + + (should (string= fn (buffer-file-name buffer))) + (should (eq start-line 3)) + (should (eq start-col 1)))) + (advice-remove 'idris-xref-idris-source-directories + #'idris-xref-idris-source-directories-stub))) + + ;; Test that the filepath is reconstructed from term + ;; and path from idris-xref-idris-source-locations + (let* ((buffer (find-file-noselect "test-data/AddClause.idr")) + (candidate `("AddClause.Test" + (:filename "(File-Not-Found)") + (:start 2 0) + (:end 2 17))) + (idris-xref-idris-source-locations (cons (file-name-directory (buffer-file-name buffer)) '())) + (result (idris-xref-normalise candidate))) + + (pcase-let ((`(,_term (:filename ,fn) + (:start ,start-line ,start-col) + (:end ,_end-line ,_end-col)) + result)) + (should (string= fn (buffer-file-name buffer))) + (should (eq start-line 3)) + (should (eq start-col 1))))) + +(provide 'idris-xref-test) +;;; idris-xref-test.el ends here diff --git a/idris-xref.el b/idris-xref.el new file mode 100644 index 00000000..bbc6cb88 --- /dev/null +++ b/idris-xref.el @@ -0,0 +1,147 @@ +;;; idris-xref.el --- Xref backend for Idris -*- lexical-binding: t -*- +;; Copyright (C) 2022 Marek L. + +;; Author: Marek L +;; Keywords: languages, Idris, Xref + +;; This program is free software; you can redistribute it and/or modify +;; it under the terms of the GNU General Public License as published by +;; the Free Software Foundation, either version 3 of the License, or +;; (at your option) any later version. + +;; This program is distributed in the hope that it will be useful, +;; but WITHOUT ANY WARRANTY; without even the implied warranty of +;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +;; GNU General Public License for more details. + +;; You should have received a copy of the GNU General Public License +;; along with this program. If not, see . + +;;; Commentary: +;; + +;;; Code: + +(require 'xref) +(require 'inferior-idris) +(require 'idris-common-utils) + +;; TODO: Define as idris-file-extension +(defconst idris-xref-idris-file-extension "idr") + +(defgroup idris-xref nil "Idris Xref Backend." :prefix 'idris :group 'idris) + +(defcustom idris-xref-idris-source-location "" + "Path to local Idris language codebase repository." + :type 'directory + :group 'idris-xref) + +(defcustom idris-xref-idris-source-locations '() + "List of additional directories to perform lookup for a term. +To support jump to definition for Idris build-in types +set `idris-xref-idris-source-location' instead." + :type '(repeat directory) + :group 'idris-xref) + +;; TODO: Memoize +(defun idris-xref-idris-source-directories () + "Return list of directories from Idris repository to do lookup for a term." + (when (and idris-xref-idris-source-location (file-directory-p idris-xref-idris-source-location)) + (let ((src-dir (expand-file-name "src" idris-xref-idris-source-location)) + (libs-dir (expand-file-name "libs" idris-xref-idris-source-location))) + (when (and (file-directory-p src-dir) (file-directory-p libs-dir)) + (cons src-dir + (seq-filter #'file-directory-p + (mapcar (lambda (dir) (expand-file-name dir libs-dir)) + (seq-remove (lambda (dir) (string-match-p "\\." dir)) + (directory-files libs-dir))))))))) + +(defun idris-xref-backend () + "An `xref-backend-functions' implementation for `idris-mode'." + 'idris) + +(cl-defmethod xref-backend-identifier-at-point ((_backend (eql idris))) + "Alias for `idris-name-at-point'." + (idris-name-at-point)) + +(cl-defmethod xref-backend-definitions ((_backend (eql idris)) symbol) + "Return a list of Xref objects candidates matching SYMBOL." + + (mapcar #'idris-xref-make-xref + (mapcar #'idris-xref-normalise (idris-xref-find-definitions symbol)))) + +(cl-defmethod xref-backend-apropos ((_backend (eql idris))) + "Not yet supported." + nil) + +(cl-defmethod xref-backend-identifier-completion-table ((_backend (eql idris))) + "Not yet supported." + nil) + +(defun idris-xref-find-definitions (symbol) + "Return a list of Idris candidate locations matching SYMBOL." + (car (idris-eval `(:name-at ,symbol)))) + +(defun idris-xref-normalise (candidate) + "Return normalised CANDIDATE. + +It will try add filename absolute path if not present and +update coordinates to be indexed from 1 as expected by Emacs." + (pcase-let ((`(,term (:filename ,fn) + (:start ,start-line ,start-col) + (:end ,end-line ,end-col)) + candidate)) + (let ((new-fn (idris-xref-filepath term fn))) + `(,term (:filename ,new-fn) + (:start ,(1+ start-line) ,(1+ start-col)) + (:end ,(1+ end-line) ,(1+ end-col)))))) + +(defun idris-xref-make-xref (location) + "Return a new Xref object from LOCATION." + (pcase-let ((`(,term (:filename ,fn) + (:start ,start-line ,start-col) + (:end ,_end-line ,_end-col)) + location)) + (xref-make term + (if (file-exists-p fn) + (xref-make-file-location fn start-line start-col) + (xref-make-bogus-location (format "%s : %s" term fn)))))) + +(defun idris-xref-filepath (term file) + "Return filepath for TERM. +If FILE is path to existing file returns the FILE. +Otherwise try find the corresponding FILE for TERM in `idris-xref-directories'." + (if (file-exists-p file) + file + (let ((file-paths (idris-xref-abs-filepaths term (idris-xref-directories)))) + (if (null file-paths) + file + ;; TODO: Instead of getting the first filepath build list of candidates + (car file-paths))))) + +(defun idris-xref-directories () + "List of directories to perform lookup for file containing a term. +The list consist of `idris-process-current-working-directory', +`idris-xref-idris-source-directories' and `idris-xref-idris-source-locations'." + (append + (and idris-process-current-working-directory (list idris-process-current-working-directory)) + (idris-xref-idris-source-directories) + (seq-filter #'file-directory-p idris-xref-idris-source-locations))) + +(defun idris-xref-relative-filepath-from-term (term) + "Return relative Idris file path created from TERM." + (let* ((term-parts (reverse (butlast (split-string term "\\.")))) + (file-base (pop term-parts)) + (file-name (concat file-base "." idris-xref-idris-file-extension))) + (apply 'idris-file-name-concat (reverse (cons file-name term-parts))))) + +(defun idris-xref-abs-filepaths (term locations) + "Return absolute filepaths build from TERM and LOCATIONS." + (let ((rel-path (idris-xref-relative-filepath-from-term term))) + ;; TODO: Check also the content of file for presence of the term + (seq-filter #'file-exists-p + (mapcar (lambda (loc) (expand-file-name rel-path loc)) + locations)))) + +(provide 'idris-xref) +;;; idris-xref.el ends here