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 have added a new mechanism to add given sets implicitly introduced by types when new elements are added.

Then, we have added a new interface to represent inferred type environments. These environments are the ones that are returned in the result of the typecheck methods of Formula and Expression.

Finally we have added 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 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 to an 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 identifier then the bound identifier will be renamed since it is identified by its de 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.

AST nodes construction

Enforcement of conditions on arguments

AST nodes construction is possible using FormulaFactory methods (direct access to constructors is now explicitly forbidden) and has been strengthened by verifying that arguments provided are valid regarding constructed node. Those verifications are documented with the exceptions raised when conditions on arguments are not respected. It allows to avoid exceptions raised later for which source is more complicated to locate.

Enforcement of formula factory equality

First of all, AST nodes and types are now keeping a reference on the factory that was used to build them which avoid the multiplication of factories passed as parameter in the rest of the code. Then, the AST library enforces that they have been built with the exact same formula factory which forbids to mix nodes and types coming from different factories. We made this decision on the fact that, in most cases, this restriction is not important as all formulas are always in the same language. As a consequence we prevent the construction of a formula with incoherent factories in its children but we also forbid the construction with different factories that are compatible. This last option has been rejected because the performance cost was important to enforce the compatibility in addition to the precedent arguments exposed.