idris2-tap/example/Example.idr

module Example
import TAP

-- this is for the examples, you don't need it for the library itself
import Data.String
import Data.IORef


E = List (String, Nat)
ToInfo Integer where toInfo n = [("val", show n)]

-- a test suite consists of a list of tests, like in haskell's tasty
-- or something like that. each one can be a group, so really it's a tree.
--
-- each test returns some `Either e a` (or `EitherT e IO a`), where
-- `Left` is failure and `Right` is success.
--
-- `a` and `b` both have to implement `ToInfo`, which allows them to be
-- printed as a YAML document. `()` implements `ToInfo` with an empty document,
-- which is probably what you want most of the time in a success. but you
-- can return any info you might need
--
-- if you expect a computation to fail, you can use `testThrows[IO]`, which
-- takes a function to classify what errors are expected
tests1 : Test
tests1 = "one" :- [
  test "success"  {e = E} $
    Right (),
  testIO "success in IO"  {e = E} $ do
    let val = Z
    r   <- newIORef val
    res <- readIORef r
    if res == val then pure () else
      throwError [("wanted", val), ("got", res)],
  test "failure"  {a = ()} $
    Left [("oops", "ouch")],
  testThrows "throws 0" (== 0)  {a = ()} $
    throwError 0
]

-- idris has trouble inferring types that seem to be obvious to me, which is why
-- i keep having to specify `e` above.
-- but anyway, most of the time i wrap these basic test functions in something
-- more specific to the situation. like an hunit-style assertion
-- (maybe the library should provide some of these?)

assertEq : (Eq a, Show a) => (label : String) -> (got, exp : a) -> Test
assertEq label got exp = test label $
  if got == exp then Right ()
                else Left [("exp", exp), ("got", got)]

tests2 : Test
tests2 = "two" :- [
  assertEq "2 + 2"  (2 + 2)          4,
  assertEq "im gay" (words "im gay") ["im", "gay"]
]

-- you can use `todo` and `skip` for tests you haven't written yet, can't run
-- in the current environment, or whatever. `todoWith` and `skipWith` take an
-- extra reason.

tests3 : Test
tests3 = "three" :- [
  todo "drink water",
  skip $ assertEq "im gay" (words "im gay") ["im", "gay"],

  todoWith "take a sippy" "drink water",
  skipWith "(everyone already knows)" $
    assertEq "im gay" (words "im gay") ["im", "gay"]
]


-- if you pass `--version 14` (or `-V 14`) you get the output:
--
-- TAP version 14
-- 1..3
-- # Subtest: one
--     1..4
--     ok 1 - success
--     ok 2 - success in IO
--     not ok 3 - failure
--       ---
--       oops: "ouch"
--       ...
--     ok 4 - throws 0
-- not ok 1 - one
-- # Subtest: two
--     1..2
--     ok 1 - 2 + 2
--     ok 2 - im gay
-- ok 2 - two
-- # Subtest: three
--     1..4
--     ok 1 - drink water  # todo
--     ok 2 - im gay  # skip
--     ok 3 - drink water  # todo take a sippy
--     ok 4 - im gay  # skip (everyone already knows)
-- ok 3 - three
--
--
-- if you pass `--version 13`, or nothing, it's flattened and you get
--
-- TAP version 13
-- 1..10
-- ok 1 - one ⟫ success
-- ok 2 - one ⟫ success in IO
-- not ok 3 - one ⟫ failure
--   ---
--   oops: "ouch"
--   ...
-- ok 4 - one ⟫ throws 0
-- ok 5 - two ⟫ 2 + 2
-- ok 6 - two ⟫ im gay
-- ok 7 - three ⟫ drink water  # todo
-- ok 8 - three ⟫ im gay  # skip
-- ok 9 - three ⟫ drink water  # todo take a sippy
-- ok 10 - three ⟫ im gay  # skip (everyone already knows)
--
-- it is `/usr/bin/prove`'s fault that flat is the default.
--
-- you can also have nice colours with `--colour/--color/-c`, and run only some
-- tests with `--filter`.
main : IO ()
main = TAP.main !getTestOpts [tests1, tests2, tests3]