CMSC 221/321
Homework set 5
Due: Tuesday, Nov 16, 2010

5.0 [Reading] Browse Chapter 3 of Huttle, Transistions and Trees,
which covers simple arithmetic and boolean expressions in roughly the
way we have done them in the class notes, but with notational
differences.  Then read Chapter 4 on Basic Imperative Statements.

5.1 [10]. Complete the proof of the Preservation Lemma for TFun (Lemma 4.12
in Lectures 8 and 9). Include all the cases not treated in Lecture 9.

5.2 [20]. Complete the proof of the Progress Lemma for TFun (Lemma 4.13).
This means adding the case for Let.

5.3 [15]. Add pairs (binary products) to TFun and the projections Fst and
Snd as new forms of exprs:

   e ::=  ... | Fst(e) | Snd(e)

Modify a TFun[BSv] implementation (prog_4_1.sml) by adding support for
pairs and projections.  Take the opportunity to change the types of
the arithmetic and relational primops:

   Plus : (Int * Int) -> Int

so the primop application redexes become, e.g. App(Plus,(n1,n2))
instead of App(App(Plus,n1),n2).

5.4 [15]. Modify the TFun type checker from Hw 4.4 to handle pairs and
projections (with the modified primop types as suggested above in
Hw 5.3).