Semantics of Parameter Lists
- Defined via semantics of declarations:
- Abstraction:
-
[[pi |- define I(F)=U: {I:pi1
-> theta}dec]]e s
= ({I=p}, s)
where p e1 s1 =
[[pi -U- pi1 |- U:
theta]](e -U- e1) s1
and pi1 = type-attrs(F)
- Invocation:
-
[[pi |- invoke I(D): theta]]e s = p e1 s1
where (e1, s1) = [[pi |- D: pi1dec]]e s
and (I=p) in e
- Store at point of invocation is supplied to actual parameters.
- Abstractions are evaluated lazily, store is ignored.
- Abstractions are evaluated eagerly, store is used.
Correspondence is forced upon language!
Author: Wolfgang Schreiner
Last Modification: May 7, 1998