Update to Rodin 3.7 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.5.0.qualifier
+Bundle-Version: 3.6.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.6.0"
+project.version = "3.7.0-SNAPSHOT"
 final isSnapshot = project.version.endsWith("-SNAPSHOT")
 
 sourceSets {

plugin.properties

 ###############################################################################
-# Copyright (c) 2005, 2011 ETH Zurich and others.
+# Copyright (c) 2005, 2022 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

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

 /*******************************************************************************
- * Copyright (c) 2010, 2016 Systerel and others.
+ * Copyright (c) 2010, 2022 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
@@ -30,6 +30,7 @@ import org.eventb.core.ast.extension.IExtensionKind;
 import org.eventb.core.ast.extension.IOperatorProperties.FormulaType;
 import org.eventb.core.ast.extension.IOperatorProperties.Notation;
 import org.eventb.core.ast.extension.IPredicateExtension;
+import org.eventb.core.ast.extension.IPredicateExtension2;
 import org.eventb.internal.core.ast.FindingAccumulator;
 import org.eventb.internal.core.ast.ITypeCheckingRewriter;
 import org.eventb.internal.core.ast.IdentListMerger;
@@ -154,9 +155,9 @@ public class ExtendedPredicate extends Predicate implements IExtendedFormula {
 	/**
 	 * Must never be called directly: use the factory method instead.
 	 * 
-	 * @see FormulaFactory#makeExtendedPredicate(IPredicateExtension,
+	 * @see FormulaFactory#makeExtendedPredicate(IPredicateExtension2,
 	 *      Expression[], Predicate[], SourceLocation)
-	 * @see FormulaFactory#makeExtendedPredicate(IPredicateExtension,
+	 * @see FormulaFactory#makeExtendedPredicate(IPredicateExtension2,
 	 *      java.util.Collection, java.util.Collection, SourceLocation)
 	 */
 	protected ExtendedPredicate(int tag, Expression[] expressions,
@@ -200,7 +201,25 @@ public class ExtendedPredicate extends Predicate implements IExtendedFormula {
 				return;
 			}
 		}
-		typeChecked = true;
+
+		final FormulaFactory ff = getFactory();
+		BoundIdentDecl[] boundDecls;
+		if (boundIdents.length > 0) {
+			boundDecls = new BoundIdentDecl[boundIdents.length];
+			for (int i = 0; i < boundIdents.length; i++) {
+				boundDecls[i] = new BoundIdentDecl("b" + i, null, boundIdents[i].getType(), ff);
+			}
+		} else {
+			boundDecls = NO_BOUND_IDENT_DECL;
+		}
+
+		if (extension instanceof IPredicateExtension2) {
+			typeChecked = ((IPredicateExtension2) extension).verifyType(childExpressions, childPredicates);
+		} else {
+			TypeCheckResult tcRes = new TypeCheckResult(ff.makeTypeEnvironment().makeSnapshot());
+			typeCheck(tcRes, boundDecls);
+			typeChecked = !tcRes.hasProblem();
+		}
 	}
 
 	@Override

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

 /*******************************************************************************
- * Copyright (c) 2005, 2018 ETH Zurich and others.
+ * Copyright (c) 2005, 2022 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
@@ -50,6 +50,7 @@ import org.eventb.core.ast.extension.IGrammar;
 import org.eventb.core.ast.extension.IOperatorGroup;
 import org.eventb.core.ast.extension.IOperatorProperties;
 import org.eventb.core.ast.extension.IPredicateExtension;
+import org.eventb.core.ast.extension.IPredicateExtension2;
 import org.eventb.internal.core.ast.Position;
 import org.eventb.internal.core.ast.Specialization;
 import org.eventb.internal.core.ast.datatype.DatatypeBuilder;
@@ -603,6 +604,36 @@ public class FormulaFactory {
 				predicates.clone(), location, this, extension);
 	}
 
+	/**
+	 * Returns a new extended predicate.
+	 * 
+	 * @param extension
+	 *            the predicate extension
+	 * @param expressions
+	 *            the children expressions
+	 * @param predicates
+	 *            the children predicates
+	 * @param location
+	 *            the source location or <code>null</code>
+	 * @return a new extended expression
+	 * @throws IllegalArgumentException
+	 *             if the extension is not supported by this factory
+	 * @throws IllegalArgumentException
+	 *             if the preconditions of the extension on children are not
+	 *             verified
+	 * @throws IllegalArgumentException
+	 *             if some given child has been built with a different factory
+	 * @since 3.6
+	 * @see IExtensionKind#checkPreconditions(Expression[], Predicate[])
+	 */
+	public ExtendedPredicate makeExtendedPredicate(
+			IPredicateExtension2 extension, Expression[] expressions,
+			Predicate[] predicates, SourceLocation location) {
+		final int tag = getCheckedExtensionTag(extension);
+		return new ExtendedPredicate(tag, expressions.clone(),
+				predicates.clone(), location, this, extension);
+	}
+
 	/**
 	 * Returns a new extended predicate.
 	 * 
@@ -633,6 +664,36 @@ public class FormulaFactory {
 				toPredArray(predicates), location, this, extension);
 	}
 
+	/**
+	 * Returns a new extended predicate.
+	 * 
+	 * @param extension
+	 *            the predicate extension
+	 * @param expressions
+	 *            the children expressions
+	 * @param predicates
+	 *            the children predicates
+	 * @param location
+	 *            the source location or <code>null</code>
+	 * @return a new extended expression
+	 * @throws IllegalArgumentException
+	 *             if the extension is not supported by this factory
+	 * @throws IllegalArgumentException
+	 *             if the preconditions of the extension on children are not
+	 *             verified
+	 * @throws IllegalArgumentException
+	 *             if some given child has been built with a different factory
+	 * @since 3.6
+	 * @see IExtensionKind#checkPreconditions(Expression[], Predicate[])
+	 */
+	public ExtendedPredicate makeExtendedPredicate(
+			IPredicateExtension2 extension, Collection<Expression> expressions,
+			Collection<Predicate> predicates, SourceLocation location) {
+		final int tag = getCheckedExtensionTag(extension);
+		return new ExtendedPredicate(tag, toExprArray(expressions),
+				toPredArray(predicates), location, this, extension);
+	}
+
 	/**
 	 * Returns the conditional expression extension. This extension takes one
 	 * predicate and two expression children. Its value is the first expression

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

 /*******************************************************************************
- * Copyright (c) 2010, 2012 Systerel and others.
+ * Copyright (c) 2010, 2022 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,12 +13,23 @@ package org.eventb.core.ast.extension;
 import org.eventb.core.ast.ExtendedPredicate;
 
 /**
+ * Common protocol for predicate extensions.
+ * 
+ * Please use {@link IPredicateExtension2} instead which is more efficient.
+ *
  * @author "Nicolas Beauger"
  * @since 2.0
- *
  */
 public interface IPredicateExtension extends IFormulaExtension {
 
+	/**
+	 * Define type check constraints for the given extended predicate. The given
+	 * type check mediator is intended to be used for creating type variables when
+	 * needed, and for adding type constraints.
+	 * 
+	 * @param predicate  the extended predicate to type check
+	 * @param tcMediator a type check mediator
+	 */
 	void typeCheck(ExtendedPredicate predicate, ITypeCheckMediator tcMediator);
 
 }

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

+/*******************************************************************************
+ * Copyright (c) 2010, 2022 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
+ * http://www.eclipse.org/legal/epl-v10.html
+ *
+ * Contributors:
+ *     Systerel - initial API and implementation
+ *******************************************************************************/
+package org.eventb.core.ast.extension;
+
+import org.eventb.core.ast.Expression;
+import org.eventb.core.ast.Predicate;
+
+/**
+ * Common protocol for predicate extensions.
+ * 
+ * This interface adds the <code>verifyType</code> method for better
+ * performance. It should be used instead of <code>IPredicateExtension</code>
+ * whenever possible.
+ *
+ * @author Laurent Voisin
+ * @since 3.6
+ */
+public interface IPredicateExtension2 extends IPredicateExtension {
+
+	/**
+	 * Verifies that the type of the given children is coherent with the semantics
+	 * of this predicate extension. It is guaranteed that all children are
+	 * well-typed and that their types are compatible with each other.
+	 * 
+	 * @param childExprs the child expressions
+	 * @param childPreds the child predicates
+	 * @return <code>true</code> iff the children types are coherent,
+	 *         <code>false</code> otherwise
+	 */
+	boolean verifyType(Expression[] childExprs, Predicate[] childPreds);
+
+}