From c57861cfa068f7ceb41a1f69df23fd05a1d1fa30 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Fri, 6 Oct 2023 14:48:52 +0200
Subject: [PATCH] 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 | 4 +-
build.gradle | 2 +-
src/org/eventb/core/ast/ISpecialization.java | 54 ++++++++++++++-
.../internal/core/ast/Specialization.java | 66 +++++++++++++------
.../internal/core/ast/wd/WDComputer.java | 16 ++++-
5 files changed, 116 insertions(+), 26 deletions(-)
diff --git a/META-INF/MANIFEST.MF b/META-INF/MANIFEST.MF
index 4e3f05d..0564041 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.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
diff --git a/build.gradle b/build.gradle
index 65b0100..f486887 100644
--- a/build.gradle
+++ b/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 {
diff --git a/src/org/eventb/core/ast/ISpecialization.java b/src/org/eventb/core/ast/ISpecialization.java
index 9770194..2f4d376 100644
--- a/src/org/eventb/core/ast/ISpecialization.java
+++ b/src/org/eventb/core/ast/ISpecialization.java
@@ -1,5 +1,5 @@
/*******************************************************************************
- * 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.
*
@@ -213,6 +242,29 @@ public interface ISpecialization extends Cloneable {
* @since 3.3
*/
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
diff --git a/src/org/eventb/internal/core/ast/Specialization.java b/src/org/eventb/internal/core/ast/Specialization.java
index 43cef43..62a8348 100644
--- a/src/org/eventb/internal/core/ast/Specialization.java
+++ b/src/org/eventb/internal/core/ast/Specialization.java
@@ -1,5 +1,5 @@
/*******************************************************************************
- * 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;
diff --git a/src/org/eventb/internal/core/ast/wd/WDComputer.java b/src/org/eventb/internal/core/ast/wd/WDComputer.java
index ed8f8c2..768f9ee 100644
--- a/src/org/eventb/internal/core/ast/wd/WDComputer.java
+++ b/src/org/eventb/internal/core/ast/wd/WDComputer.java
@@ -1,5 +1,5 @@
/*******************************************************************************
- * 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();
--
GitLab