Update to Rodin 3.6 sources

This officially requires Java 11, but I'm leaving the Gradle setting at
Java 8 for now, because it still seems to build fine...

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.4.0.qualifier
+Bundle-Version: 3.5.0.qualifier
 Bundle-Vendor: %providerName
 Bundle-Localization: plugin
 Export-Package: org.eventb.core.ast,
@@ -18,7 +18,7 @@ Export-Package: org.eventb.core.ast,
  org.eventb.internal.core.parser.operators;x-friends:="org.eventb.core.ast.tests",
  org.eventb.internal.core.typecheck;x-friends:="org.eventb.core.ast.tests"
 Bundle-ActivationPolicy: lazy
-Bundle-RequiredExecutionEnvironment: JavaSE-1.8
+Bundle-RequiredExecutionEnvironment: JavaSE-11
 Bundle-Activator: org.eventb.internal.core.ast.ASTPlugin
 Require-Bundle: org.eclipse.core.runtime
 Eclipse-ExtensibleAPI: true

build.gradle

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

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

 /*******************************************************************************
- * Copyright (c) 2012, 2017 Systerel and others.
+ * Copyright (c) 2012, 2021 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
@@ -8,6 +8,7 @@
  * Contributors:
  *     Systerel - initial API and implementation
  *     University of Southampton - added support for predicate variables
+ *     CentraleSupélec - substitution of type with expression
  *******************************************************************************/
 package org.eventb.core.ast;
 
@@ -138,6 +139,34 @@ public interface ISpecialization extends Cloneable {
 	 */
 	void put(GivenType type, Type value);
 
+	/**
+	 * Adds a new type substitution to this specialization. All substitutions will
+	 * be applied in parallel when specializing a formula. The value must be a
+	 * type-checked type expression. The added 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
+	 * @param value typed type expression replacement for the given type
+	 * @throws IllegalArgumentException
+	 *             if the value is not typed or is not a type expression, or if
+	 *             this substitution is not compatible with already registered
+	 *             substitutions or the value has been created by another formula
+	 *             factory
+	 * @see Type#getFactory()
+	 * @see Formula#isTypeChecked()
+	 * @see Expression#isATypeExpression()
+	 * @see #canPut(GivenType, Expression)
+	 * @since 3.5
+	 */
+	void put(GivenType type, Expression value);
+
 	/**
 	 * Returns the type to be substituted for the given given type.
 	 * 
@@ -214,6 +243,29 @@ public interface ISpecialization extends Cloneable {
 	 */
 	boolean canPut(GivenType type, Type value);
 
+	/**
+	 * 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, Expression)} is satisfied. The value must by a typed
+	 * type expression and 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
+	 *            typed type expression 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 is not typed, is not a type expression or has
+	 *             been created by another formula factory
+	 * @since 3.5
+	 */
+	boolean canPut(GivenType type, Expression value);
+	
 	/**
 	 * Checks whether the proposed free-identifier substitution is compatible
 	 * with already registered substitutions (for given types, free identifiers,

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

 /*******************************************************************************
- * Copyright (c) 2010, 2017 Systerel and others.
+ * Copyright (c) 2010, 2021 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
@@ -8,6 +8,7 @@
  * Contributors:
  *     Systerel - initial API and implementation
  *     University of Southamtpon - added support for predicate varialbes.
+ *     CentraleSupélec - substitution of type with expression
  *******************************************************************************/
 package org.eventb.internal.core.ast;
 
@@ -317,11 +318,36 @@ public class Specialization implements ISpecialization {
 
 	@Override
 	public boolean canPut(GivenType type, Type value) {
-		return canPutInternal(type, value) == null;
+		return canPutInternal(type, value.toExpression()) == null;
 	}
 
 	@Override
 	public void put(GivenType type, Type value) {
+		final String errorMessage = canPutInternal(type, value.toExpression());
+		if (errorMessage != null) {
+			throw new IllegalArgumentException(errorMessage);
+		}
+		addTypeSubstitution(type, value.toExpression());
+	}
+
+	private void maybeAddTypeIdentitySubstitution(GivenType type) {
+		if (!srcTypenv.contains(type.getName())) {
+			addTypeSubstitution(type, type.translate(ff).toExpression());
+		}
+	}
+	
+	@Override
+	public Type get(GivenType key) {
+		return speTypeRewriter.get(key);
+	}
+
+	@Override
+	public boolean canPut(GivenType type, Expression value) {
+		return canPutInternal(type, value) == null;
+	}
+
+	@Override
+	public void put(GivenType type, Expression value) {
 		final String errorMessage = canPutInternal(type, value);
 		if (errorMessage != null) {
 			throw new IllegalArgumentException(errorMessage);
@@ -329,52 +355,50 @@ public class Specialization implements ISpecialization {
 		addTypeSubstitution(type, value);
 	}
 
-	private String canPutInternal(GivenType type, Type value) {
+	private String canPutInternal(GivenType type, Expression value) {
 		if (type == null)
 			throw new NullPointerException("Null given type");
 		if (value == null)
-			throw new NullPointerException("Null type");
+			throw new NullPointerException("Null type expression");
 		if (ff != value.getFactory()) {
 			throw new IllegalArgumentException("Wrong factory for value: "
 					+ value.getFactory() + ", should be " + ff);
 		}
+		if (!value.isTypeChecked())
+			throw new IllegalArgumentException("Untyped value");
+		if (!value.isATypeExpression())
+			throw new IllegalArgumentException("Value is not a type expression");
 		if (!verifySrcTypenv(type.toExpression())) {
 			return "Identifier " + type
 					+ " already entered with a different type";
 		}
-		final String error = isCompatibleFormula(dstTypenv,
-				value.toExpression());
+		final String error = isCompatibleFormula(dstTypenv, value);
 		if (error != null) {
 			return error;
 		}
+		final Type newValue = value.toType();
 		final Type oldValue = speTypeRewriter.get(type);
-		if (oldValue != null && !oldValue.equals(value)) {
+		if (oldValue != null && !oldValue.equals(newValue)) {
 			return "Type substitution for " + type + " already registered";
 		}
+		final Expression oldValueExpr = formRewriter.get(type.toExpression());
+		if (oldValueExpr != null && !oldValueExpr.equals(value)) {
+			return "Identifier substitution for " + type
+					+ " already registered";
+		}
 		return null;
 	}
 
-	private void addTypeSubstitution(GivenType type, Type value) {
+	private void addTypeSubstitution(GivenType type, Expression value) {
 		final FreeIdentifier ident = type.toExpression();
 		srcTypenv.add(ident);
-		speTypeRewriter.put(type, value);
-		formRewriter.put(ident, value.toExpression());
+		speTypeRewriter.put(type, value.toType());
+		formRewriter.put(ident, value);
 		for (final GivenType given : value.getGivenTypes()) {
 			dstTypenv.addGivenSet(given.getName());
 		}
 	}
 
-	private void maybeAddTypeIdentitySubstitution(GivenType type) {
-		if (!srcTypenv.contains(type.getName())) {
-			addTypeSubstitution(type, type.translate(ff));
-		}
-	}
-	
-	@Override
-	public Type get(GivenType key) {
-		return speTypeRewriter.get(key);
-	}
-
 	@Override
 	public boolean canPut(FreeIdentifier ident, Expression value) {
 		return canPutInternal(ident, value) == null;

src/org/eventb/internal/core/ast/wd/WDComputer.java

 /*******************************************************************************
- * Copyright (c) 2010, 2013 Systerel and others.
+ * Copyright (c) 2010, 2020 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,9 +15,14 @@ import static org.eventb.core.ast.Formula.DIV;
 import static org.eventb.core.ast.Formula.EXPN;
 import static org.eventb.core.ast.Formula.FUNIMAGE;
 import static org.eventb.core.ast.Formula.KCARD;
+import static org.eventb.core.ast.Formula.KID_GEN;
 import static org.eventb.core.ast.Formula.KINTER;
 import static org.eventb.core.ast.Formula.KMAX;
 import static org.eventb.core.ast.Formula.KMIN;
+import static org.eventb.core.ast.Formula.KPRED;
+import static org.eventb.core.ast.Formula.KPRJ1_GEN;
+import static org.eventb.core.ast.Formula.KPRJ2_GEN;
+import static org.eventb.core.ast.Formula.KSUCC;
 import static org.eventb.core.ast.Formula.LAND;
 import static org.eventb.core.ast.Formula.LEQV;
 import static org.eventb.core.ast.Formula.LIMP;
@@ -181,12 +186,21 @@ public class WDComputer implements ISimpleVisitor2 {
 		case EXPN:
 			return fb.land(fb.nonNegative(left), fb.nonNegative(right));
 		case FUNIMAGE:
+			if (isBuiltinTotalFunction(left)) {
+				return fb.btrue;
+			}
 			return fb.land(fb.inDomain(left, right), fb.partial(left));
 		default:
 			return fb.btrue;
 		}
 	}
 
+	private boolean isBuiltinTotalFunction(Expression expr) {
+		final int tag = expr.getTag();
+		return tag == KPRED || tag == KSUCC //
+				|| tag == KPRJ1_GEN || tag == KPRJ2_GEN || tag == KID_GEN;
+	}
+
 	@Override
 	public void visitBinaryPredicate(BinaryPredicate predicate) {
 		final Predicate left = predicate.getLeft();