Specification of a Simple Type Checker
Specification of a Simple Type Checker
- Specification of a simple type checker for a simple language in which the type of each identifier must be declared before the identifier is used.
- The type checker is a translation scheme that synthesizes the type of each expression from the types of its subexpressions.
- The type checker can handle arrays, pointers, statements, and functions.
- Specification of a simple type checker includes the following:
- A Simple Language
- Type Checking of Expressions
- Type Checking of Statements
- Type Checking of Functions
Specification of Type Checker
Simple Language
- The following grammar generates programs, represented by the nonterminal P, consisting of a sequence of declarations D followed by a single expression E.
| P -> D ; E |
| D -> D ; D | id : T |
| T -> char | integer | array[num] of T | ‡ T |
A translation scheme for above rules:
| P -> D ; E |
| D -> D ; D |
| D -> id : T { addtype(id.entry, T.type } |
| T -> char { T.type := char } |
| T -> integer { T.type := integer } |
| T -> ‡ T1 { T.type := pointer(T1.type) } |
| T -> array[num] of T1 { T.type := array(1..num.val, T1.type) } |
Type Checking of Expressions
- The synthesized attribute type for E gives the type expression assigned by the type system to the expression generated by E.
- The following semantic rules say that constants represented by the tokens literal and num have type char and integer, respectively:
| Rule | Semantic Rule |
|---|---|
| E -> literal | { E.type := char } |
| E -> num | { E.type := integer} |
- A function lookup(e) is used to fetch the type saved in the symbol-table entry pointed to by e.
- When an identifier appears in an expression, its declared type is fetched and assigned to the attribute type;
| E -> id | { E.type := lookup(id.entry} |
- The expression formed by applying the mod operator to two subexpressions of type integer has type integer; otherwise, its type is type_error. The rule is
| E -> E1 mod E2 | { E.type := if E1.type = integer and E2.type = integer then integer else typr_error} |
- In an array reference E1 [E2], the index expression E2 must have type integer, in which case the result is the dement type t obtained from the type array(s. t ) of E1; we make no use of the index set s of the array.
| E -> E1 [ E2 ] | { E.type := if E2.type = integer and E1.type = array(s,t) then t else typr_error} |
- Within expressions, the postfix operator ↑ yields the object pointed to by its operand. The type of E ‡ is the type ‡ of the object pointed to by the pointer E:
| E -> E1 ‡ | { E.type := if E1.type = ponter(t) then t else typr_error} |
Type Checking
Type Checking of Statements
- Since language constructs like statements typically do not have values, the special basic type void can be assigned to them.
- If an error is detected within a statement, then the type type_error assigned.
- The assignment statement, conditional statement, and while statements are considered for the type checking.
- The Sequences of statements are separated by semicolons.
| Statement | Rule | Semantic Rule |
|---|---|---|
| Assignment | S -> id := E | {S.type := if id.type = E,type then void else type_error} |
| Conditional | E -> if E then S1 | { S.type := if E.type = Boolean then S1.type else type_error} |
| While | E -> while E do S1 | { S.type := if E.type = Boolean then S1.type else type_error} |
| Sequence | E -> S1 ; S2 | { S.type := if S1.type = void and S2.type = void then void else type_error} |
Type Checking Statements
Type Checking of Functions
- The application of a function to an argument can be captured by the production
| E -> E ( E ) |
- An expression is the application of one expression to another. The rules for associating type expressions with nonterminal T can be augmented by the following production and action to permit function types in declarations.
| T -> T1' -> T2' | {T.type := T1.type -> T2.type} |
- Quotes around the arrow used as a function constructor distinguish it from the arrow used as the meta symbol in a production.
- The rule for checking the type of a function application is
| E -> E1 ( E2 ) |
{ E.type := if E2.type = s and E1.type = s -> t then t else typr_error} |
Type Checking Functions