examples

it means less messing around when adding/removing skipWith, and
todoWith is just changed for consistency

TAP.idr

@@ -99,11 +99,11 @@ export
 test : (ToInfo e, ToInfo a) => String -> Lazy (Either e a) -> Test
 test label val = testIO label $ MkEitherT $ lazyToIO val
 
-||| a todo with a reason given. the reason is the first argument, e.g.
+||| a todo with a reason given, e.g.
 ||| `todo "<reason>" "<label>"` prints as `ok 1 - <label>  # todo <reason>`
 export
-todoWith : String -> String -> Test
-todoWith reason label = One $ MakeTest label $ pure $ Todo reason
+todoWith : (reason, label : String) -> Test
+todoWith {reason, label} = One $ MakeTest label $ pure $ Todo reason
 
 ||| a todo with no reason listed
 export
@@ -111,14 +111,14 @@ todo : String -> Test
 todo = todoWith ""
 
 private
-makeSkip : String -> String -> Test
-makeSkip label reason = One $ MakeTest label $ pure $ Skip reason
+makeSkip : (reason, label : String) -> Test
+makeSkip {reason, label} = One $ MakeTest label $ pure $ Skip reason
 
 ||| skip a test, with the reason given. skipping a `Note` doesn't do anything
 export
 skipWith : String -> Test -> Test
-skipWith reason (One   t)   = makeSkip t.label reason
-skipWith reason (Group l _) = makeSkip l       reason
+skipWith reason (One   t)   = makeSkip {reason, label = t.label}
+skipWith reason (Group l _) = makeSkip {reason, label = l}
 skipWith _      (Note  n)   = Note n
 
 ||| skip a test with no reason listed
@@ -126,7 +126,7 @@ export
 skip : Test -> Test
 skip = skipWith ""
 
-||| test that an expression fails in an expected way.
+||| test that an action fails in an expected way.
 ||| - if the body returns `Left err` and the predicate given returns `True`,
 |||   then the test succeeds
 ||| - if the body returns `Left err` and the predicate given returns `False`,
@@ -134,13 +134,19 @@ skip = skipWith ""
 ||| - if the body returns `Right val`, then the test fails with
 |||   `{success: val}`
 export
-testThrows : (ToInfo e, Show a) =>
-             String -> (e -> Bool) -> Lazy (Either e a) -> Test
-testThrows label p act = One $ MakeTest label $ do
-  case !(lazyToIO act) of
+testThrowsIO : (ToInfo e, Show a) =>
+               String -> (e -> Bool) -> EitherT e IO a -> Test
+testThrowsIO label p act = One $ MakeTest label $ do
+  case !(runEitherT act) of
        Left  err => if p err then result True () else result False err
        Right val => result False [("success", val)]
 
+||| pure version of `testThrowsIO`
+export
+testThrows : (ToInfo e, Show a) =>
+           String -> (e -> Bool) -> Lazy (Either e a) -> Test
+testThrows label p act = testThrowsIO label p $ MkEitherT $ lazyToIO act
+
 infix 1 :-
 ||| make a test group
 export

example/Example.idr

@@ -1,7 +1,124 @@
 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 []
+main = TAP.main !getTestOpts [tests1, tests2, tests3]