WORKED EXAMPLE QUESTION 4: -------------------------------------------------------------- let D0 == int x; proc p = int y; y = x end; proc q = int x; call p end; let C0 = = call q P[[ P0 ]] = lam s. B[[ D0 C0 ]]initenv s = let (e', s') = D[[ D0 ]]{} s in C[[ C0 ]]e' s' Consider the D0 part: D[[ int x; proc p = ...; proc q = ... ]]{} s = let (d', s') = D[[ int x ]] {} s in D[[ proc p = ...; proc q = ... ]]d' s' Now, D[[ int x ]] {} s = let (newloc, news) = allocate(s) in (bind(x, inLoc(newloc), e), news) = let (newloc, news) = (m, s+[0]) in (bind(x, inLoc(newloc), e), news) where m is the index to [0] = (bind(x, inLoc(m), {}), s+[0]) = ({x: inLoc(m)}, s+[0]) Reconsider the D0 part: = let (d', s') = ({x: inLoc(m)}, s+[0]) in D[[ proc p = ...; proc q = ... ]]d' s' = D[[ proc p = ...; proc q = ... ]] {x: inLoc(m)} s+[0] The declarations of p and q place bindings in the environment. After some calculations we have that: D[[ D0 ]]{} s = (expq, s0), where expq = { x: inLoc(m), p: inProc(B[[ int y; y = x ]]ex), q: inProc(B[[ int x; call p ]]exp) } exp = { x: inLoc(m), p: inProc(B[[ int y; y = x ]]ex) } ex = { { x: inLoc(m) } and s0 = s+[0] Now, to finish: P[[ P0 ]] = lam s. B[[ D0 C0 ]]initenv s = lam s. C[[ call q ]]expq s0 The semantics of call q does a find(q, expq): = lam s. B[[ int x; call p ]]exp s0 = ... compute D[[ int x ]]exp s0, like above ... : = lam s. C[[ call p ]]epLocalX s0+[0] where epLocalX = { x: inLoc(n), p: inProc(B[[ int y; y = x ]]ex) } where n is the index to [0] in s0+[0] x got changed to the environment, and another cell was allocated in the store: The call p extracts p's meaning in epLocalX: = lam s. B[[ int y; y = x ]]ex s00 where s00 = s0+[0] = s+[0]+[0] note that p's body uses environment ex, not epLocalX = ... compute D[[ int y ]]ex s00 ... : = lam s. C[[ y = x ]]exLocalY s000 where exLocalY = { x: inLoc(n), y: inLoc(r) } where r is the index to [0] in s000 and s000 = s00+[0] = ... = lam s. update(r, E[[ x ]]exLocalY s000, s000) = lam s. update(r, 0, s000) = lam s. s000 Finished. The meaning of this program is to allocate three cells in storage! The semantics of B[[ D ; C ]] should be repaired to "mark" the store prior to the calculation of D[[ D ]], then calculate C[[ C ]], then "release" (pop) the store back to its "marked" length. This would deallocate local vars declared in blocks: B[[D ; C ]] = lam e. lam s. let length = mark s let (e', s') = D[[D]]e s in check((lam s''. release(length, s'')), C[[ C ]]e' s') What are the definitions of mark and release ?