### Failing [ Datatype failing Funcon failed Funcon finalise-failing Funcon fail Funcon else Funcon else-choice Funcon checked Funcon check-true ] Meta-variables T <: values Datatype failing ::= failed /* `failed` is a reason for abrupt termination. */ Funcon finalise-failing(X:=>T) : =>T|null-type ~> finalise-abrupting(X) /* `finalise-failing(X)` handles abrupt termination of `X` due to executing `fail`. */ Funcon fail : =>empty-type ~> abrupt(failed) /* `fail` abruptly terminates all enclosing computations until it is handled. */ Funcon else(_:=>T, _:(=>T)+) : =>T /* `else(X1, X2, ...)` executes the arguments in turn until either some `Xi` does *not* fail, or all arguments `Xi` have been executed. The last argument executed determines the result. `else(X, Y)` is associative, with unit `fail`. */ Rule X --abrupted( )-> X' -------------------------------------- else(X, Y) --abrupted( )-> else(X', Y) Rule X --abrupted(failed)-> _ --------------------------------- else(X, Y) --abrupted( )-> Y Rule X --abrupted(V:~failing)-> X' -------------------------------------- else(X, Y) --abrupted(V)-> else(X', Y) Rule else(V:T, Y) ~> V Rule else(X, Y, Z+) ~> else(X, else(Y, Z+)) Funcon else-choice(_:(=>T)+) : =>T /* `else-choice(X,...)` executes the arguments in any order until either some `Xi` does *not* fail, or all arguments `Xi` have been executed. The last argument executed determines the result. `else(X, Y)` is associative and commutative, with unit `fail`. */ Rule else-choice(W*, X, Y, Z*) ~> choice(else(X, else-choice(W*, Y, Z*), else(Y, else-choice(W*, X, Z*)))) Rule else-choice(X) ~> X Funcon check-true(_:booleans) : =>null-type Alias check = check-true /* `check-true(X)` terminates normally if the value computed by `X` is `true`, and fails if it is `false`. */ Rule check-true(true) ~> null-value Rule check-true(false) ~> fail Funcon checked(_:(T)?) : =>T /* `checked(X)` fails when `X` gives the empty sequence of values `( )`, representing that an optional value has not been computed. It otherwise computes the same as `X`. */ Rule checked(V:T) ~> V Rule checked( ) ~> fail