View source for Rodin 3.0 Plug-in Migration Guide

Release 3.0 of the Rodin platform introduces important changes to the Rodin
Platform API.  These changes make the core platform stronger and fix some
erroneous design decisions that were taken in previous Rodin releases.

This guide details the actions that plug-in developers must take in order to
port their plug-ins from the 2.8 API to the 3.0 API.

== AST Library ==

=== Type Environments ===

Type environments have changed in Rodin 3.0 in order to reinforce their good use and their robustness. 
One of these changes concerns their mutability state and has an important impact on type environments use. 

The general principle is the following, if you want to create and build a type environment then you have to use an {{class|ITypeEnvironmentBuilder}} which is the only type providing methods that could modify the type environment. Then in some case you could need to guarantee that your type environment will not mutate anymore and make a snapshot of type {{class|ISealedTypeEnvironment}}. 

Let's consider that you dispose of a new type environment of type {{class|ITypeEnvironmentBuilder}}, in some cases you will need to provide it as a parameter and you will face 3 options depending on the parameter Java type:
* 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|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.

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|ITypeEnvrionmentBuilder}}: 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}}.

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):
* Return an {{class|ISealedTypeEnvironment}}: it guarantees that the type environment will not mutate and allow to share its reference as long as no modification is needed.
* Return an {{class|ITypeEnvrionmentBuilder}}: it allows modifications and must be used in case no reference is kept on the object or if you want to share the modifications on it.

And the last case but not the least, if you create a type environment field you have also 2 options:
* You should use an {{class|ISealedTypeEnvironment}} in one of these cases:
** It is never modified or has an expected immutable behavior.
** The type environment is built all at once and is never modified later.
** You need to return a copy of it often (allows to share the reference) and modify it only rarely.
* You should use an {{class|ITypeEnvironmentBuilder}} in one of these cases:
** The field is only internal to the class (and has builder type at least one time).
** The type environment is built to be returned externally and the reference can be shared.

Those precendent cases are only the most general examples that you will face and are made to give an idea of the new API good usage, but finally the developper is the only person that can decide of the better option to choose.

=== Free Identifier Cache ===

Every instance of {{class|Formula}} contains a cache of the free identifiers
occurring within the tree rooted at that node.  Since Rodin 3.0, the free
identifiers that correspond to the names of given types that occur in the
formula tree are also added to the free identifier cache.  Consequently, the
<tt>getFreeIdentifiers()</tt> method of class {{class|Formula}} now returns a
larger list of free identifiers.  You still can use method
<tt>getSyntacticallyFreeIdentifiers()</tt> if you are not interested in the
name of given types, at the price of a small performance penalty, because the
latter method will traverse the whole formula tree.

=== Formula Factories ===

The AST library now demands that all nodes and types of a formula have been
built by the same formula factory.  It is no longer possible to mix nodes
coming from different factories. Moreover, this modification made the notion
of language versions obsolete: references to the <tt>LanguageVersion</tt> 
enumeration have been removed.<br> In most cases, e.g., in the sequent prover,
this restriction is not important as all formulas are always in the same
language and therefore built by the same factory.  If you are in a special
case where you need to mix several formula factories, we have added the
<tt>translate(FormulaFactory)</tt> to class {{class|Formula}} which allows to
rebuild a full copy of a formula with a different formula factory.

=== Datatype ===

==== Datatype Definition ====

The definition of datatypes has completely changed to be simplest 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:
* 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).
* Add a datatype constructor {{class|IConstructorBuilder}} on the builder using method <tt>addConstructor(String)</tt> which sets the constructor name.
* Add the arguments of a constructor using <tt>addArgument(Type)</tt> (simple argument) or <tt>addArgument(String, Type)</tt> (destructor with a name). The argument type will be provided in the right format by using the <tt>parseType(String)</tt> method of the {{class|IDatatypeBuilder}}.
* Once all constructors, and their arguments, were added:
** Check that at least one basic constructor exists by using the <tt>hasBasicConstructor()</tt> method of the datatype builder
** 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. 
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)
* 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".

==== Datatype Use ====

The datatype interface {{class|IDatatype}} has also been simplified and some services have been moved in the new specialized extensions:
* {{class|ITypeConstructorExtension}} for the type constructor, it provides:
** the type parameters names
* {{class|IConstructorExtension}} for a constructor, it provides:
** the constructor name
** the constructor arguments as: destructor extensions, types, expressions
* {{class|IDestructorExtension}} for a destructor, it provides:
** the destructor name
** the destructor type
** the parent constructor

Those new interfaces provide the way to identify easily the extensions of a datatype and their relationships, it avoids in many cases the use of the {{class|IDatatype}} object like it was the case before.
Moreover the datatype interface now provides access to the datatype constructors and destructors giving their name instead of their identifier.

== Sequent Prover ==

All constants, methods and classes that were marked as deprecated in the API have been removed. If you were using one of these, please read its Javadoc in Rodin 2.7 which describes an alternative implementation.

=== New Action Rewrite Hypothesis ===
Reasoners now can use a new type of action: IRewriteHypAction. It is equivalent to a Forward Inference Action followed by a Hide Action.

The interface IForwardHypAction is still present, as well as the "HIDE" type of ISelectionHypAction. However, if your reasoner performs a forward hypothesis action directly followed by a "hide" action which hides the hypothesis used during the inference, then your reasoner indeed performs a rewrite action. We strongly encourage you to use IRewriteHypAction interface for such use.
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 ===

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 ===

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 Database structure enforcement ===
==== A bit of background ====
The contents of any file managed by the Rodin database are based on a hierarchical model, defined by item types (i.e. elements or attribute types) which the database handles and the relationships between them.<br />
Historically, the sole definition of items was provided from the Rodin Core extension points <tt>org.rodinp.core.internalElementTypes</tt> and <tt>org.rodinp.core.attributeTypes</tt> to plug-in developers. The relationship definitions were then implicit and externally managed by the Event-B UI plug-in which defined <tt>org.eventb.ui.editorItems</tt> extension point to contribute to the Event-B Editor. Thus, the structure could be considered weak, as only editors were in charge of maintaining the file structure. In other terms, it was possible to get elements or attributes at wrong locations in the Rodin database provided that edition happened outside the Event-B Editor.<br />

In Rodin 3.0, type relationships are enforced at database level, to ensure the structural coherence of any managed Rodin file in the Rodin database. In other terms, all elements which are present at some locations in the textual representation of the Rodin file (used for persistence), which however do not have sense in regard of the structural definitions on such a file, will be ignored by the Rodin database (but kept in the text file anyway).
Consequently, the way to define item type relationships is now provided to plug-in developers from the same level as the element type definition: the Rodin Core plug-in.

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

''IMPORTANT:'' Moreover, the compatibility mechanism does not offer backward compatibility for elements which are contributed to the database but are not supposed to be edited from the Event-B editor.

=== Rodin keyboard core and UI separation ===
==== A bit of background ====

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

Historically, only one plug-in has been defined to provide these two functionnalities : <tt>org.rodinp.keyboard</tt>.<br />
This was cumbersome for plug-ins developers wanting to use only the simple translation mechanism and had to manage unwanted plug-in dependencies.
Indeed, a dependency on <tt>org.eventb.ui</tt> (and on which the second mechanism relies) was imposed to them.

==== Migration instructions ====
In Rodin 3.0, the UI part and core parts of the translation capability have been separated into two different plug-ins: <tt>org.rodinp.keyboard.core</tt> and <tt>org.rodinp.keyboard.ui</tt>.<br />
The migration actions you have to perform depends on what you need from the translation mechanism:
* if your plug-in use the simple translation mechanism: you simply have to update your plug-in dependencies from <tt>org.rodinp.keyboard</tt> to <tt>org.rodinp.keyboard.core</tt>, and fix corresponding imports in your code.
* if your plug-in defines UI widgets that need to be adapted: you simply have to update your plug-in dependencies from <tt>org.rodinp.keyboard</tt> to <tt>org.rodinp.keyboard.ui</tt>, and fix corresponding imports in your code.

== Event-B Core Plug-in ==

All constants, methods and classes that were marked as deprecated in the API have been removed. If you were using one of these, please read its Javadoc in Rodin 2.7 which describes an alternative implementation.

== Event-B PP and PP Trans Plug-ins ==

Methods that were marked as deprecated in the API have been removed.

== Event-B UI Plug-in ==

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:Rodin Platform]]