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 equation, and when we have a Var type the typing is done relative to the typing environment that map between identifiers and its type.
  Then we check the correctness for each equation to determine if our program is well typed or not.

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

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