HW 10
COSC 4780
Complete the interpreter (code provided) to support procedures parametrized
by expressions under call-by-name (lazy) semantics. The syntax, typing
rules and semantic equations for this extension are found in Schmidt. You
will need to extend meaning of declaration to properly handle procedure
declarations with lazily evaluated τ exp parameters that will be evaluated
lazily.
The equations to implement are on page 801
.
[[π ` proc I1(I2 : τexp) = C : {I1 : τexp → comm}dec]] e s = ({I1 : p}, s)
where p f s0 = [[π∪−{I2 : τexp} ` C : comm]](e∪−{I2 : f})s
0
This rule becomes two rules when we specialize τ to be int or bool as
follows:
[[π ` proc I1(I2 : intexp) = C : {I1 : intexp → comm}dec]] e s = ({I1 : p}, s)
where p f s0 = [[π∪−{I2 : intexp} ` C : comm]](e∪−{I2 : f})s
0
[[π ` proc I1(I2 : boolexp) = C : {I1 : boolexp → comm}dec]] e s = ({I1 : p}, s)
where p f s0 = [[π∪−{I2 : boolexp} ` C : comm]](e∪−{I2 : f})s
0
For the first rule, you update the proc int environment and for the
second you must update the proc bool environment.
Note that for type assignments, π1∪−π2 is implemented by the following
ML code: (bar union ta pi1 pi2) and for environments e1∪−e2 is implemented by the call (union env e1 e2).
For completeness I include the semantics of the call here as well (though
it is implemented in the code provided).
[[π ` call I1(E) : comm]] e s = p f s
where hI1, pi ∈ e and f s0 = [[π ` E : τexp]] e s
1Note that the line above the semantic equations on page 80 should say
p ∈ [[τexp]] → [[comm]]
The inclusion of the Env π argument to p is incorrect. You can see this in the definition
of the type env in the code.
1
