Read Section 4 of the ChocoPy Reference Manual with the type rules of the language. In the remaining labs of the course, you will translate those type rules into formal Statix rules in order to implement a type checker. You should submit the result, a complete type system implementation of ChocoPy in Statix, in Milestone 2. You can proceed at your own pace, but in this and the following lab descriptions, we give some ideas for ordering the task.
In this lab, follow Lecture 4 and the homework assignments for Week 3 to define a predicate (say typeOfExp) to test the type correctness of expressions without names (variables, functions).
For now, ignore the contexts in the typing rules. You can see (by tracing the rules) that for expressions not involving names, those contexts are irrelevant. In the predicate, you can either leave the context out entirely, or you can pass around a dummy ‘scope’. (We will study scopes in the next lecture.) In the latter case, you need to figure out how to create the dummy scope. In the former case you will need to add scopes later, but that should be a simple find-and-replace action.