exceptions and coercions
Suresh Jagannathan
suresh@research.nj.nec.com
Thu, 19 Aug 1999 16:15:43 -0400
I've finished tex'ing the safety=>soundness proof
and the proof of correctness for the closure convertor.
I've now started tex'ing the CPS language and small-step
transition semantics.
I've got a question about exceptions though. Given
let x = e1 in handle z => e2
in e
I have the flow rule for exceptions being:
F(x) >= F(last(e1)) and F(last(e)) >= F(last(e2))
However, our notes indicate the closure converted
translation as being:
let y1 = [e1]
in X(y1,F(last(e1)),F(last(x)))
handle z =>
let y2 = [e2]
in X(y2,F(last(e2)),F(last(x)))
I'm confused about why the coercion inserted for the
handler coerces between F(last(e2)) and F(last(x));
shouldn't it be X(y2,F(last(e2)),F(last(e)))?
-- sj