print totals at the end

TAP.idr

@@ -226,9 +226,18 @@ record RunnerEnv where
   ||| 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 IO
+Runner = ReaderT RunnerEnv $ StateT Results IO
 
 ||| print some lines at the current indent level
 private
@@ -285,11 +294,25 @@ 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
@@ -297,11 +320,14 @@ 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 =>
+    Skip reason => do
+      modify $ \s : Results => {skip $= S} s
       putOk' Yellow True index "\{test.label}  # skip \{reason}"
-       Todo reason =>
+    Todo reason => do
+      modify $ \s : Results => {todo $= S} s
       putOk' Yellow True index "\{test.label}  # todo \{reason}"
   pure $ toBool res
 
@@ -317,7 +343,7 @@ parameters (skipNotes : Bool)
       putOk res index label
       pure res
     run' (_, Note note) = do
-      unless skipNotes $ putIndentLines [!(col Magenta "# ") ++ note]
+      unless skipNotes $ putComment note
       pure True
 
     private
@@ -359,10 +385,12 @@ main' : Options -> List Test -> IO ExitCode
 main' opts tests = do
   let tests = filterMatch opts.pattern $
               case opts.version of V13 => flatten tests; V14 => tests
-  let act = do putVersion opts.version; runList opts.skipComments tests
+  res <- evalStateT zeroRes $ runReaderT (RE 0 opts.color) $ do
-  pure $ if !(runReaderT (RE 0 opts.color) act)
+    putVersion opts.version
-            then ExitSuccess
+    res <- runList opts.skipComments tests
-            else ExitFailure 70
+    putFooter
+    pure res
+  pure $ if res then ExitSuccess else ExitFailure 70
 
 ||| run tests and exit with an appropriate code
 export