Type Checking

Definition

The type checker is to determine if the program is well-typed or not.

Usage

To check the type of a program use ./mincamlc -t /tests/typechecking/invalid/testname.ml
or you can call make test_typecheck to run all the tests.

Structure

• AST of the program to be type checked.
• The environment in which the program is typechecked.
  Initially, the environment contains the types of the predefined functions
  ("print_int", "print_float","float_of_int,"int_of_float","sin","cos","sqrt","abs_float","truncate","print_newline")
• The type that the program must have : Unit type

Description

• It takes the AST generated from the parser.
• Update the environment each time we define a new variable or function.
• Generate a list of typing equations that should hold for our term to be well typed.
  We do recursive traversal of the AST and generate the equivalent equations, and when we have a Var type the typing is done relative to the typing environment that map between identifiers and its type.
• Check the correctness of our program by calling a unification algorithm that solve tree equations and determine if it's well typed or throw a failwith message.

Output

If it's well typed it return "well typed" message.
If it's not well typed we throw a failwith exception with the right error message.

Handled Errors

We handled errors that could occur in All types.

Error Messages

• Unbound value
• Expression has type %s but an expression was expected of type %s
• Number of function arguments is incorrect
• Number of tuple arguments is incorrect