42 changes: 42 additions & 0 deletions idris-tests3.el
@@ -0,0 +1,42 @@
(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
34 changes: 27 additions & 7 deletions inferior-idris.el
Expand Up @@ -155,7 +155,25 @@ directory variables.")

(defvar idris-process-port-output-regexp (rx (? (group (+ any (not num)))) (group (+ (any num))))
"Regexp used to match the port of an Idris process.")

(defvar idris-process-exact-port-output-regexp (rx bol (group (+ (any num))) eol)
"Regexp to match port number")
(defvar idris-exact-port-matcher 1
"port number matcher")

(defvar idris-process-port-with-warning-output-regexp
(rx (? (group (+ any (not num)))) (group (** 3 4 (any num)))))
;; ^^^^^^^^^^^^^^^^^^^^^^^^^^ ^^^^^^^^^^^^^^^^^^^^^^
;; ^ ^
;; | |
;; | +---- port number
;; +------------------------------- warning message
(defvar idris-warning-matcher 1
"Warning from idris")
(defvar idris-warning-port-matcher 2
"port number matcher with warning")


;; idris-process-filter is broken in theoreticaly.
(defun idris-process-filter (string)
"Accept output from the process"
(if idris-connection
Expand All @@ -165,12 +183,14 @@ directory variables.")
(cl-flet ((idris-warn (msg)
(unless (or (null msg) (string-blank-p msg))
(message "Warning from Idris: %s" msg))))
(if (not (string-match idris-process-port-output-regexp string))
(idris-warn string)
(idris-warn (match-string 1 string))
(idris-connect (string-to-number (match-string 2 string))))
"")))

(if (string-match idris-process-exact-port-output-regexp string)
(idris-connect (string-to-number (match-string idris-exact-port-matcher string)))
(if (not (string-match idris-process-port-with-warning-output-regexp string))
(idris-warn string)
(idris-warn (match-string idris-warning-matcher string))
(idris-connect (string-to-number (match-string idris-warning-port-matcher string))))
""))))

(defun idris-show-process-buffer (string)
"Show the Idris process buffer if STRING is non-empty."
(when (> (length string) 0)
Expand Down
9 changes: 9 additions & 0 deletions test-data/AddClause.idr
@@ -0,0 +1,9 @@
module AddClause

data Test = A | B

--++++++++++++++++
test : Test -> Int
test x = ?test_rhs


7 changes: 7 additions & 0 deletions test-data/AddMissing.idr
@@ -0,0 +1,7 @@
module AddMissing
-- (idris-test-run-goto-char #'idris-add-missing)
data Test = A | B

test : Test -> Int
--++
test A = 1
7 changes: 7 additions & 0 deletions test-data/CaseSplit.idr
@@ -0,0 +1,7 @@
module CaseSplit
-- (idris-test-run-goto-char #'idris-case-split)
-- (idris-test-run-goto-char #'idris-case-dwim)
data Cases = Case1 | Case2 Int
testCase : Cases -> Cases
-- +++
testCase var = ?c
27 changes: 27 additions & 0 deletions test-data/GenerateDef.idr
@@ -0,0 +1,27 @@
module GenerateDef

-- (idris-test-run-goto-char #'idris-generate-def)
data Test = A | B
--++
test : Test -> Int

{-
C-c C-a idris-proof-search
C-c C-b Prefix Command
C-c C-c idris-case-dwim
C-c C-d Prefix Command
C-c C-e idris-make-lemma
C-c C-g idris-generate-def
C-c C-l idris-load-file
C-c RET idris-add-missing
C-c C-n idris-load-forward-line
C-c C-p idris-load-backward-line
C-c C-r idris-refine
C-c C-s idris-add-clause
C-c C-t idris-type-at-point
C-c C-w idris-make-with-block
C-c C-z idris-pop-to-repl
C-c C-S-a idris-proof-search-next
C-c C-S-g idris-generate-def-next
C-c C-SPC prop-menu-by-completing-read
-}
10 changes: 10 additions & 0 deletions test-data/MakeLemma.idr
@@ -0,0 +1,10 @@
module MakeLemma

-- (idris-test-run-goto-char #'idris-make-lemma)
data Test = A | B

test : Test -> Test
-- +++++++++++
test x = ?make_lemma


4 changes: 4 additions & 0 deletions test-data/MakeWithBlock.idr
@@ -0,0 +1,4 @@
module MakeWithBlock

-- (idris-test-run-goto-char #'idris-make-with-block)

Binary file added test-data/MetavarTest.ibc
Binary file not shown.
Binary file added test-data/ProofSearch.ibc
Binary file not shown.
14 changes: 14 additions & 0 deletions test-data/Refine.idr
@@ -0,0 +1,14 @@
module Refine

-- (idris-test-run-goto-char #'idris-refine "f")

data Test = A | B

f : Test -> Test
f = const A

test : Test -> Test




9 changes: 9 additions & 0 deletions test-data/TypeAtPoint.idr
@@ -0,0 +1,9 @@
module TypeAtPoint

-- (idris-test-run-goto-char #'idris-type-at-point)

test : Int -> Integer

test2 : Int -> Integer
--+++
test2 = test