Exceptions

Robert J. Simmons, Frank Pfenning

This examples is derived from Figure 10 in Substructural Operational Semantics as Ordered Logic Programming.

Exceptions

etry   : eval(try E₁ E₂) ->> catch(E₂) • eval(E₁).
eraise : eval(raise) ->> fail.
epop   : comp(F) • fail ->> fail.
ecatch : catch(E₂) • fail ->> eval(E₂).
eret   : catch(E₂) • return(V) ->> return(V).

Example trace

%trace * eval(try raise (try raise (try raise raise))).

eval(try raise (try raise (try raise raise)))

catch(try raise (try raise raise))•eval(raise)

catch(try raise (try raise raise))•fail

eval(try raise (try raise raise))

catch(try raise raise)•eval(raise)

catch(try raise raise)•fail

eval(try raise raise)

catch(raise)•eval(raise)

catch(raise)•fail

eval(raise)

fail