idris2-tap/TAP.idr

360 lines
10 KiB
Idris
Raw Normal View History

2022-05-26 09:41:48 -04:00
||| basic test framework using the TAP output format (https://testanything.org)
2022-05-26 08:23:50 -04:00
module TAP
import public TAP.Options
import public Control.Monad.Either
import Data.String
import Data.List
import Data.List.Elem
import Data.SnocList
import Control.Monad.Reader
import Control.Monad.State
import Control.ANSI
import System
%default total
2022-05-26 09:41:48 -04:00
||| extra info attached to a result (positive or negative). the TAP spec allows
||| any YAML, but this is what you get for now
2022-05-26 08:23:50 -04:00
public export
Info : Type
Info = List (String, String)
2022-05-26 09:41:48 -04:00
||| result of running a test. or not doing so, in the case of `Skip` and `Todo`
2022-05-26 08:23:50 -04:00
private
data Result = Tried Bool Info | Skip String | Todo String
private
record TestBase where
constructor MakeTest
label : String
run : IO Result
2022-05-26 09:41:48 -04:00
||| render an `Info` value as a YAML document, including the `---`/`...`
||| delimiters. returns nothing at all if the `Info` is empty
export
2022-05-26 08:23:50 -04:00
toLines : Info -> List String
toLines [] = []
2022-05-26 09:41:48 -04:00
toLines xs = "---" :: concatMap toLines1 xs <+> ["..."] where
toLines1 : (String, String) -> List String
toLines1 (k, v) =
let vs = lines v in
if length vs == 1 then ["\{k}: \{v}"]
else "\{k}: |" :: map (indent 2) vs
2022-05-26 08:23:50 -04:00
2022-05-26 09:41:48 -04:00
||| represent a value (e.g. an error message) as an `Info` for including in the
||| output.
public export
interface ToInfo e where
toInfo : e -> Info
2022-05-26 08:23:50 -04:00
2022-05-26 09:41:48 -04:00
||| an info of `()` prints nothing
2022-05-26 08:23:50 -04:00
export ToInfo () where toInfo () = []
export Show a => ToInfo (List (String, a)) where toInfo = map (map show)
2022-05-26 09:41:48 -04:00
||| a test or group of tests
2022-05-26 08:23:50 -04:00
export
data Test
= One TestBase
| Group String (List Test)
| Note String
2022-05-26 09:41:48 -04:00
||| is this a real test or just a note?
2022-05-26 08:23:50 -04:00
export
isRealTest : Test -> Bool
isRealTest (One _) = True
isRealTest (Group _ _) = True
isRealTest (Note _) = False
private
result : ToInfo a => Bool -> a -> IO Result
result ok = pure . Tried ok . toInfo
2022-05-26 09:41:48 -04:00
||| promote a lazy value to an IO action that will run it
2022-05-26 08:23:50 -04:00
private
lazyToIO : Lazy a -> IO a
lazyToIO val = primIO $ \w => MkIORes (force val) w
2022-05-26 09:41:48 -04:00
||| a test that can do some IO before returning `Left` for a failure or `Right`
||| for a success
2022-05-26 08:23:50 -04:00
export
testIO : (ToInfo e, ToInfo a) => String -> EitherT e IO a -> Test
testIO label act = One $ MakeTest label $ do
case !(runEitherT act) of
Right val => result True val
Left err => result False err
2022-05-26 09:41:48 -04:00
||| a pure test that returns `Left` for a failure or `Right` for a success
2022-05-26 08:23:50 -04:00
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, e.g.
2022-05-26 09:41:48 -04:00
||| `todo "<reason>" "<label>"` prints as `ok 1 - <label> # todo <reason>`
2022-05-26 08:23:50 -04:00
export
todoWith : (reason, label : String) -> Test
todoWith {reason, label} = One $ MakeTest label $ pure $ Todo reason
2022-05-26 08:23:50 -04:00
2022-05-26 09:41:48 -04:00
||| a todo with no reason listed
2022-05-26 08:23:50 -04:00
export
todo : String -> Test
2022-05-26 09:41:48 -04:00
todo = todoWith ""
2022-05-26 08:23:50 -04:00
private
makeSkip : (reason, label : String) -> Test
makeSkip {reason, label} = One $ MakeTest label $ pure $ Skip reason
2022-05-26 08:23:50 -04:00
2022-05-26 09:41:48 -04:00
||| skip a test, with the reason given. skipping a `Note` doesn't do anything
2022-05-26 08:23:50 -04:00
export
2022-05-26 09:41:48 -04:00
skipWith : String -> Test -> Test
skipWith reason (One t) = makeSkip {reason, label = t.label}
skipWith reason (Group l _) = makeSkip {reason, label = l}
2022-05-26 09:41:48 -04:00
skipWith _ (Note n) = Note n
2022-05-26 08:23:50 -04:00
2022-05-26 09:41:48 -04:00
||| skip a test with no reason listed
2022-05-26 08:23:50 -04:00
export
skip : Test -> Test
2022-05-26 09:41:48 -04:00
skip = skipWith ""
2022-05-27 07:31:01 -04:00
||| test that an action fails in an expected way.
2022-05-26 09:41:48 -04:00
||| - 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`,
||| then the test fails with `err`
||| - if the body returns `Right val`, then the test fails with
||| `{success: val}`
2022-05-26 08:23:50 -04:00
export
2022-05-27 07:31:01 -04:00
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
2022-05-26 08:23:50 -04:00
Left err => if p err then result True () else result False err
Right val => result False [("success", val)]
2022-05-27 07:31:01 -04:00
||| 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
2022-05-26 08:23:50 -04:00
infix 1 :-
2022-05-26 09:41:48 -04:00
||| make a test group
2022-05-26 08:23:50 -04:00
export
(:-) : String -> List Test -> Test
(:-) = Group
2022-05-26 09:41:48 -04:00
||| stop immediately and run no more tests
2022-05-26 08:23:50 -04:00
export
bailOut : Test
bailOut = One $ MakeTest "bail out" $ do
putStrLn "Bail out!"
exitFailure
2022-05-26 09:41:48 -04:00
||| include a comment in the output. not counted as an actual test
2022-05-26 08:23:50 -04:00
export
note : String -> Test
note = Note
2022-05-26 09:41:48 -04:00
||| print the "1..n" header for a group of tests
2022-05-26 08:23:50 -04:00
export
header : List Test -> String
header tests =
let count = length $ filter isRealTest tests in
"1..\{show count}"
private
withPrefix : SnocList String -> TestBase -> Test
withPrefix pfx = One . {label $= (makePrefix pfx ++)}
where makePrefix = concatMap $ \s => "\{s} "
mutual
2022-05-26 09:41:48 -04:00
||| flatten some tests, starting with the prefix given
2022-05-26 08:23:50 -04:00
export
flattenWith : SnocList String -> List Test -> List Test
flattenWith pfx tests =
concatMap (\t => flatten1With pfx (assert_smaller tests t)) tests
2022-05-26 09:41:48 -04:00
||| flatten a test group, starting with the prefix given.
||| if not a group, just add the prefix to the label
2022-05-26 08:23:50 -04:00
export
flatten1With : SnocList String -> Test -> List Test
flatten1With pfx (One t) = [withPrefix pfx t]
flatten1With pfx (Group x ts) = flattenWith (pfx :< x) ts
flatten1With pfx (Note n) = [Note n]
2022-05-26 09:41:48 -04:00
||| flatten some tests
2022-05-26 08:23:50 -04:00
export
flatten : List Test -> List Test
flatten = flattenWith [<]
2022-05-26 09:41:48 -04:00
||| flatten a group, if it is one
2022-05-26 08:23:50 -04:00
export
flatten1 : Test -> List Test
flatten1 = flatten1With [<]
2022-05-26 09:41:48 -04:00
||| environment for correctly printing test output
2022-05-26 08:23:50 -04:00
private
record RunnerEnv where
constructor RE
2022-05-26 09:41:48 -04:00
||| current indent level (for subtests)
2022-05-26 08:23:50 -04:00
indent : Nat
2022-05-26 09:41:48 -04:00
||| whether to include control codes for colours
2022-05-26 08:23:50 -04:00
color : Bool
private
Runner : Type -> Type
Runner = ReaderT RunnerEnv IO
2022-05-26 09:41:48 -04:00
||| print some lines at the current indent level
2022-05-26 08:23:50 -04:00
private
putIndentLines : List String -> Runner ()
putIndentLines xs = traverse_ (putStrLn . indent (!ask).indent) xs
private
isOk : Bool -> String
isOk b = if b then "ok" else "not ok"
2022-05-26 09:41:48 -04:00
||| whether a result counts as a "success". todos and skips are successes
2022-05-26 08:23:50 -04:00
private
toBool : Result -> Bool
toBool (Tried ok _) = ok
toBool _ = True
2022-05-26 09:41:48 -04:00
||| number the elements of a list where the predicate returns `True`,
||| starting at 1. if it returns `False` then that element is numbered with 0
2022-05-26 08:23:50 -04:00
private
numbered : (a -> Bool) -> List a -> List (Nat, a)
numbered p = go 1 where
go : Nat -> List a -> List (Nat, a)
go _ [] = []
go i (x :: xs) =
if p x then (i, x) :: go (S i) xs
else (0, x) :: go i xs
2022-05-26 09:41:48 -04:00
||| colour a string, if colours are being used
2022-05-26 08:23:50 -04:00
private
col : Color -> String -> Runner String
col c str = pure $ if (!ask).color then show $ colored c str else str
2022-05-26 09:41:48 -04:00
||| print a line in the given colour, if colours are being used
2022-05-26 08:23:50 -04:00
private
putColor : Color -> String -> Runner ()
putColor c str = putIndentLines [!(col c str)]
2022-05-26 09:41:48 -04:00
||| green for success, red for failure
2022-05-26 08:23:50 -04:00
private
okCol : Bool -> Color
okCol True = Green
okCol False = Red
2022-05-26 09:41:48 -04:00
||| print a test result line with the start highlighted in the given colour
2022-05-26 08:23:50 -04:00
private
putOk' : Color -> Bool -> Nat -> String -> Runner ()
putOk' c ok index label =
putIndentLines [!(col c "\{isOk ok} \{show index}") ++ " - \{label}"]
2022-05-26 09:41:48 -04:00
||| print a result highlighted red or green according to whether it succeeded
2022-05-26 08:23:50 -04:00
private
putOk : Bool -> Nat -> String -> Runner ()
putOk ok = putOk' (okCol ok) ok
2022-05-26 09:41:48 -04:00
||| print a TAP version line
2022-05-26 08:23:50 -04:00
private
putVersion : TAPVersion -> Runner ()
putVersion ver = putColor Cyan "TAP version \{show ver}"
2022-05-26 09:41:48 -04:00
||| run a test, print its line, and return whether it succeeded
2022-05-26 08:23:50 -04:00
private
run1' : (Nat, TestBase) -> Runner Bool
run1' (index, test) = do
res <- liftIO test.run
case res of
Tried ok info => do
putOk ok index test.label
local {indent $= plus 2} $ putIndentLines $ toLines info
Skip reason =>
putOk' Yellow True index "\{test.label} # skip \{reason}"
Todo reason =>
putOk' Yellow True index "\{test.label} # todo \{reason}"
pure $ toBool res
2023-03-03 15:04:46 -05:00
parameters (skipNotes : Bool)
mutual
||| run a test or group
private
run' : (Nat, Test) -> Runner Bool
run' (index, One test) = run1' (index, test)
run' (index, Group label tests) = do
putIndentLines [!(col Magenta "# Subtest: ") ++ label]
res <- local {indent $= plus 4} $ runList tests
putOk res index label
pure res
run' (_, Note note) = do
unless skipNotes $ putIndentLines [!(col Magenta "# ") ++ note]
pure True
private
||| run several tests
runList : List Test -> Runner Bool
runList tests = do
putColor Cyan $ header tests
let tests' = numbered isRealTest tests
all id <$> traverse (\t => run' (assert_smaller tests t)) tests'
2022-05-26 08:23:50 -04:00
mutual
2022-05-26 09:41:48 -04:00
||| filter tests by whether a string occurs in their name or in the name of
||| any of their parent groups
2022-05-26 08:23:50 -04:00
export
filterMatch : Maybe String -> List Test -> List Test
filterMatch Nothing tests = tests
filterMatch (Just pat) tests =
mapMaybe (\t => filterMatch1 pat (assert_smaller tests t)) tests
2022-05-26 09:41:48 -04:00
||| filter subtests by whether a string occurs in their name or in the name of
||| any of their parent groups. return `Nothing` if nothing remains
2022-05-26 08:23:50 -04:00
export
filterMatch1 : String -> Test -> Maybe Test
filterMatch1 pat test@(One base) =
guard (pat `isInfixOf` base.label) $> test
filterMatch1 pat whole@(Group label tests) =
if pat `isInfixOf` label then Just whole else
let res = filterMatch (Just pat) tests in
guard (any isRealTest res) $> Group label res
2022-05-26 08:23:50 -04:00
filterMatch1 pat note@(Note _) = Just note
2022-05-26 09:41:48 -04:00
||| run some tests, and return `ExitSuccess` if they were all ok, and
||| `ExitFailure 70` if not
||| (https://www.freebsd.org/cgi/man.cgi?query=sysexits)
2022-05-26 08:23:50 -04:00
export
main' : Options -> List Test -> IO ExitCode
main' opts tests = do
let tests = filterMatch opts.pattern $
case opts.version of V13 => flatten tests; V14 => tests
2023-03-03 15:04:46 -05:00
let act = do putVersion opts.version; runList opts.skipComments tests
2022-05-26 08:23:50 -04:00
pure $ if !(runReaderT (RE 0 opts.color) act)
then ExitSuccess
else ExitFailure 70
2022-05-26 09:41:48 -04:00
||| run tests and exit with an appropriate code
2022-05-26 08:23:50 -04:00
export
main : Options -> List Test -> IO ()
main opts tests = exitWith !(main' opts tests)