Specification of a Simple Type Checker

We consider the language generated by the following grammar.

P $\longmapsto$ D; E

D $\longmapsto$ D; D

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)

• A sentence of this language is a Program.
• A Program consists of a sequence of Declarations followed by an Expression.
• character and integer are the basic types whereas literal and num stand for elements of these types.
• $\bf id$ is the token for identifiers.
• $\bf array$[$\bf num$]$\bf of$T is an array type construct whereas E[E] refers to an element of an array.
• $\uparrow$ T is a pointer type construct whereas $\uparrow$ E is a pointer dereference.
• T $\rightarrow$ T is a function type construct whereas E(E) is a function call.
• E $\bf mod$ E represents a remainder computation.

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

$$\longmapsto \bf id \bf id$$ (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

• A Program consists of a sequence of Declarations followed by a sequence of Statements.
• A statement is either an assignment, an alternative or a while loop.
• boolean is a basic type.
• An expression could be E₁  $\leq$  E₂ which evaluates to boolean provided that E₁ and E₂ have the same basic type, otherwise evaluates to type_error.

Therefore we obtain the following new grammar.

P $\longmapsto$ D; S

D $\longmapsto$ D; D

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$ S₁; S₂

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$ S1; S2	{ 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$ }