Strengthening the AST Library for Rodin 3.0

A part of the Rodin 3.0 development aims to strengthen the AST library. This page explains the choices we have done during this step.

Type Environment

Type environments have changed in Rodin 3.0 in order to reinforce their good use and their robustness. First of all we add a new mechanism to add given sets implicitly introduced by types when new elements are added. Then we create the inferred type environment Java type to could differentiate a classical type environment and an inferred one which now references its initial type environment. This type is now used in the type checking result. Since an inferred type environment content depends on its initial type environment it was a necessary modification to could express all possible inferred type environments. Finally we add mechanism to separate mutable and immutable type environments by creating two children interfaces of the type environment interface, ITypeEnvironmentBuilder and ISealedTypeEnvironment. This mechanism provides a strong guarantee that a type environment will not be modified if necessary and allows at the same time to be flexible when it is needed (see Rodin 3.0 Plug-in Migration Guide for more information).

Type Checking

The type checking step has been strengthened to avoid that the type checker accepts given types implicitly introducing given sets incompatibles with the type environment and thus free identifiers. It also allowed to detect and correct a new occurrence of the bug #635 (old name #3574565) that was leading on a incoherent result of the formula type checking since the formula was not correctly type checked but the result was indicating a success.

Regarding the legibility for identifiers no modification has been done, that is to say that if the same name is used for a free and bound identifiers then the bound identifier will be renamed since it is identified by its Bruijn number.

The modification of the type checking step introduces the following modifications:

• In the typecheck() procedure of nodes, we now analyse the type of the nodes that could introduce new given sets and add those given sets to the resulting inferred type environment. It guarantees that incompatible free identifiers names or given sets are not introduced.
• In the synthesize() procedure, that is executed a first time at node creation and a second time during solving types step, we now add the given sets introduced by given types as free identifiers on concerned nodes. As a consequence if a given set and a free identifier have a name conflict it will also be detected during this step. Particularly it will provide a way to detect and raise an IllegalArgumentException when an invalid type is provided at node creation.
• If the whole type checking procedure succeeds then all free identifiers are checked and added to the inferred environment if necessary.