rhi
/
idris2-tap
1
0
Fork 0
Code Issues 1 Pull Requests Projects Releases Wiki Activity

docstrings

This commit is contained in:
rhiannon morris 2022-05-26 15:41:48 +02:00
parent 4a81280811
commit 25a779eae4
2 changed files with 128 additions and 25 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

99
TAP.idr
View File

@ -1,3 +1,4 @@
||| basic test framework using the TAP output format (https://testanything.org)
module TAP module TAP
import public TAP.Options import public TAP.Options
@ -14,10 +15,14 @@ import System
%default total %default total
||| extra info attached to a result (positive or negative). the TAP spec allows
||| any YAML, but this is what you get for now
public export public export
Info : Type Info : Type
Info = List (String, String) Info = List (String, String)
||| result of running a test. or not doing so, in the case of `Skip` and `Todo`
private private
data Result = Tried Bool Info | Skip String | Todo String data Result = Tried Bool Info | Skip String | Todo String
@ -28,27 +33,32 @@ record TestBase where
run : IO Result run : IO Result
private ||| render an `Info` value as a YAML document, including the `---`/`...`
toLines1 : (String, String) -> List String ||| delimiters. returns nothing at all if the `Info` is empty
toLines1 (k, v) = export
let vs = lines v in
if length vs == 1
then ["\{k}: \{v}"]
else "\{k}: |" :: map (indent 2) vs
private
toLines : Info -> List String toLines : Info -> List String
toLines [] = [] toLines [] = []
toLines xs = "---" :: concatMap toLines1 xs <+> ["..."] 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
public export interface ToInfo e where toInfo : e -> Info ||| 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
||| an info of `()` prints nothing
export ToInfo () where toInfo () = [] export ToInfo () where toInfo () = []
export Show a => ToInfo (List (String, a)) where toInfo = map (map show) export Show a => ToInfo (List (String, a)) where toInfo = map (map show)
||| a test or group of tests
export export
data Test data Test
= One TestBase = One TestBase
@ -56,6 +66,7 @@ data Test
| Note String | Note String
||| is this a real test or just a note?
export export
isRealTest : Test -> Bool isRealTest : Test -> Bool
isRealTest (One _) = True isRealTest (One _) = True
@ -67,10 +78,15 @@ private
result : ToInfo a => Bool -> a -> IO Result result : ToInfo a => Bool -> a -> IO Result
result ok = pure . Tried ok . toInfo result ok = pure . Tried ok . toInfo
||| promote a lazy value to an IO action that will run it
private private
lazyToIO : Lazy a -> IO a lazyToIO : Lazy a -> IO a
lazyToIO val = primIO $ \w => MkIORes (force val) w lazyToIO val = primIO $ \w => MkIORes (force val) w
||| a test that can do some IO before returning `Left` for a failure or `Right`
||| for a success
export export
testIO : (ToInfo e, ToInfo a) => String -> EitherT e IO a -> Test testIO : (ToInfo e, ToInfo a) => String -> EitherT e IO a -> Test
testIO label act = One $ MakeTest label $ do testIO label act = One $ MakeTest label $ do
@ -78,32 +94,45 @@ testIO label act = One $ MakeTest label $ do
Right val => result True val Right val => result True val
Left err => result False err Left err => result False err
||| a pure test that returns `Left` for a failure or `Right` for a success
export export
test : (ToInfo e, ToInfo a) => String -> Lazy (Either e a) -> Test test : (ToInfo e, ToInfo a) => String -> Lazy (Either e a) -> Test
test label val = testIO label $ MkEitherT $ lazyToIO val test label val = testIO label $ MkEitherT $ lazyToIO val
||| a todo with a reason given. the reason is the first argument, e.g.
||| `todo "<reason>" "<label>"` prints as `ok 1 - <label> # todo <reason>`
export export
todoWith : String -> String -> Test todoWith : String -> String -> Test
todoWith label reason = One $ MakeTest label $ pure $ Todo reason todoWith reason label = One $ MakeTest label $ pure $ Todo reason
||| a todo with no reason listed
export export
todo : String -> Test todo : String -> Test
todo label = todoWith label "" todo = todoWith ""
private private
makeSkip : String -> String -> Test makeSkip : String -> String -> Test
makeSkip label reason = One $ MakeTest label $ pure $ Skip reason makeSkip label reason = One $ MakeTest label $ pure $ Skip reason
||| skip a test, with the reason given. skipping a `Note` doesn't do anything
export export
skipWith : Test -> String -> Test skipWith : String -> Test -> Test
skipWith (One t) reason = makeSkip t.label reason skipWith reason (One t) = makeSkip t.label reason
skipWith (Group l _) reason = makeSkip l reason skipWith reason (Group l _) = makeSkip l reason
skipWith (Note n) _ = Note n skipWith _ (Note n) = Note n
||| skip a test with no reason listed
export export
skip : Test -> Test skip : Test -> Test
skip test = skipWith test "" skip = skipWith ""
||| test that an expression 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`,
||| then the test fails with `err`
||| - if the body returns `Right val`, then the test fails with
||| `{success: val}`
export export
testThrows : (ToInfo e, Show a) => testThrows : (ToInfo e, Show a) =>
String -> (e -> Bool) -> Lazy (Either e a) -> Test String -> (e -> Bool) -> Lazy (Either e a) -> Test
@ -113,22 +142,26 @@ testThrows label p act = One $ MakeTest label $ do
Right val => result False [("success", val)] Right val => result False [("success", val)]
infix 1 :- infix 1 :-
||| make a test group
export export
(:-) : String -> List Test -> Test (:-) : String -> List Test -> Test
(:-) = Group (:-) = Group
||| stop immediately and run no more tests
export export
bailOut : Test bailOut : Test
bailOut = One $ MakeTest "bail out" $ do bailOut = One $ MakeTest "bail out" $ do
putStrLn "Bail out!" putStrLn "Bail out!"
exitFailure exitFailure
||| include a comment in the output. not counted as an actual test
export export
note : String -> Test note : String -> Test
note = Note note = Note
||| print the "1..n" header for a group of tests
export export
header : List Test -> String header : List Test -> String
header tests = header tests =
@ -142,37 +175,45 @@ withPrefix pfx = One . {label $= (makePrefix pfx ++)}
where makePrefix = concatMap $ \s => "\{s} ⟫ " where makePrefix = concatMap $ \s => "\{s} ⟫ "
mutual mutual
||| flatten some tests, starting with the prefix given
export export
flattenWith : SnocList String -> List Test -> List Test flattenWith : SnocList String -> List Test -> List Test
flattenWith pfx tests = flattenWith pfx tests =
concatMap (\t => flatten1With pfx (assert_smaller tests t)) tests concatMap (\t => flatten1With pfx (assert_smaller tests t)) tests
||| flatten a test group, starting with the prefix given.
||| if not a group, just add the prefix to the label
export export
flatten1With : SnocList String -> Test -> List Test flatten1With : SnocList String -> Test -> List Test
flatten1With pfx (One t) = [withPrefix pfx t] flatten1With pfx (One t) = [withPrefix pfx t]
flatten1With pfx (Group x ts) = flattenWith (pfx :< x) ts flatten1With pfx (Group x ts) = flattenWith (pfx :< x) ts
flatten1With pfx (Note n) = [Note n] flatten1With pfx (Note n) = [Note n]
||| flatten some tests
export export
flatten : List Test -> List Test flatten : List Test -> List Test
flatten = flattenWith [<] flatten = flattenWith [<]
||| flatten a group, if it is one
export export
flatten1 : Test -> List Test flatten1 : Test -> List Test
flatten1 = flatten1With [<] flatten1 = flatten1With [<]
||| environment for correctly printing test output
private private
record RunnerEnv where record RunnerEnv where
constructor RE constructor RE
||| current indent level (for subtests)
indent : Nat indent : Nat
||| whether to include control codes for colours
color : Bool color : Bool
private private
Runner : Type -> Type Runner : Type -> Type
Runner = ReaderT RunnerEnv IO Runner = ReaderT RunnerEnv IO
||| print some lines at the current indent level
private private
putIndentLines : List String -> Runner () putIndentLines : List String -> Runner ()
putIndentLines xs = traverse_ (putStrLn . indent (!ask).indent) xs putIndentLines xs = traverse_ (putStrLn . indent (!ask).indent) xs
@ -181,12 +222,15 @@ private
isOk : Bool -> String isOk : Bool -> String
isOk b = if b then "ok" else "not ok" isOk b = if b then "ok" else "not ok"
||| whether a result counts as a "success". todos and skips are successes
private private
toBool : Result -> Bool toBool : Result -> Bool
toBool (Tried ok _) = ok toBool (Tried ok _) = ok
toBool _ = True toBool _ = True
||| 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
private private
numbered : (a -> Bool) -> List a -> List (Nat, a) numbered : (a -> Bool) -> List a -> List (Nat, a)
numbered p = go 1 where numbered p = go 1 where
@ -197,32 +241,39 @@ numbered p = go 1 where
else (0, x) :: go i xs else (0, x) :: go i xs
||| colour a string, if colours are being used
private private
col : Color -> String -> Runner String col : Color -> String -> Runner String
col c str = pure $ if (!ask).color then show $ colored c str else str col c str = pure $ if (!ask).color then show $ colored c str else str
||| print a line in the given colour, if colours are being used
private private
putColor : Color -> String -> Runner () putColor : Color -> String -> Runner ()
putColor c str = putIndentLines [!(col c str)] putColor c str = putIndentLines [!(col c str)]
||| green for success, red for failure
private private
okCol : Bool -> Color okCol : Bool -> Color
okCol True = Green okCol True = Green
okCol False = Red okCol False = Red
||| print a test result line with the start highlighted in the given colour
private private
putOk' : Color -> Bool -> Nat -> String -> Runner () putOk' : Color -> Bool -> Nat -> String -> Runner ()
putOk' c ok index label = putOk' c ok index label =
putIndentLines [!(col c "\{isOk ok} \{show index}") ++ " - \{label}"] putIndentLines [!(col c "\{isOk ok} \{show index}") ++ " - \{label}"]
||| print a result highlighted red or green according to whether it succeeded
private private
putOk : Bool -> Nat -> String -> Runner () putOk : Bool -> Nat -> String -> Runner ()
putOk ok = putOk' (okCol ok) ok putOk ok = putOk' (okCol ok) ok
||| print a TAP version line
private private
putVersion : TAPVersion -> Runner () putVersion : TAPVersion -> Runner ()
putVersion ver = putColor Cyan "TAP version \{show ver}" putVersion ver = putColor Cyan "TAP version \{show ver}"
||| run a test, print its line, and return whether it succeeded
private private
run1' : (Nat, TestBase) -> Runner Bool run1' : (Nat, TestBase) -> Runner Bool
run1' (index, test) = do run1' (index, test) = do
@ -238,6 +289,7 @@ run1' (index, test) = do
pure $ toBool res pure $ toBool res
mutual mutual
||| run a test or group
private private
run' : (Nat, Test) -> Runner Bool run' : (Nat, Test) -> Runner Bool
run' (index, One test) = run1' (index, test) run' (index, One test) = run1' (index, test)
@ -251,6 +303,7 @@ mutual
pure True pure True
private private
||| run several tests
runList : List Test -> Runner Bool runList : List Test -> Runner Bool
runList tests = do runList tests = do
putColor Cyan $ header tests putColor Cyan $ header tests
@ -259,12 +312,16 @@ mutual
mutual mutual
||| filter tests by whether a string occurs in their name or in the name of
||| any of their parent groups
export export
filterMatch : Maybe String -> List Test -> List Test filterMatch : Maybe String -> List Test -> List Test
filterMatch Nothing tests = tests filterMatch Nothing tests = tests
filterMatch (Just pat) tests = filterMatch (Just pat) tests =
mapMaybe (\t => filterMatch1 pat (assert_smaller tests t)) tests mapMaybe (\t => filterMatch1 pat (assert_smaller tests t)) tests
||| 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
export export
filterMatch1 : String -> Test -> Maybe Test filterMatch1 : String -> Test -> Maybe Test
filterMatch1 pat test@(One base) = filterMatch1 pat test@(One base) =
@ -277,6 +334,9 @@ mutual
filterMatch1 pat note@(Note _) = Just note filterMatch1 pat note@(Note _) = Just note
||| 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)
export export
main' : Options -> List Test -> IO ExitCode main' : Options -> List Test -> IO ExitCode
main' opts tests = do main' opts tests = do
@ -287,6 +347,7 @@ main' opts tests = do
then ExitSuccess then ExitSuccess
else ExitFailure 70 else ExitFailure 70
||| run tests and exit with an appropriate code
export export
main : Options -> List Test -> IO () main : Options -> List Test -> IO ()
main opts tests = exitWith !(main' opts tests) main opts tests = exitWith !(main' opts tests)

54
TAP/Options.idr
View File

@ -1,3 +1,4 @@
||| command line options
module TAP.Options module TAP.Options
import Data.String import Data.String
@ -7,25 +8,45 @@ import System.Console.GetOpt
%default total %default total
||| which TAP version to use for output.
||| - `V14` supports subtests
||| - `V13` flattens the tree before running it
public export public export
data TAPVersion = V13 | V14 data TAPVersion = V13 | V14
||| try to read a numeric TAP version number
export export
readVersion : String -> Maybe TAPVersion readVersion : String -> Maybe TAPVersion
readVersion "13" = Just V13 readVersion "13" = Just V13
readVersion "14" = Just V14 readVersion "14" = Just V14
readVersion _ = Nothing readVersion _ = Nothing
||| prints as just the number
export Show TAPVersion where show V13 = "13"; show V14 = "14" export Show TAPVersion where show V13 = "13"; show V14 = "14"
||| command line options
|||
||| apart from these there is also a usage message with
||| `-?`, `-h`, `--help`
public export public export
record Options where record Options where
constructor Opts constructor Opts
||| `-V`, `--version`:
||| which TAP version to output
version : TAPVersion version : TAPVersion
||| `-F`, `--filter`:
||| search for a substring in test or group names.
||| if it is present in a group name then all subtests are run
||| regardless of their own names
pattern : Maybe String pattern : Maybe String
||| `-c`, `--color`, `--colour`:
||| colour code test results and a few other things.
||| this is not TAP compliant so it is off by default.
color : Bool color : Bool
||| default options
||| (version 13 (because of `prove`), no filter, no colour)
export export
defaultOpts : Options defaultOpts : Options
defaultOpts = Opts { defaultOpts = Opts {
@ -34,11 +55,16 @@ defaultOpts = Opts {
color = False color = False
} }
||| value for each option.
||| i'm using the old idiom where each option is a function that updates
||| an accumulated record. with IO because of the error messages being printed
public export public export
Mod : Type Mod : Type
Mod = Options -> IO Options Mod = Options -> IO Options
||| print the given messages as TAP comments and then say `Bail out!`.
||| so the error is a valid TAP transcript too :3
export export
failureWith : List String -> IO a failureWith : List String -> IO a
failureWith msgs = do failureWith msgs = do
@ -46,6 +72,7 @@ failureWith msgs = do
putStrLn "\nBail out!" putStrLn "\nBail out!"
exitFailure exitFailure
private private
setTapVer : String -> Mod setTapVer : String -> Mod
setTapVer ver opts = setTapVer ver opts =
@ -54,10 +81,11 @@ setTapVer ver opts =
Nothing => failureWith ["unrecognised TAP version '\{ver}'"] Nothing => failureWith ["unrecognised TAP version '\{ver}'"]
private private
setPat : String -> Mod setFilter : String -> Mod
setPat str opts = pure $ {pattern := Just str} opts setFilter str opts = pure $ {pattern := Just str} opts
mutual mutual
||| option descriptions
export export
opts : List (OptDescr Mod) opts : List (OptDescr Mod)
opts = opts =
@ -74,7 +102,7 @@ mutual
MkOpt { MkOpt {
description = "only run tests containing STR in their group or label", description = "only run tests containing STR in their group or label",
shortNames = ['F'], longNames = ["filter"], shortNames = ['F'], longNames = ["filter"],
argDescr = ReqArg setPat "STR" argDescr = ReqArg setFilter "STR"
}, },
MkOpt { MkOpt {
description = "don't colour-code results (default)", description = "don't colour-code results (default)",
@ -88,16 +116,19 @@ mutual
} }
] ]
||| usage message
export export
usage : List String usage : List String
usage = assert_total $ "quox test suite" :: lines (usageInfo "" opts) usage = assert_total $ "quox test suite" :: lines (usageInfo "" opts)
||| interpret the result of `getOpt`
export export
makeOpts : List Mod -> IO Options makeOpts : List Mod -> IO Options
makeOpts = foldlM (\x, f => f x) defaultOpts makeOpts = foldlM (\x, f => f x) defaultOpts
||| like `getArgs` but skip the first one, which is the executable name
export export
getArgs1 : IO (List String) getArgs1 : IO (List String)
getArgs1 = getArgs1 =
@ -105,9 +136,20 @@ getArgs1 =
_ :: args => pure args _ :: args => pure args
[] => failureWith ["expected getArgs to start with exe name"] [] => failureWith ["expected getArgs to start with exe name"]
||| read & interpret the command line arguments
|||
||| [todo] allow unrecognised things and pass them back out
export export
getTestOpts : IO Options getTestOpts' : List String -> IO Options
getTestOpts = getTestOpts' args =
case getOpt Permute opts !getArgs1 of case getOpt Permute opts args of
MkResult opts [] [] [] => makeOpts opts MkResult opts [] [] [] => makeOpts opts
res => failureWith $ res.errors ++ usage res => failureWith $ res.errors ++ usage
||| interpret some command line arguments passed in
|||
||| [todo] allow unrecognised things and pass them back out
export
getTestOpts : IO Options
getTestOpts = getTestOpts' !getArgs1