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

Let's consider that you dispose of a new type environment of type 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 ISealedTypeEnvironment: you must provide an immutable snapshot of your type environment using method makeSnapshot().
• It is an 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 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 ISealedTypeEnvironment: if you want to provide a strong guarantee that you will not modify the parameter.
• Use an ITypeEnvrionmentBuilder: if you need to modify the received type environment by side effect
• Use an 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 ITypeEnvironmentBuilder.

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

• Return an 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 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 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 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 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 getFreeIdentifiers() method of class Formula now returns a larger list of free identifiers. You still can use method getSyntacticallyFreeIdentifiers() 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. 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 translate(FormulaFactory) to 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 IDatatypeBuilder provided by a FormulaFactory using makeDatatypeBuilder(String, GivenType[]). This step sets the datatype name and its type parameters (as given types).
• Add a datatype constructor IConstructorBuilder on the builder using method addConstructor(String) which sets the constructor name.
• Add the arguments of a constructor using addArgument(Type) (simple argument) or addArgument(String, Type) (destructor with a name). The argument type will be provided in the right format by using the parseType(String) method of the IDatatypeBuilder.
• Once all constructors, and their arguments, were added:
  • Check that at least one basic constructor exists by using the hasBasicConstructor() method of the datatype builder
  • Finalize the datatype by using the finalizeDatatype() builder method which returns the finalized datatype

As you can have noticed a constructor argument type is now represented with a standard event-B 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 parseType(String) 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 IDatatype has also been simplified and some services have been moved in the new specialized extensions:

• ITypeConstructorExtension for the type constructor, it provides:
  • the type parameters names
• IConstructorExtension for a constructor, it provides:
  • the constructor name
  • the constructor arguments as: destructor extensions, types, expressions
• 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 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.

Rodin Core Plug-in

TODO: Document DB relations
The contents of any file managed by the Rodin database are based on a hierarchical model, defined by element types which the database can handle and the relationships between these types of element.
Historically, the sole definition of elements was provided from the Rodin Core extension point org.rodinp.core.internalElementTypes to plug-in developers. The relationship definitions were then externally managed by the Event-B UI plug-in which defined org.eventb.ui.editorItems extension point to contribute to the Event-B Editor. Thus, the structure could be considered weak, as editors where in charge of maintaining file structures. In other terms, it was possible to get elements at wrong locations provided that edition happened outside the Event-B Editor.

In Rodin 3.0, type relationships are enforced at database level, to ensure the structural coherence in database of any managed Rodin file. Consequently, the definition of type relationships is now provided to plug-in developers from the same level as the element type definition: the Rodin Core plug-in.

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 UI Plug-in

TODO: Document what has changed