155 lines
3.5 KiB
Idris
155 lines
3.5 KiB
Idris
module TAP
|
|
|
|
import public Quox.Error
|
|
|
|
import Data.String
|
|
import Data.List.Elem
|
|
import Control.Monad.Reader
|
|
import Control.Monad.State
|
|
import System
|
|
|
|
public export
|
|
Info : Type
|
|
Info = List (String, String)
|
|
|
|
private
|
|
data Result = Tried Bool Info | Skip String | Todo String
|
|
|
|
private
|
|
record TestBase where
|
|
constructor MakeTest
|
|
label : String
|
|
run : IO Result
|
|
|
|
|
|
private
|
|
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
|
|
|
|
private
|
|
toLines : Info -> List String
|
|
toLines [] = []
|
|
toLines xs = "---" :: concatMap toLines1 xs <+> ["..."]
|
|
|
|
|
|
public export interface ToInfo e where toInfo : e -> Info
|
|
|
|
export
|
|
All ToInfo es => ToInfo (OneOf es) where
|
|
toInfo (One Here value) = toInfo value
|
|
toInfo (One (There x) value) = toInfo (One x value)
|
|
|
|
export %inline ToInfo () where toInfo () = []
|
|
|
|
export
|
|
data Test = One TestBase | Group String (List Test)
|
|
|
|
|
|
export
|
|
testIO : (All ToInfo es, ToInfo a) => String -> ErrorT es IO a -> Test
|
|
testIO label act = One $ MakeTest label $ do
|
|
case !(runErrorT act) of
|
|
Left err => pure $ Tried False $ toInfo err
|
|
Right val => pure $ Tried True $ toInfo val
|
|
|
|
export %inline
|
|
test : (All ToInfo es, ToInfo a) => String -> Lazy (Error es a) -> Test
|
|
test label val =
|
|
testIO label $ MkErrorT $ primIO $ \w => MkIORes (runError val) w
|
|
|
|
export %inline
|
|
todoWith : String -> String -> Test
|
|
todoWith label reason = One $ MakeTest label $ pure $ Todo reason
|
|
|
|
export %inline
|
|
todo : String -> Test
|
|
todo label = todoWith label ""
|
|
|
|
export %inline
|
|
skipWith : String -> String -> Test
|
|
skipWith label reason = One $ MakeTest label $ pure $ Skip reason
|
|
|
|
export %inline
|
|
skip : String -> Test
|
|
skip label = skipWith label ""
|
|
|
|
infix 0 :-
|
|
export %inline
|
|
(:-) : String -> List Test -> Test
|
|
(:-) = Group
|
|
|
|
|
|
|
|
export %inline
|
|
header : List a -> String
|
|
header tests = "1..\{show $ length tests}"
|
|
|
|
|
|
private
|
|
Runner : Type -> Type
|
|
Runner = ReaderT Nat IO
|
|
|
|
private %inline
|
|
putIndentLines : List String -> Runner ()
|
|
putIndentLines xs = traverse_ (putStrLn . indent !ask) xs
|
|
|
|
private %inline
|
|
isOk : Bool -> String
|
|
isOk b = if b then "ok" else "not ok"
|
|
|
|
private %inline
|
|
toBool : Result -> Bool
|
|
toBool (Tried ok _) = ok
|
|
toBool _ = True
|
|
|
|
|
|
private
|
|
numbered : List a -> List (Nat, a)
|
|
numbered = go 1 where
|
|
go : Nat -> List a -> List (Nat, a)
|
|
go _ [] = []
|
|
go i (x :: xs) = (i, x) :: go (S i) xs
|
|
|
|
private
|
|
run1' : (Nat, TestBase) -> Runner Bool
|
|
run1' (index, test) = do
|
|
res <- liftIO test.run
|
|
case res of
|
|
Tried ok info => do
|
|
putIndentLines ["\{isOk ok} \{show index} - \{test.label}"]
|
|
local (plus 2) $ putIndentLines $ toLines info
|
|
Skip reason => putIndentLines
|
|
["ok \{show index} - \{test.label} # skip \{reason}"]
|
|
Todo reason => putIndentLines
|
|
["ok \{show index} - \{test.label} # todo \{reason}"]
|
|
pure $ toBool res
|
|
|
|
mutual
|
|
private
|
|
run' : (Nat, Test) -> Runner Bool
|
|
run' (index, One test) = run1' (index, test)
|
|
run' (index, Group label tests) = do
|
|
putIndentLines ["# Subtest: \{label}"]
|
|
res <- local (plus 4) $ runList tests
|
|
putIndentLines ["\{isOk res} \{show index} - \{label}"]
|
|
pure res
|
|
|
|
private
|
|
runList : List Test -> Runner Bool
|
|
runList tests = do
|
|
putIndentLines [header tests]
|
|
all id <$> traverse run' (numbered tests)
|
|
|
|
|
|
export
|
|
run : List Test -> IO ExitCode
|
|
run tests = do
|
|
putStrLn "TAP version 14"
|
|
pure $ if !(runReaderT 0 $ runList tests)
|
|
then ExitSuccess
|
|
else ExitFailure 70
|