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

Sale!