diff --git a/META-INF/MANIFEST.MF b/META-INF/MANIFEST.MF
index 0564041182ba610b0c2a9037d3474fe86ffadb17..0d8ce7eb0657decb527a0c5288ee9a6b2cde1d34 100644
--- a/META-INF/MANIFEST.MF
+++ b/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,
diff --git a/build.gradle b/build.gradle
index 24674629dddd1f71ad6352ff7e9e6e30fd73bc54..2077b9ed8a5a2bf51d2b57cb7538ff26ee986f75 100644
--- a/build.gradle
+++ b/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 {
diff --git a/plugin.properties b/plugin.properties
index 4649e8486ddafd5d257b5712a08b166b2f330442..56482903a1b9ad719c5c5d11f001150008287e0a 100644
--- a/plugin.properties
+++ b/plugin.properties
@@ -1,5 +1,5 @@
###############################################################################
-# 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
diff --git a/src/org/eventb/core/ast/ExtendedPredicate.java b/src/org/eventb/core/ast/ExtendedPredicate.java
index 32c5d9ca2b26e3c749148cf54bf03520d9e70259..24a4bc3d598de0f641ae06869d3c48d54a92ab6c 100644
--- a/src/org/eventb/core/ast/ExtendedPredicate.java
+++ b/src/org/eventb/core/ast/ExtendedPredicate.java
@@ -1,5 +1,5 @@
/*******************************************************************************
- * 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
diff --git a/src/org/eventb/core/ast/FormulaFactory.java b/src/org/eventb/core/ast/FormulaFactory.java
index 6a4488a1061073fbcd6e1bde34b24e687cd33bda..576de160bd46ff2cf66a244670d352cd8507e16b 100644
--- a/src/org/eventb/core/ast/FormulaFactory.java
+++ b/src/org/eventb/core/ast/FormulaFactory.java
@@ -1,5 +1,5 @@
/*******************************************************************************
- * 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
diff --git a/src/org/eventb/core/ast/extension/IPredicateExtension.java b/src/org/eventb/core/ast/extension/IPredicateExtension.java
index 9234c77b930f007791d2728d0adc6a31d1488f54..b3033e5769dcac4603e07578098cfd66acce5d77 100644
--- a/src/org/eventb/core/ast/extension/IPredicateExtension.java
+++ b/src/org/eventb/core/ast/extension/IPredicateExtension.java
@@ -1,5 +1,5 @@
/*******************************************************************************
- * 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);
}
diff --git a/src/org/eventb/core/ast/extension/IPredicateExtension2.java b/src/org/eventb/core/ast/extension/IPredicateExtension2.java
new file mode 100644
index 0000000000000000000000000000000000000000..1568fa51a32551443ad9c6e4b5b4958fdb4c80de
--- /dev/null
+++ b/src/org/eventb/core/ast/extension/IPredicateExtension2.java
@@ -0,0 +1,40 @@
+/*******************************************************************************
+ * 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);
+
+}