git.iko.soy/Idris-dev
on cf47310 help sign in
Idris-dev/docs/tutorial/testing.rst
85 lines 2.6 kB history raw
1.. _tut-sect-testing:
3**********************
4Testing Idris Packages
5**********************
7The integrated build system includes a simple testing framework.
8This framework collects functions listed in the ``ipkg`` file under ``tests``.
9All test functions must return ``IO ()``.
12When you enter ``idris --testpkg yourmodule.ipkg``,
13the build system creates a temporary file in a fresh environment on your machine
14by listing the ``tests`` functions under a single ``main`` function.
15It compiles this temporary file to an executable and then executes it.
18The tests themselves are responsible for reporting their success or failure.
19Test functions commonly use ``putStrLn`` to report test results.
20The test framework does not impose any standards for reporting and consequently
21does not aggregate test results.
24For example, lets take the following list of functions that are defined in a module called ``NumOps`` for a sample package ``maths``.
26.. name: Math/NumOps.idr
27.. code-block:: idris
29 module Maths.NumOps
31 double : Num a => a -> a
32 double a = a + a
34 triple : Num a => a -> a
35 triple a = a + double a
37A simple test module, with a qualified name of ``Test.NumOps`` can be declared as
39.. name: Math/TestOps.idr
40.. code-block:: idris
42 module Test.NumOps
44 import Maths.NumOps
46 assertEq : Eq a => (given : a) -> (expected : a) -> IO ()
47 assertEq g e = if g == e
48 then putStrLn "Test Passed"
49 else putStrLn "Test Failed"
51 assertNotEq : Eq a => (given : a) -> (expected : a) -> IO ()
52 assertNotEq g e = if not (g == e)
53 then putStrLn "Test Passed"
54 else putStrLn "Test Failed"
56 testDouble : IO ()
57 testDouble = assertEq (double 2) 4
59 testTriple : IO ()
60 testTriple = assertNotEq (triple 2) 5
63The functions ``assertEq`` and ``assertNotEq`` are used to run expected passing, and failing, equality tests.
64The actual tests are ``testDouble`` and ``testTriple``, and are declared in the ``maths.ipkg`` file as follows::
66 package maths
68 modules = Maths.NumOps
69 , Test.NumOps
71 tests = Test.NumOps.testDouble
72 , Test.NumOps.testTriple
75The testing framework can then be invoked using ``idris --testpkg maths.ipkg``::
77 > idris --testpkg maths.ipkg
78 Type checking ./Maths/NumOps.idr
79 Type checking ./Test/NumOps.idr
80 Type checking /var/folders/63/np5g0d5j54x1s0z12rf41wxm0000gp/T/idristests144128232716531729.idr
81 Test Passed
82 Test Passed
84Note how both tests have reported success by printing ``Test Passed``
85as we arranged for with the ``assertEq`` and ``assertNoEq`` functions.