
  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 : App (err :: Init) a -> TestResultT IO ()
 14 | mustError act = do
 15 |   result <- lift (tryApp act)
 16 |   case result of
 17 |     Left _  => pure ()
 18 |     Right _ => mustFail "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 -> TestResultT IO ()
 23 | mustErrorWith act expected = do
 24 |   result <- lift (tryApp act)
 25 |   case result of
 26 |     Left e  => e `mustBe` expected
 27 |     Right _ => mustFail "expected error but succeeded"
 28 |