Funcons-beta : Returning.cbs | PLAIN | PDF
Returning
[ DatatypeFunconFunconFunconFunconreturningreturnedfinalise-returningreturnhandle-return ]
Meta-variablesT<:values
Datatypereturning ::= returned(_:values)
returned(V?) is a reason for abrupt termination.
Funconfinalise-returning(X:⇒T):⇒T∣null-type⇝finalise-abrupting(X)
finalise-returning(X) handles abrupt termination of X due to
executing return(V).
Funconreturn(V:T):⇒empty-type⇝abrupt(returned(V))
return(V) abruptly terminates all enclosing computations until it is
handled, then giving V. Note that V may be null-value.
Funconhandle-return(_:⇒T):⇒T
handle-return(X) first evaluates X. If X either terminates abruptly for
reason returned(V), or terminates normally with value V, it gives V.
RuleRuleRuleRulehandle-return(X)abrupted( )handle-return(X′)Xabrupted( )X′handle-return(X)abrupted( )VXabrupted(returned(V:values))X′handle-return(X)abrupted(V′)handle-return(X′)Xabrupted(V′:∼returning)X′handle-return(V:T)⇝V
←
↑
→