Go backward to Typing Rules Go up to Top Go forward to Denotational Semantics |
[[pi |- newint: intloc exp]]e s =
allocate s
[[pi |- lazy I=E: { I:theta }exp]]e s =
({ I = [[pi |- E:theta]]e }, s)
[[pi |- eager I=E: { I:tau }exp]]e s =
({ I = v }, s')
where (v, s') = [[pi |- E:tauexp]]e s
[[pi |- I: tauexp]]e s = v s, where (I=v)
in e
[[pi |- I: tau]]e s = v, where (I=v) in e
[[pi |- with E1 do E2: theta]]e s =
[[pi -U- pi1 |- E2: theta]](e
-U- [[pi |- E1: pi1]]e) s
[[pi |- with E1 do E2: pi2exp]]e
s =
[[pi -U- pi1 |- E2: pi2exp]](e
-U- e1) s1
where (e1, s1) = [[pi |- E1: pi1exp]]e s
[[pi |- with E1 do E2: store
exp]]e
s =
free (size-of s) s2
where (e1, s1) = [[pi |- E1: pi1exp]]e s
and s2 =
[[pi -U- pi1 |- E2: store exp]](e
-U- e1) s1