Strengthening the AST Library for Rodin 3.0: Difference between revisions
imported>Vinmont Created page with "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..." |
imported>Vinmont |
||
| Line 4: | Line 4: | ||
Type environments have changed in Rodin 3.0 in order to reinforce their good use and their robustness. | 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. | 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 inferred | 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, {{class|ITypeEnvironmentBuilder}} and {{class|ISealedTypeEnvironment}}. This mechanism provides a strong guarantee that a type environment will not be modified if necessary and | Finally we add mechanism to separate mutable and immutable type environments by creating two children interfaces of the type environment interface, {{class|ITypeEnvironmentBuilder}} and {{class|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 == | == Type Checking == | ||
Revision as of 08:48, 14 January 2013
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 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 idenfied 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 allow to guarantee that incompatible free identifiers names are not introduced regarding given sets.
- 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 given set and a free identifier have a name conflict it will be detected during this step (but since it could normally occur in the solving type step, the typecheck() procedure must have already reported this conflict).
- In the FreeIdentifier.synthesize() procedure if the free identifier name and its type introduces a given set name conflict, then its given type is ignored and can result in a type checking failure.
- If the whole type checking procedure succeeds then all free identifiers are checked and added to the inferred environment if necessary.
