Strengthening the AST Library for Rodin 3.0 - Revision history

imported>Vinmont: /* AST nodes construction */

2013-02-15T16:07:42Z

AST nodes construction

← Older revision		Revision as of 16:07, 15 February 2013
Line 31:		Line 31:

	== AST nodes construction ==		== AST nodes construction ==

			=== Enforcement of conditions on arguments ===
	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 allows to avoid exceptions raised later for which source is more complicated to locate.		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 allows to avoid exceptions raised later for which source is more complicated to locate.
	~~Moreover~~ AST nodes and types are now keeping a reference on the factory that was used to build them ~~and~~ AST library enforces that they have been built by the same formula factory~~. Then we now avoid incoherent~~ nodes and types ~~by construction regarding their formula factory~~ that ~~could have lead~~, ~~e.g.~~, ~~to use reserved words~~ in a ~~part~~ of a formula ~~as a free identifier name~~ in ~~another part~~.
			=== 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.

	[[Category:Design]]		[[Category:Design]]
	[[Category:Developer documentation]]		[[Category:Developer documentation]]

imported>Vinmont at 09:35, 13 February 2013

2013-02-13T09:35:56Z

← Older revision		Revision as of 09:35, 13 February 2013
Line 32:		Line 32:
	== AST nodes construction ==		== 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 allows to avoid exceptions raised later for which source is more complicated to locate.		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 allows to avoid exceptions raised later for which source is more complicated to locate.
			Moreover AST nodes and types are now keeping a reference on the factory that was used to build them and AST library enforces that they have been built by the same formula factory. Then we now avoid incoherent nodes and types by construction regarding their formula factory that could have lead, e.g., to use reserved words in a part of a formula as a free identifier name in another part.

	[[Category:Design]]		[[Category:Design]]
	[[Category:Developer documentation]]		[[Category:Developer documentation]]

imported>Laurent: /* Type Checking */

2013-02-12T17:56:57Z

Type Checking

← Older revision		Revision as of 17:56, 12 February 2013
Line 21:		Line 21:

	== Type Checking ==		== 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.		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 ~~identifiers~~ then the bound identifier will be renamed since it is identified by its Bruijn number.		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:		The modification of the type checking step introduces the following modifications:

imported>Laurent: /* Type Environment */

2013-02-12T17:54:50Z

Type Environment

← Older revision		Revision as of 17:54, 12 February 2013
Line 2:		Line 2:

	== Type Environment ==		== 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.		Type environments have changed in Rodin 3.0 in order to reinforce their good
	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.~~		use and their robustness.
	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).
			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, {{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 needed (see [[Rodin 3.0 Plug-in Migration
			Guide]] for more information).

	== Type Checking ==		== Type Checking ==

imported>Vinmont: /* AST nodes construction */

2013-01-15T10:44:47Z

AST nodes construction

← Older revision		Revision as of 10:44, 15 January 2013
Line 18:		Line 18:

	== AST nodes construction ==		== 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.		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 allows to avoid exceptions raised later for which source is more complicated to locate.

	[[Category:Design]]		[[Category:Design]]
	[[Category:Developer documentation]]		[[Category:Developer documentation]]

imported>Vinmont: /* AST nodes construction */

2013-01-14T10:40:30Z

AST nodes construction

← Older revision		Revision as of 10:40, 14 January 2013
Line 18:		Line 18:

	== AST nodes construction ==		== 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 arguments provided ~~and that given types provided was~~ valid regarding constructed node ~~type~~. Those verifications ~~is provided~~ with ~~documentation explicit~~ exceptions raised when conditions on arguments are not respected~~, it allows~~ to ~~improve exceptions meaning and~~ avoid ~~further~~ exceptions for which source is more complicated to ~~understand~~.		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:Design]]
	[[Category:Developer documentation]]		[[Category:Developer documentation]]

imported>Vinmont at 10:31, 14 January 2013

2013-01-14T10:31:57Z

← Older revision		Revision as of 10:31, 14 January 2013
Line 8:		Line 8:

	== Type Checking ==		== 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.		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.

Line 17:		Line 16:
	* 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.		* 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.		* 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 arguments provided and that given types provided was valid regarding constructed node type. Those verifications is provided with documentation explicit exceptions raised when conditions on arguments are not respected, it allows to improve exceptions meaning and avoid further exceptions for which source is more complicated to understand.

	[[Category:Design]]		[[Category:Design]]
	[[Category:Developer documentation]]		[[Category:Developer documentation]]

imported>Vinmont: /* Type Checking */

2013-01-14T09:03:49Z

Type Checking

← Older revision		Revision as of 09:03, 14 January 2013
Line 9:		Line 9:
	== Type Checking ==		== 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.		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 ~~idenfied~~ by its Bruijn number.		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:		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 ''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 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 ''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.
	* 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.		* If the whole type checking procedure succeeds then all free identifiers are checked and added to the inferred environment if necessary.

	[[Category:Design]]		[[Category:Design]]
	[[Category:Developer documentation]]		[[Category:Developer documentation]]

imported>Vinmont: /* Type Environment */

2013-01-14T08:48:37Z

Type Environment

← Older revision		Revision as of 08:48, 14 January 2013
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 ~~environment~~ which now references its initial type environment~~, this~~ type is now used ~~for~~ 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.		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 ~~allow~~ at the same time to be flexible when needed (see [[Rodin 3.0 Plug-in Migration Guide]] for more information).		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 ==

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..."

2013-01-07T10:02:05Z

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..."

New page

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 inferred environment which now references its initial type environment, this type is now used for 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 allow 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 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.

[[Category:Design]]
[[Category:Developer documentation]]