Idris2Doc : Control.App

Control.App

(>>=) : SafeBindll' => Appea -> (a -> Appeb) -> Appeb

Fixity Declaration: infixl operator, level 1
App : {defaultMayThrow _ : Path} -> ListError -> Type -> Type
A type supports throwing and catching exceptions. See `interface Exception err e` for details.
@ l An implicit Path states whether the program's execution path is linear or might throw
exceptions. The default value is `MayThrow` which represents that the program might throw.
@ es A list of exception types that can be thrown. Constrained interfaces can be defined by
parameterising with a list of errors `es`.
Totality: total
Constructor: 
MkApp : (1 _ : ((1 _ : %World) -> AppRes (execTylet))) -> Appet
App1 : {defaultOne _ : Usage} -> ListError -> Type -> Type
Totality: total
Constructor: 
MkApp1 : (1 _ : ((1 _ : %World) -> App1Resut)) -> App1et
AppHasIO : Type
When type is present in app "errors" list, app is allowed to perform I/O.
Totality: total
Cont1Type : Usage -> Type -> Usage -> ListError -> Type -> Type
Error : Type
`Error` is a type synonym for `Type`, specify for exception handling.
Exception : Type -> ListError -> Type
Parameters: err, e
Methods:
throw : (ev : err) -> Appea
Throw an exception.
@ ev Value of the exception.
catch : (act : Appea) -> (k : ((ev : err) -> Appea)) -> Appea
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.

Implementation: 
HasErrees => Exceptionees
FileEx : Type
Totality: total
Constructors:
GenericFileEx : Int -> FileEx
FileReadError : FileEx
FileWriteError : FileEx
FileNotFound : FileEx
PermissionDenied : FileEx
FileExists : FileEx
Has : List (a -> Type) -> a -> Type
HasErr : Error -> ListError -> Type
Totality: total
Constructors:
Here : HasErre (e::es)
There : HasErrees -> HasErre (e'::es)
IOError : Type
Totality: total
Constructors:
GenericErr : String -> IOError
FileErr : FileEx -> IOError
Init : ListError
Path : Type
States whether the program's execution path is linear or might throw exceptions so that we can know
whether it is safe to reference linear resources.
Totality: total
Constructors:
MayThrow : Path
NoThrow : Path
PrimIO : ListError -> Type
Parameters: e
Methods:
primIO : IOa -> Appea
primIO1 : (1 act : IOa) -> App1ea
fork : (PrimIOe' => Appe' _) -> Appe _

Implementation: 
HasErrAppHasIOe => PrimIOe
SafeBind : Path -> Path -> Type
Totality: total
Constructors:
SafeSame : SafeBindll
SafeToThrow : SafeBindNoThrowMayThrow
State : a -> Type -> ListError -> Type
Totality: total
Constructor: 
MkState : IOReft -> Statetagte
Usage : Type
Totality: total
Constructors:
One : Usage
Any : Usage
app : (1 _ : Appea) -> App1ea
app1 : (1 _ : App1ea) -> Appea
bindApp1 : (1 _ : App1ea) -> (1 _ : Cont1Typeuau'eb) -> App1eb
bindL : Appea -> (1 _ : (a -> Appeb)) -> Appeb
catch : Exceptionerre => Appea -> (err -> Appea) -> Appea
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.
fork : PrimIOe => (PrimIOe' => Appe'Unit) -> AppeUnit
get : (0 tag : {_:1793}) -> Statetagte => Appet
handle : App (err::e) a -> (a -> Appeb) -> (err -> Appeb) -> Appeb
lift : Appea -> App (err::e) a
mapState : Statetagte -> Statetagt (eff::e)
modify : (0 tag : {_:1881}) -> Statetagte => (t -> t) -> AppeUnit
new : t -> (Statetagte => Appea) -> Appea
new1 : t -> (1 _ : (Statetagte => App1ea)) -> App1ea
noThrow : AppInita -> AppInita
primIO : PrimIOe => IOa -> Appea
primIO1 : PrimIOe => (1 _ : IOa) -> App1ea
put : (0 tag : {_:1835}) -> Statetagte => t -> AppeUnit
run : AppInita -> IOa
The only way provided by `Control.App` to run an App.
@ Init A concrete list of errors.
throw : Exceptionerre => err -> Appea
Throw an exception.
@ ev Value of the exception.