branch: elpa/idris-mode
commit d0d609bff711a1f0d70b2d8f6698ca1e0ed7ac78
Author: Marek L <nospam.ke...@gmail.com>
Commit: Marek L <nospam.ke...@gmail.com>
Include tests from idris-navigate.el in idris-tests.el
---
idris-navigate.el | 292 ----------------------------------------------------
idris-test-utils.el | 67 +++++++++---
idris-tests.el | 255 +++++++++++++++++++++++++++++++++++++++++++++
3 files changed, 308 insertions(+), 306 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 df41786c71..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 ()
@@ -201,5 +203,258 @@ remain."
(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
