diff --git a/META-INF/MANIFEST.MF b/META-INF/MANIFEST.MF
index 0d8ce7eb0657decb527a0c5288ee9a6b2cde1d34..e9ed88684af0394cf58f307b50ea5690895eaa29 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.6.0.qualifier
+Bundle-Version: 3.7.0.qualifier
Bundle-Vendor: %providerName
Bundle-Localization: plugin
Export-Package: org.eventb.core.ast,
diff --git a/build.gradle b/build.gradle
index d75afa8d518fa3a9f64a3aae758a2c2e7383041c..ef14503ce5256d3eb6930b675141c1931751dea6 100644
--- a/build.gradle
+++ b/build.gradle
@@ -6,7 +6,7 @@ plugins {
}
project.group = 'de.hhu.stups'
-project.version = "3.7.0"
+project.version = "3.8.0-SNAPSHOT"
final isSnapshot = project.version.endsWith("-SNAPSHOT")
sourceSets {
diff --git a/src/org/eventb/core/ast/ExtendedPredicate.java b/src/org/eventb/core/ast/ExtendedPredicate.java
index 24a4bc3d598de0f641ae06869d3c48d54a92ab6c..6f06acec7b756c9fa7a7843cf7042225a905ccce 100644
--- a/src/org/eventb/core/ast/ExtendedPredicate.java
+++ b/src/org/eventb/core/ast/ExtendedPredicate.java
@@ -202,22 +202,14 @@ public class ExtendedPredicate extends Predicate implements IExtendedFormula {
}
}
- 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);
+ final FormulaFactory ff = getFactory();
+ ITypeEnvironmentBuilder typeEnv = ff.makeTypeEnvironment();
+ typeEnv.addAll(freeIdents);
+ TypeCheckResult tcRes = new TypeCheckResult(typeEnv.makeSnapshot());
+ extension.typeCheck(this, new TypeCheckMediator(tcRes, this, false));
typeChecked = !tcRes.hasProblem();
}
}
diff --git a/src/org/eventb/core/ast/FreeIdentifier.java b/src/org/eventb/core/ast/FreeIdentifier.java
index 81a0241286cfd45d9da2a82465719819e92851be..bb65fb5882b0e4d90c27fde94f91774e18f90c30 100644
--- a/src/org/eventb/core/ast/FreeIdentifier.java
+++ b/src/org/eventb/core/ast/FreeIdentifier.java
@@ -1,5 +1,5 @@
/*******************************************************************************
- * Copyright (c) 2005, 2017 ETH Zurich and others.
+ * Copyright (c) 2005, 2023 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
@@ -34,8 +34,7 @@ import org.eventb.internal.core.typecheck.TypeCheckResult;
import org.eventb.internal.core.typecheck.TypeUnifier;
/**
- * This class represents either identifiers occurring free in an event-B
- * formula, or a bound identifier declaration.
+ * This class represents identifiers occurring free in an event-B formula.
* <p>
* Identifiers which are bound by a quantifier are instance of the class
* {@link org.eventb.core.ast.BoundIdentifier} instead.
diff --git a/src/org/eventb/core/ast/ITypeEnvironment.java b/src/org/eventb/core/ast/ITypeEnvironment.java
index 8c72b45eeaa7e63da92ba13215367501038c5ee8..55eb2a68d4ca0af99c2e6566c3bd9548323820c2 100644
--- a/src/org/eventb/core/ast/ITypeEnvironment.java
+++ b/src/org/eventb/core/ast/ITypeEnvironment.java
@@ -1,5 +1,5 @@
/*******************************************************************************
- * Copyright (c) 2005, 2017 ETH Zurich and others.
+ * Copyright (c) 2005, 2023 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
@@ -209,6 +209,25 @@ public interface ITypeEnvironment {
*/
IExtensionTranslation makeExtensionTranslation();
+ /**
+ * Returns a fresh extension translation based on a snapshot of this type
+ * environment. The resulting translation will be applicable to any formula
+ * which is type-checked within this type environment at the time of the call to
+ * this method.
+ *
+ * The provided target factory must contain at least the extensions that are not
+ * translatable by implementations of {@link IExtensionTranslation}. If it
+ * contains more extensions, these will not be translated.
+ *
+ * @param targetFactory target factory to use
+ * @return a fresh extension translation
+ * @see Formula#translateExtensions(IExtensionTranslation)
+ * @throws IllegalArgumentException if the target factory misses some
+ * untranslatable extensions
+ * @since 3.7
+ */
+ IExtensionTranslation makeExtensionTranslation(FormulaFactory targetFactory);
+
/**
* Returns an iterator for traversing this type environment.
*
@@ -233,6 +252,18 @@ public interface ITypeEnvironment {
*/
Type getType(String name);
+ /**
+ * Returns the list of free identifiers in this type environment.
+ *
+ * This is equivalent to getting all the identifiers in this type environment
+ * with {@link #getNames()} and then getting the type of each identifier with
+ * {@link #getType(String)}.
+ *
+ * @return the list of free identifiers
+ * @since 3.7
+ */
+ FreeIdentifier[] getFreeIdentifiers();
+
/**
* Returns whether this type environment is empty.
*
diff --git a/src/org/eventb/internal/core/ast/datatype/DatatypeTranslation.java b/src/org/eventb/internal/core/ast/datatype/DatatypeTranslation.java
index 55f015f3a51d3e12640f8edad5a815c258cb2480..cd5c4d11b15948f84835ed84a413fae372c9c349 100644
--- a/src/org/eventb/internal/core/ast/datatype/DatatypeTranslation.java
+++ b/src/org/eventb/internal/core/ast/datatype/DatatypeTranslation.java
@@ -1,5 +1,5 @@
/*******************************************************************************
- * Copyright (c) 2013, 2016 Systerel and others.
+ * Copyright (c) 2013, 2023 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
@@ -136,8 +136,11 @@ public class DatatypeTranslation extends AbstractTranslation implements
}
public Type translateParametricType(ParametricType type) {
- assert type.getExprExtension().getOrigin() instanceof Datatype;
- return getTranslatorFor(type).getTranslatedType();
+ if (type.getExprExtension().getOrigin() instanceof Datatype) {
+ return getTranslatorFor(type).getTranslatedType();
+ } else {
+ return type.translate(targetFactory);
+ }
}
public Expression translate(ExtendedExpression src,
diff --git a/src/org/eventb/internal/core/ast/extension/ExtensionTranslation.java b/src/org/eventb/internal/core/ast/extension/ExtensionTranslation.java
index f7d5e7cef60891775681bfc091082a1d900b88b3..00bfe41691a4ae8a99ba3087d6150ae389cf1560 100644
--- a/src/org/eventb/internal/core/ast/extension/ExtensionTranslation.java
+++ b/src/org/eventb/internal/core/ast/extension/ExtensionTranslation.java
@@ -1,5 +1,5 @@
/*******************************************************************************
- * Copyright (c) 2014, 2016 Systerel and others.
+ * Copyright (c) 2014, 2023 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
@@ -77,8 +77,20 @@ public class ExtensionTranslation extends AbstractTranslation implements
private final ITypeCheckingRewriter rewriter;
public ExtensionTranslation(ISealedTypeEnvironment srcTypenv) {
+ this(srcTypenv, null);
+ }
+
+ public ExtensionTranslation(ISealedTypeEnvironment srcTypenv, FormulaFactory trgFac) {
super(srcTypenv);
- this.trgFactory = computeTargetFactory(srcTypenv.getFormulaFactory());
+ final Set<IFormulaExtension> requiredExtensions = computeTargetExtensions(srcTypenv.getFormulaFactory());
+ if (trgFac == null) {
+ trgFactory = FormulaFactory.getInstance(requiredExtensions);
+ } else {
+ if (!trgFac.getExtensions().containsAll(requiredExtensions)) {
+ throw new IllegalArgumentException("Target factory misses some untranslatable extensions");
+ }
+ trgFactory = trgFac;
+ }
final Set<String> usedNames = new HashSet<String>(srcTypenv.getNames());
this.nameSolver = new FreshNameSolver(usedNames, trgFactory);
@@ -90,7 +102,7 @@ public class ExtensionTranslation extends AbstractTranslation implements
populateTargetTypenv(typeRewriter);
}
- private static FormulaFactory computeTargetFactory(FormulaFactory fac) {
+ private static Set<IFormulaExtension> computeTargetExtensions(FormulaFactory fac) {
final Set<IFormulaExtension> keptExtensions;
final Set<IFormulaExtension> extensions = fac.getExtensions();
keptExtensions = new LinkedHashSet<IFormulaExtension>();
@@ -104,7 +116,7 @@ public class ExtensionTranslation extends AbstractTranslation implements
keptExtensions.add(extension);
}
}
- return FormulaFactory.getInstance(keptExtensions);
+ return keptExtensions;
}
private void populateTargetTypenv(TypeRewriter typeRewriter) {
@@ -128,6 +140,9 @@ public class ExtensionTranslation extends AbstractTranslation implements
}
public Type translate(ParametricType src) {
+ if (trgFactory.hasExtension(src.getExprExtension())) {
+ return src.translate(trgFactory);
+ }
final ExpressionExtSignature signature = getSignature(src);
final TypeExtTranslator translator = typeTranslators.get(signature);
return translator.translate();
@@ -135,6 +150,10 @@ public class ExtensionTranslation extends AbstractTranslation implements
public Expression translate(ExtendedExpression src,
Expression[] newChildExprs, Predicate[] newChildPreds) {
+ if (trgFactory.hasExtension(src.getExtension())) {
+ return trgFactory.makeExtendedExpression(src.getExtension(), newChildExprs, newChildPreds,
+ src.getSourceLocation(), src.getType().translate(trgFactory));
+ }
final ExpressionExtSignature signature = getSignature(src);
final ExpressionExtTranslator translator = exprTranslators
.get(signature);
@@ -143,6 +162,10 @@ public class ExtensionTranslation extends AbstractTranslation implements
public Predicate translate(ExtendedPredicate src,
Expression[] newChildExprs, Predicate[] newChildPreds) {
+ if (trgFactory.hasExtension(src.getExtension())) {
+ return trgFactory.makeExtendedPredicate(src.getExtension(), newChildExprs, newChildPreds,
+ src.getSourceLocation());
+ }
final PredicateExtSignature signature = getSignature(src);
final PredicateExtTranslator translator = predTranslators
.get(signature);
diff --git a/src/org/eventb/internal/core/typecheck/TypeEnvironment.java b/src/org/eventb/internal/core/typecheck/TypeEnvironment.java
index 26b9227717fe3fb0509b4f75b89f35cd0a2d5ca1..e907573b8889b76c74190a5833565f1f1851d0cf 100644
--- a/src/org/eventb/internal/core/typecheck/TypeEnvironment.java
+++ b/src/org/eventb/internal/core/typecheck/TypeEnvironment.java
@@ -1,5 +1,5 @@
/*******************************************************************************
- * Copyright (c) 2005, 2014 ETH Zurich and others.
+ * Copyright (c) 2005, 2023 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
@@ -184,6 +184,11 @@ public abstract class TypeEnvironment implements ITypeEnvironment{
return new ExtensionTranslation(this.makeSnapshot());
}
+ @Override
+ public IExtensionTranslation makeExtensionTranslation(FormulaFactory targetFactory) {
+ return new ExtensionTranslation(this.makeSnapshot(), targetFactory);
+ }
+
@Override
public IIterator getIterator(){
return new InternalIterator(map.entrySet().iterator());
@@ -199,6 +204,12 @@ public abstract class TypeEnvironment implements ITypeEnvironment{
return map.get(name);
}
+ @Override
+ public FreeIdentifier[] getFreeIdentifiers() {
+ return map.entrySet().stream().map(e -> ff.makeFreeIdentifier(e.getKey(), null, e.getValue()))
+ .toArray(FreeIdentifier[]::new);
+ }
+
@Override
public boolean isEmpty() {
return map.isEmpty();