next up previous
Next: Type Equivalence Up: Compiler Theory: Type Checking Previous: Type Systems

Specification of a Simple Type Checker

We consider the language generated by the following grammar.

P $ \longmapsto$ DE
D $ \longmapsto$ DD
D $ \longmapsto$ $ \bf id$ :  T
T $ \longmapsto$ $ \bf character$
T $ \longmapsto$ $ \bf integer$
T $ \longmapsto$ $ \bf array$[$ \bf num$]$ \bf of$T
T $ \longmapsto$ $ \uparrow$ T
T $ \longmapsto$ T $ \rightarrow$ T
E $ \longmapsto$ $ \bf literal$
E $ \longmapsto$ $ \bf num$
E $ \longmapsto$ $ \bf id$
E $ \longmapsto$ E $ \bf mod$ E
E $ \longmapsto$ E[E]
E $ \longmapsto$ $ \uparrow$ E
E $ \longmapsto$ E(E)
We consider the following attributes.
Grammar symbol Synthesized attribute Inherited attribute
E E.type (type expression)  
T T.type (type expression)  
$ \bf id$ $ \bf id$.entry $ \in$ $ \mbox{${\mathbb Z}$}$  
$ \bf num$ $ \bf num$.val $ \in$ $ \mbox{${\mathbb Z}$}$  
$ \bf literal$ $ \bf literal$.val character  
First we give a translation scheme that saves the type of an identifier.
D $ \longmapsto$ $ \bf id$ :  T { addtype(id.entry, T.type) }
T $ \longmapsto$ $ \bf character$ { T.type := $ \bf character$ }
T $ \longmapsto$ $ \bf integer$ { T.type := $ \bf integer$ }
T $ \longmapsto$ $ \bf array$[$ \bf num$]$ \bf of$T1 { T.type := array (0 ... $ \bf num$.val - 1, T1.type) }
T $ \longmapsto$ $ \uparrow$ T1 { T.type := pointer(T1) }
T $ \longmapsto$ T1 $ \rightarrow$ T2 { T.type := (T1.type  $ \rightarrow$  T2.type)
Note that because of the rule

D  $\displaystyle \longmapsto$   $\displaystyle \bf id$ :  T {addtype($\displaystyle \bf id$.entry, T.type)} (1)

the types of all identifiers are saved in the symbol table before the expression generated by E is checked. Now we give a translation scheme for type checking rules for expressions. We assume that lookup retrieves the type information about an entry of the symbol table.
E $ \longmapsto$ $ \bf literal$ { E.type := $ \bf character$ }
E $ \longmapsto$ $ \bf num$ { E.type := $ \bf integer$ }
E $ \longmapsto$ $ \bf id$ { E.type := lookup(id.entry) }
E $ \longmapsto$ E1 $ \bf mod$ E2 { E.type := if E1.type = $ \bf integer$
    and E2.type = $ \bf integer$
    then $ \bf integer$
    else $ \bf type\_error$ }
E $ \longmapsto$ E1[E2] { E.type := if E1.type = $ \bf integer$
    and E2.type = array(n, T)
    then T
    else $ \bf type\_error$ }
E $ \longmapsto$ $ \uparrow$ E1 { E.type := if E1.type = pointer(T)
    then T
    else $ \bf type\_error$ }
E $ \longmapsto$ E1(E2) { E.type := if E2.type = S
    and E1.type = S  $ \rightarrow$  T
    then T
    else $ \bf type\_error$ }
Now we extend our language by stating that Therefore we obtain the following new grammar.
P $ \longmapsto$ DS
D $ \longmapsto$ DD
D $ \longmapsto$ $ \bf id$ :  T
T $ \longmapsto$ $ \bf boolean$
T $ \longmapsto$ $ \bf character$
T $ \longmapsto$ $ \bf integer$
T $ \longmapsto$ $ \bf array$[$ \bf num$]$ \bf of$T
T $ \longmapsto$ $ \uparrow$ T
E $ \longmapsto$ $ \bf literal$
E $ \longmapsto$ $ \bf num$
E $ \longmapsto$ $ \bf id$
E $ \longmapsto$ E $ \bf mod$ E
E $ \longmapsto$ E  $ \leq$  E
E $ \longmapsto$ E[E]
E $ \longmapsto$ $ \uparrow$ E
S $ \longmapsto$ S1S2
S $ \longmapsto$ $ \bf id$ := E
S $ \longmapsto$ $ \bf if$ E $ \bf then$ S
S $ \longmapsto$ $ \bf while$ E $ \bf repeat$ S
Extending the translation scheme for statements leads to:
S $ \longmapsto$ S1S2 { S.type := if S1.type = void
    and S2.type = void
    then void
    else $ \bf type\_error$ }
S $ \longmapsto$ $ \bf id$ := E { S.type := if E.type = $ \bf id$.type
    then void
    else $ \bf type\_error$ }
S $ \longmapsto$ $ \bf if$ E $ \bf then$ S1 { S.type := if E.type = boolean
    then S1.type
    else $ \bf type\_error$ }
S $ \longmapsto$ $ \bf while$ E $ \bf repeat$ S1 { S.type := if E.type = boolean
    then S1.type
    else $ \bf type\_error$ }


next up previous
Next: Type Equivalence Up: Compiler Theory: Type Checking Previous: Type Systems
Marc Moreno Maza
2004-12-02