add ToValue interface

This commit is contained in:
rhiannon morris 2023-03-24 21:56:25 +01:00
parent 48b14e5980
commit c33bb4e96d

17
TAP.idr
View file

@ -11,6 +11,7 @@ import Control.Monad.Reader
import Control.Monad.State
import Control.ANSI
import System
import Text.PrettyPrint.Prettyprinter
%default total
@ -52,10 +53,20 @@ 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 Show a => ToInfo (List (String, a)) where toInfo = map (map show)
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
@ -134,7 +145,7 @@ skip = skipWith ""
||| - if the body returns `Right val`, then the test fails with
||| `{success: val}`
export
testThrowsIO : (ToInfo e, Show a) =>
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
@ -143,7 +154,7 @@ testThrowsIO label p act = One $ MakeTest label $ do
||| pure version of `testThrowsIO`
export
testThrows : (ToInfo e, Show a) =>
testThrows : (ToInfo e, ToValue a) =>
String -> (e -> Bool) -> Lazy (Either e a) -> Test
testThrows label p act = testThrowsIO label p $ MkEitherT $ lazyToIO act