Improve idris-filename-to-load to return a pair of

"source dir" and "relative file path" or
"work dir" and "relative file path" when idris protocol version
is greater than 1.

Why:
In Idris2 the files are loaded relative to work directory
which is a directory containing an ".ipkg" file.

Relates to:
idris-lang/Idris2#3310
idris-hackers#627

idris-commands.el

@@ -168,14 +168,14 @@
 (defun idris-filename-to-load ()
   "Compute the working directory and filename to load in Idris.
 Returning these as a cons."
-  (let* ((fn (buffer-file-name))
-         (ipkg-srcdir (idris-ipkg-find-src-dir))
-         (srcdir (or ipkg-srcdir (file-name-directory fn))))
-    (when (and  ;; check that srcdir is prefix of filename - then load relative
-           (> (length fn) (length srcdir))
-           (string= (substring fn 0 (length srcdir)) srcdir))
-      (setq fn (file-relative-name fn srcdir)))
-    (cons srcdir fn)))
+  (let* ((ipkg-file (car-safe (idris-find-file-upwards "ipkg")))
+         (file-name (buffer-file-name))
+         (work-dir (directory-file-name (idris-file-name-parent-directory (or ipkg-file file-name))))
+         (source-dir (or (idris-ipkg-find-src-dir) work-dir)))
+    ;; TODO: Update once https://github.com/idris-lang/Idris2/issues/3310 is resolved
+    (if (> idris-protocol-version 1)
+        (cons work-dir (file-relative-name file-name work-dir))
+      (cons source-dir (file-relative-name file-name source-dir)))))
 
 (defun idris-load-file (&optional set-line)
   "Pass the current buffer's file to the inferior Idris process.

idris-compat.el

@@ -41,5 +41,28 @@ attention to case differences."
       (concat (apply 'concat (mapcar 'file-name-as-directory dirs))
               (car (reverse components))))))
 
+(if (fboundp 'file-name-parent-directory)
+    (defalias 'idris-file-name-parent-directory 'file-name-parent-directory)
+  ;; Extracted from Emacs 29+ https://github.com/emacs-mirror/emacs/blob/master/lisp/files.el
+  (defun idris-file-name-parent-directory (filename)
+    "Return the directory name of the parent directory of FILENAME.
+If FILENAME is at the root of the filesystem, return nil.
+If FILENAME is relative, it is interpreted to be relative
+to `default-directory', and the result will also be relative."
+    (let* ((expanded-filename (expand-file-name filename))
+           (parent (file-name-directory (directory-file-name expanded-filename))))
+      (cond
+       ;; filename is at top-level, therefore no parent
+       ((or (null parent)
+            ;; `equal' is enough, we don't need to resolve symlinks here
+            ;; with `file-equal-p', also for performance
+            (equal parent expanded-filename))
+        nil)
+       ;; filename is relative, return relative parent
+       ((not (file-name-absolute-p filename))
+        (file-relative-name parent))
+       (t
+        parent)))))
+
 (provide 'idris-compat)
 ;;; idris-compat.el ends here

test/idris-commands-test.el

@@ -313,6 +313,46 @@ myReverse xs = revAcc [] xs where
       (delete-directory mock-directory-name t)
       (idris-quit))))
 
+(ert-deftest idris-test-idris-filename-to-load ()
+  "Test that `idris-filename-to-load' returns expected data structure."
+  (cl-flet ((idris-ipkg-find-src-dir-stub () src-dir)
+            (idris-find-file-upwards-stub (_ex) ipkg-files)
+            (buffer-file-name-stub () "/some/path/to/idris-project/src/Component/Foo.idr"))
+    (advice-add 'idris-ipkg-find-src-dir :override #'idris-ipkg-find-src-dir-stub)
+    (advice-add 'idris-find-file-upwards :override #'idris-find-file-upwards-stub)
+    (advice-add 'buffer-file-name :override #'buffer-file-name-stub)
+    (let* ((default-directory "/some/path/to/idris-project/src/Component")
+           ipkg-files
+           src-dir)
+      (unwind-protect
+          (progn
+            (let ((result (idris-filename-to-load)))
+              (should (equal default-directory (car result)))
+              (should (equal "Foo.idr" (cdr result))))
+
+            ;; When ipkg sourcedir value is set
+            ;; Then return combination of source directory
+            ;; and relative path of the file to the source directory
+            (let* ((src-dir "/some/path/to/idris-project/src")
+                   (result (idris-filename-to-load)))
+              (should (equal src-dir (car result)))
+              (should (equal "Component/Foo.idr" (cdr result))))
+
+            ;; When ipkg sourcedir value is set
+            ;; and idris-protocol-version is greater than 1
+            ;; Then return combination of work directory
+            ;; (Directory containing the first found ipkg file)
+            ;; and relative path of the file to the work directory
+            (let* ((ipkg-files '("/some/path/to/idris-project/baz.ipkg"))
+                   (idris-protocol-version 2)
+                   (result (idris-filename-to-load)))
+              (should (equal "/some/path/to/idris-project" (car result)))
+              (should (equal "src/Component/Foo.idr" (cdr result)))))
+
+        (advice-remove 'idris-ipkg-find-src-dir #'idris-ipkg-find-src-dir-stub)
+        (advice-remove 'idris-find-file-upwards #'idris-find-file-upwards-stub)
+        (advice-remove 'buffer-file-name #'buffer-file-name-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)