the executables xtypes as specified below;

the sub-directory 9/Tests/ with the required integration test; and

an optional sub-directory called 9/Other/ for all auxiliary files.

A judgment of the shape CC ⊢ Syn says that “in context CC the well-formed syntax Syn is also valid.” For example, ⊢ (mod1 ... modK imp1 ... impI def* stmt* exp) says a complete system—consisting of K modules, I import specifications, a sequence of definitions (def*), a sequence of statements (stmt*), and a final expression (exp) is valid syntax.

A judgment of the shape CC ⊢ Syn ⟹ R says that “in context CC the well-formed syntax Syn is valid and the judgment results in R.” For example, read SClasses, TVar ⊢ n ⟹ Number as “in the context of class types according to SClasses and variable types according to TVar, n is valid syntax, and the judgment produces the type Number.”

Modules is a set of modules.

SClasses is a function that maps ClassNames to Shapes.

TVar is a function that maps Variables to Types.

Subscripts range over an (interval of the) natural numbers.

Figure 20 covers the distinct judgments for complete systems, sequences of modules, individual modules, and (sequences of) import specifications.

Figure 21 displays judgments about the validity of individual classes and methods.

The rules in figure 22 determine the validity of bodies of blocks, systems, and methods.

Figure 23 explain the validity of sequences of declarations and individual declarations.

Figures 24 and 25 cover the validity of statements and expressions, respectively.

Adapt the AST data representation from Module Types to Types Mixed. It must accommodate one extra attribute of modules—the Shape of the defined Class. Update your parser for Module accordingly.

Hint In anticipation of the remaining milestones, modify your AST representation of class so that it may optionally come with a Shape.

Modify the existing validity checks for Module to accommodate the extra attribute as needed.

Implement the type checker in a bottom-up fashion, one set of rules after another.

Hint Since the type checker is called only when the preceding validity-checking passes have “blessed” the AST, your implementation of the type checker may rely on the logical properties of ASTs that these passes establish.

Add a pass that turns the AST of a well-formed and well-typed Type system into a Module AST so that the linker from 8 — Modules can create a Class program, which can then be run on the Class CESK machine.

Note Depending on your chosen implementation language and your choice of AST data representation, your linker might already work for Typed ASTs or you might find it easy to adapt the linker so that it works this way.

Comment out the cases of the CESK transition function that are superfluous due to the type system. That is, identify the cases in the transition function that a well-formed and valid system can no longer trigger.

"parser error" if the given ExampleFF is not an element of the Type grammar;

"duplicate module name" if in the well-formed Type system two of the module definitions come with the same name;

"duplicate method, field, or parameter name" if in the well-formed Type system one class definition one method definition, or one Shape comes with (at least) two fields, methods, or parameters that have the same name;

"undeclared variable error" if in the well-formed Type system one of its variable occurrences comes without declaration or one occurrence of a ClassName in a statement or an expression comes without class definition;

"type error" if the well-formed Type system fails to satisfy one of the typing judgments;

a number n if the CESK machine produces a number n for the well-formed and valid Typed system;

"run-time error" if the CESK machine produces an error outcome for the well-formed and valid Typed system.