87 lines
2.2 KiB
Plaintext
87 lines
2.2 KiB
Plaintext
### Throwing
|
|
|
|
[
|
|
Datatype throwing
|
|
Funcon thrown
|
|
Funcon finalise-throwing
|
|
Funcon throw
|
|
Funcon handle-thrown
|
|
Funcon handle-recursively
|
|
Funcon catch-else-throw
|
|
]
|
|
|
|
|
|
Meta-variables
|
|
R, S, T, T', T'' <: values
|
|
|
|
|
|
Datatype
|
|
throwing ::= thrown(_:values)
|
|
/*
|
|
`thrown(V)` is a reason for abrupt termination.
|
|
*/
|
|
|
|
|
|
Funcon
|
|
finalise-throwing(X:=>T) : =>T|null-type
|
|
~> finalise-abrupting(X)
|
|
/*
|
|
`finalise-throwing(X)` handles abrupt termination of `X` due to
|
|
executing `throw(V)`.
|
|
*/
|
|
|
|
|
|
Funcon
|
|
throw(V:T) : =>empty-type
|
|
~> abrupt(thrown(V))
|
|
/*
|
|
`throw(V)` abruptly terminates all enclosing computations uTil it is handled.
|
|
*/
|
|
|
|
|
|
Funcon
|
|
handle-thrown(_:T'=>T, _:T''=>T) : T'=>T
|
|
/*
|
|
`handle-thrown(X, Y)` first evaluates `X`. If `X` terminates normally with
|
|
value `V`, then `V` is returned and `Y` is ignored. If `X` terminates abruptly
|
|
with a thrown eTity having value `V`, then `Y` is executed with `V` as
|
|
`given` value.
|
|
|
|
`handle-thrown(X, Y)` is associative, with `throw(given)` as unit.
|
|
`handle-thrown(X, else(Y, throw(given)))` ensures that if `Y` fails, the
|
|
thrown value is re-thrown.
|
|
*/
|
|
Rule
|
|
X --abrupted( )-> X'
|
|
--------------------------------------------------------
|
|
handle-thrown(X, Y) --abrupted( )-> handle-thrown(X', Y)
|
|
Rule
|
|
X --abrupted(thrown(V'':values))-> X'
|
|
----------------------------------------------
|
|
handle-thrown(X, Y) --abrupted( )-> give(V'', Y)
|
|
Rule
|
|
X --abrupted(V':~throwing)-> X'
|
|
---------------------------------------------------------
|
|
handle-thrown(X, Y) --abrupted(V')-> handle-thrown(X', Y)
|
|
Rule
|
|
handle-thrown(V:T, Y) ~> V
|
|
|
|
|
|
Funcon
|
|
handle-recursively(X:S=>T, Y:R=>T) : S=>T
|
|
~> handle-thrown(X, else(handle-recursively(Y, Y), throw(given)))
|
|
/*
|
|
`handle-recursively(X, Y)` behaves similarly to `handle-thrown(X, Y)`, except
|
|
that another copy of the handler attempts to handle any values thrown by `Y`.
|
|
Thus, many thrown values may get handled by the same handler.
|
|
*/
|
|
|
|
|
|
Funcon
|
|
catch-else-throw(P:values, Y:=>T) : =>T
|
|
~> else(case-match(P, Y), throw(given))
|
|
/*
|
|
`handle-thrown(X, catch-else-throw(P, Y))` handles those values thrown by `X`
|
|
that match pattern `P`. Other thrown values are re-thrown.
|
|
*/
|