Update to Rodin 3.3 sources

META-INF/MANIFEST.MF

@@ -2,7 +2,7 @@ Manifest-Version: 1.0
 Bundle-ManifestVersion: 2
 Bundle-Name: %pluginName
 Bundle-SymbolicName: org.eventb.core.ast;singleton:=true
-Bundle-Version: 3.2.0.qualifier
+Bundle-Version: 3.3.0.qualifier
 Bundle-Vendor: %providerName
 Bundle-Localization: plugin
 Export-Package: org.eventb.core.ast,

build.gradle

@@ -6,7 +6,7 @@ plugins {
 }
 
 project.group = 'de.hhu.stups'
-project.version = "3.2.1"
+project.version = "3.3.0-SNAPSHOT"
 final isSnapshot = project.version.endsWith("-SNAPSHOT")
 
 sourceSets {

src/org/eventb/core/ast/ExtendedPredicate.java

 /*******************************************************************************
- * Copyright (c) 2010, 2013 Systerel and others.
+ * Copyright (c) 2010, 2016 Systerel and others.
  * All rights reserved. This program and the accompanying materials
  * are made available under the terms of the Eclipse Public License v1.0
  * which accompanies this distribution, and is available at
@@ -13,9 +13,12 @@ package org.eventb.core.ast;
 import static org.eventb.core.ast.AssociativeHelper.getSyntaxTreeHelper;
 import static org.eventb.core.ast.ExtensionHelper.makeParserPrinter;
 import static org.eventb.core.ast.extension.IOperatorProperties.FormulaType.PREDICATE;
+import static org.eventb.core.ast.extension.IOperatorProperties.Notation.INFIX;
 import static org.eventb.core.ast.extension.IOperatorProperties.Notation.PREFIX;
 import static org.eventb.internal.core.ast.extension.ArityCoverage.ANY;
 import static org.eventb.internal.core.ast.extension.ArityCoverage.ONE_OR_MORE;
+import static org.eventb.internal.core.ast.extension.ArityCoverage.TWO;
+import static org.eventb.internal.core.ast.extension.ArityCoverage.NONE;
 
 import java.util.ArrayList;
 import java.util.Arrays;
@@ -66,6 +69,16 @@ public class ExtendedPredicate extends Predicate implements IExtendedFormula {
 				return new SubParsers.ExtendedPredParen(kind, tag);
 			}
 
+		},
+		
+		EXTENDED_RELATIONAL_PREDICATE(INFIX, PREDICATE, TWO, NONE, TWO, false) {
+
+			@Override
+			protected IParserPrinter<ExtendedPredicate> makeParser(int kind,
+					int tag) {
+				return new SubParsers.ExtendedRelationalPredicateParser(kind, tag);
+			}
+			
 		},
 		;
 
@@ -98,7 +111,7 @@ public class ExtendedPredicate extends Predicate implements IExtendedFormula {
 
 				@Override
 				public boolean isSpaced() {
-					return false;
+					return ExtendedPredicateParsers.this.getOperatorCoverage().getNotation() == INFIX;
 				}
 				
 				@Override

src/org/eventb/core/ast/Formula.java

 /*******************************************************************************
- * Copyright (c) 2005, 2014 ETH Zurich and others.
+ * Copyright (c) 2005, 2017 ETH Zurich and others.
  * All rights reserved. This program and the accompanying materials
  * are made available under the terms of the Eclipse Public License v1.0
  * which accompanies this distribution, and is available at
@@ -2393,13 +2393,19 @@ public abstract class Formula<T extends Formula<T>> {
 	 *             if this formula is an assignment
 	 * @throws IllegalStateException
 	 *             if this formula is not type-checked.
+	 * @throws IllegalArgumentException
+	 *             if the given specialization is not compatible with this
+	 *             formula, that is the specialization contains a substitution
+	 *             for an identifier with the same name as an identifier in this
+	 *             formula, but with a different type
 	 * 
 	 * @since 2.6
 	 */
 	public T specialize(ISpecialization specialization) {
 		ensureTypeChecked();
 		final Specialization spec = (Specialization) specialization;
-		return rewrite(spec);
+		spec.prepare(this);
+		return rewrite(spec.getFormulaRewriter());
 	}
 
 	/**

src/org/eventb/core/ast/FreeIdentifier.java

 /*******************************************************************************
- * Copyright (c) 2005, 2013 ETH Zurich and others.
+ * Copyright (c) 2005, 2017 ETH Zurich and others.
  * All rights reserved. This program and the accompanying materials
  * are made available under the terms of the Eclipse Public License v1.0
  * which accompanies this distribution, and is available at
@@ -297,10 +297,25 @@ public class FreeIdentifier extends Identifier {
 		return false;
 	}
 
+	/**
+	 * Returns the given type corresponding to this type-checked identifier.
+	 * <p>
+	 * The returned type is <em>not</em> the type of this identifier.
+	 * </p>
+	 * 
+	 * @return the given type represented by this identifier
+	 * @throws IllegalStateException
+	 *             when this identifier is not a given type or is not
+	 *             type-checked
+	 * @see Type#toExpression()
+	 * @see #isATypeExpression()
+	 * @since 3.3 change return type to GivenType
+	 */
 	@Override
-	public Type toType() {
+	public GivenType toType() {
 		if (!isATypeExpression()) {
-			return super.toType();
+			throw new IllegalStateException(
+					"Identifier does not denote a type: " + toString());
 		}
 		return getFactory().makeGivenType(this);
 	}

src/org/eventb/core/ast/ISpecialization.java

 /*******************************************************************************
- * Copyright (c) 2012, 2014 Systerel and others.
+ * Copyright (c) 2012, 2017 Systerel and others.
  * All rights reserved. This program and the accompanying materials
  * are made available under the terms of the Eclipse Public License v1.0
  * which accompanies this distribution, and is available at
@@ -7,18 +7,21 @@
  *
  * Contributors:
  *     Systerel - initial API and implementation
+ *     University of Southampton - added support for predicate variables
  *******************************************************************************/
 package org.eventb.core.ast;
 
 /**
- * Common protocol for describing a specialization, which groups together a type
- * substitution and a free identifier substitution in one object. It allows to
- * specialize a formula by applying both substitutions at once.
+ * Common protocol for describing a specialization, which groups together type
+ * substitutions, free-identifier substitutions, and predicate-variable
+ * substitutions in one object. It allows to specialize a formula by applying
+ * all these substitutions at once.
  * <p>
- * Instances of this class can be created only through a formula factory. Type
- * and free identifier substitutions are then added one by one using
- * <code>put()</code> methods. Finally, the instance is passed as argument to a
- * <code>specialize()</code> method on a type, type environment or formula.
+ * Instances of this class can be created only through a formula factory. Type,
+ * free-identifier and predicate-variable substitutions are then added one by
+ * one using <code>put()</code> methods. Finally, the instance is passed as
+ * argument to a <code>specialize()</code> method on a type, type environment or
+ * formula.
  * </p>
  * <p>
  * The substitutions can also change the formula factory. Consequently, all
@@ -26,9 +29,9 @@ package org.eventb.core.ast;
  * specialization.
  * </p>
  * <p>
- * Both substitutions must be compatible, that is the expression to be
+ * These substitutions must be compatible, that is the expression to be
  * substituted for an identifier must bear a type which is the result of
- * applying the type substitution to the type of the identifier.
+ * applying the type substitutions to the type of the identifier.
  * </p>
  * <p>
  * This condition must hold after every method call. This implies that a type
@@ -52,19 +55,35 @@ package org.eventb.core.ast;
  * <code>T</code> for <code>x</code> of type <code>S</code>.
  * </p>
  * <p>
- * This side-effect is made on purpose to ensure that successive applications of
- * a specialization to several type environments or formulas are all compatible.
+ * When defining substitutions, a specialization also maintains a destination
+ * type environment. It contains all the identifiers that have been used in the
+ * right-hand sides of substitutions, as well as all identifiers that have
+ * occurred in a formula passed to <code>specialize()</code> methods and that
+ * have not been substituted.
+ * </p>
+ * <p>
+ * The purpose of this destination type environment, together with the automatic
+ * completion of substitutions ensures that successive applications of a
+ * specialization to several type environments or formulas are all compatible.
  * In particular, if a formula type-checks with respect to some type
  * environment, then the specialized formula also type-checks with the
  * specialized type environment, under the condition that both specialization
  * are performed with the same instance of this class.
  * </p>
  * <p>
- * In the rare cases where this side-effect is not wanted, one can always clone
+ * Similarly, when specializing a formula, an instance of this class can change
+ * by side-effect in the following manner: For each predicate variable, not
+ * already part of the predicate variable substitution and which occurs in the
+ * formula, a new predicate variable substitution is added to this
+ * specialization. It maps that predicate variable to itself.
+ * </p>
+ * <p>
+ * In the rare cases where the side-effects are not wanted, one can always clone
  * a specialization object and use the clone to apply a specialization.
  * </p>
  * 
  * @author Laurent Voisin
+ * @author htson - added support for predicate variables.
  * 
  * @see FormulaFactory#makeSpecialization()
  * @see Type#specialize(ISpecialization)
@@ -100,6 +119,11 @@ public interface ISpecialization {
 	 * substitution must be compatible with already registered substitutions
 	 * (for both given types and free identifiers). The value must have been
 	 * created by the same formula factory as this instance.
+	 * </p>
+	 * <p>
+	 * This method can have side-effects, as described in
+	 * {@link ISpecialization}.
+	 * </p>
 	 * 
 	 * @param type
 	 *            given type to specialize
@@ -110,6 +134,7 @@ public interface ISpecialization {
 	 *             registered substitutions or the value has been created by
 	 *             another formula factory
 	 * @see Type#getFactory()
+	 * @see #canPut(GivenType, Type)
 	 */
 	void put(GivenType type, Type value);
 
@@ -118,7 +143,7 @@ public interface ISpecialization {
 	 * 
 	 * @param type
 	 *            some given type
-	 * @return the type to be substituted for the given given type of
+	 * @return the type to be substituted for the given given type or
 	 *         <code>null</code> if no substitution has been defined for the
 	 *         given given type
 	 * @since 3.1
@@ -135,6 +160,10 @@ public interface ISpecialization {
 	 * bound identifiers, it is up to the caller to manage that they do not
 	 * escape their scope. The given expression must have been created by the
 	 * same formula factory as this instance.
+	 * <p>
+	 * This method can have side-effects, as described in
+	 * {@link ISpecialization}.
+	 * </p>
 	 * 
 	 * @param ident
 	 *            a typed identifier to substitute
@@ -147,6 +176,7 @@ public interface ISpecialization {
 	 *             created by another formula factory
 	 * @see Formula#isTypeChecked()
 	 * @see Formula#getFactory()
+	 * @see #canPut(FreeIdentifier, Expression)
 	 */
 	void put(FreeIdentifier ident, Expression value);
 
@@ -155,11 +185,130 @@ public interface ISpecialization {
 	 * 
 	 * @param ident
 	 *            a typed identifier
-	 * @return the expression to be substituted for the given identifier of
+	 * @return the expression to be substituted for the given identifier or
 	 *         <code>null</code> if no substitution has been defined for the
 	 *         given identifier
 	 * @since 3.1
 	 */
 	Expression get(FreeIdentifier ident);
 
+	/**
+	 * Checks whether the proposed type substitution is compatible with already
+	 * registered substitutions (for given types, free identifiers, and
+	 * predicate variables), i.e., if the precondition for
+	 * {@link #put(GivenType, Type)} is satisfied. The value must have been
+	 * created by the same formula factory as this instance. This method does
+	 * <em>not</em> modify the specialization instance.
+	 * 
+	 * @param type
+	 *            given type to specialize
+	 * @param value
+	 *            replacement for the given type
+	 * @return <code>true</code> if the proposed type substitution is compatible
+	 *         with already registered substitutions, <code>false</code>
+	 *         otherwise.
+	 * @throws IllegalArgumentException
+	 *             if the value has been created by another formula factory
+	 * @author htson
+	 * @since 3.3
+	 */
+	boolean canPut(GivenType type, Type value);
+	
+	/**
+	 * Checks whether the proposed free-identifier substitution is compatible
+	 * with already registered substitutions (for given types, free identifiers,
+	 * and predicate variables), i.e., if the precondition of
+	 * {@link #put(FreeIdentifier, Expression)} is satisfied. Both the type and
+	 * the value must be type-checked. The value expression must have been
+	 * created by the same formula factory as this instance. This method does
+	 * <em>not</em> modify the specialization instance.
+	 * 
+	 * @param ident
+	 *            a typed identifier to substitute
+	 * @param value
+	 *            a typed expression to substitute for the given identifier
+	 * @return <code>true</code> if the proposed free identifier substitution is
+	 *         compatible with already registered substitutions. Return
+	 *         <code>false</code> otherwise.
+	 * @throws IllegalArgumentException
+	 *             if either parameter is not typed, or the value has been
+	 *             created by another formula factory
+	 * @author htson
+	 * @since 3.3
+	 */
+	boolean canPut(FreeIdentifier ident, Expression value);
+
+	/**
+	 * Adds a new predicate variable substitution to this specialization. All
+	 * substitutions will be applied in parallel when specializing a formula.
+	 * The given predicate value must be typed, but needs not be well-formed. In
+	 * case the predicate value contains bound identifiers, it is up to the
+	 * caller to manage that they do not escape their scope. The given predicate
+	 * value must have been created by the same formula factory as this
+	 * instance.
+	 * <p>
+	 * This method can have side-effects, as described in
+	 * {@link ISpecialization}.
+	 * </p>
+	 * 
+	 * @param predVar
+	 *            a predicate variable to substitute
+	 * @param value
+	 *            a typed predicate to substitute for the given predicate
+	 *            variable.
+	 * @return <code>true</code> if the proposed predicate variable substitution
+	 *         is compatible with already registered substitutions, and this
+	 *         specialization instance has been changed accordingly. Return
+	 *         <code>false</code> otherwise and this specialization instance is
+	 *         unchanged.
+	 * @throws IllegalArgumentException
+	 *             if the value is not typed or has been created by another
+	 *             formula factory
+	 * @see Formula#isTypeChecked()
+	 * @see Formula#getFactory()
+	 * @author htson
+	 * @since 3.3
+	 */
+	boolean put(PredicateVariable predVar, Predicate value);
+
+	/**
+	 * Returns the predicate to be substituted for the given predicate variable.
+	 * 
+	 * @param predVar
+	 *            a predicate variable.
+	 * @return the predicate to be substituted for the given predicate variable
+	 *         or <code>null</code> if no substitution has been defined for the
+	 *         given predicate variable
+	 * @author htson
+	 * @since 3.3
+	 */
+	Predicate get(PredicateVariable predVar);
+
+	/**
+	 * Returns the set of given types to be substituted.
+	 * 
+	 * @return the set of given types to be substituted
+	 * @author htson
+	 * @since 3.3
+	 */
+	GivenType[] getTypes();
+
+	/**
+	 * Returns the set of free identifiers to be substituted.
+	 * 
+	 * @return the set of free identifiers to be substituted
+	 * @author htson
+	 * @since 3.3
+	 */
+	FreeIdentifier[] getFreeIdentifiers();
+
+	/**
+	 * Returns the set of predicate variables to be substituted.
+	 * 
+	 * @return the set of predicate variables to be substituted
+	 * @author htson
+	 * @since 3.3
+	 */
+	PredicateVariable[] getPredicateVariables();
+
 }

src/org/eventb/core/ast/ITypeEnvironment.java

 /*******************************************************************************
- * Copyright (c) 2005, 2014 ETH Zurich and others.
+ * Copyright (c) 2005, 2017 ETH Zurich and others.
  * All rights reserved. This program and the accompanying materials
  * are made available under the terms of the Eclipse Public License v1.0
  * which accompanies this distribution, and is available at
@@ -271,6 +271,12 @@ public interface ITypeEnvironment {
 	 *            the specialization to apply
 	 * @return the type environment obtained by applying the given
 	 *         specialization to this type environment
+	 * @throws IllegalArgumentException
+	 *             if the given specialization is not compatible with this type
+	 *             environment, that is the specialization contains a
+	 *             substitution for an identifier with the same name as an
+	 *             identifier in this type environment, but with a different
+	 *             type
 	 * @since 3.0
 	 */
 	ITypeEnvironmentBuilder specialize(ISpecialization specialization);

src/org/eventb/core/ast/Type.java

 /*******************************************************************************
- * Copyright (c) 2005, 2014 ETH Zurich and others.
+ * Copyright (c) 2005, 2017 ETH Zurich and others.
  * All rights reserved. This program and the accompanying materials
  * are made available under the terms of the Eclipse Public License v1.0
  * which accompanies this distribution, and is available at
@@ -296,6 +296,11 @@ public abstract class Type {
 	 * @param specialization
 	 *            the specialization to apply
 	 * @return a specialization of this type or <code>this</code> if unchanged
+	 * @throws IllegalArgumentException
+	 *             if the given specialization is not compatible with this type,
+	 *             that is the specialization contains a substitution for an
+	 *             identifier with the same name as a given type in this type,
+	 *             but with a different type
 	 * @since 2.6
 	 */
 	public final Type specialize(ISpecialization specialization) {

src/org/eventb/core/ast/extension/ExtensionFactory.java

 /*******************************************************************************
- * Copyright (c) 2010 Systerel and others.
+ * Copyright (c) 2010, 2016 Systerel and others.
  * All rights reserved. This program and the accompanying materials
  * are made available under the terms of the Eclipse Public License v1.0
  * which accompanies this distribution, and is available at
@@ -15,13 +15,14 @@ import static org.eventb.core.ast.extension.IOperatorProperties.MULTARY_2;
 import static org.eventb.core.ast.extension.IOperatorProperties.UNARY;
 import static org.eventb.core.ast.extension.IOperatorProperties.FormulaType.EXPRESSION;
 import static org.eventb.core.ast.extension.IOperatorProperties.FormulaType.PREDICATE;
+import static org.eventb.core.ast.extension.IOperatorProperties.Notation.INFIX;
 import static org.eventb.core.ast.extension.IOperatorProperties.Notation.PREFIX;
 
 import org.eventb.core.ast.extension.IOperatorProperties.FormulaType;
 import org.eventb.internal.core.ast.extension.Arity;
-import org.eventb.internal.core.ast.extension.TypeDistribs.MixedTypes;
-import org.eventb.internal.core.ast.extension.TypeDistribs.AllSameType;
 import org.eventb.internal.core.ast.extension.ExtensionKind;
+import org.eventb.internal.core.ast.extension.TypeDistribs.AllSameType;
+import org.eventb.internal.core.ast.extension.TypeDistribs.MixedTypes;
 
 /**
  * @author Nicolas Beauger
@@ -84,6 +85,24 @@ public class ExtensionFactory {
 		return new ExtensionKind(PREFIX, formulaType, childTypes, false);
 	}
 
+	/**
+	 * Make an infix extension kind.
+	 * 
+	 * @param formulaType
+	 *            type of the resulting formula
+	 * @param childTypes
+	 *            type distribution of child formulae
+	 * @param isAssociative
+	 *            <code>true</code> for associative kind, <code>false</code>
+	 *            otherwise
+	 * @return a new extension kind
+	 * @since 3.3
+	 */
+	public static IExtensionKind makeInfixKind(FormulaType formulaType,
+			ITypeDistribution childTypes, boolean isAssociative) {
+		return new ExtensionKind(INFIX, formulaType, childTypes, isAssociative);
+	}
+
 	public static IArity makeArity(int min, int max) {
 		return new Arity(min, max);
 	}

src/org/eventb/core/ast/extension/IPriorityMediator.java

 /*******************************************************************************
- * Copyright (c) 2010 Systerel and others.
+ * Copyright (c) 2010, 2016 Systerel and others.
  * All rights reserved. This program and the accompanying materials
  * are made available under the terms of the Eclipse Public License v1.0
  * which accompanies this distribution, and is available at
@@ -18,7 +18,10 @@ package org.eventb.core.ast.extension;
 public interface IPriorityMediator {
 
 	/**
-	 * Adds a priority between operators of given ids.
+	 * Adds a priority between the two operators with the given ids.
+	 * <p>
+	 * Both operators must belong to the same operator group.
+	 * </p>
 	 * <p>
 	 * lowOpId operator gets a lower priority than highOpId operator.
 	 * </p>
@@ -37,6 +40,9 @@ public interface IPriorityMediator {
 	 *            an operator id
 	 * @throws CycleError
 	 *             if adding the given priority introduces a cycle
+	 * @throws IllegalArgumentException
+	 *             if the operators do not belong to the same operator group, or
+	 *             if one of the given operator ids has not been declared
 	 */
 	void addPriority(String lowOpId, String highOpId) throws CycleError;
 
@@ -56,7 +62,8 @@ public interface IPriorityMediator {
 	 *            a group id
 	 * @throws CycleError
 	 *             if adding the given priority introduces a cycle
+	 * @throws IllegalArgumentException
+	 *             if one of the given group ids has not been declared
 	 */
-	void addGroupPriority(String lowGroupId, String highGroupId)
-			throws CycleError;
+	void addGroupPriority(String lowGroupId, String highGroupId) throws CycleError;
 }

src/org/eventb/internal/core/ast/BindingSubstitution.java

 /*******************************************************************************
- * Copyright (c) 2005, 2013 ETH Zurich and others.
+ * Copyright (c) 2005, 2016 ETH Zurich and others.
  * All rights reserved. This program and the accompanying materials
  * are made available under the terms of the Eclipse Public License v1.0
  * which accompanies this distribution, and is available at
@@ -41,7 +41,7 @@ public class BindingSubstitution extends SimpleSubstitution {
 		
 		super(ff);
 		this.offset = identsToBind.size();
-		map = new HashMap<FreeIdentifier, Substitute>(offset * 4 / 3 + 1);
+		map = new HashMap<FreeIdentifier, Substitute<Expression>>(offset * 4 / 3 + 1);
 
 		int index = offset - 1;
 		for (FreeIdentifier ident : identsToBind) {

src/org/eventb/internal/core/ast/BoundIdentDeclRemover.java

 /*******************************************************************************
- * Copyright (c) 2005, 2013 ETH Zurich and others.
+ * Copyright (c) 2005, 2016 ETH Zurich and others.
  * All rights reserved. This program and the accompanying materials
  * are made available under the terms of the Eclipse Public License v1.0
  * which accompanies this distribution, and is available at
@@ -33,7 +33,7 @@ public class BoundIdentDeclRemover extends Substitution {
 	protected final List<BoundIdentDecl> newDecls;
 	
 	// Reversed array of substitutes
-	protected final Substitute[] substitutes;
+	protected final Substitute<Expression>[] substitutes;
 	
 	/**
 	 * Creates a new substitution for removing some bound identifier
@@ -60,7 +60,9 @@ public class BoundIdentDeclRemover extends Substitution {
 		assert decls.length == keep.length;
 
 		final int lastIndex = decls.length - 1;
-		substitutes = new Substitute[keep.length];
+		@SuppressWarnings("unchecked")
+		final Substitute<Expression>[] temp = new Substitute[keep.length];
+		substitutes = temp;
 		newDecls = new ArrayList<BoundIdentDecl>(decls.length);
 		int newIndex = 0;
 		// We need to traverse both arrays backward to compute the new indexes

src/org/eventb/internal/core/ast/DefaultTypeCheckingRewriter.java

 /*******************************************************************************
- * Copyright (c) 2012, 2013 Systerel and others.
+ * Copyright (c) 2012, 2016 Systerel and others.
  * All rights reserved. This program and the accompanying materials
  * are made available under the terms of the Eclipse Public License v1.0
  * which accompanies this distribution, and is available at
@@ -39,12 +39,20 @@ import org.eventb.core.ast.UnaryPredicate;
 
 /**
  * Default implementation of a type-checking rewriter that does not perform any
- * rewrite. In this class, we do not use the <code>checkReplacement()</code>
- * methods because the result bears the same type by construction. However,
- * these methods must be used by sub-classes that actually perform a rewrite
- * when it cannot be proven that the rewrite is always type-checked.
+ * rewrite by default. In this class, we do not use the
+ * <code>checkReplacement()</code> methods because the result bears the expected
+ * type by construction. However, these methods must be used by sub-classes that
+ * actually perform a rewrite when it cannot be proven that the rewrite is
+ * always type-checked. Note that these methods cannot be used in the case where
+ * types are also rewritten (it checks that the types did not change).
  * 
  * <p>
+ * If a type rewriter is given to the constructor, then this class will
+ * implement type rewriting for all nodes. It is then expected to be sub-classed
+ * so that free identifiers (among others) are also rewritten to conform to the
+ * new type.
+ * </p>
+ * <p>
  * This implementation guarantees that a leaf node is rebuilt with the rewriter
  * factory if the factory of the node is different as required by
  * {@link ITypeCheckingRewriter}. Consequently, when extending this class,
@@ -94,6 +102,13 @@ public class DefaultTypeCheckingRewriter implements ITypeCheckingRewriter {
 		this.typeRewriter = new TypeRewriter(ff);
 	}
 
+	// Version with a type rewriter provided by the caller and which therefore
+	// allows to also modify the types at the same time.
+	public DefaultTypeCheckingRewriter(TypeRewriter typeRewriter) {
+		this.ff = typeRewriter.getFactory();
+		this.typeRewriter = typeRewriter;
+	}
+
 	@Override
 	public boolean autoFlatteningMode() {
 		return false;
@@ -126,11 +141,13 @@ public class DefaultTypeCheckingRewriter implements ITypeCheckingRewriter {
 
 	@Override
 	public BoundIdentDecl rewrite(BoundIdentDecl src) {
-		if (ff == src.getFactory()) {
+		final Type srcType = src.getType();
+		final Type trgType = typeRewriter.rewrite(srcType);
+		if (trgType == srcType && ff == src.getFactory()) {
 			return src;
 		}
 		return ff.makeBoundIdentDecl(src.getName(), src.getSourceLocation(),
-				typeRewriter.rewrite(src.getType()));
+				trgType);
 	}
 
 	@Override
@@ -146,11 +163,13 @@ public class DefaultTypeCheckingRewriter implements ITypeCheckingRewriter {
 
 	@Override
 	public Expression rewrite(AtomicExpression src) {
-		if (ff == src.getFactory()) {
+		final Type srcType = src.getType();
+		final Type trgType = typeRewriter.rewrite(srcType);
+		if (trgType == srcType && ff == src.getFactory()) {
 			return src;
 		}
 		return ff.makeAtomicExpression(src.getTag(), src.getSourceLocation(),
-				typeRewriter.rewrite(src.getType()));
+				trgType);
 	}
 
 	@Override
@@ -170,22 +189,26 @@ public class DefaultTypeCheckingRewriter implements ITypeCheckingRewriter {
 
 	@Override
 	public Expression rewrite(BoundIdentifier src) {
-		if (ff == src.getFactory()) {
+		final Type srcType = src.getType();
+		final Type trgType = typeRewriter.rewrite(srcType);
+		if (trgType == srcType && ff == src.getFactory()) {
 			return src;
 		}
 		return ff.makeBoundIdentifier(src.getBoundIndex(),
-				src.getSourceLocation(), typeRewriter.rewrite(src.getType()));
+				src.getSourceLocation(), trgType);
 	}
 
 	@Override
 	public Expression rewrite(ExtendedExpression src, boolean changed,
 			Expression[] newChildExprs, Predicate[] newChildPreds) {
-		if (!changed && ff == src.getFactory()) {
+		final Type srcType = src.getType();
+		final Type trgType = typeRewriter.rewrite(srcType);
+		if (trgType == srcType && !changed && ff == src.getFactory()) {
 			return src;
 		}
 		return ff.makeExtendedExpression(src.getExtension(), newChildExprs,
 				newChildPreds, src.getSourceLocation(),
-				typeRewriter.rewrite(src.getType()));
+				trgType);
 	}
 
 	@Override
@@ -200,11 +223,13 @@ public class DefaultTypeCheckingRewriter implements ITypeCheckingRewriter {
 
 	@Override
 	public Expression rewrite(FreeIdentifier src) {
-		if (ff == src.getFactory()) {
+		final Type srcType = src.getType();
+		final Type trgType = typeRewriter.rewrite(srcType);
+		if (trgType == srcType && ff == src.getFactory()) {
 			return src;
 		}
 		return ff.makeFreeIdentifier(src.getName(), src.getSourceLocation(),
-				typeRewriter.rewrite(src.getType()));
+				trgType);
 	}
 
 	@Override
@@ -254,15 +279,15 @@ public class DefaultTypeCheckingRewriter implements ITypeCheckingRewriter {
 
 	@Override
 	public Expression rewrite(SetExtension src, SetExtension expr) {
-		if (ff == expr.getFactory()) {
+		final Type srcType = src.getType();
+		final Type trgType = typeRewriter.rewrite(srcType);
+		if (trgType == srcType && ff == expr.getFactory()) {
 			return expr;
 		}
 		if (expr.getMembers().length == 0) {
-			return ff.makeEmptySetExtension(
-					typeRewriter.rewrite(expr.getType()),
-					expr.getSourceLocation());
+			return ff.makeEmptySetExtension(trgType, src.getSourceLocation());
 		}
-		return ff.makeSetExtension(expr.getMembers(), expr.getSourceLocation());
+		return ff.makeSetExtension(expr.getMembers(), src.getSourceLocation());
 	}
 
 	@Override
@@ -279,7 +304,9 @@ public class DefaultTypeCheckingRewriter implements ITypeCheckingRewriter {
 	@Override
 	public Expression rewrite(UnaryExpression src, boolean changed,
 			Expression newChild) {
-		if (!changed) {
+		final Type srcType = src.getType();
+		final Type trgType = typeRewriter.rewrite(srcType);
+		if (trgType == srcType && !changed) {
 			assert ff == src.getFactory();
 			return src;
 		}

src/org/eventb/internal/core/ast/SimpleSubstitution.java

 /*******************************************************************************
- * Copyright (c) 2006, 2013 ETH Zurich and others.
+ * Copyright (c) 2006, 2016 ETH Zurich and others.
  * All rights reserved. This program and the accompanying materials
  * are made available under the terms of the Eclipse Public License v1.0
  * which accompanies this distribution, and is available at
@@ -26,7 +26,7 @@ import org.eventb.core.ast.FreeIdentifier;
  */
 public class SimpleSubstitution extends Substitution {
 	
-	protected Map<FreeIdentifier, Substitute> map;
+	protected Map<FreeIdentifier, Substitute<Expression>> map;
 
 	// Constructor for sub-classes that build directly the map.
 	protected SimpleSubstitution(FormulaFactory ff) {
@@ -43,7 +43,7 @@ public class SimpleSubstitution extends Substitution {
 	 */
 	public SimpleSubstitution(Map<FreeIdentifier, Expression> map, FormulaFactory ff) {
 		super(ff);
-		this.map = new HashMap<FreeIdentifier, Substitute>(map.size() * 4/3 + 1);
+		this.map = new HashMap<FreeIdentifier, Substitute<Expression>>(map.size() * 4/3 + 1);
 		for (Map.Entry<FreeIdentifier, Expression> entry : map.entrySet()) {
 			FreeIdentifier ident = entry.getKey();
 			Expression expr = entry.getValue();
@@ -59,7 +59,7 @@ public class SimpleSubstitution extends Substitution {
 
 	@Override
 	public Expression rewrite(FreeIdentifier ident) {
-		Substitute repl = map.get(ident);
+		Substitute<Expression> repl = map.get(ident);
 		if (repl == null) {
 			return super.rewrite(ident);
 		}

src/org/eventb/internal/core/ast/Substitute.java

 /*******************************************************************************
- * Copyright (c) 2006, 2014 ETH Zurich and others.
+ * Copyright (c) 2006, 2016 ETH Zurich and others.
  * All rights reserved. This program and the accompanying materials
  * are made available under the terms of the Eclipse Public License v1.0
  * which accompanies this distribution, and is available at
@@ -7,41 +7,44 @@
  *
  * Contributors:
  *     ETH Zurich - initial API and implementation
+ *     Systerel - Make this class generic
  *******************************************************************************/
 package org.eventb.internal.core.ast;
 
 import org.eventb.core.ast.Expression;
+import org.eventb.core.ast.Formula;
 
 /**
- * Common abstraction for a substitute expression used in a substitution.
+ * Common abstraction for a substitute formula used in a substitution.
  * <p>
  * This class is not public API. Don't use it.
  * </p>
  * 
  * @author Laurent Voisin
  */
-public abstract class Substitute {
+public abstract class Substitute<T extends Formula<T>> {
 
 	/**
-	 * Simple substitute where the expression doesn't contain any externally
+	 * Simple substitute where the formula doesn't contain any externally
 	 * bound identifier.
 	 */
-	private static class SimpleSubstitute extends Substitute {
+	private static class SimpleSubstitute<T extends Formula<T>>
+			extends Substitute<T> {
 
-		Expression expr;
+		T formula;
 
-		public SimpleSubstitute(Expression expr) {
-			this.expr = expr;
+		public SimpleSubstitute(T formula) {
+			this.formula = formula;
 		}
 
 		@Override
-		public Expression getSubstitute(Expression original, int nbOfInternallyBound) {
-			return expr;
+		public T getSubstitute(T original, int nbOfInternallyBound) {
+			return formula;
 		}
 
 		@Override
 		public int hashCode() {
-			return expr.hashCode();
+			return formula.hashCode();
 		}
 
 		@Override
@@ -52,27 +55,29 @@ public abstract class Substitute {
 			if (obj == null || this.getClass() != obj.getClass()) {
 				return false;
 			}
-			final SimpleSubstitute other = (SimpleSubstitute) obj;
-			return expr.equals(other.expr);
+			@SuppressWarnings("unchecked")
+			final SimpleSubstitute<T> other = (SimpleSubstitute<T>) obj;
+			return formula.equals(other.formula);
 		}
 
 		@Override
 		public String toString() {
-			return expr.toString();
+			return formula.toString();
 		}
 
 	}
 
 	/**
-	 * Susbtitute where the expression consists of a bound identifier.
+	 * Susbtitute where the formula consists of a bound identifier.
 	 * <p>
 	 * This means that we must renumber the index of this identifier, taking
 	 * into account the offset.
 	 * </p>
 	 * This class corresponds to an optimized simple version of
-	 * {@link ComplexSubstitute}.
+	 * {@link org.eventb.internal.core.ast.Substitute.ComplexSubstitute
+	 * ComplexSubstitute}.
 	 */
-	private static class BoundIdentSubstitute extends Substitute {
+	private static class BoundIdentSubstitute extends Substitute<Expression> {
 
 		/**
 		 * Index of the bound variable, before correction.
@@ -115,7 +120,7 @@ public abstract class Substitute {
 	}
 
 	/**
-	 * Complex substitute where the expression does contain some externally
+	 * Complex substitute where the formula does contain some externally
 	 * bound identifiers.
 	 * <p>
 	 * This means that we must renumber the index of these identifiers, taking
@@ -123,26 +128,27 @@ public abstract class Substitute {
 	 * small cache.
 	 * </p>
 	 */
-	private static class ComplexSubstitute extends Substitute {
+	private static class ComplexSubstitute<T extends Formula<T>>
+			extends Substitute<T> {
 
 		/**
-		 * Cache of substitute expressions, indexed by the offset applied to
+		 * Cache of substitute formulas, indexed by the offset applied to
 		 * them. For instance, the first element of the list contains the
-		 * original expression untouched.
+		 * original formula untouched.
 		 */
-		private Cache<Expression> cache;
+		private Cache<T> cache;
 
-		public ComplexSubstitute(Expression expr) {
-			this.cache = new Cache<Expression>();
-			this.cache.set(0, expr);
+		public ComplexSubstitute(T formula) {
+			this.cache = new Cache<T>();
+			this.cache.set(0, formula);
 		}
 
 		@Override
-		public Expression getSubstitute(Expression original, int nbOfInternallyBound) {
-			Expression result = cache.get(nbOfInternallyBound);
+		public T getSubstitute(T original, int nbOfInternallyBound) {
+			T result = cache.get(nbOfInternallyBound);
 			if (result == null) {
-				Expression expr = cache.get(0);
-				result = expr.shiftBoundIdentifiers(nbOfInternallyBound);
+				T formula = cache.get(0);
+				result = formula.shiftBoundIdentifiers(nbOfInternallyBound);
 				cache.set(nbOfInternallyBound, result);
 			}
 			return result;
@@ -161,11 +167,13 @@ public abstract class Substitute {
 			if (obj == null || this.getClass() != obj.getClass()) {
 				return false;
 			}
-			return equalExpressions((ComplexSubstitute) obj);
+			@SuppressWarnings("unchecked")
+			final ComplexSubstitute<T> other = (ComplexSubstitute<T>) obj;
+			return equalFormulas(other);
 		}
 
 		// Test extracted to a method for subclass comparison
-		protected boolean equalExpressions(ComplexSubstitute other) {
+		protected boolean equalFormulas(ComplexSubstitute<T> other) {
 			return cache.get(0).equals(other.cache.get(0));
 		}
 
@@ -177,20 +185,21 @@ public abstract class Substitute {
 	}
 
 	/**
-	 * Complex substitute where the expression does contain some externally
+	 * Complex substitute where the formula does contain some externally
 	 * bound identifiers, and where an additional offset needs to be applied.
 	 */
-	private static class ComplexSubstituteWithOffset extends ComplexSubstitute {
+	private static class ComplexSubstituteWithOffset<T extends Formula<T>>
+			extends ComplexSubstitute<T> {
 
 		private final int offset;
 
-		public ComplexSubstituteWithOffset(Expression expr, int offset) {
-			super(expr);
+		public ComplexSubstituteWithOffset(T formula, int offset) {
+			super(formula);
 			this.offset = offset;
 		}
 
 		@Override
-		public Expression getSubstitute(Expression original, int nbOfInternallyBound) {
+		public T getSubstitute(T original, int nbOfInternallyBound) {
 			return super.getSubstitute(original, nbOfInternallyBound + offset);
 		}
 
@@ -207,8 +216,9 @@ public abstract class Substitute {
 			if (obj == null || this.getClass() != obj.getClass()) {
 				return false;
 			}
-			final ComplexSubstituteWithOffset other = (ComplexSubstituteWithOffset) obj;
-			return equalExpressions(other) && offset == other.offset;
+			@SuppressWarnings("unchecked")
+			final ComplexSubstituteWithOffset<T> other = (ComplexSubstituteWithOffset<T>) obj;
+			return equalFormulas(other) && offset == other.offset;
 		}
 
 		@Override
@@ -219,31 +229,32 @@ public abstract class Substitute {
 	}
 
 	/**
-	 * Factory method to create a substitute with an arbitrary expression.
+	 * Factory method to create a substitute with an arbitrary formula.
 	 * 
-	 * @param expr
-	 *            initial substitute expression
-	 * @return the substitute object for that expression
+	 * @param formula
+	 *            initial substitute formula
+	 * @return the substitute object for that formula
 	 */
-	public static Substitute makeSubstitute(Expression expr) {
-		if (expr.isWellFormed()) {
-			return new SimpleSubstitute(expr);
+	public static <T extends Formula<T>> Substitute<T> makeSubstitute(T formula) {
+		if (formula.isWellFormed()) {
+			return new SimpleSubstitute<T>(formula);
 		}
-		return new ComplexSubstitute(expr);
+		return new ComplexSubstitute<T>(formula);
 	}
 
 	/**
-	 * Factory method to create a substitute with an arbitrary expression and
+	 * Factory method to create a substitute with an arbitrary formula and
 	 * applying a constant offset to its bound identifiers.
 	 * 
-	 * @param expr
-	 *            initial substitute expression
+	 * @param formula
+	 *            initial substitute formula
 	 * @param offset
 	 *            offset to systematically apply
-	 * @return the substitute object for that expression
+	 * @return the substitute object for that formula
 	 */
-	public static Substitute makeSubstitute(Expression expr, int offset) {
-		return new ComplexSubstituteWithOffset(expr, offset);
+	public static <T extends Formula<T>> Substitute<T> makeSubstitute(T formula,
+			int offset) {
+		return new ComplexSubstituteWithOffset<T>(formula, offset);
 	}
 
 	/**
@@ -253,23 +264,23 @@ public abstract class Substitute {
 	 *            initial index of the bound identifier
 	 * @return the substitute object for that identifier
 	 */
-	public static Substitute makeSubstitute(int index) {
+	public static Substitute<Expression> makeSubstitute(int index) {
 		return new BoundIdentSubstitute(index);
 	}
 
 	/**
-	 * Returns the substitute expression where bound identifier occurrences have
+	 * Returns the substitute formula where bound identifier occurrences have
 	 * been renumbered using the given offset.
 	 * 
 	 * @param original
-	 *            original expression that gets substituted
+	 *            original formula that gets substituted
 	 * @param nbOfInternallyBound
 	 *            offset to use, that is the number of identifiers bound between
-	 *            the point where the substitute expression was given and the
+	 *            the point where the substitute formula was given and the
 	 *            place where it is used
 	 * 
-	 * @return the actual substitute expression to use
+	 * @return the actual substitute formula to use
 	 */
-	public abstract Expression getSubstitute(Expression original, int nbOfInternallyBound);
+	public abstract T getSubstitute(T original, int nbOfInternallyBound);
 
 }

src/org/eventb/internal/core/ast/Substitution.java

 /*******************************************************************************
- * Copyright (c) 2006, 2012 ETH Zurich and others.
+ * Copyright (c) 2006, 2016 ETH Zurich and others.
  * All rights reserved. This program and the accompanying materials
  * are made available under the terms of the Eclipse Public License v1.0
  * which accompanies this distribution, and is available at
@@ -23,4 +23,8 @@ public abstract class Substitution extends DefaultTypeCheckingRewriter {
 		super(ff);
 	}
 
+	public Substitution(TypeRewriter typeRewriter) {
+		super(typeRewriter);
+	}
+
 }

src/org/eventb/internal/core/ast/TypeRewriter.java

 /*******************************************************************************
- * Copyright (c) 2012, 2013 Systerel and others.
+ * Copyright (c) 2012, 2016 Systerel and others.
  * All rights reserved. This program and the accompanying materials
  * are made available under the terms of the Eclipse Public License v1.0
  * which accompanies this distribution, and is available at
@@ -38,7 +38,7 @@ import org.eventb.core.ast.extension.IExpressionExtension;
 public class TypeRewriter implements ITypeVisitor {
 
 	// Formula factory to use for building the rewritten types
-	private final FormulaFactory ff;
+	protected final FormulaFactory ff;
 
 	// Result of the last call to visit()
 	protected Type result;
@@ -47,6 +47,10 @@ public class TypeRewriter implements ITypeVisitor {
 		this.ff = ff;
 	}
 
+	public FormulaFactory getFactory() {
+		return ff;
+	}
+
 	public Type rewrite(Type type) {
 		if (type == null) {
 			return null;

src/org/eventb/internal/core/ast/datatype/Datatype.java

@@ -161,17 +161,24 @@ public class Datatype implements IDatatype {
 		return unmodifiableSet(extensions);
 	}
 
+	/**
+	 * The hash code is computed from the datatype's type constructors,
+	 * constructor extensions, and the origin.
+	 */
 	@Override
 	public int hashCode() {
 		final int prime = 31;
 		int result = 1;
 		result = prime * result + typeCons.hashCode();
 		result = prime * result + constructors.hashCode();
-		result = prime * result + ((origin == null) ? 0 : origin.hashCode());
+		result = prime * result + (origin == null ? 0 : origin.hashCode());
 		return result;
 	}
 
-
+	/**
+	 * The datatypes are the same if they have the same name and "similar" type
+	 * constructors, constructor extensions, and origins.
+	 */
 	@Override
 	public boolean equals(Object obj) {
 		if (this == obj) {
@@ -183,15 +190,23 @@ public class Datatype implements IDatatype {
 		final Datatype other = (Datatype) obj;
 		return this.typeCons.isSimilarTo(other.typeCons)
 				&& areSimilarConstructors(this.constructors.values(),
-						other.constructors.values())
-				&& areEqualOrigins(this.origin, other.origin);
+						other.constructors.values()) &&
+						areSimilarOrigins(this.getOrigin(), other.getOrigin());
 	}
 
-	private static boolean areEqualOrigins(Object origin1, Object origin2) {
-		if (origin1 == null) {
-			return origin2 == null;
-		}
-		return origin1.equals(origin2);
+	/**
+	 * Utility method to compare the datatype origin.
+	 * 
+	 * @param mine
+	 *            mine origin
+	 * @param other
+	 *            the other's origin
+	 * @return <code>true</code> if the two origin are equal.
+	 */
+	private boolean areSimilarOrigins(Object mine, Object other) {
+		if (mine == null)
+			return (other == null);
+		return mine.equals(other);
 	}
 
 	private static boolean areSimilarConstructors(

src/org/eventb/internal/core/ast/datatype/DatatypeRewriter.java

 /*******************************************************************************
- * Copyright (c) 2013 Systerel and others.
+ * Copyright (c) 2013, 2016 Systerel and others.
  * All rights reserved. This program and the accompanying materials
  * are made available under the terms of the Eclipse Public License v1.0
  * which accompanies this distribution, and is available at
@@ -10,16 +10,9 @@
  *******************************************************************************/
 package org.eventb.internal.core.ast.datatype;
 
-import org.eventb.core.ast.AtomicExpression;
-import org.eventb.core.ast.BoundIdentDecl;
-import org.eventb.core.ast.BoundIdentifier;
 import org.eventb.core.ast.Expression;
 import org.eventb.core.ast.ExtendedExpression;
-import org.eventb.core.ast.FreeIdentifier;
 import org.eventb.core.ast.Predicate;
-import org.eventb.core.ast.SetExtension;
-import org.eventb.core.ast.SourceLocation;
-import org.eventb.core.ast.Type;
 import org.eventb.core.ast.datatype.IDatatype;
 import org.eventb.core.ast.extension.IExpressionExtension;
 import org.eventb.internal.core.ast.DefaultTypeCheckingRewriter;
@@ -40,71 +33,10 @@ public class DatatypeRewriter extends DefaultTypeCheckingRewriter {
 	private final DatatypeTranslation translation;
 
 	public DatatypeRewriter(DatatypeTranslation translation) {
-		super(translation.getTargetFormulaFactory());
+		super(translation.getTypeRewriter());
 		this.translation = translation;
 	}
 
-	@Override
-	public BoundIdentDecl rewrite(BoundIdentDecl decl) {
-		final Type type = decl.getType();
-		final Type newType = translation.translate(type);
-		if (newType == type) {
-			return super.rewrite(decl);
-		}
-		final String name = decl.getName();
-		final SourceLocation sLoc = decl.getSourceLocation();
-		return ff.makeBoundIdentDecl(name, sLoc, newType);
-	}
-
-	@Override
-	public Expression rewrite(AtomicExpression expression) {
-		final Type type = expression.getType();
-		final Type newType = translation.translate(type);
-		if (newType == type) {
-			return super.rewrite(expression);
-		}
-		final SourceLocation sLoc = expression.getSourceLocation();
-		return ff.makeAtomicExpression(expression.getTag(), sLoc, newType);
-	}
-
-	@Override
-	public Expression rewrite(BoundIdentifier identifier) {
-		final Type type = identifier.getType();
-		final Type newType = translation.translate(type);
-		if (newType == type) {
-			return super.rewrite(identifier);
-		}
-		final SourceLocation sLoc = identifier.getSourceLocation();
-		final int index = identifier.getBoundIndex();
-		return ff.makeBoundIdentifier(index, sLoc, newType);
-	}
-
-	@Override
-	public Expression rewrite(FreeIdentifier ident) {
-		final Type type = ident.getType();
-		final Type newType = translation.translate(type);
-		if (newType == type) {
-			return super.rewrite(ident);
-		}
-		final SourceLocation sLoc = ident.getSourceLocation();
-		final String name = ident.getName();
-		return ff.makeFreeIdentifier(name, sLoc, newType);
-	}
-
-	@Override
-	public Expression rewrite(SetExtension src, SetExtension expr) {
-		if (expr.getChildCount() != 0) {
-			return expr;
-		}
-		final Type type = expr.getType();
-		final Type newType = translation.translate(type);
-		if (newType == type) {
-			return expr;
-		}
-		final SourceLocation sLoc = expr.getSourceLocation();
-		return ff.makeEmptySetExtension(newType, sLoc);
-	}
-
 	@Override
 	public Expression rewrite(ExtendedExpression src, boolean changed,
 			Expression[] newChildExprs, Predicate[] newChildPreds) {
@@ -116,10 +48,7 @@ public class DatatypeRewriter extends DefaultTypeCheckingRewriter {
 			return translation.translate(src, newChildExprs);
 		} else {
 			// Not a datatype operator, just translate the type
-			final SourceLocation sLoc = src.getSourceLocation();
-			final Type type = translation.translate(src.getType());
-			return ff.makeExtendedExpression(extension, newChildExprs,
-					newChildPreds, sLoc, type);
+			return super.rewrite(src, changed, newChildExprs, newChildPreds);
 		}
 	}