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 ?