0 | -- SPDX-FileCopyrightText: 2021 The test-idr developers
  1 | --
  2 | -- SPDX-License-Identifier: MPL-2.0
  3 |
  4 | module Tester
  5 |
  6 | import public Control.Monad.Either
  7 | import Data.String
  8 | import Control.ANSI
  9 | import Language.Reflection
 10 | import Language.Reflection.TTImp
 11 |
 12 | %language ElabReflection
 13 |
 14 | ||| A function which can report test failures.
 15 | public export
 16 | TestFunc : Type -> Type
 17 | TestFunc = EitherT String IO
 18 |
 19 | ||| Value representing a test.
 20 | |||
 21 | ||| Use the `test` function to create a value of this type.
 22 | public export
 23 | record Test where
 24 |     constructor MkTest
 25 |     description : String
 26 |     run : TestFunc ()
 27 |
 28 | red : String -> String
 29 | red s = show $ colored Red s
 30 |
 31 | ||| Create a new `Test` with a description and function to run.
 32 | |||
 33 | ||| Use `Test.Runner.runTests` to run the tests.
 34 | |||
 35 | ||| ```idris example
 36 | ||| itWorks = test "it works" $ do
 37 | |||     assertEq (1 + 1) 2
 38 | ||| ```
 39 | public export
 40 | test : (description : String) -> (run : TestFunc ()) -> Test
 41 | test = MkTest
 42 |
 43 | public export
 44 | record Location where
 45 |     constructor Loc
 46 |     inner : FC
 47 |
 48 | export
 49 | emptyLoc : Location
 50 | emptyLoc = Loc EmptyFC
 51 |
 52 | ||| Get a `Location` token
 53 | ||| This can be passed to assertion to attach source location
 54 | |||
 55 | ||| ```idris example
 56 | ||| let loc = here `(())
 57 | |||  in assertEq {loc} 
 58 | export %macro
 59 | here : TTImp -> Elab Location
 60 | here ttimp = pure $ Loc $ getFC ttimp
 61 |
 62 | getFile : OriginDesc -> String
 63 | getFile (PhysicalIdrSrc (MkMI path)) = showSep "/" (reverse path) ++ ".idr"
 64 | getFile (PhysicalPkgSrc fname) = fname
 65 | getFile (Virtual _) = "virtual"
 66 |
 67 | formatFC : FC -> String
 68 | formatFC (MkFC origin (startLn, startCol) (endLn, endCol)) = " at \{getFile origin}:\{show startLn}:\{show startCol}--\{show endLn}:\{show endCol}"
 69 | formatFC (MkVirtualFC origin (startLn, startCol) (endLn, endCol)) = " at \{getFile origin}:\{show startLn}:\{show startCol}--\{show endLn}:\{show endCol}"
 70 | formatFC EmptyFC = ""
 71 |
 72 | export
 73 | formatLoc : Location -> String
 74 | formatLoc loc = formatFC loc.inner
 75 |
 76 | ||| Assert that two values are equal.
 77 | |||
 78 | ||| Stops the test and reports a test failure if the values are not equal.
 79 | public export
 80 | assertEq :
 81 |     (Eq a, Show a) =>
 82 |     {default emptyLoc loc : Location} ->
 83 |     (left, right : a) ->
 84 |     TestFunc ()
 85 | assertEq left right =
 86 |     unless (left == right) $
 87 |         let msg = unlines [
 88 |                     red "assertEq" ++ " failed\{formatLoc loc}",
 89 |                     "  left  `" ++ red (show left) ++ "`",
 90 |                     "  right `" ++ red (show right) ++ "`"
 91 |                 ]
 92 |         in throwE msg
 93 |
 94 | ||| Assert that two values are not equal.
 95 | |||
 96 | ||| Stops the test and reports a test failure if the values are equal.
 97 | public export
 98 | assertNotEq :
 99 |     (Eq a, Show a) =>
100 |     {default emptyLoc loc : Location} ->
101 |     (left, right : a) ->
102 |     TestFunc ()
103 | assertNotEq left right =
104 |     if left == right then 
105 |         let msg = unlines [
106 |                     red "assertNotEq" ++ " failed\{formatLoc loc}:",
107 |                     "  left  `" ++ red (show left) ++ "`",
108 |                     "  right `" ++ red (show right) ++ "`"
109 |                 ]
110 |         in throwE msg
111 |     else
112 |         pure ()
113 |
114 | ||| Assert that a condition holds.
115 | |||
116 | ||| Stops the test and reports a test failure if the condition does not hold.
117 | public export
118 | assert :
119 |     {default emptyLoc loc : Location} ->
120 |     (cond : Bool) ->
121 |     TestFunc ()
122 | assert cond =
123 |     if not cond then 
124 |         let msg = red "assert" ++ "failed\{formatLoc loc}"
125 |         in throwE msg
126 |     else
127 |         pure ()
128 |
129 | ||| Cause a test failure with a message.
130 | public export
131 | throw : (msg : String) -> TestFunc a
132 | throw = throwE
133 |