git.iko.soy/Idris-dev
on master help sign in
Merge pull request #4186 from jfdm/simple-test-suite

A Simple Unit test suite for Idris.

commit5e7d01c43164074ef1d0877ff347eed241f861b6 authorJan de Muijnck-Hughes <jfdm@users.noreply.github.com> dateThu 9 Nov 2017, 12:24 (9 years ago) parentac06bdfbb6f3ab
7 files changed+178−3
compare with master
unifiedsplit
CHANGELOG.md+1 libs/contrib/Test/Unit.idr+14 libs/contrib/Test/Unit/Assertions.idr+37 libs/contrib/Test/Unit/Display.idr+27 libs/contrib/Test/Unit/Generic.idr+43 libs/contrib/Test/Unit/Runners.idr+36 libs/contrib/contrib.ipkg+20−3
CHANGELOG.md+1
@@ -54,6 +54,7 @@
5454 * Generalised many combinators to use an unknown `commit` flag where possible.
5555+ `Prelude.Doubles.atan2` is now implemented as a primitive instead of
5656 being coded in Idris.
57++ Added `Test.Unit` to `contrib` for simple unit testing.
5758
5859## Tool Updates
5960
libs/contrib/Test/Unit.idrnew file+14
@@ -0,0 +1,14 @@
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
13+
14+-- --------------------------------------------------------------------- [ EOF ]
libs/contrib/Test/Unit/Assertions.idrnew file+37
@@ -0,0 +1,37 @@
1+-- ---------------------------------------------------------- [ Assertions.idr ]
2+-- Module : Assertions.idr
3+-- Copyright : (c) The Idris Community
4+-- License : see LICENSE
5+-- --------------------------------------------------------------------- [ EOH ]
6+||| Some simple assertions.
7+module Test.Unit.Assertions
8+
9+import Test.Unit.Generic
10+
11+%access export
12+
13+assertTrue : (given : Bool) -> IO Bool
14+assertTrue b = genericTest (Just "Assert True") b True (==)
15+
16+assertFalse : (given : Bool) -> IO Bool
17+assertFalse b = genericTest (Just "Assert False") b False (==)
18+
19+assertEquals : (Eq a, Show a) => (given : a) -> (expected : a) -> IO Bool
20+assertEquals g e = genericTest (Just "Assert Equals") g e (==)
21+
22+assertNotEquals : (Eq a, Show a) => (given : a) -> (expected : a) -> IO Bool
23+assertNotEquals g e = genericTest (Just "Assert Not Equals") g e (\x,y => not (x == y))
24+
25+assertJust : Show a => (given : Maybe a) -> IO Bool
26+assertJust g = genericTest (Just "Assert Is Just") (isJust g) True (==)
27+
28+assertNothing : Show a => (given : Maybe a) -> IO Bool
29+assertNothing g = genericTest (Just "Assert Is Nothing") (isNothing g) True (==)
30+
31+assertLeft : (Show a, Show b) => (given : Either a b) -> IO Bool
32+assertLeft g = genericTest (Just "Assert is Left") (isLeft g) True (==)
33+
34+assertRight : (Show a, Show b) => (given : Either a b) -> IO Bool
35+assertRight g = genericTest (Just "Assert is Right") (isRight g) True (==)
36+
37+-- --------------------------------------------------------------------- [ 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+43
@@ -0,0 +1,43 @@
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 Text.PrettyPrint.WL
10+
11+import Test.Unit.Display
12+
13+%default total
14+%access export
15+
16+||| Run a generic test.
17+|||
18+||| @title Optional Test title
19+||| @given The given string to parse
20+||| @expected The expected result
21+||| @tFunc The testing function to compare the results.
22+genericTest : Show a
23+ => (title : Maybe String)
24+ -> (given : a)
25+ -> (expected : a)
26+ -> (tFunc : a -> a -> Bool)
27+ -> IO Bool
28+genericTest title g e eq = do
29+ putStrLn $ unwords ["Test:" , fromMaybe "Unnamed Test" title]
30+ let res = eq g e
31+ when (not res) $ do
32+ let errMsg = vcat [
33+ text errLine
34+ , text "An error occured" <+> colon
35+ , indent 2 $ text "Given" <+> colon
36+ , indent 4 $ text (show g)
37+ , indent 2 $ text "Expected" <+> colon
38+ , indent 4 $ text (show e)
39+ , text errLine]
40+ putStrLn $ Default.toString errMsg
41+ pure res
42+
43+-- --------------------------------------------------------------------- [ EOF ]
libs/contrib/Test/Unit/Runners.idrnew file+36
@@ -0,0 +1,36 @@
1+-- ------------------------------------------------------------- [ Runners.idr ]
2+-- Module : Runners.idr
3+-- Copyright : (c) The Idris Community.
4+-- License : see LICENSE
5+-- --------------------------------------------------------------------- [ EOH ]
6+||| Given a series of tests, execute them and report results.
7+module Test.Unit.Runners
8+
9+import Test.Unit.Display
10+
11+%default total
12+%access export
13+
14+namespace NonReporting
15+ ||| Run the given set of tests, but don't return the results.
16+ runTests : List (IO Bool) -> IO ()
17+ runTests Nil = do
18+ putStrLn "All Tests have been performed."
19+ putStrLn succLine
20+ runTests (t::ts) = do t; runTests ts
21+
22+namespace Reporting
23+ ||| Run the given set of tests and return the results.
24+ runTests : List (IO Bool) -> IO (List Bool)
25+ runTests Nil = do
26+ putStrLn "All tests have been performed."
27+ putStrLn succLine
28+ pure Nil
29+ runTests (x::xs) = do
30+ r <- x
31+ rs <- Reporting.runTests xs
32+ pure (r::rs)
33+
34+
35+
36+-- --------------------------------------------------------------------- [ EOF ]
libs/contrib/contrib.ipkg+20−3
@@ -5,18 +5,22 @@ opts = "--nobasepkgs --partial-eval --total -i ../prelude -i ../base"
55modules = CFFI
66 , CFFI.Memory
77 , CFFI.Types
8+
89 , Control.Algebra
910 , Control.Algebra.Lattice
1011 , Control.Algebra.NumericImplementations
1112 , Control.Algebra.VectorSpace
13+
1214 , Control.Delayed
1315 , Control.Isomorphism.Primitives
1416 , Control.Partial
1517 , Control.Pipeline
18+
1619 , Control.ST
1720 , Control.ST.Exception
1821 , Control.ST.ImplicitCall
1922 , Control.ST.Random
23+
2024 , Data.Bool.Extra
2125 , Data.BoundedList
2226 , Data.CoList
@@ -43,22 +47,35 @@ modules = CFFI
4347 , Data.Stream.Extra
4448 , Data.String.Extra
4549 , Data.ZZ
50+
4651 , Decidable.Decidable
4752 , Decidable.Order
53+
4854 , Interfaces.Correlative
4955 , Interfaces.Verified
56+
5057 , Network.Cgi
5158 , Network.Socket
5259 , Network.Socket.Data
5360 , Network.Socket.Raw
61+
5462 , System.Concurrency.Process
63+
5564 , Text.Lexer
5665 , Text.Lexer.Core
5766 , Text.Literate
5867 , Text.Parser
5968 , Text.Parser.Core
60− , Text.PrettyPrint.WL
61− , Text.PrettyPrint.WL.Characters
62− , Text.PrettyPrint.WL.Combinators
69+
6370 , Text.PrettyPrint.WL.Core
71+ , Text.PrettyPrint.WL.Combinators
72+ , Text.PrettyPrint.WL.Characters
73+ , Text.PrettyPrint.WL
74+
6475 , Text.Quantity
76+
77+ , Test.Unit.Display
78+ , Test.Unit.Runners
79+ , Test.Unit.Generic
80+ , Test.Unit.Assertions
81+ , Test.Unit