From acebf907e188cb178e45f34770be92f25bb5dc69 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Fri, 6 Oct 2023 15:22:28 +0200
Subject: [PATCH] Update to Rodin 3.7 sources
---
META-INF/MANIFEST.MF | 2 +-
build.gradle | 2 +-
plugin.properties | 2 +-
.../eventb/core/ast/ExtendedPredicate.java | 27 ++++++--
src/org/eventb/core/ast/FormulaFactory.java | 63 ++++++++++++++++++-
.../ast/extension/IPredicateExtension.java | 15 ++++-
.../ast/extension/IPredicateExtension2.java | 40 ++++++++++++
7 files changed, 141 insertions(+), 10 deletions(-)
create mode 100644 src/org/eventb/core/ast/extension/IPredicateExtension2.java
diff --git a/META-INF/MANIFEST.MF b/META-INF/MANIFEST.MF
index 0564041..0d8ce7e 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 2467462..2077b9e 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 4649e84..5648290 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 32c5d9c..24a4bc3 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 6a4488a..576de16 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 9234c77..b3033e5 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 0000000..1568fa5
--- /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);
+
+}
--
GitLab