1 module Test.TestTree
2 
3 %default total
4 
5 public export
6 data TestResult = MkSuccess | MkFailure String
7 
8 public export
9 record TestCase where
10   constructor MkTestCase
11   name : String
12   run : IO TestResult
13 
14 runTestCase : TestCase -> IO TestResult
15 runTestCase testCase =
16   do putStrLn $ "Running test case: " <+> testCase.name
17      result <- testCase.run
18      case result of
19        MkSuccess => putStrLn "Success"
20        MkFailure message => putStrLn $ "Failure: " <+> message
21      pure result
22 
23 public export
24 data TestTree = MkTestLeaf TestCase | MkTestGroup String (List TestTree)
25 
26 mutual
27   -- Helper. We can't just call use sequence . map runTestTree in runTestTree because the compiler wouldn't be able to tell runTestTree is total.
28   runTestTrees : List TestResult -> List TestTree -> IO (List TestResult)
29   runTestTrees acc [] = pure $ reverse acc
30   runTestTrees acc (tree :: trees) =
31     do result <- runTestTree tree
32        runTestTrees (result :: acc) trees
33 
34   export
35   runTestTree : TestTree -> IO TestResult
36   runTestTree (MkTestLeaf testCase) = runTestCase testCase
37   runTestTree (MkTestGroup name subTrees) =
38     let resultToNumFailures : TestResult -> Nat
39         resultToNumFailures MkSuccess = 0
40         resultToNumFailures (MkFailure _) = 1
41     in
42     do putStrLn $ "Starting test group: " <+> name
43        results <- runTestTrees [] subTrees
44        let numFailures = sum $ map resultToNumFailures results
45        putStrLn $
46            "Test group finished: " <+> name <+> ". " <+>
47            show numFailures <+> "/" <+> show (length results) <+>
48            " failed."
49        pure $
50          if numFailures == 0
51            then MkSuccess
52            else MkFailure name