module TAP import public Quox.Error import Data.String import Data.List.Elem import Control.Monad.Reader import Control.Monad.State 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 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 header : List a -> String header tests = "1..\{show $ length tests}" private Runner : Type -> Type Runner = ReaderT Nat IO private putIndentLines : List String -> Runner () putIndentLines xs = traverse_ (putStrLn . indent !ask) xs private isOk : Bool -> String isOk b = if b then "ok" else "not ok" private 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 => putIndentLines $ "\{isOk ok} \{show index} - \{test.label}" :: 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 () run tests = do putStrLn "TAP version 14" ignore $ runReaderT 0 $ runList tests