||| basic test framework using the TAP output format (https://testanything.org)
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
import Text.PrettyPrint.Prettyprinter

%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
Info : Type
Info = List (String, String)


||| result of running a test. or not doing so, in the case of `Skip` and `Todo`
private
data Result = Tried Bool Info | Skip String | Todo String

private
record TestBase where
  constructor MakeTest
  label : String
  run   : IO Result


||| render an `Info` value as a YAML document, including the `---`/`...`
||| delimiters. returns nothing at all if the `Info` is empty
export
toLines : Info -> List String
toLines [] = []
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


||| 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

||| represent a value as a string value in an `Info`.
public export
interface ToValue e where
  toValue : e -> String

||| an info of `()` prints nothing
export ToInfo () where toInfo () = []

export
(ToValue a, Foldable t) => ToInfo (t (String, a)) where
  toInfo = map (mapSnd toValue) . toList

export ToValue String where toValue = id
export ToValue (Doc a) where toValue = show . align


||| a test or group of tests
export
data Test
= One TestBase
| Group String (List Test)
| Note String


||| is this a real test or just a note?
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


||| promote a lazy value to an IO action that will run it
private
lazyToIO : Lazy a -> IO a
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
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

||| a pure test that returns `Left` for a failure or `Right` for a success
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.
||| `todo "<reason>" "<label>"` prints as `ok 1 - <label>  # todo <reason>`
export
todoWith : (reason, label : String) -> Test
todoWith {reason, label} = One $ MakeTest label $ pure $ Todo reason

||| a todo with no reason listed
export
todo : String -> Test
todo = todoWith ""

private
makeSkip : (reason, label : String) -> Test
makeSkip {reason, label} = One $ MakeTest label $ pure $ Skip reason

||| skip a test, with the reason given. skipping a `Note` doesn't do anything
export
skipWith : String -> Test -> Test
skipWith reason (One   t)   = makeSkip {reason, label = t.label}
skipWith reason (Group l _) = makeSkip {reason, label = l}
skipWith _      (Note  n)   = Note n

||| skip a test with no reason listed
export
skip : Test -> Test
skip = skipWith ""

||| test that an action 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
testThrowsIO : (ToInfo e, ToValue a) =>
               String -> (e -> Bool) -> EitherT e IO a -> Test
testThrowsIO label p act = One $ MakeTest label $ do
  case !(runEitherT act) of
       Left  err => if p err then result True () else result False err
       Right val => result False [("success", val)]

||| pure version of `testThrowsIO`
export
testThrows : (ToInfo e, ToValue a) =>
             String -> (e -> Bool) -> Lazy (Either e a) -> Test
testThrows label p act = testThrowsIO label p $ MkEitherT $ lazyToIO act

infix 1 :-
||| make a test group
export
(:-) : String -> List Test -> Test
(:-) = Group

||| stop immediately and run no more tests
export
bailOut : Test
bailOut = One $ MakeTest "bail out" $ do
  putStrLn "Bail out!"
  exitFailure

||| include a comment in the output. not counted as an actual test
export
note : String -> Test
note = Note



||| print the "1..n" header for a group of tests
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 : SnocList String -> String
        makePrefix = concatMap $ \s => "\{s} » "

mutual
  ||| flatten some tests, starting with the prefix given
  export
  flattenWith : SnocList String -> List Test -> List Test
  flattenWith pfx 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
  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]

||| flatten some tests
export
flatten : List Test -> List Test
flatten = flattenWith [<]

||| flatten a group, if it is one
export
flatten1 : Test -> List Test
flatten1 = flatten1With [<]


||| environment for correctly printing test output
private
record RunnerEnv where
  constructor RE
  ||| current indent level (for subtests)
  indent : Nat
  ||| whether to include control codes for colours
  color  : Bool

public export
record Results where
  constructor Res
  pass, fail, skip, todo : Nat

public export
zeroRes : Results
zeroRes = Res 0 0 0 0

private
Runner : Type -> Type
Runner = ReaderT RunnerEnv $ StateT Results IO

||| print some lines at the current indent level
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"

||| whether a result counts as a "success". todos and skips are successes
private
toBool : Result -> Bool
toBool (Tried ok _) = ok
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
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


||| colour a string, if colours are being used
private
col : Color -> String -> Runner String
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
putColor : Color -> String -> Runner ()
putColor c str = putIndentLines [!(col c str)]

||| green for success, red for failure
private
okCol : Bool -> Color
okCol True  = Green
okCol False = Red

||| print a test result line with the start highlighted in the given colour
private
putOk' : Color -> Bool -> Nat -> String -> Runner ()
putOk' c ok index label =
  putIndentLines [!(col c "\{isOk ok} \{show index}") ++ " - \{label}"]

||| print a result highlighted red or green according to whether it succeeded
private
putOk : Bool -> Nat -> String -> Runner ()
putOk ok = putOk' (okCol ok) ok

private
putComment : String -> Runner ()
putComment str = putIndentLines [!(col Magenta "# ") ++ str]

||| print a TAP version line
private
putVersion : TAPVersion -> Runner ()
putVersion ver = putColor Cyan "TAP version \{show ver}"

||| print comments at the end counting passes, failures, skips, and todos
private
putFooter : Runner ()
putFooter = do
  res <- get
  putComment "passed:  \{show res.pass}"
  putComment "failed:  \{show res.fail}"
  putComment "skipped: \{show res.skip}"
  putComment "todo:    \{show res.todo}"

||| run a test, print its line, and return whether it succeeded
private
run1' : (Nat, TestBase) -> Runner Bool
run1' (index, test) = do
  res <- liftIO test.run
  case res of
    Tried ok info => do
      modify $ \s : Results => if ok then {pass $= S} s else {fail $= S} s
      putOk ok index test.label
      local {indent $= plus 2} $ putIndentLines $ toLines info
    Skip reason => do
      modify $ \s : Results => {skip $= S} s
      putOk' Yellow True index "\{test.label}  # skip \{reason}"
    Todo reason => do
      modify $ \s : Results => {todo $= S} s
      putOk' Yellow False index "\{test.label}  # todo \{reason}"
  pure $ toBool res

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 $ putComment 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'


export
filterMatchStr : List String -> String -> List String
filterMatchStr pats label = filter (\p => not $ p `isInfixOf` label) pats

mutual
  ||| filter tests by whether a string occurs in their name or in the name of
  ||| any of their parent groups
  export
  filterMatch : List String -> List Test -> List Test
  filterMatch []   tests = tests
  filterMatch pats tests =
    mapMaybe (\t => filterMatch1 pats $ 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
  filterMatch1 : List String -> Test -> Maybe Test
  filterMatch1 pats test@(One base) = do
    guard $ null $ filterMatchStr pats base.label
    pure test
  filterMatch1 pats whole@(Group label tests) =
    case filterMatchStr pats label of
      []   => Just whole
      rest => do let res = filterMatch rest tests
                 guard $ any isRealTest res
                 pure $ Group label res
  filterMatch1 _ 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
main' : Options -> List Test -> IO ExitCode
main' opts tests = do
  let tests = filterMatch opts.pattern $
              case opts.version of V13 => flatten tests; V14 => tests
  res <- evalStateT zeroRes $ runReaderT (RE 0 opts.color) $ do
    putVersion opts.version
    res <- runList opts.skipComments tests
    putFooter
    pure res
  pure $ if res then ExitSuccess else ExitFailure 70

||| run tests and exit with an appropriate code
export
main : Options -> List Test -> IO ()
main opts tests = exitWith !(main' opts tests)