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 E1 E2) ->> catch(E2) • eval(E1).
eraise : eval(raise) ->> fail.
epop : comp(F) • fail ->> fail.
ecatch : catch(E2) • fail ->> eval(E2).
eret : catch(E2) • return(V) ->> return(V).
eraise : eval(raise) ->> fail.
epop : comp(F) • fail ->> fail.
ecatch : catch(E2) • fail ->> eval(E2).
eret : catch(E2) • 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