The general form a type checking rule is:
The rule for object identifiers is simply that if the environment
assigns an identifier type , then has type .
The rule for assignment to a variable is more complex:
The type rules for constants are all easy:
There are two cases for new, one for new SELF_TYPE and
one for any other form:
Dispatch expressions are the most complex to type check.
To type check a dispatch, each of the subexpressions must first be type checked. The type of determines which declaration of the method is used. The argument types of the dispatch must conform to the declared argument types. Note that the type of the result of the dispatch is either the declared return type or in the case that the declared return type is . The only difference in type checking a static dispatch is that the class of the method is given in the dispatch, and the type must conform to .
The type checking rules for if and {-}
expressions are straightforward. See Section 7.5 for
the definition of the operation.
The let rule has some interesting aspects.
Each branch of a case is type checked in an environment where variable has type . The type of the entire case is the join of the types of its branches. The variables declared on each branch of a case must all have distinct types.
With the exception of the rule for equality,
the type checking rules for the primitive
logical and arithmetic operations are easy.
The wrinkle in the rule for equality is that any types may be
freely compared except Int, String and Bool, which
may only be compared with objects of the same type. The cases for
< and <= are similar to the rule for equality.
The final cases are type checking rules for attributes and methods.
For a class , let the object environment give the types of all
attributes of (including any inherited attributes). More formally,
if is an attribute (inherited or not) of , and the declaration of
is , then
The method environment is global to the entire program and defines for every class the signatures of all of the methods of (including any inherited methods).
The two rules for type checking attribute defininitions are similar
the rules for let. The essential difference is that
attributes are visible within their initialization expressions.
Note that self is bound in the initialization.
The rule for typing methods checks the body of the method in an environment where is extended with bindings for the formal parameters and self. The type of the method body must conform to the declared return type.
The order in which these other checks are performed is not specified. If a Cool program contains both an inheritance cycle and also a class htat inherits from String, the Cool compiler may report whichever error it prefers.