60 lines
1.2 KiB
Plaintext
60 lines
1.2 KiB
Plaintext
### Breaking
|
|
|
|
[
|
|
Datatype breaking
|
|
Funcon broken
|
|
Funcon finalise-breaking
|
|
Funcon break
|
|
Funcon handle-break
|
|
]
|
|
|
|
|
|
Meta-variables
|
|
T <: values
|
|
|
|
|
|
Datatype
|
|
breaking ::= broken
|
|
/*
|
|
`broken` is a reason for abrupt termination.
|
|
*/
|
|
|
|
|
|
Funcon
|
|
finalise-breaking(X:=>T) : =>T|null-type
|
|
~> finalise-abrupting(X)
|
|
/*
|
|
`finalise-breaking(X)` handles abrupt termination of `X` due to executing
|
|
`break`.
|
|
*/
|
|
|
|
|
|
Funcon
|
|
break : =>empty-type
|
|
~> abrupt(broken)
|
|
/*
|
|
`break` abruptly terminates all enclosing computations until it is handled.
|
|
*/
|
|
|
|
|
|
Funcon
|
|
handle-break(_:=>null-type) : =>null-type
|
|
/*
|
|
`handle-break(X)` terminates normally when `X` terminates abruptly for the
|
|
reason `broken`.
|
|
*/
|
|
Rule
|
|
X --abrupted( )-> X'
|
|
------------------------------------------------
|
|
handle-break(X) --abrupted( )-> handle-break(X')
|
|
Rule
|
|
X --abrupted(broken)-> _
|
|
---------------------------------------
|
|
handle-break(X) --abrupted( )-> null-value
|
|
Rule
|
|
X --abrupted(V:~breaking)-> X'
|
|
------------------------------------------------
|
|
handle-break(X) --abrupted(V)-> handle-break(X')
|
|
Rule
|
|
handle-break(null-value) ~> null-value
|