More reliable exception handling in Control.App

Convert `App.Control.Exception` interface to an alias to `HasErr`.

Probably `Exception` interface need to be deprecated or removed.

Note similar problem exists with `PrimIO` calling `PrimIO, Exception`,
also need to be fixed.

Fix this scenario:

```
throwBoth : Has [Exception String, Exception Int] es => App es ()

throwOne : Has [Exception Int] es => App es Int
throwOne {es} = handle {err = String} {e = es} throwBoth (\r => pure 1) (\e => pure 3)
```

With this commit it works, before this commit it failed with:

```
Error: While processing right hand side of throwOne. Can't find an implementation for Exception Int (String :: es).

TestException.idr:8:48--8:57
   |
 8 | throwOne {es} = handle {err = String} {e = es} throwBoth (\r => pure 1) (\e => pure 3)
   |                                                ^^^^^^^^^
```
This commit is contained in:
Stiopa Koltsov 2021-02-02 19:42:03 +00:00 committed by G. Allais
parent 9c63e90fd2
commit 8fd58b3bdd
6 changed files with 24 additions and 15 deletions

View File

@ -263,17 +263,10 @@ new val prog
MkApp res = prog @{st} in
res
||| An alias for `HasErr`.
public export
interface Exception err e where
||| Throw an exception.
||| @ ev Value of the exception.
throw : (ev : err) -> App e a
||| Use with a given computation to do exception-catching.
||| If any exception is raised then the handler is executed.
||| @ act The computation to run.
||| @ k Handler to invoke if an exception is raised.
||| @ ev Value of the exception passed as an argument to the handler.
catch : (act : App e a) -> (k : (ev : err) -> App e a) -> App e a
Exception : Error -> List Error -> Type
Exception = HasErr
findException : HasErr e es -> e -> OneOf es MayThrow
findException Here err = First err
@ -284,10 +277,11 @@ findError Here (First err) = Just err
findError (There p) (Later q) = findError p q
findError _ _ = Nothing
export
HasErr e es => Exception e es where
throw err = MkApp $ MkAppRes (Left (findException %search err))
catch (MkApp prog) handler
throw : HasErr err es => err -> App es a
throw err = MkApp $ MkAppRes (Left (findException %search err))
catch : HasErr err es => App es a -> (err -> App es a) -> App es a
catch (MkApp prog) handler
= MkApp $
prim_app_bind prog $ \res =>
case res of

View File

@ -286,7 +286,8 @@ templateTests = MkTestPool "Test templates" [] Nothing
-- available.
baseLibraryTests : TestPool
baseLibraryTests = MkTestPool "Base library" [Chez, Node] Nothing
[ "system_file001"
[ "control_app001"
, "system_file001"
, "system_info_os001"
, "system_system"
, "data_bits001"

View File

@ -0,0 +1,8 @@
module TestException
import Control.App
throwBoth : Has [Exception String, Exception Int] es => App es ()
throwOne : Has [Exception Int] es => App es Int
throwOne {es} = handle {err = String} {e = es} throwBoth (\r => pure 1) (\e => pure 3)

View File

@ -0,0 +1,3 @@
1/1: Building TestException (TestException.idr)
TestException>
Bye for now!

View File

3
tests/base/control_app001/run Executable file
View File

@ -0,0 +1,3 @@
$1 --no-color --console-width 0 --no-banner TestException.idr < input
rm -rf build