From 25a779eae40489e17a5ec35445f26f26ce0dc9f6 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Thu, 26 May 2022 15:41:48 +0200
Subject: [PATCH] docstrings

---
 TAP.idr         | 99 +++++++++++++++++++++++++++++++++++++++----------
 TAP/Options.idr | 54 ++++++++++++++++++++++++---
 2 files changed, 128 insertions(+), 25 deletions(-)

diff --git a/TAP.idr b/TAP.idr
index 8e61271..a83f976 100644
--- a/TAP.idr
+++ b/TAP.idr
@@ -1,3 +1,4 @@
+||| basic test framework using the TAP output format (https://testanything.org)
 module TAP
 
 import public TAP.Options
@@ -14,10 +15,14 @@ import System
 %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
 
@@ -28,27 +33,32 @@ record TestBase where
   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
+||| 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 <+> ["..."]
+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
 
 
-public export interface ToInfo e where toInfo : e -> Info
+||| 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
 
+||| an info of `()` prints nothing
 export ToInfo () where toInfo () = []
 
 export Show a => ToInfo (List (String, a)) where toInfo = map (map show)
 
 
+||| a test or group of tests
 export
 data Test
 = One TestBase
@@ -56,6 +66,7 @@ data Test
 | Note String
 
 
+||| is this a real test or just a note?
 export
 isRealTest : Test -> Bool
 isRealTest (One   _)   = True
@@ -67,10 +78,15 @@ 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
@@ -78,32 +94,45 @@ testIO label act = One $ MakeTest label $ do
        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. the reason is the first argument, e.g.
+||| `todo "<reason>" "<label>"` prints as `ok 1 - <label>  # todo <reason>`
 export
 todoWith : String -> String -> Test
-todoWith label reason = One $ MakeTest label $ pure $ Todo reason
+todoWith reason label = One $ MakeTest label $ pure $ Todo reason
 
+||| a todo with no reason listed
 export
 todo : String -> Test
-todo label = todoWith label ""
+todo = todoWith ""
 
 private
 makeSkip : String -> String -> Test
 makeSkip label reason = One $ MakeTest label $ pure $ Skip reason
 
+||| skip a test, with the reason given. skipping a `Note` doesn't do anything
 export
-skipWith : Test -> String -> Test
-skipWith (One   t)   reason = makeSkip t.label reason
-skipWith (Group l _) reason = makeSkip l       reason
-skipWith (Note  n)   _      = Note n
+skipWith : String -> Test -> Test
+skipWith reason (One   t)   = makeSkip t.label reason
+skipWith reason (Group l _) = makeSkip l       reason
+skipWith _      (Note  n)   = Note n
 
+||| skip a test with no reason listed
 export
 skip : Test -> Test
-skip test = skipWith test ""
+skip = skipWith ""
 
+||| test that an expression 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
 testThrows : (ToInfo e, Show a) =>
              String -> (e -> Bool) -> Lazy (Either e a) -> Test
@@ -113,22 +142,26 @@ testThrows label p act = One $ MakeTest label $ do
        Right val => result False [("success", val)]
 
 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 =
@@ -142,37 +175,45 @@ withPrefix pfx = One . {label $= (makePrefix pfx ++)}
   where 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
 
-
 private
 Runner : Type -> Type
 Runner = ReaderT RunnerEnv IO
 
+||| print some lines at the current indent level
 private
 putIndentLines : List String -> Runner ()
 putIndentLines xs = traverse_ (putStrLn . indent (!ask).indent) xs
@@ -181,12 +222,15 @@ 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
@@ -197,32 +241,39 @@ numbered p = go 1 where
            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
 
+||| print a TAP version line
 private
 putVersion : TAPVersion -> Runner ()
 putVersion ver = putColor Cyan "TAP version \{show ver}"
 
+||| run a test, print its line, and return whether it succeeded
 private
 run1' : (Nat, TestBase) -> Runner Bool
 run1' (index, test) = do
@@ -238,6 +289,7 @@ run1' (index, test) = do
   pure $ toBool res
 
 mutual
+  ||| run a test or group
   private
   run' : (Nat, Test) -> Runner Bool
   run' (index, One test) = run1' (index, test)
@@ -251,6 +303,7 @@ mutual
     pure True
 
   private
+  ||| run several tests
   runList : List Test -> Runner Bool
   runList tests = do
     putColor Cyan $ header tests
@@ -259,12 +312,16 @@ mutual
 
 
 mutual
+  ||| filter tests by whether a string occurs in their name or in the name of
+  ||| any of their parent groups
   export
   filterMatch : Maybe String -> List Test -> List Test
   filterMatch Nothing    tests = tests
   filterMatch (Just pat) tests =
     mapMaybe (\t => filterMatch1 pat (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 : String -> Test -> Maybe Test
   filterMatch1 pat test@(One base) =
@@ -277,6 +334,9 @@ mutual
   filterMatch1 pat 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
@@ -287,6 +347,7 @@ main' opts tests = do
             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)
diff --git a/TAP/Options.idr b/TAP/Options.idr
index 8212970..fd9b5bd 100644
--- a/TAP/Options.idr
+++ b/TAP/Options.idr
@@ -1,3 +1,4 @@
+||| command line options
 module TAP.Options
 
 import Data.String
@@ -7,25 +8,45 @@ import System.Console.GetOpt
 %default total
 
 
+||| which TAP version to use for output.
+||| - `V14` supports subtests
+||| - `V13` flattens the tree before running it
 public export
 data TAPVersion = V13 | V14
 
+||| try to read a numeric TAP version number
 export
 readVersion : String -> Maybe TAPVersion
 readVersion "13" = Just V13
 readVersion "14" = Just V14
 readVersion _    = Nothing
 
+||| prints as just the number
 export Show TAPVersion where show V13 = "13"; show V14 = "14"
 
 
+||| command line options
+|||
+||| apart from these there is also a usage message with
+||| `-?`, `-h`, `--help`
 public export
 record Options where
   constructor Opts
+  ||| `-V`, `--version`:
+  ||| which TAP version to output
   version : TAPVersion
+  ||| `-F`, `--filter`:
+  ||| search for a substring in test or group names.
+  ||| if it is present in a group name then all subtests are run
+  ||| regardless of their own names
   pattern : Maybe String
+  ||| `-c`, `--color`, `--colour`:
+  ||| colour code test results and a few other things.
+  ||| this is not TAP compliant so it is off by default.
   color   : Bool
 
+||| default options
+||| (version 13 (because of `prove`), no filter, no colour)
 export
 defaultOpts : Options
 defaultOpts = Opts {
@@ -34,11 +55,16 @@ defaultOpts = Opts {
   color   = False
 }
 
+||| value for each option.
+||| i'm using the old idiom where each option is a function that updates
+||| an accumulated record. with IO because of the error messages being printed
 public export
 Mod : Type
 Mod = Options -> IO Options
 
 
+||| print the given messages as TAP comments and then say `Bail out!`.
+||| so the error is a valid TAP transcript too :3
 export
 failureWith : List String -> IO a
 failureWith msgs = do
@@ -46,6 +72,7 @@ failureWith msgs = do
   putStrLn "\nBail out!"
   exitFailure
 
+
 private
 setTapVer : String -> Mod
 setTapVer ver opts =
@@ -54,10 +81,11 @@ setTapVer ver opts =
        Nothing => failureWith ["unrecognised TAP version '\{ver}'"]
 
 private
-setPat : String -> Mod
-setPat str opts = pure $ {pattern := Just str} opts
+setFilter : String -> Mod
+setFilter str opts = pure $ {pattern := Just str} opts
 
 mutual
+  ||| option descriptions
   export
   opts : List (OptDescr Mod)
   opts =
@@ -74,7 +102,7 @@ mutual
       MkOpt {
         description = "only run tests containing STR in their group or label",
         shortNames  = ['F'], longNames = ["filter"],
-        argDescr    = ReqArg setPat "STR"
+        argDescr    = ReqArg setFilter "STR"
       },
       MkOpt {
         description = "don't colour-code results (default)",
@@ -88,16 +116,19 @@ mutual
       }
     ]
 
+  ||| usage message
   export
   usage : List String
   usage = assert_total $ "quox test suite" :: lines (usageInfo "" opts)
 
 
+||| interpret the result of `getOpt`
 export
 makeOpts : List Mod -> IO Options
 makeOpts = foldlM (\x, f => f x) defaultOpts
 
 
+||| like `getArgs` but skip the first one, which is the executable name
 export
 getArgs1 : IO (List String)
 getArgs1 =
@@ -105,9 +136,20 @@ getArgs1 =
        _ :: args => pure args
        []        => failureWith ["expected getArgs to start with exe name"]
 
+
+||| read & interpret the command line arguments
+|||
+||| [todo] allow unrecognised things and pass them back out
 export
-getTestOpts : IO Options
-getTestOpts =
-  case getOpt Permute opts !getArgs1 of
+getTestOpts' : List String -> IO Options
+getTestOpts' args =
+  case getOpt Permute opts args of
        MkResult opts [] [] [] => makeOpts opts
        res                    => failureWith $ res.errors ++ usage
+
+||| interpret some command line arguments passed in
+|||
+||| [todo] allow unrecognised things and pass them back out
+export
+getTestOpts : IO Options
+getTestOpts = getTestOpts' !getArgs1