CS173 - Type Checker

Type Checker

You will be working with a new group for this assignment and for Written 3. (i.e. your group for this assignment will be the same as your group for Written 3 which will be different from your group for previous assignments.)

In this assignment, you will work with a typed language that includes numbers, booleans, conditionals, functions, and numeric lists. The concrete syntax for the language is given by the following BNF grammars:

   <expr> ::= <num>
            | true
            | false
            | {+ <expr> <expr>}
            | {- <expr> <expr>}
            | {* <expr> <expr>}
            | {iszero <expr>}
            | {bif <expr> <expr> <expr>}

            | <id>
            | {with {<id> <expr>} <expr>}
            | {fun {<id> : <type>} : <type> <expr>}
            | {<expr> <expr>}

            | nempty
            | {ncons <expr> <expr>}
            | {nempty? <expr>}
            | {nfirst <expr>}
            | {nrest <expr>}

   <type> ::= number
            | boolean
            | nlist
            | (<type> -> <type>)

In the surface syntax for types, base types are represented by symbols, and the arrow type by a Scheme list of three elements: the type of the argument, the symbol ->, and the type of the result.

You have not implemented some of these constructs yet, but they should be familiar:

iszero consumes a number, and returns true if it is 0, false otherwise
the test expression of bif ("boolean if") must evaluate to true or false
ncons consumes a number and a numeric list, and produces a numeric list

You have three tasks:

Define the function parse, which consumes the concrete representation of a program, and returns its abstract syntax tree. You may assume that the concrete representation conforms to the above grammer.
Write down type judgments for the five numeric list constructs: nempty, ncons, nempty?, nfirst, and nrest. You should turn in hard copy to the cs173 handin bin.
Implement the function type-of, which consumes the abstract representation of a program (i.e. the result of parse) and an escape continuation that accepts a string. If the program has no type errors, type-of returns the type of the program, using the names of the types given in the grammar above. If the program does have a type error, type-of invokes the continuation with some string as an argument. For example:
```
      (let/cc esc (type-of (parse '{+ 1 2}) esc))
    
```
should produce number, while:
```
      (let/cc esc (type-of (parse '{3 4}) esc))
    
```
would invoke esc with some string, (e.g. "Number is not a function").

Hand In

Only one partner should submit the your Scheme code and a readme to WebCT. The readme file should contain the names of the members of the group. Put the hard copy of the type judgements in the cs173 handin bin. The other member of the group should submit an empty file. If you do not submit to WebCT, you will not receive a grade for the assignment.

-.-. ... .---- --... ...--

Type Checker

Hand In