Funcons-beta : Failing.cbs | PRETTY | PDF

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

← ↑ →