[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[nongnu] elpa/idris-mode ee551230ed 7/9: Merge pull request #579 from ke
|
From: |
ELPA Syncer |
|
Subject: |
[nongnu] elpa/idris-mode ee551230ed 7/9: Merge pull request #579 from keram/tests-impro |
|
Date: |
Tue, 6 Dec 2022 05:59:06 -0500 (EST) |
branch: elpa/idris-mode
commit ee551230edafadee519fba9edf15fcd82ea339f7
Merge: 0cae4b8086 d0d609bff7
Author: Jan de Muijnck-Hughes <jfdm@users.noreply.github.com>
Commit: GitHub <noreply@github.com>
Merge pull request #579 from keram/tests-impro
Tests improvements
---
idris-navigate.el | 292 ----------------------------------------------------
idris-test-utils.el | 67 +++++++++---
idris-tests.el | 276 +++++++++++++++++++++++++++++++++++++++++++++++--
3 files changed, 319 insertions(+), 316 deletions(-)
diff --git a/idris-navigate.el b/idris-navigate.el
index 13ea74a068..ae44090043 100644
--- a/idris-navigate.el
+++ b/idris-navigate.el
@@ -891,297 +891,5 @@ If no error, customize `idris-max-specpdl-size'"))
(and idris-verbose-p (interactive-p) (message "%s" erg)))
erg)))
-(defmacro idris-test-with-temp-buffer-point-min (contents &rest body)
- "Create temp buffer in `idris-mode' inserting CONTENTS.
-BODY is code to be executed within the temp buffer. Point is
- at the beginning of buffer."
- (declare (indent 1) (debug t))
- `(with-temp-buffer
- ;; requires idris.el
- ;; (and (featurep 'semantic) (unload-feature 'semantic))
- ;; (and (featurep 'idris) (unload-feature 'idris))
- (let (hs-minor-mode)
- (insert ,contents)
- (idris-mode)
- (goto-char (point-min))
- ;; (message "(current-buffer): %s" (current-buffer))
- (when idris-debug-p (switch-to-buffer (current-buffer))
- ;; (font-lock-fontify-buffer)
- (font-lock-ensure)
- )
- ,@body)
- (sit-for 0.1)))
-
-(defmacro idris-test-with-temp-buffer (contents &rest body)
- "Create temp buffer in `idris-mode' inserting CONTENTS.
-BODY is code to be executed within the temp buffer. Point is
- at the end of buffer."
- (declare (indent 1) (debug t))
- `(with-temp-buffer
- ;; (and (featurep 'idris) (unload-feature 'idris))
- (let (hs-minor-mode)
- (insert ,contents)
- (idris-mode)
- (when idris-debug-p (switch-to-buffer (current-buffer))
- ;; (font-lock-fontify-buffer)
- (font-lock-ensure)
- )
- ;; (message "ERT %s" (point))
- ,@body)
- (sit-for 0.1)))
-
-(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)
;;; idris-navigate.el ends here
diff --git a/idris-test-utils.el b/idris-test-utils.el
index 5bce9536b2..564314babb 100644
--- a/idris-test-utils.el
+++ b/idris-test-utils.el
@@ -56,15 +56,15 @@ It is used for the command
- otherwise test failure
As this is not for a test of Idris itself, we do not care the results."
`(ert-deftest ,(intern (concat (symbol-name test-fun) "/"
(string-remove-suffix ".idr" test-case))) ()
-
+
(let ((buffer (find-file ,test-case)))
(with-current-buffer buffer
- (idris-load-file)
- (dotimes (_ 5) (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))))
- (kill-buffer))
+ (idris-load-file)
+ (dotimes (_ 5) (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))))
+ (kill-buffer))
(idris-quit)))
(defmacro idris-ert-command-action2 (test-case test-fun buffer-p)
@@ -74,15 +74,15 @@ It is used for the command
- otherwise test failure
As this is not for a test of Idris itself, we do not care the results."
`(ert-deftest ,(intern (concat (symbol-name test-fun) "/"
(string-remove-suffix ".idr" test-case))) ()
-
+
(let ((buffer (find-file ,test-case)))
(with-current-buffer buffer
- (idris-load-file)
- (dotimes (_ 5) (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))))
- (kill-buffer))
+ (idris-load-file)
+ (dotimes (_ 5) (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))))
+ (kill-buffer))
(idris-quit)))
@@ -92,5 +92,44 @@ As this is not for a test of Idris itself, we do not care
the results."
(defmacro check-rest (&rest args)
`(listp (quote ,args)))
+(defmacro idris-test-with-temp-buffer-point-min (contents &rest body)
+ "Create temp buffer in `idris-mode' inserting CONTENTS.
+BODY is code to be executed within the temp buffer. Point is
+ at the beginning of buffer."
+ (declare (indent 1) (debug t))
+ `(with-temp-buffer
+ ;; requires idris.el
+ ;; (and (featurep 'semantic) (unload-feature 'semantic))
+ ;; (and (featurep 'idris) (unload-feature 'idris))
+ (let (hs-minor-mode)
+ (insert ,contents)
+ (idris-mode)
+ (goto-char (point-min))
+ ;; (message "(current-buffer): %s" (current-buffer))
+ (when idris-debug-p (switch-to-buffer (current-buffer))
+ ;; (font-lock-fontify-buffer)
+ (font-lock-ensure)
+ )
+ ,@body)
+ (sit-for 0.1)))
+
+(defmacro idris-test-with-temp-buffer (contents &rest body)
+ "Create temp buffer in `idris-mode' inserting CONTENTS.
+BODY is code to be executed within the temp buffer. Point is
+ at the end of buffer."
+ (declare (indent 1) (debug t))
+ `(with-temp-buffer
+ ;; (and (featurep 'idris) (unload-feature 'idris))
+ (let (hs-minor-mode)
+ (insert ,contents)
+ (idris-mode)
+ (when idris-debug-p (switch-to-buffer (current-buffer))
+ ;; (font-lock-fontify-buffer)
+ (font-lock-ensure)
+ )
+ ;; (message "ERT %s" (point))
+ ,@body)
+ (sit-for 0.1)))
+
(provide 'idris-test-utils)
;;; idris-test-utils.el ends here
diff --git a/idris-tests.el b/idris-tests.el
index c841472604..a042a5d61d 100644
--- a/idris-tests.el
+++ b/idris-tests.el
@@ -25,9 +25,11 @@
;;; 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 ()
@@ -159,14 +161,12 @@ remain."
(ert-deftest idris-test-idris-type-search ()
"Test that `idris-type-search' produces output in Idris info buffer."
- (let ((buffer (find-file "test-data/AddClause.idr")))
- (with-current-buffer buffer
- (idris-load-file)
- (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)))
+ (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."
@@ -189,16 +189,272 @@ remain."
(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"))
+
;; Cleanup
(erase-buffer)
(insert buffer-content)
(save-buffer)
- (kill-buffer)))
- (idris-quit))
+ (kill-buffer))
+ (idris-quit)))
+
+(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-tests)
;;; idris-tests.el ends here
- [nongnu] elpa/idris-mode updated (0cae4b8086 -> 4a36953e76), ELPA Syncer, 2022/12/06
- [nongnu] elpa/idris-mode 6fbd9cff31 6/9: Improve `idris-switch-working-directory` by, ELPA Syncer, 2022/12/06
- [nongnu] elpa/idris-mode 4a36953e76 9/9: Merge pull request #580 from keram/load-file-switch-dir-idris2, ELPA Syncer, 2022/12/06
- [nongnu] elpa/idris-mode ee551230ed 7/9: Merge pull request #579 from keram/tests-impro,
ELPA Syncer <=
- [nongnu] elpa/idris-mode 71ab6a35e3 5/9: [semantic-highlight] Remove and rebuild overlays in file on reload only in changed area, ELPA Syncer, 2022/12/06
- [nongnu] elpa/idris-mode 7ebd8e721b 8/9: Merge pull request #581 from keram/highlight-partial, ELPA Syncer, 2022/12/06
- [nongnu] elpa/idris-mode d6ac9524f6 1/9: Simplify `idris-test-idris-type-search` by removing loading a file, ELPA Syncer, 2022/12/06
- [nongnu] elpa/idris-mode 928f785bb7 4/9: Remove conditional for srcdir in `idris-load-file` used to switch work directory, ELPA Syncer, 2022/12/06
- [nongnu] elpa/idris-mode d0d609bff7 3/9: Include tests from idris-navigate.el in idris-tests.el, ELPA Syncer, 2022/12/06
- [nongnu] elpa/idris-mode 8a4ce46373 2/9: Delete AddClause.ibc between and after tests, ELPA Syncer, 2022/12/06