Rodin 3.0 Plug-in Migration Guide - Revision history

imported>Tommy: /* Migration instructions */

2014-02-14T16:25:56Z

Migration instructions

← Older revision		Revision as of 16:25, 14 February 2014
Line 142:		Line 142:

	==== Migration instructions ====		==== Migration instructions ====
	If you do (or intend to) contribute model elements and attribute types to the Rodin database, you now have to define the relationships they can have between them, or with the core elements. The relationships are defined in a simple manner using two kinds of relationship definitions.		If you do (or intend to) contribute model elements and attribute types to the Rodin database, you now have to define the relationships they can have between them, or with the core elements. The relationships are defined in a simple manner using two kinds of relationship definitions:
	*parent-children relationships (i.e. between a parent type and the child types it accepts,		*parent-children relationships (i.e. between a parent type and the child types it accepts,
	*ubiquitous item relationships (i.e. the item concerned in the ubiquitous can be "everywhere", which means it can be held (if an element) or carried (if an attribute) by any element in the database).		*ubiquitous item relationships (i.e. the item concerned in the ubiquitous can be "everywhere", which means it can be held (if an element) or carried (if an attribute) by any element in the database).

imported>Tommy: /* Rodin Core Plug-ins */

2014-02-14T16:25:34Z

Rodin Core Plug-ins

← Older revision		Revision as of 16:25, 14 February 2014
Line 142:		Line 142:

	==== Migration instructions ====		==== Migration instructions ====
	If you do (or intend to) contribute model elements and attribute types to the Rodin database, you now have to define the relationships they can have between them, or with the core elements. The relationships are defined in a simple manner using parent-child(~~ren~~) ~~relationship definitions~~.		If you do (or intend to) contribute model elements and attribute types to the Rodin database, you now have to define the relationships they can have between them, or with the core elements. The relationships are defined in a simple manner using two kinds of relationship definitions.
	To define such permissions, you have to contribute to the new dedicated extension point <tt>org.rodinp.core.itemRelations</tt>. Please refer to the documentation of the extension point for further details on how to implement things.		*parent-children relationships (i.e. between a parent type and the child types it accepts,
			*ubiquitous item relationships (i.e. the item concerned in the ubiquitous can be "everywhere", which means it can be held (if an element) or carried (if an attribute) by any element in the database).
			To define such permissions, you have to contribute to the new dedicated extension point <tt>org.rodinp.core.itemRelations</tt>.
			Please refer to the documentation of the extension point for further details on how to implement things.

	If your plug-in already contributes model element and attribute types, using contributions to <tt>org.eventb.ui.editorItems</tt>, a compatibility mechanism has been activated in order to integrate legacy relationships. However, it is not advised to rely on such compatibility mechanism.		If your plug-in already contributes model element and attribute types, using contributions to <tt>org.eventb.ui.editorItems</tt>, a compatibility mechanism has been activated in order to integrate legacy relationships. However, it is not advised to rely on such compatibility mechanism.

imported>Nicolas: /* Rodin Keyboard Plug-ins */

2014-01-27T14:06:38Z

Rodin Keyboard Plug-ins

← Older revision		Revision as of 14:06, 27 January 2014
Line 179:		Line 179:
	There isn't any change from Event-B UI Plug-in which impacts its downstream plug-ins.		There isn't any change from Event-B UI Plug-in which impacts its downstream plug-ins.

	~~== Rodin Keyboard Plug-ins ==~~
	The translation of mathematical symbols has been refactored to avoid a dependency on the Event-B UI plug-in: there is now a separation between symbol translation and translation which occurs in graphical components.<br>
	~~The plug-in <tt>org.rodinp.keyboard</tt> is now split into two plug-ins :~~
	* org.rodinp.keyboard.core : this plug-in contains the core translation utilities that one can access through the following method <tt>org.rodinp.keyboard.core.RodinKeyboardCore.translate(String)</tt>,
	* org.rodinp.keyboard.ui : this plug-in contains the UI translation capabilties that where previously available from <tt>org.rodinp.keyboard</tt>.

	[[Category:Developer documentation]]		[[Category:Developer documentation]]
	[[Category:Rodin Platform]]		[[Category:Rodin Platform]]

imported>Nicolas: /* A bit of background */

2014-01-27T14:04:29Z

A bit of background

← Older revision		Revision as of 14:04, 27 January 2014
Line 154:		Line 154:
	The Rodin keyboard translation capability lets keyboard key combinations entered by the end user be transformed into dedicated Unicode representations (e.g. the following string <tt>/<<:</tt> is translated to ⊄).		The Rodin keyboard translation capability lets keyboard key combinations entered by the end user be transformed into dedicated Unicode representations (e.g. the following string <tt>/<<:</tt> is translated to ⊄).
	Two kinds of translation mechanisms are provided :		Two kinds of translation mechanisms are provided :
	- a simple string translation mechanism: from a given string, it returns a string where all symbols are translated,		* a simple string translation mechanism: from a given string, it returns a string where all symbols are translated,
	- an Event-B UI text widgets adaptation mechanism: textual widgets can be adapted for "on-the-fly" symbol translation.		* an Event-B UI text widgets adaptation mechanism: textual widgets can be adapted for "on-the-fly" symbol translation.

	Historically, only one plug-in has been defined to provide these two functionnalities : <tt>org.rodinp.keyboard</tt>.<br />		Historically, only one plug-in has been defined to provide these two functionnalities : <tt>org.rodinp.keyboard</tt>.<br />

imported>Nicolas: /* Datatype Definition */

2014-01-27T10:03:25Z

Datatype Definition

← Older revision		Revision as of 10:03, 27 January 2014
Line 69:		Line 69:
	==== Datatype Definition ====		==== Datatype Definition ====

	The definition of datatypes has completely changed to be ~~simplest~~ and more compact.		The definition of datatypes has completely changed to be simpler and more compact.
	A datatype must now be defined in a declarative way with a datatype builder. Here are the few steps necessary to declare a new datatype:		A datatype must now be defined in a declarative way with a datatype builder. Here are the few steps necessary to declare a new datatype:
	* Retrieve a datatype builder {{class\|IDatatypeBuilder}} provided by a {{class\|FormulaFactory}} using <tt>makeDatatypeBuilder(String, GivenType[])</tt>. This step sets the datatype name and its type parameters (as given types).		* Retrieve a datatype builder {{class\|IDatatypeBuilder}} provided by a {{class\|FormulaFactory}} using <tt>makeDatatypeBuilder(String, GivenType[])</tt>. This step sets the datatype name and its type parameters (as given types).
Line 78:		Line 78:
	** Finalize the datatype by using the <tt>finalizeDatatype()</tt> builder method which returns the finalized datatype {{class\|\|IDatatype}}		** Finalize the datatype by using the <tt>finalizeDatatype()</tt> builder method which returns the finalized datatype {{class\|\|IDatatype}}

	As you ~~can~~ have noticed a constructor argument type is now represented with a standard event-B {{class\|Type}} object.		As you may have noticed a constructor argument type is now represented with a standard event-B {{class\|Type}} object.
	The type representation principle is the following:		The type representation principle is the following:
	* A type parameter is always represented by the given type defined by the type parameter name (as provided to retrieve the ~~dataype~~ builder)		* A type parameter is always represented by the given type defined by the type parameter name (as provided to retrieve the datatype builder)
	* The datatype is represented by the given type defined by the datatype name		* The datatype is represented by the given type defined by the datatype name
	But since the string representation of a datatype must contain its type parameters, the datatype builder provides the <tt>parseType(String)</tt> parser. It allows to transform the string representation into the type representation as soon as the datatype is represented with its type parameters correctly named and ordered. E.g.: For the datatype "DT" with the type parameters "X", "Y" and "Z", the string representation is "DT(X,Y,Z)" and the type representation is the given type "DT".		But since the string representation of a datatype must contain its type parameters, the datatype builder provides the <tt>parseType(String)</tt> parser. It allows to transform the string representation into the type representation as soon as the datatype is represented with its type parameters correctly named and ordered. E.g.: For the datatype "DT" with the type parameters "X", "Y" and "Z", the string representation is "DT(X,Y,Z)" and the type representation is the given type "DT".

imported>Nicolas: /* Type Environments */

2014-01-27T09:58:01Z

Type Environments

← Older revision		Revision as of 09:58, 27 January 2014
Line 18:		Line 18:
	* It is an {{class\|ISealedTypeEnvironment}}: you must provide an immutable snapshot of your type environment using method ''makeSnapshot()''.		* It is an {{class\|ISealedTypeEnvironment}}: you must provide an immutable snapshot of your type environment using method ''makeSnapshot()''.
	* It is an {{class\|ITypeEnvironmentBuilder}}: here two choices are possible, you could give your object reference as parameter and it will be modified if a further treatment is made on it or you could give a copy of your object using method ''makeBuilder()'' to prevent side effect on your object.		* It is an {{class\|ITypeEnvironmentBuilder}}: here two choices are possible, you could give your object reference as parameter and it will be modified if a further treatment is made on it or you could give a copy of your object using method ''makeBuilder()'' to prevent side effect on your object.
	* It is an {{class\|~~ITypeEnvrionment~~}}: it is a convenient way to have genericity since it is the super type of both preceding ones. You can opt for any options above. There is a convention that a parameter of type ITypeEnvironment is not modified by the callee, but this is not enforced. If you want a strong guarantee that the type environment that you pass cannot be modified, pass it as a sealed environment.		* It is an {{class\|ITypeEnvironment}}: it is a convenient way to have genericity since it is the super type of both preceding ones. You can opt for any options above. There is a convention that a parameter of type ITypeEnvironment is not modified by the callee, but this is not enforced. If you want a strong guarantee that the type environment that you pass cannot be modified, pass it as a sealed environment.

	Reciprocally, if you ask for a type environment as parameter, these 3 options are available:		Reciprocally, if you ask for a type environment as parameter, these 3 options are available:
	* Use an {{class\|ISealedTypeEnvironment}}: if you want to provide a strong guarantee that you will not modify the parameter.		* Use an {{class\|ISealedTypeEnvironment}}: if you want to provide a strong guarantee that you will not modify the parameter.
	* Use an {{class\|~~ITypeEnvrionmentBuilder~~}}: if you need to modify the received type environment by side effect		* Use an {{class\|ITypeEnvironmentBuilder}}: if you need to modify the received type environment by side effect
	* Use an {{class\|~~ITypeEnvrionment~~}}: in case you will not modify the type environment and allow the user to provide the most convenient type for him. You must not later cast the parameter to type {{class\|ITypeEnvironmentBuilder}}.		* Use an {{class\|ITypeEnvironment}}: in case you will not modify the type environment and allow the user to provide the most convenient type for him. You must not later cast the parameter to type {{class\|ITypeEnvironmentBuilder}}.

	Finally regarding return type of methods, you should use only one of the two following choices ({{class\|ITypeEnvironment}} is discouraged since it provides no information about what is actually returned):		Finally regarding return type of methods, you should use only one of the two following choices ({{class\|ITypeEnvironment}} is discouraged since it provides no information about what is actually returned):

imported>Nicolas: /* FormulaFactory and Proofs */

2014-01-14T18:42:29Z

FormulaFactory and Proofs

← Older revision		Revision as of 18:42, 14 January 2014
Line 110:		Line 110:
	Indeed, it allows to define a strong relationship between the inference action and the hide action: during reuse, the hide action is performed only if the forward inference occurs.		Indeed, it allows to define a strong relationship between the inference action and the hide action: during reuse, the hide action is performed only if the forward inference occurs.

	=== ~~FormulaFactory~~ and Proofs ===		=== Formula Factories and Proofs ===

	Formula factories have been growing in importance since the mathematical extensions and the theory plug-in have been developed.		Formula factories have been growing in importance since the mathematical extensions and the theory plug-in have been developed.

imported>Nicolas: /* FormulaFactory */

2014-01-14T18:38:24Z

FormulaFactory

← Older revision		Revision as of 18:38, 14 January 2014
Line 110:		Line 110:
	Indeed, it allows to define a strong relationship between the inference action and the hide action: during reuse, the hide action is performed only if the forward inference occurs.		Indeed, it allows to define a strong relationship between the inference action and the hide action: during reuse, the hide action is performed only if the forward inference occurs.

	=== FormulaFactory ===		=== FormulaFactory and Proofs ===

	Formula factories have been growing in importance since the mathematical extensions and the theory plug-in have been developed.		Formula factories have been growing in importance since the mathematical extensions and the theory plug-in have been developed.
Line 117:		Line 117:
	A FormulaFactory instance is used to parse and make formulas in a given mathematical language.		A FormulaFactory instance is used to parse and make formulas in a given mathematical language.
	Proofs now bear their own formula factory, potentially different from the formula factories of the other proofs in the same file, hence the addition of ''IProofTree.getFormulaFactory()'' and ''IPRProof.getFormulaFactory()'' methods. You must be aware of that fact if you pass formula factory arguments in method calls, in order to use the right one.		Proofs now bear their own formula factory, potentially different from the formula factories of the other proofs in the same file, hence the addition of ''IProofTree.getFormulaFactory()'' and ''IPRProof.getFormulaFactory()'' methods. You must be aware of that fact if you pass formula factory arguments in method calls, in order to use the right one.

			In order to store formula factories in proofs, the '''org.eventb.core.extension.IFormulaExtensionProvider''' has evolved and must now provide loading and saving capabilities.

			But when the language changes, losing all proofs is not an option. Various translation methods have been implemented in order to reuse proofs made with a different formula factory.
			However, reasoner inputs ('''implementors of IReasonerInput''') are defined on the client side and may contain language dependent data, like predicates or expressions.
			These cannot be handled on the core platform side, hence the addition of the ''org.eventb.core.seqprover.ITranslatableReasonerInput''. If you implement or subclass a reasoner input, you must also implement this interface in order to support mathematical language changes in proofs.

	=== Context Dependent Reasoners ===		=== Context Dependent Reasoners ===

imported>Nicolas: /* Formula Factory */

2014-01-14T18:23:48Z

Formula Factory

← Older revision		Revision as of 18:23, 14 January 2014
Line 110:		Line 110:
	Indeed, it allows to define a strong relationship between the inference action and the hide action: during reuse, the hide action is performed only if the forward inference occurs.		Indeed, it allows to define a strong relationship between the inference action and the hide action: during reuse, the hide action is performed only if the forward inference occurs.

	=== ~~Formula Factory~~ ===		=== FormulaFactory ===

			Formula factories have been growing in importance since the mathematical extensions and the theory plug-in have been developed.
			They are now found in many places, and in Rodin 3.0 they are even more present.

			A FormulaFactory instance is used to parse and make formulas in a given mathematical language.
			Proofs now bear their own formula factory, potentially different from the formula factories of the other proofs in the same file, hence the addition of ''IProofTree.getFormulaFactory()'' and ''IPRProof.getFormulaFactory()'' methods. You must be aware of that fact if you pass formula factory arguments in method calls, in order to use the right one.

	=== Context Dependent Reasoners ===		=== Context Dependent Reasoners ===

imported>Nicolas: /* Sequent Prover */

2014-01-14T18:00:58Z

Sequent Prover

← Older revision		Revision as of 18:00, 14 January 2014
Line 111:		Line 111:

	=== Formula Factory ===		=== Formula Factory ===

			=== Context Dependent Reasoners ===

			The older notion of Signature Reasoner has been replaced by that of Context Dependent Reasoner.
			In org.eventb.core.seqprover.reasoners extension point, reasoners now have an optional ''contextDependent'' boolean. The proofs that use a context dependent reasoner will not be trusted merely based on their dependencies, but instead they will be replayed in order to update their status.

			This applies in particular to '''Theory Plug-in reasoners''', that depend on the mathematical language and proof rules defined in theories, which change over time. Thus, these reasoners shall be declared as ''context dependent'' in Rodin 3.0.

	== Rodin Core Plug-ins ==		== Rodin Core Plug-ins ==

← Older revision		Revision as of 09:58, 27 January 2014
Line 18:		Line 18:
	* It is an {{class\|ISealedTypeEnvironment}}: you must provide an immutable snapshot of your type environment using method ''makeSnapshot()''.		* It is an {{class\|ISealedTypeEnvironment}}: you must provide an immutable snapshot of your type environment using method ''makeSnapshot()''.
	* It is an {{class\|ITypeEnvironmentBuilder}}: here two choices are possible, you could give your object reference as parameter and it will be modified if a further treatment is made on it or you could give a copy of your object using method ''makeBuilder()'' to prevent side effect on your object.		* It is an {{class\|ITypeEnvironmentBuilder}}: here two choices are possible, you could give your object reference as parameter and it will be modified if a further treatment is made on it or you could give a copy of your object using method ''makeBuilder()'' to prevent side effect on your object.
	* It is an {{class\|~~ITypeEnvrionment~~}}: it is a convenient way to have genericity since it is the super type of both preceding ones. You can opt for any options above. There is a convention that a parameter of type ITypeEnvironment is not modified by the callee, but this is not enforced. If you want a strong guarantee that the type environment that you pass cannot be modified, pass it as a sealed environment.		* It is an {{class\|ITypeEnvironment}}: it is a convenient way to have genericity since it is the super type of both preceding ones. You can opt for any options above. There is a convention that a parameter of type ITypeEnvironment is not modified by the callee, but this is not enforced. If you want a strong guarantee that the type environment that you pass cannot be modified, pass it as a sealed environment.

	Reciprocally, if you ask for a type environment as parameter, these 3 options are available:		Reciprocally, if you ask for a type environment as parameter, these 3 options are available:
	* Use an {{class\|ISealedTypeEnvironment}}: if you want to provide a strong guarantee that you will not modify the parameter.		* Use an {{class\|ISealedTypeEnvironment}}: if you want to provide a strong guarantee that you will not modify the parameter.
	* Use an {{class\|~~ITypeEnvrionmentBuilder~~}}: if you need to modify the received type environment by side effect		* Use an {{class\|ITypeEnvironmentBuilder}}: if you need to modify the received type environment by side effect
	* Use an {{class\|~~ITypeEnvrionment~~}}: in case you will not modify the type environment and allow the user to provide the most convenient type for him. You must not later cast the parameter to type {{class\|ITypeEnvironmentBuilder}}.		* Use an {{class\|ITypeEnvironment}}: in case you will not modify the type environment and allow the user to provide the most convenient type for him. You must not later cast the parameter to type {{class\|ITypeEnvironmentBuilder}}.

	Finally regarding return type of methods, you should use only one of the two following choices ({{class\|ITypeEnvironment}} is discouraged since it provides no information about what is actually returned):		Finally regarding return type of methods, you should use only one of the two following choices ({{class\|ITypeEnvironment}} is discouraged since it provides no information about what is actually returned):