
   0 | ||| A simple library for simple unit tests
   1 | module Test.Simple
   2 | 
   3 | import Control.Monad.Writer
   4 | import Data.DPair
   5 | 
   6 | import Control.ANSI
   7 | import System
   8 | 
   9 | record Testing (a: Type) where
  10 |   constructor MkT
  11 |   name : String
  12 |   eq : a -> a -> Bool
  13 |   first : a
  14 |   second : a
  15 | 
  16 | export
  17 | ETest : Type
  18 | ETest = Exists Testing
  19 | 
  20 | record TestValues (a : Type) where
  21 |   constructor MkV
  22 |   f : a
  23 |   s : a
  24 | 
  25 | record EqValues (a : Type) where
  26 |   constructor MkEV
  27 |   eq : a -> a -> Bool
  28 |   vals : TestValues a
  29 | 
  30 | record OrValues (0 a, b : Type) where
  31 |   constructor MkOr
  32 |   left : a
  33 |   right : b
  34 | 
  35 | export
  36 | Eq a => Eq b => Eq (OrValues a b) where
  37 |   (MkOr a1 a2) == (MkOr b1 b2) = a1 == b1 || a2 == b2
  38 | 
  39 | export
  40 | by : (a -> a -> Bool) -> TestValues a -> EqValues a
  41 | by = MkEV
  42 | 
  43 | runTestList : List ETest -> Nat -> IO Nat
  44 | runTestList [] acc = pure acc
  45 | runTestList ((Evidence fst (MkT name eq first second)) :: xs) acc =
  46 |   if first `eq` second
  47 |      then putStrLn (show $ colored Green "success: \{name}") >> runTestList xs (S acc)
  48 |      else putStrLn (show $ colored Red "failure: \{name}") >> runTestList xs acc
  49 | 
  50 | export
  51 | runTests : List ETest -> IO ()
  52 | runTests xs = let l = length xs
  53 |              in runTestList xs 0 >>= printOut l
  54 |   where
  55 |     printOut : Nat -> Nat -> IO ()
  56 |     printOut allTests successes =
  57 |       putStrLn "Done \{show successes}/\{show allTests}"  >>
  58 |       if allTests == successes
  59 |          then pure ()
  60 |          else exitFailure
  61 | 
  62 | namespace Test
  63 |   export
  64 |   (>>) : List ETest -> List ETest ->  List ETest
  65 |   (>>) = (++)
  66 |   export
  67 |   pure : Testing a -> List ETest
  68 |   pure x = [Evidence a x]
  69 | 
  70 | 
  71 | export
  72 | test : String -> Eq a => TestValues a -> List ETest
  73 | test name values = [ Evidence a $ MkT name (==) values.f values.s ]
  74 | 
  75 | export
  76 | testEq : String -> EqValues a -> List ETest
  77 | testEq name (MkEV f (MkV x y)) = [ Evidence a $ MkT name f x y ]
  78 | 
  79 | export
  80 | shouldBe : a -> a -> TestValues a
  81 | shouldBe = MkV
  82 | 
  83 | export
  84 | and : TestValues a -> TestValues b -> TestValues (a, b)
  85 | and (MkV a1 a2) (MkV b1 b2) = MkV (a1, b1) (a2, b2)
  86 | 
  87 | export
  88 | or : TestValues a -> TestValues b -> TestValues (OrValues a b)
  89 | or (MkV a1 a2) (MkV b1 b2) = MkV (MkOr a1 b1) (MkOr a2 b2)
  90 | 
  91 | export
  92 | (.shouldBeTrue) : Bool -> TestValues Bool
  93 | (.shouldBeTrue) = MkV True
  94 | 
  95 | export
  96 | (.shouldBeFalse) : Bool -> TestValues Bool
  97 | (.shouldBeFalse) = MkV False
  98 | 
  99 | export infixl 9 `shouldBe`
 100 | export infixl 8 `or`
 101 | export infixl 7 `and`
 102 |