Difference between pages "Rodin Workshop 2012" and "Strengthening the AST Library for Rodin 3.0"
imported>WikiSysop |
imported>Vinmont |
||
| Line 1: | Line 1: | ||
| − | + | 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, {{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 == | |
| − | + | 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 {{class|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 == | |
| + | AST nodes construction is possible using {{class|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 allow to avoid exceptions raised later for which source is more complicated to locate. | ||
| − | + | [[Category:Design]] | |
| − | + | [[Category:Developer documentation]] | |
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
Revision as of 10:40, 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 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.
AST nodes construction
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 allow to avoid exceptions raised later for which source is more complicated to locate.
