Homework # 7
due 2008/3/25

Typing Proofs

Complete the following proof tree using empty $O$ and $M$ mappings:

$$\sbox{\Above}{$\ldots$} \sbox{\Name}{[\textit{Name}]} \sbo... ... in if x == void then true else 0 fi end} : \ldots} \end{array}$$

Label all proof steps with the name of the appropriate rule in the CoolAid manual, Section 13.2.

Type Checking

Add type checking to your attribute grammar from Homework # 6. Recall that every expression (and branch) will have two attributes:

env The referencing environment (inherited). This environment contains all the information you need to perform name lookup in an expression. It will support all three namespaces: objects, methods and classes. Looking up an object will get a VarBinding*; looking up a class will get a class__class * and looking up a method will get a method_class *. You may also assume that there is a member function add_object (with two symbol parameters) that returns a new referencing environment for an inner scope in which the given identifier has the given type.

type The type of the expression (synthesized). The type will be a symbol that indicates the static type of the expression.

In this assignment, you will write the rules for types only, while assuming the rules for name resolution are complete.

You may also assume the following additional pieces of information were computed in the name resolution part:

binding

Both assignment expressions and object expressions will have a local attribute (like a local variable) named binding. This local attribute will have as value a pointer to an object of type VarBinding. You may assume that this class includes the member function get_type that returns the static type of the variable referred to in this node (the target of the assignment or the referent of the object expression).

method

Both dispatch and static dispatch nodes will have a local attribute names method that points to the statically selected method of the method call. You may assume that this object has appropriate member functions to access the list of formal parameters and the return type.

Before you write the attribute grammar, please answer the following questions:

• Why is type a synthesized attribute?
• What information is needed to compute the $\leq$ relationship for types?
• What kinds of errors are found?
• If you solved Homework # 6 correctly, you needed the type of some expressions to perform name resolution. If you solve this homework correctly, you will need the results of name resolution (the local attributes mentioned above) to compute the types of expressions. Give an example of this interdependence in a Cool program fragment. Why is the interdependence well-defined? Why doesn't it cause a circularity in the language definition of Cool ?

You may work in your PA4 groups for this part of Homework # 7. Each person in the group should turn in their own copy (which may be identical) which should include the names of the people working together.

Here's some rules to get you started:

cond(pred, then_exp, else_exp : Expression)
    type = then_exp.type else_expr.type
    unless pred.type = Boolean
      error "Predicate for ``if'' must be Boolean"

assign_expr(name : Symbol; expr : Expression)
    type = expr.type

    // Actually the following check is a name resolution
    // check, for Homework #6, not this homework:
    unless name != #self
      error « "Cannot assign to 'self'"

    unless expr.type binding->get_type()
      error « "type mismatch in assignment: " « expr.type
            « " not a subtype of " « binding->get_type()

You may assume the operators $\vee$ and $\leq$ are defined on symbols representing types (as seen in the previous example).

You only need to write the rules to define the type attribute and use it to give error messages You do not need to write rules for any other attributes.