[[pi |- newint: intloc exp]] =
allocate
[[pi |- lazy I=E: { I:theta }exp]] =
({ I = [[pi |- E:theta]] }, )
[[pi |- eager I=E: { I:tau }exp]] =
({ I = }, )
where (, ) = [[pi |- E:tauexp]]
[[pi |- I: tauexp]] = , where (I=)
in
[[pi |- I: tau]] = , where (I=) in
[[pi |- with E do E: theta]] =
[[pi -U- pi |- E: theta]](
-U- [[pi |- E: pi]])
[[pi |- with E do E: piexp]]
=
[[pi -U- pi |- E: piexp]](
-U- )
where (, ) = [[pi |- E: piexp]]
[[pi |- with E do E: store
exp]]
=
free (size-of )
where (, ) = [[pi |- E: piexp]]
and =
[[pi -U- pi |- E: store exp]](
-U- )