0 | module Evince.App
 1 |
 2 | import Control.App
 3 | import Evince.Core
 4 | import Evince.Expectations
 5 |
 6 | ||| Run an App computation, capturing the typed error as Either.
 7 | export covering
 8 | tryApp : App (err :: Init) a -> IO (Either err a)
 9 | tryApp act = run $ handle act (\ok => pure (Right ok)) (\e => pure (Left e))
10 |
11 | ||| Passes if the App computation produces an error of the expected type.
12 | export covering
13 | mustError : Show err => App (err :: Init) a -> IO (TestResult ())
14 | mustError act = do
15 |   result <- tryApp act
16 |   case result of
17 |     Left _  => pure (Pass ())
18 |     Right _ => pure (Fail (Reason "expected error but succeeded"))
19 |
20 | ||| Passes if the App computation produces the specific error value.
21 | export covering
22 | mustErrorWith : (Show err, DecEq err) => App (err :: Init) a -> err -> IO (TestResult ())
23 | mustErrorWith act expected = do
24 |   result <- tryApp act
25 |   case result of
26 |     Left e  => pure (e `mustBe` expected)
27 |     Right _ => pure (Fail (Reason "expected error but succeeded"))
28 |