### 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
*/
Funcon finalise-failing(X:=>T) : =>T|null-type
~> finalise-abrupting(X)
*/
Funcon fail : =>empty-type
~> abrupt(failed)
*/
Funcon
else(_:=>T, _:(=>T)+) : =>T
*/
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
*/
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
*/
Rule
check-true(true) ~> null-value
Rule
check-true(false) ~> fail
Funcon
checked(_:(T)?) : =>T
*/
Rule
checked(V:T) ~> V
Rule
checked( ) ~> fail
/*
`failed` is a reason for abrupt termination.