branch: elpa/idris-mode
commit f5bf588ef37fd710cfb71a3ea74f47f6d606d81d
Merge: f69b32d689 19aa3d7b02
Author: Jan de Muijnck-Hughes <j...@users.noreply.github.com>
Commit: GitHub <nore...@github.com>
Merge pull request #606 from keram/test-restruct-draft
Move test files to test/ directory
---
.github/workflows/idris2.yml | 1 -
Makefile | 25 +-
idris-tests.el | 581 ---------------------
idris-tests3.el | 42 --
test/idris-commands-test.el | 295 +++++++++++
test/idris-navigate-test.el | 265 ++++++++++
idris-test-utils.el => test/idris-test-utils.el | 18 +-
test/idris-tests.el | 142 +++++
idris-xref-test.el => test/idris-xref-test.el | 0
{test-data => test/test-data}/AddClause.idr | 0
{test-data => test/test-data}/AddMissing.idr | 0
{test-data => test/test-data}/CaseSplit.idr | 0
test/test-data/Empty.idr | 0
{test-data => test/test-data}/GenerateDef.idr | 0
{test-data => test/test-data}/MakeLemma.idr | 0
{test-data => test/test-data}/MakeWithBlock.idr | 0
{test-data => test/test-data}/MetavarTest.idr | 0
{test-data => test/test-data}/ProofSearch.idr | 0
{test-data => test/test-data}/Refine.idr | 0
{test-data => test/test-data}/TypeAtPoint.idr | 0
{test-data => test/test-data}/TypeError.idr | 0
.../test-data}/cmdline/commandlinetest.ipkg | 0
.../test-data}/cmdline/src/Command/Line/Test.idr | 0
.../test-data}/package-test/Packaging.idr | 0
.../test-data}/package-test/test.ipkg | 0
25 files changed, 722 insertions(+), 647 deletions(-)
diff --git a/.github/workflows/idris2.yml b/.github/workflows/idris2.yml
index 838da56786..f7d83570fb 100644
--- a/.github/workflows/idris2.yml
+++ b/.github/workflows/idris2.yml
@@ -94,6 +94,5 @@ jobs:
make clean
make build
make test2
- make test3
# -- [ EOF ]
diff --git a/Makefile b/Makefile
index c80e51c4bb..46994f0f13 100644
--- a/Makefile
+++ b/Makefile
@@ -46,32 +46,27 @@ OBJS = idris-commands.elc \
build: getdeps $(OBJS)
test: getdeps build
- $(BATCHEMACS) -L . -l ert -l idris-tests.el -f
ert-run-tests-batch-and-exit
+ $(BATCHEMACS) -L . -l ert -l test/idris-tests.el -f
ert-run-tests-batch-and-exit
test2: getdeps build
$(BATCHEMACS) -L . \
-eval '(setq idris-interpreter-path (executable-find
"idris2"))' \
- -l ert -l idris-tests.el -f ert-run-tests-batch-and-exit
-
-test3: getdeps build
- $(BATCHEMACS) -L . \
- -eval '(setq idris-interpreter-path (executable-find
"idris2"))' \
- -l ert -l idris-tests3.el -f ert-run-tests-batch-and-exit
+ -l ert -l test/idris-tests.el -f ert-run-tests-batch-and-exit
clean:
-${RM} -f $(OBJS)
- -${RM} -f test-data/*ibc
- -${RM} -rf test-data/build/
+ -${RM} -f test/test-data/*ibc
+ -${RM} -rf test/test-data/build/
-${RM} -r docs/auto docs/*.aux docs/*.log docs/*.pdf
getdeps:
$(BATCHEMACS) -eval \
"(let* \
- ((need-pkgs '($(NEED_PKGS))) \
- (want-pkgs (seq-remove #'package-installed-p need-pkgs))) \
- (unless (null want-pkgs) \
- (package-initialize) \
- (package-refresh-contents) \
- (mapcar #'package-install want-pkgs)))"
+ ((need-pkgs '($(NEED_PKGS))) \
+ (want-pkgs (seq-remove #'package-installed-p
need-pkgs))) \
+ (unless (null want-pkgs) \
+ (package-initialize) \
+ (package-refresh-contents) \
+ (mapcar #'package-install want-pkgs)))"
docs: docs/documentation.tex
-@( cd docs/ && latexmk -xelatex documentation.tex )
diff --git a/idris-tests.el b/idris-tests.el
deleted file mode 100644
index 5f3476ab04..0000000000
--- a/idris-tests.el
+++ /dev/null
@@ -1,581 +0,0 @@
-;;; idris-tests.el --- Tests for idris-mode -*- lexical-binding: t -*-
-
-;; Copyright (C) 2014 David Raymond Christiansen
-
-;; Author: David Raymond Christiansen <d...@itu.dk>
-;; Keywords: languages
-
-;; 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 <http://www.gnu.org/licenses/>.
-
-;;; Commentary:
-
-;; This is a collection of simple tests for idris-mode.
-
-;;; Code:
-
-(require 'idris-mode)
-(require 'idris-navigate)
-(require 'inferior-idris)
-(require 'idris-ipkg-mode)
-(require 'cl-lib)
-(require 'idris-test-utils)
-
-
-(ert-deftest trivial-test ()
- (should t))
-
-(ert-deftest idris-test-idris-editor-port ()
- (let ((output "Can't find import Prelude\n37072\n"))
- (should (string-match idris-process-port-output-regexp output))
- (should (string= "Can't find import Prelude\n" (match-string 1 output)))
- (should (string= "37072" (match-string 2 output))))
- (let ((output "37072\n"))
- (should (string-match idris-process-port-output-regexp output))
- (should (null (match-string 1 output)))
- (should (string= "37072" (match-string 2 output)))))
-
-(ert-deftest idris-test-idris-quit ()
- "Ensure that running Idris and quitting doesn't leave behind
-unwanted buffers."
- (let ((before (buffer-list)))
- (idris-repl)
- (dotimes (_ 5) (accept-process-output nil 1))
- (idris-quit)
- (let* ((after (buffer-list))
- (extra (cl-set-difference after before)))
- (should (= (length extra) 0)))))
-
-(ert-deftest idris-test-idris-quit-logging-enabled ()
- "Ensure that running Idris and quitting doesn't leave behind
-unwanted buffers. In particular, only *idris-events* should
-remain."
- (let ((before (buffer-list))
- (idris-log-events 't))
- (idris-repl)
- (dotimes (_ 5) (accept-process-output nil 1))
- (idris-quit)
- (let* ((after (buffer-list))
- (extra (cl-set-difference after before)))
- (should (= (length extra) 1))
- (should (string= (buffer-name (car extra)) idris-event-buffer-name)))
-
- ;; Cleanup
- (kill-buffer idris-event-buffer-name)))
-
-(ert-deftest idris-test-hole-load ()
- "Test the hole-list-on-load setting."
- ;;; The default setting should be to show holes
- (should idris-hole-show-on-load)
-
- (let ((buffer (find-file "test-data/MetavarTest.idr")))
- ;;; Check that the file was loaded
- (should (bufferp buffer))
-
- ;;; Check that it shows the hole list with the option turned on
- (with-current-buffer buffer
- (idris-load-file))
- ;;; Allow async stuff to happen
- (dotimes (_ 5) (accept-process-output nil 1))
- (let ((mv-buffer (get-buffer idris-hole-list-buffer-name)))
- ;; The buffer exists and contains characters
- (should (bufferp mv-buffer))
- (should (> (buffer-size mv-buffer) 10)))
- (idris-quit)
-
- ;; Now check that it works with the setting the other way
- (let ((idris-hole-show-on-load nil))
- (with-current-buffer buffer
- (idris-load-file))
- (dotimes (_ 5) (accept-process-output nil 1))
- (let ((mv-buffer (get-buffer idris-hole-list-buffer-name)))
- (should-not (bufferp mv-buffer))
- (should (null mv-buffer))))
- ;; Clean up
- (kill-buffer))
-
- ;; More cleanup
- (idris-quit))
-
-(ert-deftest idris-list-holes ()
- "Test `idris-list-holes' command."
- (let ((buffer (find-file-noselect "test-data/MetavarTest.idr"))
- (other-buffer (find-file-noselect "test-data/MakeWithBlock.idr")))
- ;; Test that hole info is present without need to load file manually
- (with-current-buffer buffer
- (idris-list-holes)
- (dotimes (_ 5) (accept-process-output nil 1))
- (let ((holes-buffer (get-buffer idris-hole-list-buffer-name)))
- (should (bufferp holes-buffer))
- (should (> (buffer-size holes-buffer) 10))))
- ;; Test that the hole info is updated for the other current buffer
- (with-current-buffer other-buffer
- (idris-list-holes)
- (dotimes (_ 5) (accept-process-output nil 1))
- (let ((holes-buffer (get-buffer idris-hole-list-buffer-name)))
- (should (not (bufferp holes-buffer)))))
-
- (kill-buffer buffer)
- (kill-buffer other-buffer)
- (idris-quit)))
-
-(ert-deftest idris-test-proof-search ()
- "Test that proof search works"
- :expected-result (if (string-match-p "idris2" idris-interpreter-path)
- :failed
- :passed)
- (unwind-protect
- (let ((buffer (find-file "test-data/ProofSearch.idr")))
- (with-current-buffer buffer
- (idris-load-file)
- (dotimes (_ 5) (accept-process-output nil 1))
- (goto-char (point-min))
- (re-search-forward "search_here")
- (goto-char (match-beginning 0))
- (idris-proof-search)
- (dotimes (_ 5) (accept-process-output nil 1))
- (should (looking-at-p "lteSucc (lteSucc (lteSucc (lteSucc (lteSucc
lteZero))))"))
- (move-beginning-of-line nil)
- (delete-region (point) (line-end-position))
- (insert "prf = ?search_here")
- (save-buffer)
- (kill-buffer)))
-
- ;; More cleanup
- (idris-quit)))
-
-(ert-deftest idris-test-find-cmdline-args ()
- "Test that idris-mode calculates command line arguments from .ipkg files."
- ;; Outside of a project, none are found
- (let ((buffer (find-file "test-data/ProofSearch.idr")))
- (with-current-buffer buffer
- (should (null (idris-ipkg-flags-for-current-buffer)))
- (kill-buffer)))
- ;; Inside of a project, the correct ones are found
- (let ((buffer (find-file "test-data/cmdline/src/Command/Line/Test.idr")))
- (with-current-buffer buffer
- (should (equal (idris-ipkg-flags-for-current-buffer)
- (list "-p" "effects")))
- (kill-buffer))))
-
-(ert-deftest idris-test-error-buffer ()
- "Test that loading a type-incorrect Idris buffer results in an error message
buffer."
- (let ((buffer (find-file "test-data/TypeError.idr")))
- (with-current-buffer buffer
- (idris-load-file)
- (dotimes (_ 5) (accept-process-output nil 1))
- (should (get-buffer idris-notes-buffer-name)))
- (with-current-buffer (get-buffer idris-notes-buffer-name)
- (goto-char (point-min))
- (should (re-search-forward "Nat" nil t))) ;; check that the buffer has
something error-like
- (with-current-buffer buffer
- (kill-buffer))
- (idris-quit)))
-
-(ert-deftest idris-test-idris-type-search ()
- "Test that `idris-type-search' produces output in Idris info buffer."
- (idris-run)
- (funcall-interactively 'idris-type-search "Nat")
- (with-current-buffer (get-buffer idris-info-buffer-name)
- (goto-char (point-min))
- (should (re-search-forward "Zero" nil t)))
- (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."
- (let ((buffer (find-file "test-data/package-test/Packaging.idr")))
- (with-current-buffer buffer
- (should (equal '("-p" "idris-free" "-p" "recursion_schemes")
- (idris-ipkg-pkgs-flags-for-current-buffer)))
- (kill-buffer buffer))
- (idris-quit)))
-
-(ert-deftest idris-test-idris-add-clause ()
- "Test that `idris-add-clause' generates definition with hole."
- (let ((buffer (find-file-noselect "test-data/AddClause.idr"))
- (buffer-content (with-temp-buffer
- (insert-file-contents "test-data/AddClause.idr")
- (buffer-string))))
- (with-current-buffer buffer
- (goto-char (point-min))
- (re-search-forward "test :")
- (goto-char (match-beginning 0))
- (funcall-interactively 'idris-add-clause nil)
- (should (looking-at-p "test \\w+ = \\?test_rhs"))
- (idris-delete-ibc t)
-
- (re-search-forward "(-) :")
- (goto-char (1+ (match-beginning 0)))
- (funcall-interactively 'idris-add-clause nil)
- (should (looking-at-p "(-) = \\?\\w+_rhs"))
- (idris-delete-ibc t)
-
- ;; Test that response with indentation (Idris2) are aligned correctly
- ;; Idris1 response: "revAcc xs ys = ?revAcc_rhs"
- ;; Idris2 response: " revAcc xs ys = ?revAcc_rhs"
- (goto-char (point-max))
- (insert "
-myReverse : List a -> List a
-myReverse xs = revAcc [] xs where
- revAcc : List a -> List a -> List a")
- (search-backward "evAcc")
- (funcall-interactively 'idris-add-clause nil)
- (beginning-of-line)
- (should (looking-at-p "^ revAcc xs ys = \\?revAcc_rhs"))
-
- ;; Cleanup
- (erase-buffer)
- (insert buffer-content)
- (save-buffer)
- (kill-buffer))
- (idris-quit)))
-
-(ert-deftest idris-test-idris-refine ()
- "Test that `idris-refine' works as expected."
- (let* ((buffer (find-file "test-data/Refine.idr"))
- (buffer-content (buffer-substring-no-properties (point-min)
(point-max))))
- (goto-char (point-min))
- (search-forward "test : T")
- (beginning-of-line)
- (funcall-interactively 'idris-add-clause nil)
- (should (looking-at-p "test \\w+ = \\?test_rhs"))
- (idris-delete-ibc t)
- (search-forward "?test")
- (funcall-interactively 'idris-refine "x")
- (should (looking-at-p
- (if (>=-protocol-version 2 1)
- "x"
- "?test_rhs1")))
- (idris-delete-ibc t)
- ;; Cleanup
- ;; (sit-for 3) ;; usefull for manual inspection before restore
- (erase-buffer)
- (insert buffer-content)
- (save-buffer)
- (kill-buffer)
- (idris-quit)))
-
-(ert-deftest idris-test-idris-type-at-point ()
- "Test that `idris-type-at-point' works."
- (let ((buffer (find-file-noselect "test-data/AddClause.idr")))
- ;; Assert that we have clean global test state
- (should (not idris-connection))
- (with-current-buffer buffer
- ;; Hack to reduce random failures
- ;; TODO: Fix the leak
- (idris-delete-ibc t)
- (goto-char (point-min))
- (re-search-forward "data Test")
- (funcall-interactively 'idris-type-at-point nil)
- ;; Assert that Idris connection is created
- (should idris-connection)
- ;; Assert that focus is in the Idris info buffer
- (should (string= (buffer-name) idris-info-buffer-name))
- ;; Assert that the info buffer displays a type
- (should (string-match-p "Test : Type" (buffer-substring-no-properties
(point-min) (point-max))))
-
- ;; TODO: How to emulate "q" key binding to quit info buffer?
- (idris-info-quit)
- ;; Assert leaving info buffer will get us back to Idris code buffer
- (should (eq (current-buffer) buffer))
-
- ;; Cleanup
- (kill-buffer))
- (idris-quit)))
-
-(ert-deftest idris-test-warning-overlay ()
- "Test that `idris-warning-overaly-point' works as expected."
- (let* ((buffer (find-file-noselect "test-data/AddClause.idr"))
- (warning '("AddClause.idr" (5 7) (5 17) "Some warning message" ()))
- (idris-raw-warnings '())
- (idris-process-current-working-directory (file-name-directory
(buffer-file-name buffer)))
- (expected-position)
- (expected-overlay))
- (with-current-buffer buffer
- (goto-char (point-min))
- (re-search-forward "data Test")
- (setq expected-position (point))
-
- (idris-warning-overlay warning)
-
- ;; Assert that the point position does not change
- ;; https://github.com/idris-community/idris2-mode/issues/36
- (should (eq (point) expected-position))
-
- ;; Assert side effect
- (should (not (null idris-raw-warnings)))
-
- ;; Assert that overlay was added
- (setq expected-overlay (car (overlays-in (point-min) (point-max))))
- (should (not (null expected-overlay)))
- (should (string= (overlay-get expected-overlay 'help-echo)
- "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
- "interface DataStore (m : Type -> Type) where
- data Store : Access -> Type
-
- connect : ST m Var [add (Store LoggedOut)]
- disconnect : (store : Var) -> ST m () [remove store (Store LoggedOut)]
-
- readSecret : (store : Var) -> ST m String [store ::: Store LoggedIn]
- login : (store : Var) ->
- ST m LoginResult [store ::: Store LoggedOut :->
- (\\res => Store (case res of
- OK => LoggedIn
- BadPassword => LoggedOut))]
- logout : (store : Var) ->
- ST m () [store ::: Store LoggedIn :-> Store LoggedOut]
-
-getData : (ConsoleIO m, DataStore m) =>
- (failcount : Var) -> ST m () [failcount ::: State Integer]
-getData failcount
- = do st <- call connect
- OK <- login st
- | BadPassword => do putStrLn \"Failure\"
- fc <- read failcount
- write failcount (fc + 1)
- putStrLn (\"Number of failures: \" ++ show (fc
+ 1))
- disconnect st
- getData failcount
- secret <- readSecret st
- putStrLn (\"Secret is: \" ++ show secret)
- logout st
- disconnect st
- getData failcount
-
-getData2 : (ConsoleIO m, DataStore m) =>
- (st, failcount : Var) ->
- ST m () [st ::: Store {m} LoggedOut, failcount ::: State Integer]
-getData2 st failcount
- = do OK <- login st
- | BadPassword => do putStrLn \"Failure\"
- fc <- read failcount
- write failcount (fc + 1)
- putStrLn (\"Number of failures: \" ++ show (fc
+ 1))
- getData2 st failcount
- secret <- readSecret st
- putStrLn (\"Secret is: \" ++ show secret)
- logout st
- getData2 st failcount"
- (goto-char (point-max))
- (idris-backward-toplevel)
- (should (looking-at "getData2 st"))
- ;; (goto-char (point-max))
- (search-backward "Number")
- (idris-backward-toplevel)
- (should (looking-at "getData failcount"))
- (search-backward "LoggedIn")
- (idris-backward-toplevel)
- (should (looking-at "interface DataStore"))
- ))
-
-(ert-deftest idris-forward-toplevel-navigation-test-2pTac9 ()
- "Test idris-forard-toplevel navigation command."
- (idris-test-with-temp-buffer-point-min
- "interface DataStore (m : Type -> Type) where
- data Store : Access -> Type
-
- connect : ST m Var [add (Store LoggedOut)]
- disconnect : (store : Var) -> ST m () [remove store (Store LoggedOut)]
-
- readSecret : (store : Var) -> ST m String [store ::: Store LoggedIn]
- login : (store : Var) ->
- ST m LoginResult [store ::: Store LoggedOut :->
- (\\res => Store (case res of
- OK => LoggedIn
- BadPassword => LoggedOut))]
- logout : (store : Var) ->
- ST m () [store ::: Store LoggedIn :-> Store LoggedOut]
-
-getData : (ConsoleIO m, DataStore m) =>
- (failcount : Var) -> ST m () [failcount ::: State Integer]
-getData failcount
- = do st <- call connect
- OK <- login st
- | BadPassword => do putStrLn \"Failure\"
- fc <- read failcount
- write failcount (fc + 1)
- putStrLn (\"Number of failures: \" ++ show (fc
+ 1))
- disconnect st
- getData failcount
- secret <- readSecret st
- putStrLn (\"Secret is: \" ++ show secret)
- logout st
- disconnect st
- getData failcount
-
-getData2 : (ConsoleIO m, DataStore m) =>
- (st, failcount : Var) ->
- ST m () [st ::: Store {m} LoggedOut, failcount ::: State Integer]
-getData2 st failcount
- = do OK <- login st
- | BadPassword => do putStrLn \"Failure\"
- fc <- read failcount
- write failcount (fc + 1)
- putStrLn (\"Number of failures: \" ++ show (fc
+ 1))
- getData2 st failcount
- secret <- readSecret st
- putStrLn (\"Secret is: \" ++ show secret)
- logout st
- getData2 st failcount"
- (search-forward "DataStore")
- (idris-forward-toplevel)
- (should (empty-line-p))
- (skip-chars-backward " \t\r\n\f")
- (should (looking-back "Store LoggedOut]" (line-beginning-position)))
- (idris-forward-toplevel)
- (should (looking-at "getData failcount"))
- (idris-forward-toplevel)
- (should (empty-line-p))
- (skip-chars-backward " \t\r\n\f")
- (should (looking-back "getData failcount" (line-beginning-position)))
- ;; (goto-char (point-max))
- (search-forward "Number")
- (idris-forward-toplevel)
- (should (looking-back "getData2 st failcount" (line-beginning-position)))
- ))
-
-(ert-deftest idris-backard-statement-navigation-test-2pTac9 ()
- "Test idris-backard-statement navigation command."
- (idris-test-with-temp-buffer
- "interface DataStore (m : Type -> Type) where
- data Store : Access -> Type
-
- connect : ST m Var [add (Store LoggedOut)]
- disconnect : (store : Var) -> ST m () [remove store (Store LoggedOut)]
-
- readSecret : (store : Var) -> ST m String [store ::: Store LoggedIn]
- login : (store : Var) ->
- ST m LoginResult [store ::: Store LoggedOut :->
- (\\res => Store (case res of
- OK => LoggedIn
- BadPassword => LoggedOut))]
- logout : (store : Var) ->
- ST m () [store ::: Store LoggedIn :-> Store LoggedOut]
-
-getData : (ConsoleIO m, DataStore m) =>
- (failcount : Var) -> ST m () [failcount ::: State Integer]
-getData failcount
- = do st <- call connect
- OK <- login st
- | BadPassword => do putStrLn \"Failure\"
- fc <- read failcount
- write failcount (fc + 1)
- putStrLn (\"Number of failures: \" ++ show (fc
+ 1))
- disconnect st
- getData failcount
- secret <- readSecret st
- putStrLn (\"Secret is: \" ++ show secret)
- logout st
- disconnect st
- getData failcount
-
-getData2 : (ConsoleIO m, DataStore m) =>
- (st, failcount : Var) ->
- ST m () [st ::: Store {m} LoggedOut, failcount ::: State Integer]
-getData2 st failcount
- = do OK <- login st
- | BadPassword => do putStrLn \"Failure\"
- fc <- read failcount
- write failcount (fc + 1)
- putStrLn (\"Number of failures: \" ++ show (fc
+ 1))
- getData2 st failcount
- secret <- readSecret st
- putStrLn (\"Secret is: \" ++ show secret)
- logout st
- getData2 st failcount"
- (goto-char (point-max))
- (idris-backward-statement)
- (should (looking-at "getData2 st"))
- (search-backward "Number")
- (idris-backward-statement)
- (should (looking-at "putStrLn ("))
- (idris-backward-statement)
- (should (looking-at "write failcount"))
- (search-backward "BadPassword")
- (idris-backward-statement)
- (should (looking-at "| BadPassword"))
- (idris-backward-statement)
- (should (looking-at "= do OK"))
- (idris-backward-statement)
- (should (looking-at "getData2 st"))
- (idris-backward-statement)
- (should (looking-at "ST m ()"))
- ))
-
-(ert-deftest idris-forward-statement-navigation-test-2pTac9 ()
- "Test idris-forard-statement navigation command."
- (idris-test-with-temp-buffer-point-min
- "interface DataStore (m : Type -> Type) where
- data Store : Access -> Type
-
- connect : ST m Var [add (Store LoggedOut)]
- disconnect : (store : Var) -> ST m () [remove store (Store LoggedOut)]
-
- readSecret : (store : Var) -> ST m String [store ::: Store LoggedIn]
- login : (store : Var) ->
- ST m LoginResult [store ::: Store LoggedOut :->
- (\\res => Store (case res of
- OK => LoggedIn
- BadPassword => LoggedOut))]
- logout : (store : Var) ->
- ST m () [store ::: Store LoggedIn :-> Store LoggedOut]
-
-getData : (ConsoleIO m, DataStore m) =>
- (failcount : Var) -> ST m () [failcount ::: State Integer]
-getData failcount
- = do st <- call connect
- OK <- login st
- | BadPassword => do putStrLn \"Failure\"
- fc <- read failcount
- write failcount (fc + 1)
- putStrLn (\"Number of failures: \" ++ show (fc
+ 1))
- disconnect st
- getData failcount
- secret <- readSecret st
- putStrLn (\"Secret is: \" ++ show secret)
- logout st
- disconnect st
- getData failcount
-
-getData2 : (ConsoleIO m, DataStore m) =>
- (st, failcount : Var) ->
- ST m () [st ::: Store {m} LoggedOut, failcount ::: State Integer]
-getData2 st failcount
- = do OK <- login st
- | BadPassword => do putStrLn \"Failure\"
- fc <- read failcount
- write failcount (fc + 1)
- putStrLn (\"Number of failures: \" ++ show (fc
+ 1))
- getData2 st failcount
- secret <- readSecret st
- putStrLn (\"Secret is: \" ++ show secret)
- logout st
- getData2 st failcount"
- (search-forward "DataStore")
- (idris-forward-statement)
- (should (looking-back "where" (line-beginning-position)))
- (idris-forward-statement)
- (should (looking-back "Access -> Type" (line-beginning-position)))
- (idris-forward-statement)
- (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-tests3.el b/idris-tests3.el
deleted file mode 100644
index c03c790b91..0000000000
--- a/idris-tests3.el
+++ /dev/null
@@ -1,42 +0,0 @@
-(require 'idris-mode)
-(require 'idris-commands)
-(require 'inferior-idris)
-(require 'idris-ipkg-mode)
-(require 'cl-lib)
-(require 'idris-test-utils)
-
-
-
-;(idris-test-text-update-command "test-data/CaseSplit.idr" idris-case-split
'(lambda (x y) 'eq))
-(ert-deftest idris-test-idris-run ()
- (let ((buffer (find-file "test-data/Empty.idr")))
- (should buffer)
- (with-current-buffer buffer
- (idris-run)
- (dotimes (_ 5) (accept-process-output nil 0.1))
- (should idris-process)
- )
- (kill-buffer))
- (idris-quit))
-
-
-(ert-deftest idris-test-idris-connect-after-idris-run ()
- (let ((buffer (find-file "test-data/Empty.idr")))
- (with-current-buffer buffer
- (idris-load-file)
- (dotimes (_ 5) (accept-process-output nil 0.1))
- (should idris-connection)
- (kill-buffer)))
- (idris-quit))
-
-(idris-ert-command-action "test-data/CaseSplit.idr" idris-case-split
idris-test-eq-buffer)
-(idris-ert-command-action "test-data/MakeLemma.idr" idris-make-lemma
idris-test-eq-buffer)
-(idris-ert-command-action "test-data/GenerateDef.idr" idris-generate-def
idris-test-eq-buffer)
-(idris-ert-command-action2 "test-data/AddClause.idr"
- idris-add-clause
- idris-test-eq-buffer)
-
-
-(null nil)
-(provide 'idris-tests3)
-;;; idris-tests.el ends here
diff --git a/test/idris-commands-test.el b/test/idris-commands-test.el
new file mode 100644
index 0000000000..98a430f0f6
--- /dev/null
+++ b/test/idris-commands-test.el
@@ -0,0 +1,295 @@
+;;; idris-commands-test.el --- Tests for interactive commands
+
+;; Keywords: languages
+
+;; 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 <http://www.gnu.org/licenses/>.
+
+;;; Commentary:
+
+;; This is a collection of tests for interactive commands in idris-mode.
+
+;;; Code:
+
+(require 'idris-commands)
+(require 'idris-test-utils)
+
+(require 'ert)
+(require 'cl-lib)
+
+(defun normalised-buffer-list ()
+ "Buffer list without randomly appearing internal buffer(s)."
+ (cl-delete-if (lambda (b) (string-match-p "code-conversion-work"
(buffer-name b)))
+ (buffer-list)))
+
+(ert-deftest idris-test-idris-run ()
+ (let ((buffer (find-file "test-data/Empty.idr")))
+ (should buffer)
+ (with-current-buffer buffer
+ (idris-run)
+ (dotimes (_ 10) (accept-process-output nil 0.1))
+ (should idris-process)
+ (should idris-connection))
+ (idris-delete-ibc t)
+ (kill-buffer))
+ (idris-quit))
+
+(ert-deftest idris-test-idris-quit ()
+ "Ensure that running Idris and quitting doesn't leave behind unwanted
buffers."
+ (let ((before (normalised-buffer-list)))
+ (idris-repl)
+ (dotimes (_ 10) (accept-process-output nil 0.1))
+ (idris-quit)
+ (let* ((after (normalised-buffer-list))
+ (extra (cl-set-difference after before)))
+ (should (= (length extra) 0)))))
+
+(ert-deftest idris-test-idris-quit-logging-enabled ()
+ "Ensure that running Idris and quitting doesn't leave behind unwanted
buffers.
+In particular, only *idris-events* should remain."
+ (let ((before (normalised-buffer-list))
+ (idris-log-events t))
+
+ (idris-repl)
+ (dotimes (_ 10) (accept-process-output nil 0.1))
+ (idris-quit)
+ (let* ((after (normalised-buffer-list))
+ (extra (cl-set-difference after before)))
+ (should (= (length extra) 1))
+ (should (string= (buffer-name (car extra)) idris-event-buffer-name)))
+
+ ;; Cleanup
+ (kill-buffer idris-event-buffer-name)))
+
+(ert-deftest idris-load-file-idris-hole-show-on-load-enabled ()
+ "Test that the holes buffer is created."
+ (let ((buffer (find-file-noselect "test-data/MetavarTest.idr"))
+ (idris-hole-show-on-load t))
+ (with-current-buffer buffer
+ (idris-load-file)
+
+ ;; Allow async stuff to happen
+ (dotimes (_ 10) (accept-process-output nil 0.1))
+ (let ((mv-buffer (get-buffer idris-hole-list-buffer-name)))
+ ;; The buffer exists and contains characters
+ (should (bufferp mv-buffer))
+ (should (> (buffer-size mv-buffer) 10))
+ (kill-buffer mv-buffer))
+
+ ;; Clean up
+ (with-current-buffer buffer
+ (idris-delete-ibc t)
+ (kill-buffer))))
+
+ ;; More cleanup
+ (idris-quit))
+
+(ert-deftest idris-load-file-idris-hole-show-on-load-disabled ()
+ "Test that holes buffer is not created."
+ (let ((buffer (find-file-noselect "test-data/MetavarTest.idr"))
+ (idris-hole-show-on-load nil))
+ (with-current-buffer buffer
+ (idris-load-file))
+ (dotimes (_ 10) (accept-process-output nil 0.1))
+ (let ((mv-buffer (get-buffer idris-hole-list-buffer-name)))
+ (should-not (bufferp mv-buffer))
+ (should (null mv-buffer)))
+
+ ;; Clean up
+ (with-current-buffer buffer
+ (idris-delete-ibc t)
+ (kill-buffer)))
+
+ ;; More cleanup
+ (idris-quit))
+
+(ert-deftest idris-list-holes ()
+ "Test `idris-list-holes' command."
+ (let ((other-buffer (find-file-noselect "test-data/MakeWithBlock.idr"))
+ (buffer (find-file-noselect "test-data/MetavarTest.idr")))
+
+ ;; Test that hole info is present without need to load file manually
+ (with-current-buffer buffer
+ (idris-list-holes)
+ (dotimes (_ 10) (accept-process-output nil 0.1))
+ (let ((holes-buffer (get-buffer idris-hole-list-buffer-name)))
+ (should (bufferp holes-buffer))
+ (should (> (buffer-size holes-buffer) 10)))
+ (idris-delete-ibc t))
+
+ ;; Test that the hole info is updated for the other current buffer
+ (with-current-buffer other-buffer
+ (idris-list-holes)
+ (dotimes (_ 10) (accept-process-output nil 0.1))
+ (let ((holes-buffer (get-buffer idris-hole-list-buffer-name)))
+ (should (not (bufferp holes-buffer))))
+ (idris-delete-ibc t))
+
+ (kill-buffer buffer)
+ (kill-buffer other-buffer)
+ (idris-quit)))
+
+(when (string-match-p "idris$" idris-interpreter-path)
+ (ert-deftest idris-test-proof-search ()
+ "Test that proof search works."
+ :expected-result (if (string-match-p "idris2$" idris-interpreter-path)
+ :failed
+ :passed)
+ (skip-unless (string-match-p "idris$" idris-interpreter-path))
+
+ (let ((buffer (find-file "test-data/ProofSearch.idr")))
+ (with-current-buffer buffer
+ (idris-load-file)
+ (dotimes (_ 10) (accept-process-output nil 0.1))
+ (goto-char (point-min))
+ (re-search-forward "search_here")
+ (goto-char (match-beginning 0))
+ (idris-proof-search)
+ (dotimes (_ 10) (accept-process-output nil 0.1))
+ (should (looking-at-p "lteSucc (lteSucc (lteSucc (lteSucc (lteSucc
lteZero))))"))
+ (move-beginning-of-line nil)
+ (delete-region (point) (line-end-position))
+ (insert "prf = ?search_here")
+ (save-buffer)
+ (idris-delete-ibc t)
+ (kill-buffer)))
+
+ ;; More cleanup
+ (idris-quit)))
+
+(ert-deftest idris-test-idris-type-search ()
+ "Test that `idris-type-search' produces output in Idris info buffer."
+ (idris-run)
+ (funcall-interactively 'idris-type-search "Nat")
+ (with-current-buffer (get-buffer idris-info-buffer-name)
+ (goto-char (point-min))
+ (should (re-search-forward "Zero" nil t)))
+ (idris-quit))
+
+(ert-deftest idris-test-idris-add-clause ()
+ "Test that `idris-add-clause' generates definition with hole."
+ (let ((buffer (find-file-noselect "test-data/AddClause.idr"))
+ (buffer-content (with-temp-buffer
+ (insert-file-contents "test-data/AddClause.idr")
+ (buffer-string))))
+ (with-current-buffer buffer
+ (goto-char (point-min))
+ (re-search-forward "test :")
+ (goto-char (match-beginning 0))
+ (funcall-interactively 'idris-add-clause nil)
+ (should (looking-at-p "test \\w+ = \\?test_rhs"))
+ (idris-delete-ibc t)
+
+ (re-search-forward "(-) :")
+ (goto-char (1+ (match-beginning 0)))
+ (funcall-interactively 'idris-add-clause nil)
+ (should (looking-at-p "(-) = \\?\\w+_rhs"))
+ (idris-delete-ibc t)
+
+ ;; Test that response with indentation (Idris2) are aligned correctly
+ ;; Idris1 response: "revAcc xs ys = ?revAcc_rhs"
+ ;; Idris2 response: " revAcc xs ys = ?revAcc_rhs"
+ (goto-char (point-max))
+ (insert "
+myReverse : List a -> List a
+myReverse xs = revAcc [] xs where
+ revAcc : List a -> List a -> List a")
+ (search-backward "evAcc")
+ (funcall-interactively 'idris-add-clause nil)
+ (beginning-of-line)
+ (should (looking-at-p "^ revAcc xs ys = \\?revAcc_rhs"))
+
+ ;; Cleanup
+ (erase-buffer)
+ (insert buffer-content)
+ (save-buffer)
+ (kill-buffer))
+ (idris-quit)))
+
+(ert-deftest idris-test-idris-refine ()
+ "Test that `idris-refine' works as expected."
+ (let* ((buffer (find-file "test-data/Refine.idr"))
+ (buffer-content (buffer-substring-no-properties (point-min)
(point-max))))
+ (goto-char (point-min))
+ (search-forward "test : T")
+ (beginning-of-line)
+ (funcall-interactively 'idris-add-clause nil)
+ (should (looking-at-p "test \\w+ = \\?test_rhs"))
+ (idris-delete-ibc t)
+ (search-forward "?test")
+ (funcall-interactively 'idris-refine "x")
+ (should (looking-at-p
+ (if (>=-protocol-version 2 1)
+ "x"
+ "?test_rhs1")))
+
+ ;; Cleanup
+ (idris-delete-ibc t)
+ (erase-buffer)
+ (insert buffer-content)
+ (save-buffer)
+ (kill-buffer)
+ (idris-quit)))
+
+(ert-deftest idris-test-idris-type-at-point ()
+ "Test that `idris-type-at-point' works."
+ (let ((buffer (find-file-noselect "test-data/AddClause.idr"))
+ file-loaded-p
+ eval-args)
+ (cl-flet ((idris-load-file-sync-stub () (setq file-loaded-p t) nil)
+ (idris-eval-stub (&optional &rest args)
+ (setq eval-args args)
+ '("Test : Type"
+ (0 4 ((:name "AddClause.Test")
+ (:implicit :False)
+ (:key "AQAAAAAAAAAA")
+ (:decor :type)
+ (:doc-overview "")
+ (:type "Type")
+ (:namespace "AddClause")))
+ (7 4 ((:decor :type)
+ (:type "Type")
+ (:doc-overview "The type of types")
+ (:name "Type")))
+ (7 4 ((:tt-term "AAAAAAAAAAAHAAAAAAA"))))))
+ (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
+ (switch-to-buffer buffer)
+ (goto-char (point-min))
+ (re-search-forward "data Test")
+ (funcall-interactively 'idris-type-at-point nil)
+ (should (eq file-loaded-p t))
+ (should (equal eval-args '((:type-of "Test"))))
+ (should (string= (buffer-name) idris-info-buffer-name))
+ (should (string-match-p "Test : Type"
(buffer-substring-no-properties (point-min) (point-max))))
+ (idris-info-quit)
+ (should (eq (current-buffer) buffer)))
+
+ (advice-remove 'idris-load-file-sync #'idris-load-file-sync-stub)
+ (advice-remove 'idris-eval #'idris-eval-stub)
+ (kill-buffer buffer)
+ (idris-quit)))))
+
+;; 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)
+(idris-ert-command-action "test-data/MakeLemma.idr" idris-make-lemma
idris-test-eq-buffer)
+(when (string-match-p "idris2$" idris-interpreter-path)
+ (idris-ert-command-action "test-data/GenerateDef.idr" idris-generate-def
idris-test-eq-buffer))
+(idris-ert-command-action2 "test-data/AddClause.idr" idris-add-clause
idris-test-eq-buffer)
+
+(provide 'idris-commands-test)
+;;; idris-commands-test.el ends here
diff --git a/test/idris-navigate-test.el b/test/idris-navigate-test.el
new file mode 100644
index 0000000000..5e469d4a14
--- /dev/null
+++ b/test/idris-navigate-test.el
@@ -0,0 +1,265 @@
+;;; idris-navigate-test.el --- Tests for idris-navigate
+
+(require 'idris-mode)
+(require 'idris-navigate)
+
+(require 'ert)
+(require 'idris-test-utils)
+
+;;; Code:
+
+(ert-deftest idris-backard-toplevel-navigation-test-2pTac9 ()
+ "Test idris-backard-toplevel navigation command."
+ (idris-test-with-temp-buffer
+ "interface DataStore (m : Type -> Type) where
+ data Store : Access -> Type
+
+ connect : ST m Var [add (Store LoggedOut)]
+ disconnect : (store : Var) -> ST m () [remove store (Store LoggedOut)]
+
+ readSecret : (store : Var) -> ST m String [store ::: Store LoggedIn]
+ login : (store : Var) ->
+ ST m LoginResult [store ::: Store LoggedOut :->
+ (\\res => Store (case res of
+ OK => LoggedIn
+ BadPassword => LoggedOut))]
+ logout : (store : Var) ->
+ ST m () [store ::: Store LoggedIn :-> Store LoggedOut]
+
+getData : (ConsoleIO m, DataStore m) =>
+ (failcount : Var) -> ST m () [failcount ::: State Integer]
+getData failcount
+ = do st <- call connect
+ OK <- login st
+ | BadPassword => do putStrLn \"Failure\"
+ fc <- read failcount
+ write failcount (fc + 1)
+ putStrLn (\"Number of failures: \" ++ show (fc
+ 1))
+ disconnect st
+ getData failcount
+ secret <- readSecret st
+ putStrLn (\"Secret is: \" ++ show secret)
+ logout st
+ disconnect st
+ getData failcount
+
+getData2 : (ConsoleIO m, DataStore m) =>
+ (st, failcount : Var) ->
+ ST m () [st ::: Store {m} LoggedOut, failcount ::: State Integer]
+getData2 st failcount
+ = do OK <- login st
+ | BadPassword => do putStrLn \"Failure\"
+ fc <- read failcount
+ write failcount (fc + 1)
+ putStrLn (\"Number of failures: \" ++ show (fc
+ 1))
+ getData2 st failcount
+ secret <- readSecret st
+ putStrLn (\"Secret is: \" ++ show secret)
+ logout st
+ getData2 st failcount"
+ (goto-char (point-max))
+ (idris-backward-toplevel)
+ (should (looking-at "getData2 st"))
+ ;; (goto-char (point-max))
+ (search-backward "Number")
+ (idris-backward-toplevel)
+ (should (looking-at "getData failcount"))
+ (search-backward "LoggedIn")
+ (idris-backward-toplevel)
+ (should (looking-at "interface DataStore"))
+ ))
+
+(ert-deftest idris-forward-toplevel-navigation-test-2pTac9 ()
+ "Test idris-forard-toplevel navigation command."
+ (idris-test-with-temp-buffer-point-min
+ "interface DataStore (m : Type -> Type) where
+ data Store : Access -> Type
+
+ connect : ST m Var [add (Store LoggedOut)]
+ disconnect : (store : Var) -> ST m () [remove store (Store LoggedOut)]
+
+ readSecret : (store : Var) -> ST m String [store ::: Store LoggedIn]
+ login : (store : Var) ->
+ ST m LoginResult [store ::: Store LoggedOut :->
+ (\\res => Store (case res of
+ OK => LoggedIn
+ BadPassword => LoggedOut))]
+ logout : (store : Var) ->
+ ST m () [store ::: Store LoggedIn :-> Store LoggedOut]
+
+getData : (ConsoleIO m, DataStore m) =>
+ (failcount : Var) -> ST m () [failcount ::: State Integer]
+getData failcount
+ = do st <- call connect
+ OK <- login st
+ | BadPassword => do putStrLn \"Failure\"
+ fc <- read failcount
+ write failcount (fc + 1)
+ putStrLn (\"Number of failures: \" ++ show (fc
+ 1))
+ disconnect st
+ getData failcount
+ secret <- readSecret st
+ putStrLn (\"Secret is: \" ++ show secret)
+ logout st
+ disconnect st
+ getData failcount
+
+getData2 : (ConsoleIO m, DataStore m) =>
+ (st, failcount : Var) ->
+ ST m () [st ::: Store {m} LoggedOut, failcount ::: State Integer]
+getData2 st failcount
+ = do OK <- login st
+ | BadPassword => do putStrLn \"Failure\"
+ fc <- read failcount
+ write failcount (fc + 1)
+ putStrLn (\"Number of failures: \" ++ show (fc
+ 1))
+ getData2 st failcount
+ secret <- readSecret st
+ putStrLn (\"Secret is: \" ++ show secret)
+ logout st
+ getData2 st failcount"
+ (search-forward "DataStore")
+ (idris-forward-toplevel)
+ (should (empty-line-p))
+ (skip-chars-backward " \t\r\n\f")
+ (should (looking-back "Store LoggedOut]" (line-beginning-position)))
+ (idris-forward-toplevel)
+ (should (looking-at "getData failcount"))
+ (idris-forward-toplevel)
+ (should (empty-line-p))
+ (skip-chars-backward " \t\r\n\f")
+ (should (looking-back "getData failcount" (line-beginning-position)))
+ ;; (goto-char (point-max))
+ (search-forward "Number")
+ (idris-forward-toplevel)
+ (should (looking-back "getData2 st failcount" (line-beginning-position)))
+ ))
+
+(ert-deftest idris-backard-statement-navigation-test-2pTac9 ()
+ "Test idris-backard-statement navigation command."
+ (idris-test-with-temp-buffer
+ "interface DataStore (m : Type -> Type) where
+ data Store : Access -> Type
+
+ connect : ST m Var [add (Store LoggedOut)]
+ disconnect : (store : Var) -> ST m () [remove store (Store LoggedOut)]
+
+ readSecret : (store : Var) -> ST m String [store ::: Store LoggedIn]
+ login : (store : Var) ->
+ ST m LoginResult [store ::: Store LoggedOut :->
+ (\\res => Store (case res of
+ OK => LoggedIn
+ BadPassword => LoggedOut))]
+ logout : (store : Var) ->
+ ST m () [store ::: Store LoggedIn :-> Store LoggedOut]
+
+getData : (ConsoleIO m, DataStore m) =>
+ (failcount : Var) -> ST m () [failcount ::: State Integer]
+getData failcount
+ = do st <- call connect
+ OK <- login st
+ | BadPassword => do putStrLn \"Failure\"
+ fc <- read failcount
+ write failcount (fc + 1)
+ putStrLn (\"Number of failures: \" ++ show (fc
+ 1))
+ disconnect st
+ getData failcount
+ secret <- readSecret st
+ putStrLn (\"Secret is: \" ++ show secret)
+ logout st
+ disconnect st
+ getData failcount
+
+getData2 : (ConsoleIO m, DataStore m) =>
+ (st, failcount : Var) ->
+ ST m () [st ::: Store {m} LoggedOut, failcount ::: State Integer]
+getData2 st failcount
+ = do OK <- login st
+ | BadPassword => do putStrLn \"Failure\"
+ fc <- read failcount
+ write failcount (fc + 1)
+ putStrLn (\"Number of failures: \" ++ show (fc
+ 1))
+ getData2 st failcount
+ secret <- readSecret st
+ putStrLn (\"Secret is: \" ++ show secret)
+ logout st
+ getData2 st failcount"
+ (goto-char (point-max))
+ (idris-backward-statement)
+ (should (looking-at "getData2 st"))
+ (search-backward "Number")
+ (idris-backward-statement)
+ (should (looking-at "putStrLn ("))
+ (idris-backward-statement)
+ (should (looking-at "write failcount"))
+ (search-backward "BadPassword")
+ (idris-backward-statement)
+ (should (looking-at "| BadPassword"))
+ (idris-backward-statement)
+ (should (looking-at "= do OK"))
+ (idris-backward-statement)
+ (should (looking-at "getData2 st"))
+ (idris-backward-statement)
+ (should (looking-at "ST m ()"))
+ ))
+
+(ert-deftest idris-forward-statement-navigation-test-2pTac9 ()
+ "Test idris-forard-statement navigation command."
+ (idris-test-with-temp-buffer-point-min
+ "interface DataStore (m : Type -> Type) where
+ data Store : Access -> Type
+
+ connect : ST m Var [add (Store LoggedOut)]
+ disconnect : (store : Var) -> ST m () [remove store (Store LoggedOut)]
+
+ readSecret : (store : Var) -> ST m String [store ::: Store LoggedIn]
+ login : (store : Var) ->
+ ST m LoginResult [store ::: Store LoggedOut :->
+ (\\res => Store (case res of
+ OK => LoggedIn
+ BadPassword => LoggedOut))]
+ logout : (store : Var) ->
+ ST m () [store ::: Store LoggedIn :-> Store LoggedOut]
+
+getData : (ConsoleIO m, DataStore m) =>
+ (failcount : Var) -> ST m () [failcount ::: State Integer]
+getData failcount
+ = do st <- call connect
+ OK <- login st
+ | BadPassword => do putStrLn \"Failure\"
+ fc <- read failcount
+ write failcount (fc + 1)
+ putStrLn (\"Number of failures: \" ++ show (fc
+ 1))
+ disconnect st
+ getData failcount
+ secret <- readSecret st
+ putStrLn (\"Secret is: \" ++ show secret)
+ logout st
+ disconnect st
+ getData failcount
+
+getData2 : (ConsoleIO m, DataStore m) =>
+ (st, failcount : Var) ->
+ ST m () [st ::: Store {m} LoggedOut, failcount ::: State Integer]
+getData2 st failcount
+ = do OK <- login st
+ | BadPassword => do putStrLn \"Failure\"
+ fc <- read failcount
+ write failcount (fc + 1)
+ putStrLn (\"Number of failures: \" ++ show (fc
+ 1))
+ getData2 st failcount
+ secret <- readSecret st
+ putStrLn (\"Secret is: \" ++ show secret)
+ logout st
+ getData2 st failcount"
+ (search-forward "DataStore")
+ (idris-forward-statement)
+ (should (looking-back "where" (line-beginning-position)))
+ (idris-forward-statement)
+ (should (looking-back "Access -> Type" (line-beginning-position)))
+ (idris-forward-statement)
+ (should (looking-back "Store LoggedOut)]" (line-beginning-position)))
+ ))
+
+(provide 'idris-navigate-test)
+;;; idris-navigate-test.el ends here
diff --git a/idris-test-utils.el b/test/idris-test-utils.el
similarity index 91%
rename from idris-test-utils.el
rename to test/idris-test-utils.el
index 564314babb..4c3d8fc19b 100644
--- a/idris-test-utils.el
+++ b/test/idris-test-utils.el
@@ -1,4 +1,4 @@
-;;; idris-tests.el --- Tests utilty for idris-mode -*- lexical-binding: t -*-
+;;; idris-test-utils.el --- Tests utility for idris-mode -*- lexical-binding:
t -*-
;; Copyright (C) 2021 Yasuhiko Watanabe
@@ -20,11 +20,10 @@
;;; Commentary:
-;; This is a collection of simple tests for idris-mode.
+;; This is a collection of utilities used in tests for idris-mode.
;;; Code:
-(require 'cl-lib)
-(require 'idris-mode)
+(require 'subr-x)
(defun idris-test-run-goto-char (test-fun &rest args)
"To run commands like idris-case-split, we have to move the cursor to an
appropriate location.
@@ -42,8 +41,10 @@ test var = ?cases_rhs
(progn
(goto-char (point-min))
(search-forward-regexp "^--.*\\+")
- (goto-char (- (point) 1))
- (next-line)
+ (goto-char (1- (point)))
+ (let ((col (current-column)))
+ (forward-line)
+ (move-to-column col))
(apply test-fun args)
))
@@ -60,10 +61,11 @@ As this is not for a test of Idris itself, we do not care
the results."
(let ((buffer (find-file ,test-case)))
(with-current-buffer buffer
(idris-load-file)
- (dotimes (_ 5) (accept-process-output nil 0.1)) ;;
+ (dotimes (_ 10) (accept-process-output nil 0.1)) ;;
(idris-test-run-goto-char (function ,test-fun))
(let ((this-buffer (current-buffer)))
(should (,buffer-p buffer this-buffer))))
+ (idris-delete-ibc t)
(kill-buffer))
(idris-quit)))
@@ -78,7 +80,7 @@ As this is not for a test of Idris itself, we do not care the
results."
(let ((buffer (find-file ,test-case)))
(with-current-buffer buffer
(idris-load-file)
- (dotimes (_ 5) (accept-process-output nil 0.1)) ;;
+ (dotimes (_ 10) (accept-process-output nil 0.1)) ;;
(idris-test-run-goto-char (function ,test-fun) nil)
(let ((this-buffer (current-buffer)))
(should (,buffer-p buffer this-buffer))))
diff --git a/test/idris-tests.el b/test/idris-tests.el
new file mode 100644
index 0000000000..ce243e8c13
--- /dev/null
+++ b/test/idris-tests.el
@@ -0,0 +1,142 @@
+;;; idris-tests.el --- Tests for idris-mode -*- lexical-binding: t -*-
+
+;; Copyright (C) 2014 David Raymond Christiansen
+
+;; Author: David Raymond Christiansen <d...@itu.dk>
+;; Keywords: languages
+
+;; 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 <http://www.gnu.org/licenses/>.
+
+;;; Commentary:
+
+;; This is a collection of simple tests for idris-mode.
+;; Structuring:
+;; Packages modules (files) have their own corresponding test files.
+;; idris-commands.el -> idris-commands-test.el
+;; idris-navigate.el -> idris-navigate-test.el
+;; ..
+;; Tests for modules that are too small or not yet covered enough by tests
+;; can be left as part of the idris-tests.el
+;;
+;; Naming tests:
+;; `ert-deftest idris-X-Y`
+;; where X stands for function or state to be tested
+;; and Y for additional context or behaviour.
+;; Example:
+;; `ert-deftest idris-quit`
+;; `ert-deftest idris-quit-logging-enabled`
+
+;;; Code:
+
+;; Implementations
+(require 'idris-mode)
+
+;; Testing
+;; load-file-name is present in batch mode and buffer-file-name in interactive
+(let ((test-dir (file-name-directory (or load-file-name (buffer-file-name)))))
+ (add-to-list 'load-path test-dir)
+ ;; In batch mode default dir points to ../ and causing issues with saving
+ ;; Idris fixtures so we set it to the test-dir to avoid the issues.
+ (setq default-directory test-dir))
+
+(require 'ert)
+(require 'seq)
+
+(ert-deftest trivial-test ()
+ (should t))
+
+(ert-deftest idris-editor-port ()
+ (let ((output "Can't find import Prelude\n37072\n"))
+ (should (string-match idris-process-port-output-regexp output))
+ (should (string= "Can't find import Prelude\n" (match-string 1 output)))
+ (should (string= "37072" (match-string 2 output))))
+ (let ((output "37072\n"))
+ (should (string-match idris-process-port-output-regexp output))
+ (should (null (match-string 1 output)))
+ (should (string= "37072" (match-string 2 output)))))
+
+(ert-deftest idris-test-find-cmdline-args ()
+ "Test that idris-mode calculates command line arguments from .ipkg files."
+ ;; Outside of a project, none are found
+ (let ((buffer (find-file "test-data/ProofSearch.idr")))
+ (with-current-buffer buffer
+ (should (null (idris-ipkg-flags-for-current-buffer)))
+ (kill-buffer)))
+ ;; Inside of a project, the correct ones are found
+ (let ((buffer (find-file "test-data/cmdline/src/Command/Line/Test.idr")))
+ (with-current-buffer buffer
+ (should (equal (idris-ipkg-flags-for-current-buffer)
+ (list "-p" "effects")))
+ (kill-buffer))))
+
+(ert-deftest idris-test-error-buffer ()
+ "Test that loading a type-incorrect Idris buffer results in an error message
buffer."
+ (let ((buffer (find-file "test-data/TypeError.idr")))
+ (with-current-buffer buffer
+ (idris-load-file)
+ (dotimes (_ 10) (accept-process-output nil 0.1))
+ (should (get-buffer idris-notes-buffer-name)))
+ (with-current-buffer (get-buffer idris-notes-buffer-name)
+ (goto-char (point-min))
+ (should (re-search-forward "Nat" nil t))) ;; check that the buffer has
something error-like
+ (with-current-buffer buffer
+ (kill-buffer))
+ (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."
+ (let ((buffer (find-file "test-data/package-test/Packaging.idr")))
+ (with-current-buffer buffer
+ (should (equal '("-p" "idris-free" "-p" "recursion_schemes")
+ (idris-ipkg-pkgs-flags-for-current-buffer)))
+ (kill-buffer buffer))
+ (idris-quit)))
+
+(ert-deftest idris-test-warning-overlay ()
+ "Test that `idris-warning-overaly-point' works as expected."
+ (let* ((buffer (find-file-noselect "test-data/AddClause.idr"))
+ (warning '("AddClause.idr" (5 7) (5 17) "Some warning message" ()))
+ (idris-raw-warnings '())
+ (idris-process-current-working-directory (file-name-directory
(buffer-file-name buffer)))
+ (expected-position)
+ (expected-overlay))
+ (with-current-buffer buffer
+ (goto-char (point-min))
+ (re-search-forward "data Test")
+ (setq expected-position (point))
+
+ (idris-warning-overlay warning)
+
+ ;; Assert that the point position does not change
+ ;; https://github.com/idris-community/idris2-mode/issues/36
+ (should (eq (point) expected-position))
+
+ ;; Assert side effect
+ (should (not (null idris-raw-warnings)))
+
+ ;; Assert that overlay was added
+ (setq expected-overlay (car (overlays-in (point-min) (point-max))))
+ (should (not (null expected-overlay)))
+ (should (string= (overlay-get expected-overlay 'help-echo)
+ "Some warning message"))
+ ;; Cleanup
+ (idris-delete-ibc t)
+ (kill-buffer))))
+
+(load "idris-commands-test")
+(load "idris-navigate-test")
+(load "idris-xref-test")
+
+(provide 'idris-tests)
+;;; idris-tests.el ends here
diff --git a/idris-xref-test.el b/test/idris-xref-test.el
similarity index 100%
rename from idris-xref-test.el
rename to test/idris-xref-test.el
diff --git a/test-data/AddClause.idr b/test/test-data/AddClause.idr
similarity index 100%
rename from test-data/AddClause.idr
rename to test/test-data/AddClause.idr
diff --git a/test-data/AddMissing.idr b/test/test-data/AddMissing.idr
similarity index 100%
rename from test-data/AddMissing.idr
rename to test/test-data/AddMissing.idr
diff --git a/test-data/CaseSplit.idr b/test/test-data/CaseSplit.idr
similarity index 100%
rename from test-data/CaseSplit.idr
rename to test/test-data/CaseSplit.idr
diff --git a/test/test-data/Empty.idr b/test/test-data/Empty.idr
new file mode 100644
index 0000000000..e69de29bb2
diff --git a/test-data/GenerateDef.idr b/test/test-data/GenerateDef.idr
similarity index 100%
rename from test-data/GenerateDef.idr
rename to test/test-data/GenerateDef.idr
diff --git a/test-data/MakeLemma.idr b/test/test-data/MakeLemma.idr
similarity index 100%
rename from test-data/MakeLemma.idr
rename to test/test-data/MakeLemma.idr
diff --git a/test-data/MakeWithBlock.idr b/test/test-data/MakeWithBlock.idr
similarity index 100%
rename from test-data/MakeWithBlock.idr
rename to test/test-data/MakeWithBlock.idr
diff --git a/test-data/MetavarTest.idr b/test/test-data/MetavarTest.idr
similarity index 100%
rename from test-data/MetavarTest.idr
rename to test/test-data/MetavarTest.idr
diff --git a/test-data/ProofSearch.idr b/test/test-data/ProofSearch.idr
similarity index 100%
rename from test-data/ProofSearch.idr
rename to test/test-data/ProofSearch.idr
diff --git a/test-data/Refine.idr b/test/test-data/Refine.idr
similarity index 100%
rename from test-data/Refine.idr
rename to test/test-data/Refine.idr
diff --git a/test-data/TypeAtPoint.idr b/test/test-data/TypeAtPoint.idr
similarity index 100%
rename from test-data/TypeAtPoint.idr
rename to test/test-data/TypeAtPoint.idr
diff --git a/test-data/TypeError.idr b/test/test-data/TypeError.idr
similarity index 100%
rename from test-data/TypeError.idr
rename to test/test-data/TypeError.idr
diff --git a/test-data/cmdline/commandlinetest.ipkg
b/test/test-data/cmdline/commandlinetest.ipkg
similarity index 100%
rename from test-data/cmdline/commandlinetest.ipkg
rename to test/test-data/cmdline/commandlinetest.ipkg
diff --git a/test-data/cmdline/src/Command/Line/Test.idr
b/test/test-data/cmdline/src/Command/Line/Test.idr
similarity index 100%
rename from test-data/cmdline/src/Command/Line/Test.idr
rename to test/test-data/cmdline/src/Command/Line/Test.idr
diff --git a/test-data/package-test/Packaging.idr
b/test/test-data/package-test/Packaging.idr
similarity index 100%
rename from test-data/package-test/Packaging.idr
rename to test/test-data/package-test/Packaging.idr
diff --git a/test-data/package-test/test.ipkg
b/test/test-data/package-test/test.ipkg
similarity index 100%
rename from test-data/package-test/test.ipkg
rename to test/test-data/package-test/test.ipkg
