CBS-beta / Funcons-beta
Failing 
### 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