add TAP framework. if you could call it that

src/Quox/Error.idr

@@ -2,7 +2,7 @@ module Quox.Error
 
 import Data.List.Elem
 
-import Control.Monad.Identity
+import public Control.Monad.Identity
 import Control.Monad.Trans
 import Control.Monad.Reader
 import Control.Monad.Writer

tests/TAP.idr

@@ -0,0 +1,144 @@
+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
+toLines : Info -> List String
+toLines [] = []
+toLines xs =
+  "---" ::
+  concatMap (\(k, v) => "\{k}: |" :: map (indent 2) (lines v)) 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

tests/Tests.idr

@@ -0,0 +1,7 @@
+module Tests
+
+import TAP
+
+export main : IO ()
+main = run
+  [todo "write tests"]

tests/tests.ipkg

@@ -0,0 +1,6 @@
+package quox-tests
+
+executable = quox-tests
+main = Tests
+
+depends = base, contrib, quox