on master help sign in
A Simple Unit test suite for Idris.

This was developed many years ago and I've used it in many a project. I've decided to integrate into Idris' contrib library for more exposure, in the hope others will like it.

commit4e2b7264a1e0d83bc839464bcf616468656d3a8a authorJan de Muijnck-Hughes <jan.deMuijnck-Hughes@glasgow.ac.uk> dateWed 8 Nov 2017, 21:45 (9 years ago) parentac06bdf
6 files changed+153
libs/contrib/Test/Unit.idr+12 libs/contrib/Test/Unit/Assertions.idr+36 libs/contrib/Test/Unit/Display.idr+27 libs/contrib/Test/Unit/Generic.idr+45 libs/contrib/Test/Unit/Runners.idr+28 libs/contrib/contrib.ipkg+5
libs/contrib/Test/Unit.idrnew file+12
@@ -0,0 +1,12 @@
1+-- ---------------------------------------------------------------- [ Unit.idr ]
2+-- Module : Unit.idr
3+-- Copyright : (c) The Idris Community.
4+-- License : see LICENSE
5+-- --------------------------------------------------------------------- [ EOH ]
6+||| A simple Unit testing framework.
7+module Test.Unit
8+
9+import public Test.Unit.Display
10+import public Test.Unit.Generic
11+import public Test.Unit.Assertions
12+import public Test.Unit.Runners
libs/contrib/Test/Unit/Assertions.idrnew file+36
@@ -0,0 +1,36 @@
1+-- ---------------------------------------------------------- [ Assertions.idr ]
2+-- Module : Assertions.idr
3+-- Copyright : (c) The Idris Community
4+-- License : see LICENSE
5+-- --------------------------------------------------------------------- [ EOH ]
6+module Test.Unit.Assertions
7+
8+import Test.Unit.Generic
9+
10+%access export
11+
12+assertTrue : Bool -> IO Bool
13+assertTrue b = genericTest (Just "Assert True") b True (==)
14+
15+assertFalse : Bool -> IO Bool
16+assertFalse b = genericTest (Just "Assert False") b False (==)
17+
18+assertEquals : (Eq a, Show a) => (given : a) -> (expected : a) -> IO Bool
19+assertEquals g e = genericTest (Just "Assert Equals") g e (==)
20+
21+assertNotEquals : (Eq a, Show a) => (given : a) -> (expected : a) -> IO Bool
22+assertNotEquals g e = genericTest (Just "Assert Not Equals") g e (\x,y => not (x == y))
23+
24+assertJust : Show a => Maybe a -> IO Bool
25+assertJust g = genericTest (Just "Assert Is Just") (isJust g) True (==)
26+
27+assertNothing : Show a => Maybe a -> IO Bool
28+assertNothing g = genericTest (Just "Assert Is Nothing") (isNothing g) True (==)
29+
30+assertLeft : (Show a, Show b) => Either a b -> IO Bool
31+assertLeft g = genericTest (Just "Assert is Left") (isLeft g) True (==)
32+
33+assertRight : (Show a, Show b) => Either a b -> IO Bool
34+assertRight g = genericTest (Just "Assert is Right") (isRight g) True (==)
35+
36+-- --------------------------------------------------------------------- [ EOF ]
libs/contrib/Test/Unit/Display.idrnew file+27
@@ -0,0 +1,27 @@
1+-- ------------------------------------------------------------- [ Display.idr ]
2+-- Module : Display.idr
3+-- Copyright : (c) The Idris Community.
4+-- License : see LICENSE
5+-- --------------------------------------------------------------------- [ EOH ]
6+||| Some simple utilities to make the display fancier.
7+module Test.Unit.Display
8+
9+%access export
10+
11+fancyLine : Nat -> Char -> String
12+fancyLine l c = pack $ replicate l c
13+
14+infoLine : String
15+infoLine = fancyLine 40 '-'
16+
17+succLine : String
18+succLine = fancyLine 40 '='
19+
20+errLine : String
21+errLine = fancyLine 40 '+'
22+
23+heading : String -> String
24+heading n = unlines [infoLine, n, infoLine]
25+
26+
27+-- --------------------------------------------------------------------- [ EOF ]
libs/contrib/Test/Unit/Generic.idrnew file+45
@@ -0,0 +1,45 @@
1+-- ------------------------------------------------------------- [ Generic.idr ]
2+-- Module : Generic.idr
3+-- Copyright : (c) The Idris Community
4+-- License : see LICENSE
5+-- --------------------------------------------------------------------- [ EOH ]
6+||| Generic Tests
7+module Test.Unit.Generic
8+
9+import Test.Unit.Display
10+
11+%default total
12+%access export
13+
14+||| Run a generic test.
15+|||
16+||| @title Optional Test title
17+||| @given The given string to parse
18+||| @expected The expected result
19+||| @tFunc The testing function to compare the results.
20+genericTest : Show a
21+ => (title : Maybe String)
22+ -> (given : a)
23+ -> (expected : a)
24+ -> (tFunc : a -> a -> Bool)
25+ -> IO Bool
26+genericTest title g e eq = do
27+ putStrLn $ unwords ["Test:" , fromMaybe "Unnamed Test" title]
28+ let res = eq g e
29+ when (not res) $ with List do
30+ putStrLn $ unwords [
31+ errLine
32+ , "\n"
33+ , "Error:\n\n"
34+ , "Given:\n\t"
35+ , show g
36+ , "\n"
37+ , "Expected:\n\t"
38+ , show e
39+ , "\n"
40+ , errLine
41+ , "\n"
42+ ]
43+ pure res
44+
45+-- --------------------------------------------------------------------- [ EOF ]
libs/contrib/Test/Unit/Runners.idrnew file+28
@@ -0,0 +1,28 @@
1+-- ------------------------------------------------------------- [ Runners.idr ]
2+-- Module : Runners.idr
3+-- Copyright : (c) Jan de Muijnck-Hughes
4+-- License : see LICENSE
5+-- --------------------------------------------------------------------- [ EOH ]
6+module Test.Unit.Runners
7+
8+import Test.Unit.Display
9+
10+%default total
11+%access export
12+
13+namespace NonReporting
14+ runTests : List (IO a) -> IO ()
15+ runTests Nil = do putStrLn "All Tests have passed"; putStrLn succLine
16+ runTests (t::ts) = do t; runTests ts
17+
18+namespace Reporting
19+ runTests : List (IO a) -> IO (List a)
20+ runTests Nil = pure Nil
21+ runTests (x::xs) = do
22+ r <- x
23+ rs <- Reporting.runTests xs
24+ pure (r::rs)
25+
26+
27+
28+-- --------------------------------------------------------------------- [ EOF ]
libs/contrib/contrib.ipkg+5
@@ -62,3 +62,8 @@ modules = CFFI
6262 , Text.PrettyPrint.WL.Combinators
6363 , Text.PrettyPrint.WL.Core
6464 , Text.Quantity
65+ , Test.Unit.Display
66+ , Test.Unit.Runners
67+ , Test.Unit.Assertions
68+ , Test.Unit.Generic
69+ , Test.Unit