### Abruptly terminating

[
  Funcon stuck
  Entity abrupted
  Funcon finalise-abrupting
  Funcon abrupt
  Funcon handle-abrupt
  Funcon finally
]


Meta-variables
  T, T', T'' <: values


Funcon
  stuck : =>empty-type
/*
  `stuck` does not have any computation. It is used to represent the result of
  a transition that causes the computation to terminate abruptly.
*/


Entity
  _ --abrupted(_:values?)-> _
/*
  `abrupted(V)` in a label on a tranistion indicates abrupt termination for
  reason `V`. `abrupted( )` indicates the absence of abrupt termination.
*/


Funcon
  finalise-abrupting(X:=>T) : =>T|null-type
   ~> handle-abrupt(X, null-value)
/*
  `finalise-abrupting(X)` handles abrupt termination of `X` for any reason.
*/


Funcon
  abrupt(_:values) :=>empty-type
/*
  `abrupt(V)` terminates abruptly for reason `V`.
*/
Rule
  abrupt(V:values) --abrupted(V)-> stuck


Funcon
  handle-abrupt(_:T'=>T, _:T''=>T) : T'=>T
/*
  `handle-abrupt(X, Y)` first evaluates `X`. If `X` terminates normally with
  value `V`, then `V` is returned and `Y` is ignored. If `X` terminates abruptly
  for reason `V`, then `Y` is executed with `V` as `given` value.

  `handle-abrupt(X, Y)` is associative, with `abrupt(given)` as left and right
  unit. `handle-abrupt(X, else(Y, abrupt(given)))` ensures propagation of 
  abrupt termination for the given reason if `Y` fails
*/
Rule
                    X --abrupted( )-> X'
  --------------------------------------------------------
  handle-abrupt(X, Y) --abrupted( )-> handle-abrupt(X', Y)
Rule
                    X --abrupted(V:T'')-> X'
  ----------------------------------------------
  handle-abrupt(X, Y) --abrupted( )-> give(V, Y)
Rule
  handle-abrupt(V:T, Y) ~> V


Funcon
  finally(_:=>T, _:=>null-type) : =>T
/*
  `finally(X, Y)` first executes `X`. If `X` terminates normally with 
  value `V`, then `Y` is executed before terminating normally with value `V`.
  If `X` terminates abruptly for reason `V`, then `Y` is executed before
  terminating abruptly with the same reason `V`.
*/
Rule
              X --abrupted( )-> X'
  --------------------------------------------
  finally(X, Y) --abrupted( )-> finally(X', Y)
Rule
              X --abrupted(V:values)-> X'
  -----------------------------------------------------
  finally(X, Y) --abrupted()-> sequential(Y, abrupt(V))
Rule
  finally(V:T, Y) ~> sequential(Y,V)