From 97deb5f288fccc091d62f708a5bd2efabd08e220 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Fri, 27 May 2022 13:31:11 +0200 Subject: [PATCH] examples --- example/Example.idr | 121 +++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 119 insertions(+), 2 deletions(-) diff --git a/example/Example.idr b/example/Example.idr index 08a41dc..f5ed058 100644 --- a/example/Example.idr +++ b/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]