From be1632c6c4e933a117cf2286a0c6c6acb70f51ac Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Fri, 6 Oct 2023 11:29:10 +0200
Subject: [PATCH] Update to Rodin 3.3 sources
---
META-INF/MANIFEST.MF | 2 +-
build.gradle | 2 +-
.../eventb/core/ast/ExtendedPredicate.java | 17 +-
src/org/eventb/core/ast/Formula.java | 10 +-
src/org/eventb/core/ast/FreeIdentifier.java | 21 +-
src/org/eventb/core/ast/ISpecialization.java | 179 ++++-
src/org/eventb/core/ast/ITypeEnvironment.java | 8 +-
src/org/eventb/core/ast/Type.java | 7 +-
.../core/ast/extension/ExtensionFactory.java | 25 +-
.../core/ast/extension/IPriorityMediator.java | 15 +-
.../core/ast/BindingSubstitution.java | 4 +-
.../core/ast/BoundIdentDeclRemover.java | 8 +-
.../core/ast/DefaultTypeCheckingRewriter.java | 69 +-
.../internal/core/ast/SimpleSubstitution.java | 8 +-
.../internal/core/ast/Specialization.java | 691 ++++++++++++++----
.../eventb/internal/core/ast/Substitute.java | 127 ++--
.../internal/core/ast/Substitution.java | 6 +-
.../internal/core/ast/TypeRewriter.java | 8 +-
.../internal/core/ast/datatype/Datatype.java | 43 +-
.../core/ast/datatype/DatatypeRewriter.java | 79 +-
.../ast/datatype/DatatypeTranslation.java | 8 +-
.../ast/extension/ExtensionSignature.java | 145 ++--
.../ast/extension/ExtensionTranslation.java | 108 ++-
.../ast/extension/ExtensionTranslator.java | 147 +++-
.../ast/extension/FunctionalTypeBuilder.java | 91 +++
.../ast/extension/TranslatorRegistry.java | 40 +-
.../internal/core/parser/SubParsers.java | 55 +-
27 files changed, 1445 insertions(+), 478 deletions(-)
create mode 100644 src/org/eventb/internal/core/ast/extension/FunctionalTypeBuilder.java
diff --git a/META-INF/MANIFEST.MF b/META-INF/MANIFEST.MF
index 50e84de..91b52c6 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.2.0.qualifier
+Bundle-Version: 3.3.0.qualifier
Bundle-Vendor: %providerName
Bundle-Localization: plugin
Export-Package: org.eventb.core.ast,
diff --git a/build.gradle b/build.gradle
index ec7a6e3..c9f019f 100644
--- a/build.gradle
+++ b/build.gradle
@@ -6,7 +6,7 @@ plugins {
}
project.group = 'de.hhu.stups'
-project.version = "3.2.1"
+project.version = "3.3.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 2ae4f52..32c5d9c 100644
--- a/src/org/eventb/core/ast/ExtendedPredicate.java
+++ b/src/org/eventb/core/ast/ExtendedPredicate.java
@@ -1,5 +1,5 @@
/*******************************************************************************
- * Copyright (c) 2010, 2013 Systerel and others.
+ * Copyright (c) 2010, 2016 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,9 +13,12 @@ package org.eventb.core.ast;
import static org.eventb.core.ast.AssociativeHelper.getSyntaxTreeHelper;
import static org.eventb.core.ast.ExtensionHelper.makeParserPrinter;
import static org.eventb.core.ast.extension.IOperatorProperties.FormulaType.PREDICATE;
+import static org.eventb.core.ast.extension.IOperatorProperties.Notation.INFIX;
import static org.eventb.core.ast.extension.IOperatorProperties.Notation.PREFIX;
import static org.eventb.internal.core.ast.extension.ArityCoverage.ANY;
import static org.eventb.internal.core.ast.extension.ArityCoverage.ONE_OR_MORE;
+import static org.eventb.internal.core.ast.extension.ArityCoverage.TWO;
+import static org.eventb.internal.core.ast.extension.ArityCoverage.NONE;
import java.util.ArrayList;
import java.util.Arrays;
@@ -66,6 +69,16 @@ public class ExtendedPredicate extends Predicate implements IExtendedFormula {
return new SubParsers.ExtendedPredParen(kind, tag);
}
+ },
+
+ EXTENDED_RELATIONAL_PREDICATE(INFIX, PREDICATE, TWO, NONE, TWO, false) {
+
+ @Override
+ protected IParserPrinter<ExtendedPredicate> makeParser(int kind,
+ int tag) {
+ return new SubParsers.ExtendedRelationalPredicateParser(kind, tag);
+ }
+
},
;
@@ -98,7 +111,7 @@ public class ExtendedPredicate extends Predicate implements IExtendedFormula {
@Override
public boolean isSpaced() {
- return false;
+ return ExtendedPredicateParsers.this.getOperatorCoverage().getNotation() == INFIX;
}
@Override
diff --git a/src/org/eventb/core/ast/Formula.java b/src/org/eventb/core/ast/Formula.java
index 3d76447..39fbe60 100644
--- a/src/org/eventb/core/ast/Formula.java
+++ b/src/org/eventb/core/ast/Formula.java
@@ -1,5 +1,5 @@
/*******************************************************************************
- * Copyright (c) 2005, 2014 ETH Zurich and others.
+ * Copyright (c) 2005, 2017 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
@@ -2393,13 +2393,19 @@ public abstract class Formula<T extends Formula<T>> {
* if this formula is an assignment
* @throws IllegalStateException
* if this formula is not type-checked.
+ * @throws IllegalArgumentException
+ * if the given specialization is not compatible with this
+ * formula, that is the specialization contains a substitution
+ * for an identifier with the same name as an identifier in this
+ * formula, but with a different type
*
* @since 2.6
*/
public T specialize(ISpecialization specialization) {
ensureTypeChecked();
final Specialization spec = (Specialization) specialization;
- return rewrite(spec);
+ spec.prepare(this);
+ return rewrite(spec.getFormulaRewriter());
}
/**
diff --git a/src/org/eventb/core/ast/FreeIdentifier.java b/src/org/eventb/core/ast/FreeIdentifier.java
index 37978b9..81a0241 100644
--- a/src/org/eventb/core/ast/FreeIdentifier.java
+++ b/src/org/eventb/core/ast/FreeIdentifier.java
@@ -1,5 +1,5 @@
/*******************************************************************************
- * Copyright (c) 2005, 2013 ETH Zurich and others.
+ * Copyright (c) 2005, 2017 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
@@ -297,10 +297,25 @@ public class FreeIdentifier extends Identifier {
return false;
}
+ /**
+ * Returns the given type corresponding to this type-checked identifier.
+ * <p>
+ * The returned type is <em>not</em> the type of this identifier.
+ * </p>
+ *
+ * @return the given type represented by this identifier
+ * @throws IllegalStateException
+ * when this identifier is not a given type or is not
+ * type-checked
+ * @see Type#toExpression()
+ * @see #isATypeExpression()
+ * @since 3.3 change return type to GivenType
+ */
@Override
- public Type toType() {
+ public GivenType toType() {
if (!isATypeExpression()) {
- return super.toType();
+ throw new IllegalStateException(
+ "Identifier does not denote a type: " + toString());
}
return getFactory().makeGivenType(this);
}
diff --git a/src/org/eventb/core/ast/ISpecialization.java b/src/org/eventb/core/ast/ISpecialization.java
index ae2524f..b89d27f 100644
--- a/src/org/eventb/core/ast/ISpecialization.java
+++ b/src/org/eventb/core/ast/ISpecialization.java
@@ -1,5 +1,5 @@
/*******************************************************************************
- * Copyright (c) 2012, 2014 Systerel and others.
+ * Copyright (c) 2012, 2017 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
@@ -7,18 +7,21 @@
*
* Contributors:
* Systerel - initial API and implementation
+ * University of Southampton - added support for predicate variables
*******************************************************************************/
package org.eventb.core.ast;
/**
- * Common protocol for describing a specialization, which groups together a type
- * substitution and a free identifier substitution in one object. It allows to
- * specialize a formula by applying both substitutions at once.
+ * Common protocol for describing a specialization, which groups together type
+ * substitutions, free-identifier substitutions, and predicate-variable
+ * substitutions in one object. It allows to specialize a formula by applying
+ * all these substitutions at once.
* <p>
- * Instances of this class can be created only through a formula factory. Type
- * and free identifier substitutions are then added one by one using
- * <code>put()</code> methods. Finally, the instance is passed as argument to a
- * <code>specialize()</code> method on a type, type environment or formula.
+ * Instances of this class can be created only through a formula factory. Type,
+ * free-identifier and predicate-variable substitutions are then added one by
+ * one using <code>put()</code> methods. Finally, the instance is passed as
+ * argument to a <code>specialize()</code> method on a type, type environment or
+ * formula.
* </p>
* <p>
* The substitutions can also change the formula factory. Consequently, all
@@ -26,9 +29,9 @@ package org.eventb.core.ast;
* specialization.
* </p>
* <p>
- * Both substitutions must be compatible, that is the expression to be
+ * These substitutions must be compatible, that is the expression to be
* substituted for an identifier must bear a type which is the result of
- * applying the type substitution to the type of the identifier.
+ * applying the type substitutions to the type of the identifier.
* </p>
* <p>
* This condition must hold after every method call. This implies that a type
@@ -52,19 +55,35 @@ package org.eventb.core.ast;
* <code>T</code> for <code>x</code> of type <code>S</code>.
* </p>
* <p>
- * This side-effect is made on purpose to ensure that successive applications of
- * a specialization to several type environments or formulas are all compatible.
+ * When defining substitutions, a specialization also maintains a destination
+ * type environment. It contains all the identifiers that have been used in the
+ * right-hand sides of substitutions, as well as all identifiers that have
+ * occurred in a formula passed to <code>specialize()</code> methods and that
+ * have not been substituted.
+ * </p>
+ * <p>
+ * The purpose of this destination type environment, together with the automatic
+ * completion of substitutions ensures that successive applications of a
+ * specialization to several type environments or formulas are all compatible.
* In particular, if a formula type-checks with respect to some type
* environment, then the specialized formula also type-checks with the
* specialized type environment, under the condition that both specialization
* are performed with the same instance of this class.
* </p>
* <p>
- * In the rare cases where this side-effect is not wanted, one can always clone
+ * Similarly, when specializing a formula, an instance of this class can change
+ * by side-effect in the following manner: For each predicate variable, not
+ * already part of the predicate variable substitution and which occurs in the
+ * formula, a new predicate variable substitution is added to this
+ * specialization. It maps that predicate variable to itself.
+ * </p>
+ * <p>
+ * In the rare cases where the side-effects are not wanted, one can always clone
* a specialization object and use the clone to apply a specialization.
* </p>
*
* @author Laurent Voisin
+ * @author htson - added support for predicate variables.
*
* @see FormulaFactory#makeSpecialization()
* @see Type#specialize(ISpecialization)
@@ -100,6 +119,11 @@ public interface ISpecialization {
* 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
@@ -110,6 +134,7 @@ public interface ISpecialization {
* registered substitutions or the value has been created by
* another formula factory
* @see Type#getFactory()
+ * @see #canPut(GivenType, Type)
*/
void put(GivenType type, Type value);
@@ -118,7 +143,7 @@ public interface ISpecialization {
*
* @param type
* some given type
- * @return the type to be substituted for the given given type of
+ * @return the type to be substituted for the given given type or
* <code>null</code> if no substitution has been defined for the
* given given type
* @since 3.1
@@ -135,6 +160,10 @@ public interface ISpecialization {
* bound identifiers, it is up to the caller to manage that they do not
* escape their scope. The given expression must have been created by the
* same formula factory as this instance.
+ * <p>
+ * This method can have side-effects, as described in
+ * {@link ISpecialization}.
+ * </p>
*
* @param ident
* a typed identifier to substitute
@@ -147,6 +176,7 @@ public interface ISpecialization {
* created by another formula factory
* @see Formula#isTypeChecked()
* @see Formula#getFactory()
+ * @see #canPut(FreeIdentifier, Expression)
*/
void put(FreeIdentifier ident, Expression value);
@@ -155,11 +185,130 @@ public interface ISpecialization {
*
* @param ident
* a typed identifier
- * @return the expression to be substituted for the given identifier of
+ * @return the expression to be substituted for the given identifier or
* <code>null</code> if no substitution has been defined for the
* given identifier
* @since 3.1
*/
Expression get(FreeIdentifier ident);
+ /**
+ * 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, Type)} is satisfied. The value 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
+ * 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 has been created by another formula factory
+ * @author htson
+ * @since 3.3
+ */
+ boolean canPut(GivenType type, Type value);
+
+ /**
+ * Checks whether the proposed free-identifier substitution is compatible
+ * with already registered substitutions (for given types, free identifiers,
+ * and predicate variables), i.e., if the precondition of
+ * {@link #put(FreeIdentifier, Expression)} is satisfied. Both the type and
+ * the value must be type-checked. The value expression must have been
+ * created by the same formula factory as this instance. This method does
+ * <em>not</em> modify the specialization instance.
+ *
+ * @param ident
+ * a typed identifier to substitute
+ * @param value
+ * a typed expression to substitute for the given identifier
+ * @return <code>true</code> if the proposed free identifier substitution is
+ * compatible with already registered substitutions. Return
+ * <code>false</code> otherwise.
+ * @throws IllegalArgumentException
+ * if either parameter is not typed, or the value has been
+ * created by another formula factory
+ * @author htson
+ * @since 3.3
+ */
+ boolean canPut(FreeIdentifier ident, Expression value);
+
+ /**
+ * Adds a new predicate variable substitution to this specialization. All
+ * substitutions will be applied in parallel when specializing a formula.
+ * The given predicate value must be typed, but needs not be well-formed. In
+ * case the predicate value contains bound identifiers, it is up to the
+ * caller to manage that they do not escape their scope. The given predicate
+ * value must have been created by the same formula factory as this
+ * instance.
+ * <p>
+ * This method can have side-effects, as described in
+ * {@link ISpecialization}.
+ * </p>
+ *
+ * @param predVar
+ * a predicate variable to substitute
+ * @param value
+ * a typed predicate to substitute for the given predicate
+ * variable.
+ * @return <code>true</code> if the proposed predicate variable substitution
+ * is compatible with already registered substitutions, and this
+ * specialization instance has been changed accordingly. Return
+ * <code>false</code> otherwise and this specialization instance is
+ * unchanged.
+ * @throws IllegalArgumentException
+ * if the value is not typed or has been created by another
+ * formula factory
+ * @see Formula#isTypeChecked()
+ * @see Formula#getFactory()
+ * @author htson
+ * @since 3.3
+ */
+ boolean put(PredicateVariable predVar, Predicate value);
+
+ /**
+ * Returns the predicate to be substituted for the given predicate variable.
+ *
+ * @param predVar
+ * a predicate variable.
+ * @return the predicate to be substituted for the given predicate variable
+ * or <code>null</code> if no substitution has been defined for the
+ * given predicate variable
+ * @author htson
+ * @since 3.3
+ */
+ Predicate get(PredicateVariable predVar);
+
+ /**
+ * Returns the set of given types to be substituted.
+ *
+ * @return the set of given types to be substituted
+ * @author htson
+ * @since 3.3
+ */
+ GivenType[] getTypes();
+
+ /**
+ * Returns the set of free identifiers to be substituted.
+ *
+ * @return the set of free identifiers to be substituted
+ * @author htson
+ * @since 3.3
+ */
+ FreeIdentifier[] getFreeIdentifiers();
+
+ /**
+ * Returns the set of predicate variables to be substituted.
+ *
+ * @return the set of predicate variables to be substituted
+ * @author htson
+ * @since 3.3
+ */
+ PredicateVariable[] getPredicateVariables();
+
}
diff --git a/src/org/eventb/core/ast/ITypeEnvironment.java b/src/org/eventb/core/ast/ITypeEnvironment.java
index f9dc087..8c72b45 100644
--- a/src/org/eventb/core/ast/ITypeEnvironment.java
+++ b/src/org/eventb/core/ast/ITypeEnvironment.java
@@ -1,5 +1,5 @@
/*******************************************************************************
- * Copyright (c) 2005, 2014 ETH Zurich and others.
+ * Copyright (c) 2005, 2017 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
@@ -271,6 +271,12 @@ public interface ITypeEnvironment {
* the specialization to apply
* @return the type environment obtained by applying the given
* specialization to this type environment
+ * @throws IllegalArgumentException
+ * if the given specialization is not compatible with this type
+ * environment, that is the specialization contains a
+ * substitution for an identifier with the same name as an
+ * identifier in this type environment, but with a different
+ * type
* @since 3.0
*/
ITypeEnvironmentBuilder specialize(ISpecialization specialization);
diff --git a/src/org/eventb/core/ast/Type.java b/src/org/eventb/core/ast/Type.java
index fd6a72f..2bc492f 100644
--- a/src/org/eventb/core/ast/Type.java
+++ b/src/org/eventb/core/ast/Type.java
@@ -1,5 +1,5 @@
/*******************************************************************************
- * Copyright (c) 2005, 2014 ETH Zurich and others.
+ * Copyright (c) 2005, 2017 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
@@ -296,6 +296,11 @@ public abstract class Type {
* @param specialization
* the specialization to apply
* @return a specialization of this type or <code>this</code> if unchanged
+ * @throws IllegalArgumentException
+ * if the given specialization is not compatible with this type,
+ * that is the specialization contains a substitution for an
+ * identifier with the same name as a given type in this type,
+ * but with a different type
* @since 2.6
*/
public final Type specialize(ISpecialization specialization) {
diff --git a/src/org/eventb/core/ast/extension/ExtensionFactory.java b/src/org/eventb/core/ast/extension/ExtensionFactory.java
index f97f779..91c3a19 100644
--- a/src/org/eventb/core/ast/extension/ExtensionFactory.java
+++ b/src/org/eventb/core/ast/extension/ExtensionFactory.java
@@ -1,5 +1,5 @@
/*******************************************************************************
- * Copyright (c) 2010 Systerel and others.
+ * Copyright (c) 2010, 2016 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,13 +15,14 @@ import static org.eventb.core.ast.extension.IOperatorProperties.MULTARY_2;
import static org.eventb.core.ast.extension.IOperatorProperties.UNARY;
import static org.eventb.core.ast.extension.IOperatorProperties.FormulaType.EXPRESSION;
import static org.eventb.core.ast.extension.IOperatorProperties.FormulaType.PREDICATE;
+import static org.eventb.core.ast.extension.IOperatorProperties.Notation.INFIX;
import static org.eventb.core.ast.extension.IOperatorProperties.Notation.PREFIX;
import org.eventb.core.ast.extension.IOperatorProperties.FormulaType;
import org.eventb.internal.core.ast.extension.Arity;
-import org.eventb.internal.core.ast.extension.TypeDistribs.MixedTypes;
-import org.eventb.internal.core.ast.extension.TypeDistribs.AllSameType;
import org.eventb.internal.core.ast.extension.ExtensionKind;
+import org.eventb.internal.core.ast.extension.TypeDistribs.AllSameType;
+import org.eventb.internal.core.ast.extension.TypeDistribs.MixedTypes;
/**
* @author Nicolas Beauger
@@ -84,6 +85,24 @@ public class ExtensionFactory {
return new ExtensionKind(PREFIX, formulaType, childTypes, false);
}
+ /**
+ * Make an infix extension kind.
+ *
+ * @param formulaType
+ * type of the resulting formula
+ * @param childTypes
+ * type distribution of child formulae
+ * @param isAssociative
+ * <code>true</code> for associative kind, <code>false</code>
+ * otherwise
+ * @return a new extension kind
+ * @since 3.3
+ */
+ public static IExtensionKind makeInfixKind(FormulaType formulaType,
+ ITypeDistribution childTypes, boolean isAssociative) {
+ return new ExtensionKind(INFIX, formulaType, childTypes, isAssociative);
+ }
+
public static IArity makeArity(int min, int max) {
return new Arity(min, max);
}
diff --git a/src/org/eventb/core/ast/extension/IPriorityMediator.java b/src/org/eventb/core/ast/extension/IPriorityMediator.java
index 26563ad..a4d0804 100644
--- a/src/org/eventb/core/ast/extension/IPriorityMediator.java
+++ b/src/org/eventb/core/ast/extension/IPriorityMediator.java
@@ -1,5 +1,5 @@
/*******************************************************************************
- * Copyright (c) 2010 Systerel and others.
+ * Copyright (c) 2010, 2016 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
@@ -18,7 +18,10 @@ package org.eventb.core.ast.extension;
public interface IPriorityMediator {
/**
- * Adds a priority between operators of given ids.
+ * Adds a priority between the two operators with the given ids.
+ * <p>
+ * Both operators must belong to the same operator group.
+ * </p>
* <p>
* lowOpId operator gets a lower priority than highOpId operator.
* </p>
@@ -37,6 +40,9 @@ public interface IPriorityMediator {
* an operator id
* @throws CycleError
* if adding the given priority introduces a cycle
+ * @throws IllegalArgumentException
+ * if the operators do not belong to the same operator group, or
+ * if one of the given operator ids has not been declared
*/
void addPriority(String lowOpId, String highOpId) throws CycleError;
@@ -56,7 +62,8 @@ public interface IPriorityMediator {
* a group id
* @throws CycleError
* if adding the given priority introduces a cycle
+ * @throws IllegalArgumentException
+ * if one of the given group ids has not been declared
*/
- void addGroupPriority(String lowGroupId, String highGroupId)
- throws CycleError;
+ void addGroupPriority(String lowGroupId, String highGroupId) throws CycleError;
}
diff --git a/src/org/eventb/internal/core/ast/BindingSubstitution.java b/src/org/eventb/internal/core/ast/BindingSubstitution.java
index 73208b9..7aa2ec7 100644
--- a/src/org/eventb/internal/core/ast/BindingSubstitution.java
+++ b/src/org/eventb/internal/core/ast/BindingSubstitution.java
@@ -1,5 +1,5 @@
/*******************************************************************************
- * Copyright (c) 2005, 2013 ETH Zurich and others.
+ * Copyright (c) 2005, 2016 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
@@ -41,7 +41,7 @@ public class BindingSubstitution extends SimpleSubstitution {
super(ff);
this.offset = identsToBind.size();
- map = new HashMap<FreeIdentifier, Substitute>(offset * 4 / 3 + 1);
+ map = new HashMap<FreeIdentifier, Substitute<Expression>>(offset * 4 / 3 + 1);
int index = offset - 1;
for (FreeIdentifier ident : identsToBind) {
diff --git a/src/org/eventb/internal/core/ast/BoundIdentDeclRemover.java b/src/org/eventb/internal/core/ast/BoundIdentDeclRemover.java
index 298239b..7065c26 100644
--- a/src/org/eventb/internal/core/ast/BoundIdentDeclRemover.java
+++ b/src/org/eventb/internal/core/ast/BoundIdentDeclRemover.java
@@ -1,5 +1,5 @@
/*******************************************************************************
- * Copyright (c) 2005, 2013 ETH Zurich and others.
+ * Copyright (c) 2005, 2016 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
@@ -33,7 +33,7 @@ public class BoundIdentDeclRemover extends Substitution {
protected final List<BoundIdentDecl> newDecls;
// Reversed array of substitutes
- protected final Substitute[] substitutes;
+ protected final Substitute<Expression>[] substitutes;
/**
* Creates a new substitution for removing some bound identifier
@@ -60,7 +60,9 @@ public class BoundIdentDeclRemover extends Substitution {
assert decls.length == keep.length;
final int lastIndex = decls.length - 1;
- substitutes = new Substitute[keep.length];
+ @SuppressWarnings("unchecked")
+ final Substitute<Expression>[] temp = new Substitute[keep.length];
+ substitutes = temp;
newDecls = new ArrayList<BoundIdentDecl>(decls.length);
int newIndex = 0;
// We need to traverse both arrays backward to compute the new indexes
diff --git a/src/org/eventb/internal/core/ast/DefaultTypeCheckingRewriter.java b/src/org/eventb/internal/core/ast/DefaultTypeCheckingRewriter.java
index fb73dd9..40fecde 100644
--- a/src/org/eventb/internal/core/ast/DefaultTypeCheckingRewriter.java
+++ b/src/org/eventb/internal/core/ast/DefaultTypeCheckingRewriter.java
@@ -1,5 +1,5 @@
/*******************************************************************************
- * Copyright (c) 2012, 2013 Systerel and others.
+ * Copyright (c) 2012, 2016 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
@@ -39,12 +39,20 @@ import org.eventb.core.ast.UnaryPredicate;
/**
* Default implementation of a type-checking rewriter that does not perform any
- * rewrite. In this class, we do not use the <code>checkReplacement()</code>
- * methods because the result bears the same type by construction. However,
- * these methods must be used by sub-classes that actually perform a rewrite
- * when it cannot be proven that the rewrite is always type-checked.
+ * rewrite by default. In this class, we do not use the
+ * <code>checkReplacement()</code> methods because the result bears the expected
+ * type by construction. However, these methods must be used by sub-classes that
+ * actually perform a rewrite when it cannot be proven that the rewrite is
+ * always type-checked. Note that these methods cannot be used in the case where
+ * types are also rewritten (it checks that the types did not change).
*
* <p>
+ * If a type rewriter is given to the constructor, then this class will
+ * implement type rewriting for all nodes. It is then expected to be sub-classed
+ * so that free identifiers (among others) are also rewritten to conform to the
+ * new type.
+ * </p>
+ * <p>
* This implementation guarantees that a leaf node is rebuilt with the rewriter
* factory if the factory of the node is different as required by
* {@link ITypeCheckingRewriter}. Consequently, when extending this class,
@@ -94,6 +102,13 @@ public class DefaultTypeCheckingRewriter implements ITypeCheckingRewriter {
this.typeRewriter = new TypeRewriter(ff);
}
+ // Version with a type rewriter provided by the caller and which therefore
+ // allows to also modify the types at the same time.
+ public DefaultTypeCheckingRewriter(TypeRewriter typeRewriter) {
+ this.ff = typeRewriter.getFactory();
+ this.typeRewriter = typeRewriter;
+ }
+
@Override
public boolean autoFlatteningMode() {
return false;
@@ -126,11 +141,13 @@ public class DefaultTypeCheckingRewriter implements ITypeCheckingRewriter {
@Override
public BoundIdentDecl rewrite(BoundIdentDecl src) {
- if (ff == src.getFactory()) {
+ final Type srcType = src.getType();
+ final Type trgType = typeRewriter.rewrite(srcType);
+ if (trgType == srcType && ff == src.getFactory()) {
return src;
}
return ff.makeBoundIdentDecl(src.getName(), src.getSourceLocation(),
- typeRewriter.rewrite(src.getType()));
+ trgType);
}
@Override
@@ -146,11 +163,13 @@ public class DefaultTypeCheckingRewriter implements ITypeCheckingRewriter {
@Override
public Expression rewrite(AtomicExpression src) {
- if (ff == src.getFactory()) {
+ final Type srcType = src.getType();
+ final Type trgType = typeRewriter.rewrite(srcType);
+ if (trgType == srcType && ff == src.getFactory()) {
return src;
}
return ff.makeAtomicExpression(src.getTag(), src.getSourceLocation(),
- typeRewriter.rewrite(src.getType()));
+ trgType);
}
@Override
@@ -170,22 +189,26 @@ public class DefaultTypeCheckingRewriter implements ITypeCheckingRewriter {
@Override
public Expression rewrite(BoundIdentifier src) {
- if (ff == src.getFactory()) {
+ final Type srcType = src.getType();
+ final Type trgType = typeRewriter.rewrite(srcType);
+ if (trgType == srcType && ff == src.getFactory()) {
return src;
}
return ff.makeBoundIdentifier(src.getBoundIndex(),
- src.getSourceLocation(), typeRewriter.rewrite(src.getType()));
+ src.getSourceLocation(), trgType);
}
@Override
public Expression rewrite(ExtendedExpression src, boolean changed,
Expression[] newChildExprs, Predicate[] newChildPreds) {
- if (!changed && ff == src.getFactory()) {
+ final Type srcType = src.getType();
+ final Type trgType = typeRewriter.rewrite(srcType);
+ if (trgType == srcType && !changed && ff == src.getFactory()) {
return src;
}
return ff.makeExtendedExpression(src.getExtension(), newChildExprs,
newChildPreds, src.getSourceLocation(),
- typeRewriter.rewrite(src.getType()));
+ trgType);
}
@Override
@@ -200,11 +223,13 @@ public class DefaultTypeCheckingRewriter implements ITypeCheckingRewriter {
@Override
public Expression rewrite(FreeIdentifier src) {
- if (ff == src.getFactory()) {
+ final Type srcType = src.getType();
+ final Type trgType = typeRewriter.rewrite(srcType);
+ if (trgType == srcType && ff == src.getFactory()) {
return src;
}
return ff.makeFreeIdentifier(src.getName(), src.getSourceLocation(),
- typeRewriter.rewrite(src.getType()));
+ trgType);
}
@Override
@@ -254,15 +279,15 @@ public class DefaultTypeCheckingRewriter implements ITypeCheckingRewriter {
@Override
public Expression rewrite(SetExtension src, SetExtension expr) {
- if (ff == expr.getFactory()) {
+ final Type srcType = src.getType();
+ final Type trgType = typeRewriter.rewrite(srcType);
+ if (trgType == srcType && ff == expr.getFactory()) {
return expr;
}
if (expr.getMembers().length == 0) {
- return ff.makeEmptySetExtension(
- typeRewriter.rewrite(expr.getType()),
- expr.getSourceLocation());
+ return ff.makeEmptySetExtension(trgType, src.getSourceLocation());
}
- return ff.makeSetExtension(expr.getMembers(), expr.getSourceLocation());
+ return ff.makeSetExtension(expr.getMembers(), src.getSourceLocation());
}
@Override
@@ -279,7 +304,9 @@ public class DefaultTypeCheckingRewriter implements ITypeCheckingRewriter {
@Override
public Expression rewrite(UnaryExpression src, boolean changed,
Expression newChild) {
- if (!changed) {
+ final Type srcType = src.getType();
+ final Type trgType = typeRewriter.rewrite(srcType);
+ if (trgType == srcType && !changed) {
assert ff == src.getFactory();
return src;
}
diff --git a/src/org/eventb/internal/core/ast/SimpleSubstitution.java b/src/org/eventb/internal/core/ast/SimpleSubstitution.java
index f9bf041..dbcc54b 100644
--- a/src/org/eventb/internal/core/ast/SimpleSubstitution.java
+++ b/src/org/eventb/internal/core/ast/SimpleSubstitution.java
@@ -1,5 +1,5 @@
/*******************************************************************************
- * Copyright (c) 2006, 2013 ETH Zurich and others.
+ * Copyright (c) 2006, 2016 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
@@ -26,7 +26,7 @@ import org.eventb.core.ast.FreeIdentifier;
*/
public class SimpleSubstitution extends Substitution {
- protected Map<FreeIdentifier, Substitute> map;
+ protected Map<FreeIdentifier, Substitute<Expression>> map;
// Constructor for sub-classes that build directly the map.
protected SimpleSubstitution(FormulaFactory ff) {
@@ -43,7 +43,7 @@ public class SimpleSubstitution extends Substitution {
*/
public SimpleSubstitution(Map<FreeIdentifier, Expression> map, FormulaFactory ff) {
super(ff);
- this.map = new HashMap<FreeIdentifier, Substitute>(map.size() * 4/3 + 1);
+ this.map = new HashMap<FreeIdentifier, Substitute<Expression>>(map.size() * 4/3 + 1);
for (Map.Entry<FreeIdentifier, Expression> entry : map.entrySet()) {
FreeIdentifier ident = entry.getKey();
Expression expr = entry.getValue();
@@ -59,7 +59,7 @@ public class SimpleSubstitution extends Substitution {
@Override
public Expression rewrite(FreeIdentifier ident) {
- Substitute repl = map.get(ident);
+ Substitute<Expression> repl = map.get(ident);
if (repl == null) {
return super.rewrite(ident);
}
diff --git a/src/org/eventb/internal/core/ast/Specialization.java b/src/org/eventb/internal/core/ast/Specialization.java
index ce09c67..43cef43 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, 2014 Systerel and others.
+ * Copyright (c) 2010, 2017 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
@@ -7,6 +7,7 @@
*
* Contributors:
* Systerel - initial API and implementation
+ * University of Southamtpon - added support for predicate varialbes.
*******************************************************************************/
package org.eventb.internal.core.ast;
@@ -15,23 +16,20 @@ import static org.eventb.internal.core.ast.Substitute.makeSubstitute;
import java.util.HashMap;
import java.util.Map;
import java.util.Map.Entry;
+import java.util.Set;
-import org.eventb.core.ast.AtomicExpression;
-import org.eventb.core.ast.BoundIdentDecl;
-import org.eventb.core.ast.BoundIdentifier;
import org.eventb.core.ast.Expression;
-import org.eventb.core.ast.ExtendedExpression;
+import org.eventb.core.ast.Formula;
import org.eventb.core.ast.FormulaFactory;
import org.eventb.core.ast.FreeIdentifier;
import org.eventb.core.ast.GivenType;
import org.eventb.core.ast.ISpecialization;
+import org.eventb.core.ast.ITypeEnvironment;
import org.eventb.core.ast.ITypeEnvironment.IIterator;
import org.eventb.core.ast.ITypeEnvironmentBuilder;
import org.eventb.core.ast.Predicate;
-import org.eventb.core.ast.SetExtension;
-import org.eventb.core.ast.SourceLocation;
+import org.eventb.core.ast.PredicateVariable;
import org.eventb.core.ast.Type;
-import org.eventb.core.ast.extension.IExpressionExtension;
import org.eventb.internal.core.typecheck.TypeEnvironment;
/**
@@ -42,41 +40,255 @@ import org.eventb.internal.core.typecheck.TypeEnvironment;
* doubled as an identifier substitution.
*
* @author Laurent Voisin
+ * @author htson - added support for predicate variables.
*/
-public class Specialization extends Substitution implements ISpecialization {
+public class Specialization implements ISpecialization {
- // Type substitutions
- private final Map<GivenType, Type> typeSubst;
+ private static class SpecializationTypeRewriter extends TypeRewriter {
- // Identifier substitutions
- private final Map<FreeIdentifier, Substitute> identSubst;
+ // Type substitutions
+ private final Map<GivenType, Type> typeSubst;
+
+ public SpecializationTypeRewriter(FormulaFactory ff) {
+ super(ff);
+ typeSubst = new HashMap<GivenType, Type>();
+ }
+
+ public SpecializationTypeRewriter(SpecializationTypeRewriter other) {
+ super(other.ff);
+ typeSubst = new HashMap<GivenType, Type>(other.typeSubst);
+ }
+
+ public Type get(GivenType key) {
+ return typeSubst.get(key);
+ }
+
+ public Type getWithDefault(GivenType key) {
+ Type value = typeSubst.get(key);
+ if (value == null) {
+ value = key.translate(ff);
+ }
+ return value;
+ }
+
+ public GivenType[] getTypes() {
+ final Set<GivenType> keySet = typeSubst.keySet();
+ return keySet.toArray(new GivenType[keySet.size()]);
+ }
+
+ public void put(GivenType type, Type value) {
+ final Type oldValue = typeSubst.put(type, value);
+ if (oldValue != null && !oldValue.equals(value)) {
+ typeSubst.put(type, oldValue); // repair
+ throw new IllegalArgumentException("Type substitution for "
+ + type + " already registered");
+ }
+ }
+
+ @Override
+ public void visit(GivenType type) {
+ final Type rewritten = getWithDefault(type);
+ // If the given type is not rewritten, use the super algorithm
+ // (this implements factory translation)
+ if (type.equals(rewritten)) {
+ super.visit(type);
+ } else {
+ result = rewritten;
+ }
+ }
+
+ // For debugging purpose
+ @Override
+ public String toString() {
+ final StringBuilder sb = new StringBuilder();
+ toString(sb);
+ return sb.toString();
+ }
+
+ public void toString(StringBuilder sb) {
+ sb.append("{");
+ String sep = "";
+ for (Entry<GivenType, Type> entry : typeSubst.entrySet()) {
+ sb.append(sep);
+ sep = " || ";
+ sb.append(entry.getKey());
+ sb.append("=");
+ sb.append(entry.getValue());
+ }
+ sb.append("}");
+ }
+ }
+
+ private static class SpecializationFormulaRewriter extends Substitution {
+
+ // Identifier substitutions
+ private final Map<FreeIdentifier, Substitute<Expression>> identSubst;
+
+ // Predicate variable substitutions
+ private final Map<PredicateVariable, Substitute<Predicate>> predSubst;
+
+ public SpecializationFormulaRewriter(SpecializationTypeRewriter typeRewriter) {
+ super(typeRewriter);
+ identSubst = new HashMap<FreeIdentifier, Substitute<Expression>>();
+ predSubst = new HashMap<PredicateVariable, Substitute<Predicate>>();
+ }
+
+ public SpecializationFormulaRewriter(
+ SpecializationFormulaRewriter other,
+ SpecializationTypeRewriter otherTypeRewriter) {
+ super(otherTypeRewriter);
+ identSubst = new HashMap<FreeIdentifier, Substitute<Expression>>(
+ other.identSubst);
+ predSubst = new HashMap<PredicateVariable, Substitute<Predicate>>(
+ other.predSubst);
+ }
+
+ public Expression get(FreeIdentifier ident) {
+ final Substitute<Expression> subst = identSubst.get(ident);
+ return subst == null ? null : subst.getSubstitute(ident, 0);
+ }
+
+ public Predicate get(PredicateVariable predVar) {
+ final Substitute<Predicate> subst = predSubst.get(predVar);
+ return subst == null ? null : subst.getSubstitute(predVar, 0);
+ }
+
+ public Expression getWithDefault(FreeIdentifier ident) {
+ final Substitute<Expression> subst = identSubst.get(ident);
+ if (subst != null) {
+ return subst.getSubstitute(ident, getBindingDepth());
+ }
+ final Type type = ident.getType();
+ final Type newType = typeRewriter.rewrite(type);
+ if (newType == type) {
+ return super.rewrite(ident);
+ }
+ return ff.makeFreeIdentifier(ident.getName(),
+ ident.getSourceLocation(), newType);
+ }
+
+ public Predicate getWithDefault(PredicateVariable predVar) {
+ Substitute<Predicate> subst = predSubst.get(predVar);
+ if (subst != null) {
+ return subst.getSubstitute(predVar, getBindingDepth());
+ }
+ return super.rewrite(predVar);
+ }
+
+ public FreeIdentifier[] getFreeIdentifiers() {
+ final Set<FreeIdentifier> keySet = identSubst.keySet();
+ return keySet.toArray(new FreeIdentifier[keySet.size()]);
+ }
+
+ public PredicateVariable[] getPredicateVariables() {
+ final Set<PredicateVariable> keySet = predSubst.keySet();
+ return keySet.toArray(new PredicateVariable[keySet.size()]);
+ }
+
+ public void put(FreeIdentifier ident, Expression value) {
+ final Substitute<Expression> subst = makeSubstitute(value);
+ final Substitute<Expression> oldSubst = identSubst.put(ident,
+ subst);
+ if (oldSubst != null && !oldSubst.equals(subst)) {
+ identSubst.put(ident, oldSubst); // repair
+ throw new IllegalArgumentException(
+ "Identifier substitution for " + ident
+ + " already registered");
+ }
+ }
+
+ public boolean put(PredicateVariable predVar, Predicate value) {
+ final Substitute<Predicate> subst = makeSubstitute(value);
+ final Substitute<Predicate> oldSubst = predSubst.put(predVar,
+ subst);
+ if (oldSubst != null && !oldSubst.equals(subst)) {
+ predSubst.put(predVar, oldSubst);
+ return false;
+ }
+ return true;
+ }
+
+ @Override
+ public Expression rewrite(FreeIdentifier identifier) {
+ final Expression newIdent = getWithDefault(identifier);
+ if (newIdent.equals(identifier)) {
+ return super.rewrite(identifier);
+ }
+ return newIdent;
+ }
+
+ @Override
+ public Predicate rewrite(PredicateVariable predVar) {
+ final Predicate newPred = getWithDefault(predVar);
+ if (newPred.equals(predVar)) {
+ return super.rewrite(predVar);
+ }
+ return newPred;
+ }
+
+ // For debugging purpose
+ @Override
+ public String toString() {
+ final StringBuilder sb = new StringBuilder();
+ toString(sb);
+ return sb.toString();
+ }
+
+ public void toString(StringBuilder sb) {
+ sb.append("{");
+ String sep = "";
+ for (Entry<FreeIdentifier, Substitute<Expression>> entry : identSubst
+ .entrySet()) {
+ sb.append(sep);
+ sep = " || ";
+ sb.append(entry.getKey());
+ sb.append("=");
+ sb.append(entry.getValue());
+ }
+ sb.append("} + {");
+ sep = "";
+ for (Entry<PredicateVariable, Substitute<Predicate>> entry : predSubst
+ .entrySet()) {
+ sb.append(sep);
+ sep = " || ";
+ sb.append(entry.getKey());
+ sb.append("=");
+ sb.append(entry.getValue());
+ }
+ sb.append("}");
+ }
+ }
+
+ // The type environment of the source language (quasi-final field to be
+ // set once at the first use and never changed after).
+ private ITypeEnvironmentBuilder srcTypenv;
+
+ // The type environment of the destination language.
+ private ITypeEnvironmentBuilder dstTypenv;
- private final TypeRewriter speTypeRewriter;
+ // The language of the right-hand sides of substitutions
+ private final FormulaFactory ff;
+
+ private final SpecializationTypeRewriter speTypeRewriter;
+
+ private final SpecializationFormulaRewriter formRewriter;
public Specialization(FormulaFactory ff) {
- super(ff);
- typeSubst = new HashMap<GivenType, Type>();
- identSubst = new HashMap<FreeIdentifier, Substitute>();
- speTypeRewriter = new TypeRewriter(ff) {
- @Override
- public void visit(GivenType type) {
- final Type rewritten = getOrSetDefault(type);
- // If the given type is not rewritten, use the super algorithm
- // (this implements factory translation)
- if (type.equals(rewritten)) {
- super.visit(type);
- } else {
- result = rewritten;
- }
- }
- };
+ this.srcTypenv = null;
+ this.dstTypenv = ff.makeTypeEnvironment();
+ this.ff = ff;
+ speTypeRewriter = new SpecializationTypeRewriter(ff);
+ formRewriter = new SpecializationFormulaRewriter(speTypeRewriter);
}
public Specialization(Specialization other) {
- super(other.ff);
- typeSubst = new HashMap<GivenType, Type>(other.typeSubst);
- identSubst = new HashMap<FreeIdentifier, Substitute>(other.identSubst);
- speTypeRewriter = other.speTypeRewriter;
+ this.srcTypenv = other.srcTypenv == null ? null
+ : other.srcTypenv.makeBuilder();
+ this.dstTypenv = other.dstTypenv.makeBuilder();
+ this.ff = other.ff;
+ speTypeRewriter = new SpecializationTypeRewriter(other.speTypeRewriter);
+ formRewriter = new SpecializationFormulaRewriter(other.formRewriter,
+ speTypeRewriter);
}
@Override
@@ -84,8 +296,40 @@ public class Specialization extends Substitution implements ISpecialization {
return new Specialization(this);
}
+ // For testing purpose, do not publish.
+ public ITypeEnvironmentBuilder getSourceTypenv() {
+ return srcTypenv;
+ }
+
+ @Override
+ public FormulaFactory getFactory() {
+ return ff;
+ }
+
+ // For testing purpose
+ public ITypeEnvironmentBuilder getDestinationTypenv() {
+ return dstTypenv;
+ }
+
+ public ITypeCheckingRewriter getFormulaRewriter() {
+ return formRewriter;
+ }
+
+ @Override
+ public boolean canPut(GivenType type, Type value) {
+ return canPutInternal(type, value) == null;
+ }
+
@Override
public void put(GivenType type, Type value) {
+ final String errorMessage = canPutInternal(type, value);
+ if (errorMessage != null) {
+ throw new IllegalArgumentException(errorMessage);
+ }
+ addTypeSubstitution(type, value);
+ }
+
+ private String canPutInternal(GivenType type, Type value) {
if (type == null)
throw new NullPointerException("Null given type");
if (value == null)
@@ -94,71 +338,148 @@ public class Specialization extends Substitution implements ISpecialization {
throw new IllegalArgumentException("Wrong factory for value: "
+ value.getFactory() + ", should be " + ff);
}
- final Type oldValue = typeSubst.put(type, value);
+ if (!verifySrcTypenv(type.toExpression())) {
+ return "Identifier " + type
+ + " already entered with a different type";
+ }
+ final String error = isCompatibleFormula(dstTypenv,
+ value.toExpression());
+ if (error != null) {
+ return error;
+ }
+ final Type oldValue = speTypeRewriter.get(type);
if (oldValue != null && !oldValue.equals(value)) {
- typeSubst.put(type, oldValue); // repair
- throw new IllegalArgumentException("Type substitution for " + type
- + " already registered");
+ return "Type substitution for " + type + " already registered";
+ }
+ return null;
+ }
+
+ private void addTypeSubstitution(GivenType type, Type value) {
+ final FreeIdentifier ident = type.toExpression();
+ srcTypenv.add(ident);
+ speTypeRewriter.put(type, value);
+ formRewriter.put(ident, value.toExpression());
+ for (final GivenType given : value.getGivenTypes()) {
+ dstTypenv.addGivenSet(given.getName());
}
- final Substitute subst = makeSubstitute(value.toExpression());
- identSubst.put(type.toExpression(), subst);
}
+ private void maybeAddTypeIdentitySubstitution(GivenType type) {
+ if (!srcTypenv.contains(type.getName())) {
+ addTypeSubstitution(type, type.translate(ff));
+ }
+ }
+
@Override
public Type get(GivenType key) {
- return typeSubst.get(key);
+ return speTypeRewriter.get(key);
}
- public Type getOrSetDefault(GivenType key) {
- Type value = get(key);
- if (value == null) {
- value = key.translate(ff);
- put(key, value);
- }
- return value;
+ @Override
+ public boolean canPut(FreeIdentifier ident, Expression value) {
+ return canPutInternal(ident, value) == null;
}
@Override
public void put(FreeIdentifier ident, Expression value) {
+ final String errorMessage = canPutInternal(ident, value);
+ if (errorMessage != null) {
+ throw new IllegalArgumentException(errorMessage);
+ }
+ addIdentSubstitution(ident, value);
+ }
+
+ private String canPutInternal(FreeIdentifier ident, Expression value) {
if (ident == null)
throw new NullPointerException("Null identifier");
if (!ident.isTypeChecked())
throw new IllegalArgumentException("Untyped identifier");
if (value == null)
throw new NullPointerException("Null value");
+ if (!value.isTypeChecked())
+ throw new IllegalArgumentException("Untyped value");
if (ff != value.getFactory()) {
throw new IllegalArgumentException("Wrong factory for value: "
+ value.getFactory() + ", should be " + ff);
}
- if (!value.isTypeChecked())
- throw new IllegalArgumentException("Untyped value");
- verify(ident, value);
- final Substitute subst = makeSubstitute(value);
- final Substitute oldSubst = identSubst.put(ident, subst);
- if (oldSubst != null && !oldSubst.equals(subst)) {
- identSubst.put(ident, oldSubst); // repair
- throw new IllegalArgumentException("Identifier substitution for "
- + ident + " already registered");
+ if (!verifySrcTypenv(ident)) {
+ return "Incompatible types for " + ident;
}
+ if (!verify(ident, value)) {
+ return "Incompatible types for " + ident;
+ }
+ final String error = isCompatibleFormula(dstTypenv, value);
+ if (error != null) {
+ return error;
+ }
+ final Expression oldValue = formRewriter.get(ident);
+ if (oldValue != null && !oldValue.equals(value)) {
+ return "Identifier substitution for " + ident
+ + " already registered";
+ }
+ return null;
}
/*
- * Checks that a new substitution is compatible. We also save the given sets
- * that are now frozen and must not change afterwards.
+ * Tells whether the new substitution is compatible with existing ones. If
+ * commit is true, we also save the given sets that are now frozen and must
+ * not change afterwards.
*/
- private void verify(FreeIdentifier ident, Expression value) {
+ private boolean verify(FreeIdentifier ident, Expression value) {
final Type identType = ident.getType();
- final Type newType = identType.specialize(this);
- if (!value.getType().equals(newType)) {
- throw new IllegalArgumentException("Incompatible types for "
- + ident);
+ final Type newType = speTypeRewriter.rewrite(identType);
+ return value.getType().equals(newType);
+ }
+
+ private void addIdentSubstitution(FreeIdentifier ident, Expression value) {
+ for (final GivenType given : ident.getGivenTypes()) {
+ maybeAddTypeIdentitySubstitution(given);
}
+ srcTypenv.add(ident);
+ formRewriter.put(ident, value);
+ dstTypenv.addAll(value.getFreeIdentifiers());
}
+ private void maybeAddIdentIdentitySubstitution(FreeIdentifier ident) {
+ if (!srcTypenv.contains(ident.getName())) {
+ addIdentSubstitution(ident, formRewriter.rewrite(ident));
+ }
+ }
+
public Type specialize(Type type) {
+ prepare(type);
return speTypeRewriter.rewrite(type);
}
+ /*
+ * Prepares the specialization of a type.
+ *
+ * We check here that the specialization will not encounter a typing error
+ * and perform the side-effects for types not yet registered with this
+ * specialization.
+ */
+ public void prepare(Type type) {
+ final Set<GivenType> givens = type.getGivenTypes();
+
+ // Ensure that type environments are compatible
+ for (final GivenType given : givens) {
+ if (!verifySrcTypenv(given.toExpression())) {
+ throw new IllegalArgumentException("Type " + given
+ + " already entered with a different type");
+ }
+ if (speTypeRewriter.get(given) == null
+ && !isCompatible(dstTypenv, given)) {
+ throw new IllegalArgumentException("Destination name " + given
+ + " already used with a different type");
+ }
+ }
+
+ // Then insert the identity substitutions not already there
+ for (final GivenType given : givens) {
+ maybeAddTypeIdentitySubstitution(given);
+ }
+ }
+
/*
* Specializing a type environment consists in, starting from an empty type
* environment, adding all given sets and free identifiers that occur in the
@@ -166,12 +487,13 @@ public class Specialization extends Substitution implements ISpecialization {
* environment.
*/
public ITypeEnvironmentBuilder specialize(TypeEnvironment typenv) {
+ prepare(typenv);
final ITypeEnvironmentBuilder result = ff.makeTypeEnvironment();
final IIterator iter = typenv.getIterator();
while (iter.hasNext()) {
iter.advance();
final FreeIdentifier ident = iter.asFreeIdentifier();
- final Expression expr = this.getOrSetDefault(ident);
+ final Expression expr = formRewriter.rewrite(ident);
for (final FreeIdentifier free : expr.getFreeIdentifiers()) {
result.add(free);
}
@@ -179,124 +501,177 @@ public class Specialization extends Substitution implements ISpecialization {
return result;
}
- @Override
- public Expression get(FreeIdentifier ident) {
- final Substitute subst = identSubst.get(ident);
- return subst == null ? null : subst.getSubstitute(ident, 0);
- }
-
- private Expression getOrSetDefault(FreeIdentifier ident) {
- final Substitute subst = identSubst.get(ident);
- if (subst != null) {
- return subst.getSubstitute(ident, getBindingDepth());
- }
- final Type type = ident.getType();
- final Type newType = type.specialize(this);
- final Expression result;
- if (newType == type) {
- result = super.rewrite(ident);
- } else {
- result = ff.makeFreeIdentifier(ident.getName(),
- ident.getSourceLocation(), newType);
+ /*
+ * Prepares the specialization of a type environment.
+ *
+ * We check here that the specialization will not encounter a typing error
+ * and perform the side-effects for identifiers not yet registered with this
+ * specialization.
+ */
+ public void prepare(TypeEnvironment typenv) {
+ // Ensure that type environments are compatible
+ final IIterator iter = typenv.getIterator();
+ while (iter.hasNext()) {
+ iter.advance();
+ final FreeIdentifier ident = iter.asFreeIdentifier();
+ if (!verifySrcTypenv(ident)) {
+ throw new IllegalArgumentException("Identifier " + ident
+ + " already entered with a different type");
+ }
+ verifyDstTypenv(ident);
}
- identSubst.put(ident, makeSubstitute(result));
- return result;
- }
- @Override
- public Expression rewrite(FreeIdentifier identifier) {
- final Expression newIdent = getOrSetDefault(identifier);
- if (newIdent.equals(identifier)) {
- return super.rewrite(identifier);
+ // Then insert the identity substitutions not yet there
+ final IIterator iter2 = typenv.getIterator();
+ while (iter2.hasNext()) {
+ iter2.advance();
+ final FreeIdentifier ident = iter2.asFreeIdentifier();
+ maybeAddIdentIdentitySubstitution(ident);
}
- return newIdent;
}
- @Override
- public BoundIdentDecl rewrite(BoundIdentDecl decl) {
- final Type type = decl.getType();
- final Type newType = type.specialize(this);
- if (newType == type) {
- return super.rewrite(decl);
+ /*
+ * Prepares the specialization of an arbitrary formula. The specialization
+ * itself cannot be performed here, as it must use the non-API rewrite
+ * method of class Formula.
+ *
+ * We check here that the specialization will not encounter a typing error
+ * and perform the side-effects for identifiers and predicate variables not
+ * yet registered with this specialization.
+ */
+ public <T extends Formula<T>> void prepare(Formula<T> formula) {
+ final FreeIdentifier[] localEnv = formula.getFreeIdentifiers();
+
+ // Ensure that type environments are compatible
+ for (final FreeIdentifier ident : localEnv) {
+ if (!verifySrcTypenv(ident)) {
+ throw new IllegalArgumentException("Identifier " + ident
+ + " already entered with a different type");
+ }
+ verifyDstTypenv(ident);
+ }
+
+ // Then protect the identity substitutions not already there
+ for (final FreeIdentifier ident : localEnv) {
+ maybeAddIdentIdentitySubstitution(ident);
+ }
+
+ // Also add identity substitutions for the predicate variables that do
+ // not have a substitution yet.
+ final PredicateVariable[] predVars = formula.getPredicateVariables();
+ for (final PredicateVariable predVar : predVars) {
+ if (formRewriter.get(predVar) == null) {
+ formRewriter.put(predVar, predVar.translate(ff));
+ }
}
- final String name = decl.getName();
- final SourceLocation sloc = decl.getSourceLocation();
- return ff.makeBoundIdentDecl(name, sloc, newType);
}
- @Override
- public Expression rewrite(BoundIdentifier identifier) {
- final Type type = identifier.getType();
- final Type newType = type.specialize(this);
- if (newType == type) {
- return super.rewrite(identifier);
+ /*
+ * Ensures that the specialization of srcIdent will be compatible with the
+ * destination environment.
+ */
+ private void verifyDstTypenv(FreeIdentifier srcIdent) {
+ if (formRewriter.get(srcIdent) != null) {
+ return;
+ }
+ final Expression dstExpr = formRewriter.rewrite(srcIdent);
+ final FreeIdentifier dstIdent = (FreeIdentifier) dstExpr;
+ if (!isCompatible(dstTypenv, dstIdent)) {
+ throw new IllegalArgumentException("Destination name " + dstIdent
+ + " already used with a different type");
}
- return ff.makeBoundIdentifier(identifier.getBoundIndex(),
- identifier.getSourceLocation(), newType);
}
@Override
- public Expression rewrite(AtomicExpression expression) {
- final Type type = expression.getType();
- final Type newType = type.specialize(this);
- if (newType == type) {
- return super.rewrite(expression);
- }
- final SourceLocation loc = expression.getSourceLocation();
- return ff.makeAtomicExpression(expression.getTag(), loc, newType);
+ public Expression get(FreeIdentifier ident) {
+ return formRewriter.get(ident);
}
+ // For debugging purposes
@Override
- public Expression rewrite(ExtendedExpression expr, boolean changed,
- Expression[] newChildExprs, Predicate[] newChildPreds) {
- final Type type = expr.getType();
- final Type newType = type.specialize(this);
- if (!changed && newType == type) {
- return super.rewrite(expr, changed, newChildExprs, newChildPreds);
- }
- final IExpressionExtension extension = expr.getExtension();
- final SourceLocation loc = expr.getSourceLocation();
- return ff.makeExtendedExpression(extension, newChildExprs,
- newChildPreds, loc, newType);
+ public String toString() {
+ final StringBuilder sb = new StringBuilder();
+ speTypeRewriter.toString(sb);
+ sb.append(" + ");
+ formRewriter.toString(sb);
+ return sb.toString();
}
/*
- * For a set extension, the only special case is that of an empty extension,
- * where we have to specialize the type.
+ * Tells whether the given identifier is compatible with the source type
+ * environment.
*/
- @Override
- public Expression rewrite(SetExtension src, SetExtension expr) {
- if (expr.getChildCount() != 0) {
- return expr;
+ private boolean verifySrcTypenv(FreeIdentifier ident) {
+ if (srcTypenv == null) {
+ srcTypenv = ident.getFactory().makeTypeEnvironment();
}
- final Type type = expr.getType();
- final Type newType = type.specialize(this);
- if (newType == type) {
- return super.rewrite(src, expr);
+ return isCompatible(srcTypenv, ident);
+ }
+
+ private <T extends Formula<T>> String isCompatibleFormula(
+ ITypeEnvironment typenv, T value) {
+ for (final FreeIdentifier ident : value.getFreeIdentifiers()) {
+ if (!isCompatible(typenv, ident)) {
+ return "Destination name " + ident
+ + " already used with a different type";
+ }
}
- return ff.makeEmptySetExtension(newType, expr.getSourceLocation());
+ return null;
+ }
+
+ private boolean isCompatible(ITypeEnvironment typenv,
+ FreeIdentifier ident) {
+ final Type knownType = typenv.getType(ident.getName());
+ return knownType == null || knownType.equals(ident.getType());
+ }
+
+ private boolean isCompatible(ITypeEnvironment typenv, GivenType type) {
+ final Type knownType = typenv.getType(type.getName());
+ return knownType == null || type.equals(knownType.getBaseType());
}
- // For debugging purposes
@Override
- public String toString() {
- final StringBuilder sb = new StringBuilder();
- String sep = "";
- for (Entry<GivenType, Type> entry : typeSubst.entrySet()) {
- sb.append(sep);
- sep = " || ";
- sb.append(entry.getKey());
- sb.append("=");
- sb.append(entry.getValue());
- }
- for (Entry<FreeIdentifier, Substitute> entry : identSubst.entrySet()) {
- sb.append(sep);
- sep = " || ";
- sb.append(entry.getKey());
- sb.append("=");
- sb.append(entry.getValue());
+ public boolean put(PredicateVariable predVar, Predicate value) {
+ if (predVar == null)
+ throw new NullPointerException("Null predicate variable");
+ if (value == null)
+ throw new NullPointerException("Null value");
+ if (!value.isTypeChecked())
+ throw new IllegalArgumentException("Untyped value");
+ if (ff != value.getFactory()) {
+ throw new IllegalArgumentException("Wrong factory for value: "
+ + value.getFactory() + ", should be " + ff);
}
- return sb.toString();
+
+ if (isCompatibleFormula(dstTypenv, value) != null) {
+ return false;
+ }
+
+ final boolean result = formRewriter.put(predVar, value);
+ if (result) {
+ dstTypenv.addAll(value.getFreeIdentifiers());
+ }
+ return result;
+ }
+
+ @Override
+ public Predicate get(PredicateVariable predVar) {
+ return formRewriter.get(predVar);
+ }
+
+ @Override
+ public GivenType[] getTypes() {
+ return speTypeRewriter.getTypes();
+ }
+
+ @Override
+ public FreeIdentifier[] getFreeIdentifiers() {
+ return formRewriter.getFreeIdentifiers();
+ }
+
+ @Override
+ public PredicateVariable[] getPredicateVariables() {
+ return formRewriter.getPredicateVariables();
}
}
diff --git a/src/org/eventb/internal/core/ast/Substitute.java b/src/org/eventb/internal/core/ast/Substitute.java
index f8cd659..ddc8cdf 100644
--- a/src/org/eventb/internal/core/ast/Substitute.java
+++ b/src/org/eventb/internal/core/ast/Substitute.java
@@ -1,5 +1,5 @@
/*******************************************************************************
- * Copyright (c) 2006, 2014 ETH Zurich and others.
+ * Copyright (c) 2006, 2016 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
@@ -7,41 +7,44 @@
*
* Contributors:
* ETH Zurich - initial API and implementation
+ * Systerel - Make this class generic
*******************************************************************************/
package org.eventb.internal.core.ast;
import org.eventb.core.ast.Expression;
+import org.eventb.core.ast.Formula;
/**
- * Common abstraction for a substitute expression used in a substitution.
+ * Common abstraction for a substitute formula used in a substitution.
* <p>
* This class is not public API. Don't use it.
* </p>
*
* @author Laurent Voisin
*/
-public abstract class Substitute {
+public abstract class Substitute<T extends Formula<T>> {
/**
- * Simple substitute where the expression doesn't contain any externally
+ * Simple substitute where the formula doesn't contain any externally
* bound identifier.
*/
- private static class SimpleSubstitute extends Substitute {
+ private static class SimpleSubstitute<T extends Formula<T>>
+ extends Substitute<T> {
- Expression expr;
+ T formula;
- public SimpleSubstitute(Expression expr) {
- this.expr = expr;
+ public SimpleSubstitute(T formula) {
+ this.formula = formula;
}
@Override
- public Expression getSubstitute(Expression original, int nbOfInternallyBound) {
- return expr;
+ public T getSubstitute(T original, int nbOfInternallyBound) {
+ return formula;
}
@Override
public int hashCode() {
- return expr.hashCode();
+ return formula.hashCode();
}
@Override
@@ -52,27 +55,29 @@ public abstract class Substitute {
if (obj == null || this.getClass() != obj.getClass()) {
return false;
}
- final SimpleSubstitute other = (SimpleSubstitute) obj;
- return expr.equals(other.expr);
+ @SuppressWarnings("unchecked")
+ final SimpleSubstitute<T> other = (SimpleSubstitute<T>) obj;
+ return formula.equals(other.formula);
}
@Override
public String toString() {
- return expr.toString();
+ return formula.toString();
}
}
/**
- * Susbtitute where the expression consists of a bound identifier.
+ * Susbtitute where the formula consists of a bound identifier.
* <p>
* This means that we must renumber the index of this identifier, taking
* into account the offset.
* </p>
* This class corresponds to an optimized simple version of
- * {@link ComplexSubstitute}.
+ * {@link org.eventb.internal.core.ast.Substitute.ComplexSubstitute
+ * ComplexSubstitute}.
*/
- private static class BoundIdentSubstitute extends Substitute {
+ private static class BoundIdentSubstitute extends Substitute<Expression> {
/**
* Index of the bound variable, before correction.
@@ -115,7 +120,7 @@ public abstract class Substitute {
}
/**
- * Complex substitute where the expression does contain some externally
+ * Complex substitute where the formula does contain some externally
* bound identifiers.
* <p>
* This means that we must renumber the index of these identifiers, taking
@@ -123,26 +128,27 @@ public abstract class Substitute {
* small cache.
* </p>
*/
- private static class ComplexSubstitute extends Substitute {
+ private static class ComplexSubstitute<T extends Formula<T>>
+ extends Substitute<T> {
/**
- * Cache of substitute expressions, indexed by the offset applied to
+ * Cache of substitute formulas, indexed by the offset applied to
* them. For instance, the first element of the list contains the
- * original expression untouched.
+ * original formula untouched.
*/
- private Cache<Expression> cache;
+ private Cache<T> cache;
- public ComplexSubstitute(Expression expr) {
- this.cache = new Cache<Expression>();
- this.cache.set(0, expr);
+ public ComplexSubstitute(T formula) {
+ this.cache = new Cache<T>();
+ this.cache.set(0, formula);
}
@Override
- public Expression getSubstitute(Expression original, int nbOfInternallyBound) {
- Expression result = cache.get(nbOfInternallyBound);
+ public T getSubstitute(T original, int nbOfInternallyBound) {
+ T result = cache.get(nbOfInternallyBound);
if (result == null) {
- Expression expr = cache.get(0);
- result = expr.shiftBoundIdentifiers(nbOfInternallyBound);
+ T formula = cache.get(0);
+ result = formula.shiftBoundIdentifiers(nbOfInternallyBound);
cache.set(nbOfInternallyBound, result);
}
return result;
@@ -161,11 +167,13 @@ public abstract class Substitute {
if (obj == null || this.getClass() != obj.getClass()) {
return false;
}
- return equalExpressions((ComplexSubstitute) obj);
+ @SuppressWarnings("unchecked")
+ final ComplexSubstitute<T> other = (ComplexSubstitute<T>) obj;
+ return equalFormulas(other);
}
// Test extracted to a method for subclass comparison
- protected boolean equalExpressions(ComplexSubstitute other) {
+ protected boolean equalFormulas(ComplexSubstitute<T> other) {
return cache.get(0).equals(other.cache.get(0));
}
@@ -177,20 +185,21 @@ public abstract class Substitute {
}
/**
- * Complex substitute where the expression does contain some externally
+ * Complex substitute where the formula does contain some externally
* bound identifiers, and where an additional offset needs to be applied.
*/
- private static class ComplexSubstituteWithOffset extends ComplexSubstitute {
+ private static class ComplexSubstituteWithOffset<T extends Formula<T>>
+ extends ComplexSubstitute<T> {
private final int offset;
- public ComplexSubstituteWithOffset(Expression expr, int offset) {
- super(expr);
+ public ComplexSubstituteWithOffset(T formula, int offset) {
+ super(formula);
this.offset = offset;
}
@Override
- public Expression getSubstitute(Expression original, int nbOfInternallyBound) {
+ public T getSubstitute(T original, int nbOfInternallyBound) {
return super.getSubstitute(original, nbOfInternallyBound + offset);
}
@@ -207,8 +216,9 @@ public abstract class Substitute {
if (obj == null || this.getClass() != obj.getClass()) {
return false;
}
- final ComplexSubstituteWithOffset other = (ComplexSubstituteWithOffset) obj;
- return equalExpressions(other) && offset == other.offset;
+ @SuppressWarnings("unchecked")
+ final ComplexSubstituteWithOffset<T> other = (ComplexSubstituteWithOffset<T>) obj;
+ return equalFormulas(other) && offset == other.offset;
}
@Override
@@ -219,31 +229,32 @@ public abstract class Substitute {
}
/**
- * Factory method to create a substitute with an arbitrary expression.
+ * Factory method to create a substitute with an arbitrary formula.
*
- * @param expr
- * initial substitute expression
- * @return the substitute object for that expression
+ * @param formula
+ * initial substitute formula
+ * @return the substitute object for that formula
*/
- public static Substitute makeSubstitute(Expression expr) {
- if (expr.isWellFormed()) {
- return new SimpleSubstitute(expr);
+ public static <T extends Formula<T>> Substitute<T> makeSubstitute(T formula) {
+ if (formula.isWellFormed()) {
+ return new SimpleSubstitute<T>(formula);
}
- return new ComplexSubstitute(expr);
+ return new ComplexSubstitute<T>(formula);
}
/**
- * Factory method to create a substitute with an arbitrary expression and
+ * Factory method to create a substitute with an arbitrary formula and
* applying a constant offset to its bound identifiers.
*
- * @param expr
- * initial substitute expression
+ * @param formula
+ * initial substitute formula
* @param offset
* offset to systematically apply
- * @return the substitute object for that expression
+ * @return the substitute object for that formula
*/
- public static Substitute makeSubstitute(Expression expr, int offset) {
- return new ComplexSubstituteWithOffset(expr, offset);
+ public static <T extends Formula<T>> Substitute<T> makeSubstitute(T formula,
+ int offset) {
+ return new ComplexSubstituteWithOffset<T>(formula, offset);
}
/**
@@ -253,23 +264,23 @@ public abstract class Substitute {
* initial index of the bound identifier
* @return the substitute object for that identifier
*/
- public static Substitute makeSubstitute(int index) {
+ public static Substitute<Expression> makeSubstitute(int index) {
return new BoundIdentSubstitute(index);
}
/**
- * Returns the substitute expression where bound identifier occurrences have
+ * Returns the substitute formula where bound identifier occurrences have
* been renumbered using the given offset.
*
* @param original
- * original expression that gets substituted
+ * original formula that gets substituted
* @param nbOfInternallyBound
* offset to use, that is the number of identifiers bound between
- * the point where the substitute expression was given and the
+ * the point where the substitute formula was given and the
* place where it is used
*
- * @return the actual substitute expression to use
+ * @return the actual substitute formula to use
*/
- public abstract Expression getSubstitute(Expression original, int nbOfInternallyBound);
+ public abstract T getSubstitute(T original, int nbOfInternallyBound);
}
diff --git a/src/org/eventb/internal/core/ast/Substitution.java b/src/org/eventb/internal/core/ast/Substitution.java
index 5a67f97..3af6df0 100644
--- a/src/org/eventb/internal/core/ast/Substitution.java
+++ b/src/org/eventb/internal/core/ast/Substitution.java
@@ -1,5 +1,5 @@
/*******************************************************************************
- * Copyright (c) 2006, 2012 ETH Zurich and others.
+ * Copyright (c) 2006, 2016 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
@@ -23,4 +23,8 @@ public abstract class Substitution extends DefaultTypeCheckingRewriter {
super(ff);
}
+ public Substitution(TypeRewriter typeRewriter) {
+ super(typeRewriter);
+ }
+
}
diff --git a/src/org/eventb/internal/core/ast/TypeRewriter.java b/src/org/eventb/internal/core/ast/TypeRewriter.java
index b08b07b..59e7ef6 100644
--- a/src/org/eventb/internal/core/ast/TypeRewriter.java
+++ b/src/org/eventb/internal/core/ast/TypeRewriter.java
@@ -1,5 +1,5 @@
/*******************************************************************************
- * Copyright (c) 2012, 2013 Systerel and others.
+ * Copyright (c) 2012, 2016 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
@@ -38,7 +38,7 @@ import org.eventb.core.ast.extension.IExpressionExtension;
public class TypeRewriter implements ITypeVisitor {
// Formula factory to use for building the rewritten types
- private final FormulaFactory ff;
+ protected final FormulaFactory ff;
// Result of the last call to visit()
protected Type result;
@@ -47,6 +47,10 @@ public class TypeRewriter implements ITypeVisitor {
this.ff = ff;
}
+ public FormulaFactory getFactory() {
+ return ff;
+ }
+
public Type rewrite(Type type) {
if (type == null) {
return null;
diff --git a/src/org/eventb/internal/core/ast/datatype/Datatype.java b/src/org/eventb/internal/core/ast/datatype/Datatype.java
index 26572ed..8d742b2 100644
--- a/src/org/eventb/internal/core/ast/datatype/Datatype.java
+++ b/src/org/eventb/internal/core/ast/datatype/Datatype.java
@@ -79,7 +79,7 @@ public class Datatype implements IDatatype {
// Cache of the extensions provided by this datatype
private final Set<IFormulaExtension> extensions;
-
+
private final Object origin;
private Datatype(DatatypeBuilder dtBuilder) {
@@ -87,7 +87,7 @@ public class Datatype implements IDatatype {
origin = dtBuilder.getOrigin();
typeCons = new TypeConstructorExtension(this, dtBuilder);
constructors = new LinkedHashMap<String, ConstructorExtension>();
- destructors = new HashMap<String, DestructorExtension>();
+ destructors = new HashMap<String, DestructorExtension>();
final List<ConstructorBuilder> dtConstrs = dtBuilder.getConstructors();
for (final ConstructorBuilder dtCons : dtConstrs) {
final ConstructorExtension constructor = dtCons.makeExtension(this);
@@ -161,17 +161,24 @@ public class Datatype implements IDatatype {
return unmodifiableSet(extensions);
}
+ /**
+ * The hash code is computed from the datatype's type constructors,
+ * constructor extensions, and the origin.
+ */
@Override
public int hashCode() {
final int prime = 31;
int result = 1;
- result = prime * result + typeCons.hashCode();
+ result = prime * result + typeCons.hashCode();
result = prime * result + constructors.hashCode();
- result = prime * result + ((origin == null) ? 0 : origin.hashCode());
+ result = prime * result + (origin == null ? 0 : origin.hashCode());
return result;
}
-
+ /**
+ * The datatypes are the same if they have the same name and "similar" type
+ * constructors, constructor extensions, and origins.
+ */
@Override
public boolean equals(Object obj) {
if (this == obj) {
@@ -183,15 +190,23 @@ public class Datatype implements IDatatype {
final Datatype other = (Datatype) obj;
return this.typeCons.isSimilarTo(other.typeCons)
&& areSimilarConstructors(this.constructors.values(),
- other.constructors.values())
- && areEqualOrigins(this.origin, other.origin);
- }
-
- private static boolean areEqualOrigins(Object origin1, Object origin2) {
- if (origin1 == null) {
- return origin2 == null;
- }
- return origin1.equals(origin2);
+ other.constructors.values()) &&
+ areSimilarOrigins(this.getOrigin(), other.getOrigin());
+ }
+
+ /**
+ * Utility method to compare the datatype origin.
+ *
+ * @param mine
+ * mine origin
+ * @param other
+ * the other's origin
+ * @return <code>true</code> if the two origin are equal.
+ */
+ private boolean areSimilarOrigins(Object mine, Object other) {
+ if (mine == null)
+ return (other == null);
+ return mine.equals(other);
}
private static boolean areSimilarConstructors(
diff --git a/src/org/eventb/internal/core/ast/datatype/DatatypeRewriter.java b/src/org/eventb/internal/core/ast/datatype/DatatypeRewriter.java
index bfd8e8d..58ed267 100644
--- a/src/org/eventb/internal/core/ast/datatype/DatatypeRewriter.java
+++ b/src/org/eventb/internal/core/ast/datatype/DatatypeRewriter.java
@@ -1,5 +1,5 @@
/*******************************************************************************
- * Copyright (c) 2013 Systerel and others.
+ * Copyright (c) 2013, 2016 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
@@ -10,16 +10,9 @@
*******************************************************************************/
package org.eventb.internal.core.ast.datatype;
-import org.eventb.core.ast.AtomicExpression;
-import org.eventb.core.ast.BoundIdentDecl;
-import org.eventb.core.ast.BoundIdentifier;
import org.eventb.core.ast.Expression;
import org.eventb.core.ast.ExtendedExpression;
-import org.eventb.core.ast.FreeIdentifier;
import org.eventb.core.ast.Predicate;
-import org.eventb.core.ast.SetExtension;
-import org.eventb.core.ast.SourceLocation;
-import org.eventb.core.ast.Type;
import org.eventb.core.ast.datatype.IDatatype;
import org.eventb.core.ast.extension.IExpressionExtension;
import org.eventb.internal.core.ast.DefaultTypeCheckingRewriter;
@@ -40,71 +33,10 @@ public class DatatypeRewriter extends DefaultTypeCheckingRewriter {
private final DatatypeTranslation translation;
public DatatypeRewriter(DatatypeTranslation translation) {
- super(translation.getTargetFormulaFactory());
+ super(translation.getTypeRewriter());
this.translation = translation;
}
- @Override
- public BoundIdentDecl rewrite(BoundIdentDecl decl) {
- final Type type = decl.getType();
- final Type newType = translation.translate(type);
- if (newType == type) {
- return super.rewrite(decl);
- }
- final String name = decl.getName();
- final SourceLocation sLoc = decl.getSourceLocation();
- return ff.makeBoundIdentDecl(name, sLoc, newType);
- }
-
- @Override
- public Expression rewrite(AtomicExpression expression) {
- final Type type = expression.getType();
- final Type newType = translation.translate(type);
- if (newType == type) {
- return super.rewrite(expression);
- }
- final SourceLocation sLoc = expression.getSourceLocation();
- return ff.makeAtomicExpression(expression.getTag(), sLoc, newType);
- }
-
- @Override
- public Expression rewrite(BoundIdentifier identifier) {
- final Type type = identifier.getType();
- final Type newType = translation.translate(type);
- if (newType == type) {
- return super.rewrite(identifier);
- }
- final SourceLocation sLoc = identifier.getSourceLocation();
- final int index = identifier.getBoundIndex();
- return ff.makeBoundIdentifier(index, sLoc, newType);
- }
-
- @Override
- public Expression rewrite(FreeIdentifier ident) {
- final Type type = ident.getType();
- final Type newType = translation.translate(type);
- if (newType == type) {
- return super.rewrite(ident);
- }
- final SourceLocation sLoc = ident.getSourceLocation();
- final String name = ident.getName();
- return ff.makeFreeIdentifier(name, sLoc, newType);
- }
-
- @Override
- public Expression rewrite(SetExtension src, SetExtension expr) {
- if (expr.getChildCount() != 0) {
- return expr;
- }
- final Type type = expr.getType();
- final Type newType = translation.translate(type);
- if (newType == type) {
- return expr;
- }
- final SourceLocation sLoc = expr.getSourceLocation();
- return ff.makeEmptySetExtension(newType, sLoc);
- }
-
@Override
public Expression rewrite(ExtendedExpression src, boolean changed,
Expression[] newChildExprs, Predicate[] newChildPreds) {
@@ -116,11 +48,8 @@ public class DatatypeRewriter extends DefaultTypeCheckingRewriter {
return translation.translate(src, newChildExprs);
} else {
// Not a datatype operator, just translate the type
- final SourceLocation sLoc = src.getSourceLocation();
- final Type type = translation.translate(src.getType());
- return ff.makeExtendedExpression(extension, newChildExprs,
- newChildPreds, sLoc, type);
+ return super.rewrite(src, changed, newChildExprs, newChildPreds);
}
}
-}
\ No newline at end of file
+}
diff --git a/src/org/eventb/internal/core/ast/datatype/DatatypeTranslation.java b/src/org/eventb/internal/core/ast/datatype/DatatypeTranslation.java
index 889fa88..55f015f 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, 2014 Systerel and others.
+ * Copyright (c) 2013, 2016 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
@@ -117,6 +117,10 @@ public class DatatypeTranslation extends AbstractTranslation implements
return formulaRewriter;
}
+ public TypeRewriter getTypeRewriter() {
+ return typeRewriter;
+ }
+
public final GivenType solveGivenType(String typeSymbol) {
final String solvedTypeName = nameSolver.solveAndAdd(typeSymbol);
return targetFactory.makeGivenType(solvedTypeName);
@@ -172,4 +176,4 @@ public class DatatypeTranslation extends AbstractTranslation implements
return "Datatype Translation for factory: " + sourceFactory
+ " in type environment: " + srcTypenv;
}
-}
\ No newline at end of file
+}
diff --git a/src/org/eventb/internal/core/ast/extension/ExtensionSignature.java b/src/org/eventb/internal/core/ast/extension/ExtensionSignature.java
index 172179f..a62e88f 100644
--- a/src/org/eventb/internal/core/ast/extension/ExtensionSignature.java
+++ b/src/org/eventb/internal/core/ast/extension/ExtensionSignature.java
@@ -1,5 +1,5 @@
/*******************************************************************************
- * Copyright (c) 2014 Systerel and others.
+ * Copyright (c) 2014, 2016 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
@@ -17,7 +17,9 @@ import org.eventb.core.ast.ExtendedExpression;
import org.eventb.core.ast.ExtendedPredicate;
import org.eventb.core.ast.Formula;
import org.eventb.core.ast.FormulaFactory;
+import org.eventb.core.ast.ParametricType;
import org.eventb.core.ast.Type;
+import org.eventb.core.ast.extension.IExpressionExtension;
import org.eventb.core.ast.extension.IExtendedFormula;
import org.eventb.core.ast.extension.IFormulaExtension;
@@ -30,6 +32,17 @@ import org.eventb.core.ast.extension.IFormulaExtension;
*/
public abstract class ExtensionSignature {
+ /**
+ * Returns the signature of a parametric type occurrence.
+ *
+ * @param src
+ * some parametric type
+ * @return the signature of the parametric type
+ */
+ public static ExpressionExtSignature getSignature(ParametricType src) {
+ return new ExpressionExtSignature(src);
+ }
+
/**
* Returns the signature of an expression extension occurrence.
*
@@ -62,13 +75,26 @@ public abstract class ExtensionSignature {
return childTypes;
}
+ private static Type[] makePowerSetTypes(Type[] src) {
+ if (src.length == 0) {
+ return src;
+ }
+ final FormulaFactory fac = src[0].getFactory();
+ final Type[] result = new Type[src.length];
+ for (int i = 0; i < src.length; i++) {
+ result[i] = fac.makePowerSetType(src[i]);
+ }
+ return result;
+ }
+
private static final int PRIME = 31;
- // The formula factory for this signature
+ // The formula factory for this signature, i.e., the factory containing the
+ // extension.
protected final FormulaFactory factory;
// The extension definition corresponding to this signature
- private final IFormulaExtension extension;
+ protected final IFormulaExtension extension;
// Number of child predicates
private final int numberOfPredicates;
@@ -83,6 +109,13 @@ public abstract class ExtensionSignature {
this.childTypes = getChildTypes(src);
}
+ protected ExtensionSignature(ParametricType src) {
+ this.factory = src.getFactory();
+ this.extension = src.getExprExtension();
+ this.numberOfPredicates = 0;
+ this.childTypes = makePowerSetTypes(src.getTypeParameters());
+ }
+
// For testing purposes
protected ExtensionSignature(FormulaFactory factory,
IFormulaExtension extension, int numberOfPredicates,
@@ -94,12 +127,30 @@ public abstract class ExtensionSignature {
}
/**
- * Returns the formula extension definition associated to this signature
+ * Returns the symbol associated to this signature. This symbol might not be
+ * a valid identifier.
*
- * @return the IFormulaExtension associated to this signature
+ * @return the symbol associated to this signature
*/
- public IFormulaExtension getExtension() {
- return extension;
+ public String getSymbol() {
+ return extension.getSyntaxSymbol();
+ }
+
+ /**
+ * Returns whether the extension with this signature is a type constructor.
+ *
+ * @return whether this signature corresponds to a type constructor
+ */
+ public abstract boolean isATypeConstructor();
+
+ /**
+ * Returns whether this signature is atomic, that is denotes an operator
+ * that does not have any child.
+ *
+ * @return whether this signature is atomic
+ */
+ public boolean isAtomic() {
+ return numberOfPredicates == 0 && childTypes.length == 0;
}
/**
@@ -108,7 +159,25 @@ public abstract class ExtensionSignature {
*
* @return the type of a replacement function
*/
- public abstract Type getFunctionalType();
+ public Type getFunctionalType(FunctionalTypeBuilder builder) {
+ return builder.makeFunctionalType(childTypes, numberOfPredicates,
+ getReturnType());
+ }
+
+ /**
+ * Returns the type of a relation that could be used to replace an
+ * occurrence of the extension with this signature. To be used in the
+ * special case of type constructors.
+ *
+ * @return the type of a replacement relation
+ */
+ public Type getRelationalType(FunctionalTypeBuilder builder) {
+ assert isATypeConstructor();
+ return builder.makeRelationalType(childTypes, getReturnType());
+ }
+
+ // What is the range type of the operator ?
+ protected abstract Type getReturnType();
@Override
public int hashCode() {
@@ -133,37 +202,6 @@ public abstract class ExtensionSignature {
&& Arrays.equals(this.childTypes, other.childTypes);
}
- protected Type makeDomainType() {
- Type result = null;
- for (Type childType : childTypes) {
- result = join(result, childType);
- }
- final Type boolType = makeBooleanType();
- for (int i = 0; i < numberOfPredicates; i++) {
- result = join(result, boolType);
- }
- return result;
- }
-
- private Type join(Type left, Type right) {
- if (left == null) {
- return right;
- }
- return factory.makeProductType(left, right);
- }
-
- protected Type makeBooleanType() {
- return factory.makeBooleanType();
- }
-
- protected Type makeRelationalType(Type left, Type right) {
- if (left == null) {
- // Atomic operator
- return right;
- }
- return factory.makeRelationalType(left, right);
- }
-
public static class PredicateExtSignature extends ExtensionSignature {
public PredicateExtSignature(ExtendedPredicate src) {
@@ -178,8 +216,13 @@ public abstract class ExtensionSignature {
}
@Override
- public Type getFunctionalType() {
- return makeRelationalType(makeDomainType(), makeBooleanType());
+ protected Type getReturnType() {
+ return factory.makeBooleanType();
+ }
+
+ @Override
+ public boolean isATypeConstructor() {
+ return false;
}
}
@@ -191,20 +234,31 @@ public abstract class ExtensionSignature {
public ExpressionExtSignature(ExtendedExpression src) {
super(src);
+ if (src.getType() == null) {
+ throw new NullPointerException();
+ }
this.returnType = src.getType();
}
+ public ExpressionExtSignature(ParametricType src) {
+ super(src);
+ this.returnType = factory.makePowerSetType(src);
+ }
+
// For testing purposes
public ExpressionExtSignature(FormulaFactory factory,
IFormulaExtension extension, Type returnType,
int numberOfPredicates, Type[] childTypes) {
super(factory, extension, numberOfPredicates, childTypes);
+ if (returnType == null) {
+ throw new NullPointerException();
+ }
this.returnType = returnType;
}
@Override
- public Type getFunctionalType() {
- return makeRelationalType(makeDomainType(), returnType);
+ protected Type getReturnType() {
+ return returnType;
}
@Override
@@ -223,6 +277,11 @@ public abstract class ExtensionSignature {
return result;
}
+ @Override
+ public boolean isATypeConstructor() {
+ return ((IExpressionExtension) extension).isATypeConstructor();
+ }
+
}
}
diff --git a/src/org/eventb/internal/core/ast/extension/ExtensionTranslation.java b/src/org/eventb/internal/core/ast/extension/ExtensionTranslation.java
index e7ec66b..f7d5e7c 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 Systerel and others.
+ * Copyright (c) 2014, 2016 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
@@ -12,6 +12,7 @@ package org.eventb.internal.core.ast.extension;
import static org.eventb.internal.core.ast.extension.ExtensionSignature.getSignature;
+import java.util.HashSet;
import java.util.LinkedHashSet;
import java.util.Set;
@@ -20,9 +21,12 @@ import org.eventb.core.ast.ExtendedExpression;
import org.eventb.core.ast.ExtendedPredicate;
import org.eventb.core.ast.FormulaFactory;
import org.eventb.core.ast.FreeIdentifier;
+import org.eventb.core.ast.GivenType;
import org.eventb.core.ast.IExtensionTranslation;
import org.eventb.core.ast.ISealedTypeEnvironment;
+import org.eventb.core.ast.ITypeEnvironment.IIterator;
import org.eventb.core.ast.ITypeEnvironmentBuilder;
+import org.eventb.core.ast.ParametricType;
import org.eventb.core.ast.Predicate;
import org.eventb.core.ast.Type;
import org.eventb.core.ast.datatype.IDatatype;
@@ -31,13 +35,17 @@ import org.eventb.internal.core.ast.AbstractTranslation;
import org.eventb.internal.core.ast.DefaultTypeCheckingRewriter;
import org.eventb.internal.core.ast.FreshNameSolver;
import org.eventb.internal.core.ast.ITypeCheckingRewriter;
+import org.eventb.internal.core.ast.TypeRewriter;
import org.eventb.internal.core.ast.datatype.DatatypeTranslation;
import org.eventb.internal.core.ast.extension.ExtensionSignature.ExpressionExtSignature;
import org.eventb.internal.core.ast.extension.ExtensionSignature.PredicateExtSignature;
import org.eventb.internal.core.ast.extension.ExtensionTranslator.ExpressionExtTranslator;
import org.eventb.internal.core.ast.extension.ExtensionTranslator.PredicateExtTranslator;
+import org.eventb.internal.core.ast.extension.ExtensionTranslator.TypeExtTranslator;
import org.eventb.internal.core.ast.extension.TranslatorRegistry.ExprTranslatorRegistry;
import org.eventb.internal.core.ast.extension.TranslatorRegistry.PredTranslatorRegistry;
+import org.eventb.internal.core.ast.extension.TranslatorRegistry.TypeTranslatorRegistry;
+import org.eventb.internal.core.typecheck.TypeEnvironmentBuilder;
/**
* Translation of operator extensions to function applications. We do not
@@ -57,19 +65,29 @@ public class ExtensionTranslation extends AbstractTranslation implements
private final ITypeEnvironmentBuilder trgTypenv;
private final FreshNameSolver nameSolver;
+ private final TypeTranslatorRegistry typeTranslators //
+ = new TypeTranslatorRegistry(this);
private final ExprTranslatorRegistry exprTranslators //
= new ExprTranslatorRegistry(this);
private final PredTranslatorRegistry predTranslators //
= new PredTranslatorRegistry(this);
- private ITypeCheckingRewriter rewriter;
+ private final FunctionalTypeBuilder typeBuilder;
+
+ private final ITypeCheckingRewriter rewriter;
public ExtensionTranslation(ISealedTypeEnvironment srcTypenv) {
super(srcTypenv);
this.trgFactory = computeTargetFactory(srcTypenv.getFormulaFactory());
- this.trgTypenv = srcTypenv.translate(trgFactory).makeBuilder();
- this.nameSolver = new FreshNameSolver(trgTypenv);
- this.rewriter = new ExtensionRewriter(trgFactory, this);
+ final Set<String> usedNames = new HashSet<String>(srcTypenv.getNames());
+ this.nameSolver = new FreshNameSolver(usedNames, trgFactory);
+
+ final TypeRewriter typeRewriter;
+ typeRewriter = new ExtensionTypeRewriter(trgFactory, this);
+ this.typeBuilder = new FunctionalTypeBuilder(typeRewriter);
+ this.rewriter = new ExtensionRewriter(typeRewriter, this);
+ this.trgTypenv = new TypeEnvironmentBuilder(trgFactory);
+ populateTargetTypenv(typeRewriter);
}
private static FormulaFactory computeTargetFactory(FormulaFactory fac) {
@@ -89,6 +107,17 @@ public class ExtensionTranslation extends AbstractTranslation implements
return FormulaFactory.getInstance(keptExtensions);
}
+ private void populateTargetTypenv(TypeRewriter typeRewriter) {
+ final IIterator iter = srcTypenv.getIterator();
+ while (iter.hasNext()) {
+ iter.advance();
+ final String name = iter.getName();
+ final Type srcType = iter.getType();
+ final Type trgType = typeRewriter.rewrite(srcType);
+ trgTypenv.addName(name, trgType);
+ }
+ }
+
public FormulaFactory getTargetFactory() {
return trgFactory;
}
@@ -98,6 +127,12 @@ public class ExtensionTranslation extends AbstractTranslation implements
return trgTypenv.makeSnapshot();
}
+ public Type translate(ParametricType src) {
+ final ExpressionExtSignature signature = getSignature(src);
+ final TypeExtTranslator translator = typeTranslators.get(signature);
+ return translator.translate();
+ }
+
public Expression translate(ExtendedExpression src,
Expression[] newChildExprs, Predicate[] newChildPreds) {
final ExpressionExtSignature signature = getSignature(src);
@@ -114,12 +149,34 @@ public class ExtensionTranslation extends AbstractTranslation implements
return translator.translate(newChildExprs, newChildPreds);
}
- public FreeIdentifier makeFunction(ExtensionSignature signature) {
+ public GivenType makeType(ExtensionSignature signature) {
+ assert signature.isATypeConstructor();
final String baseName = makeBaseName(signature);
- final String name = nameSolver.solve(baseName);
- final Type type = signature.getFunctionalType().translate(trgFactory);
+ final String name = nameSolver.solveAndAdd(baseName);
+ final GivenType trgType = trgFactory.makeGivenType(name);
+ trgTypenv.add(trgType.toExpression());
+ return trgType;
+ }
+
+ public FreeIdentifier makeFunction(ExtensionSignature signature) {
+ String baseName = makeBaseName(signature);
+
+ final Type type;
+ if (signature.isATypeConstructor()) {
+ type = signature.getRelationalType(typeBuilder);
+ if (signature.isAtomic()) {
+ final GivenType givenType = (GivenType) type.getBaseType();
+ return givenType.toExpression();
+ }
+ baseName += "_constr";
+ } else {
+ type = signature.getFunctionalType(typeBuilder);
+ }
+
+ final String name = nameSolver.solveAndAdd(baseName);
final FreeIdentifier ident = trgFactory.makeFreeIdentifier(name, null,
type);
+
trgTypenv.add(ident);
return ident;
}
@@ -130,10 +187,9 @@ public class ExtensionTranslation extends AbstractTranslation implements
* fresh name solver will loop forever.
*/
private String makeBaseName(ExtensionSignature signature) {
- final IFormulaExtension extension = signature.getExtension();
- final String id = extension.getId();
- if (trgFactory.isValidIdentifierName(id)) {
- return id;
+ final String symbol = signature.getSymbol();
+ if (trgFactory.isValidIdentifierName(symbol)) {
+ return symbol;
}
// Use some arbitrary name which can be used for identifiers
return "ext";
@@ -150,17 +206,39 @@ public class ExtensionTranslation extends AbstractTranslation implements
+ srcTypenv.getFormulaFactory() + " in type environment: "
+ srcTypenv;
}
-
- private static class ExtensionRewriter extends DefaultTypeCheckingRewriter {
+
+ private static class ExtensionTypeRewriter extends TypeRewriter {
private ExtensionTranslation translation;
- public ExtensionRewriter(FormulaFactory targetFactory,
+ public ExtensionTypeRewriter(FormulaFactory targetFactory,
ExtensionTranslation translation) {
super(targetFactory);
this.translation = translation;
}
+ @Override
+ public void visit(ParametricType type) {
+ if (type.getExprExtension().getOrigin() instanceof IDatatype) {
+ super.visit(type);
+ return;
+ }
+
+ result = translation.translate(type);
+ }
+
+ }
+
+ private static class ExtensionRewriter extends DefaultTypeCheckingRewriter {
+
+ private ExtensionTranslation translation;
+
+ public ExtensionRewriter(TypeRewriter typeRewriter,
+ ExtensionTranslation translation) {
+ super(typeRewriter);
+ this.translation = translation;
+ }
+
@Override
public Expression rewrite(ExtendedExpression src, boolean changed,
Expression[] newChildExprs, Predicate[] newChildPreds) {
diff --git a/src/org/eventb/internal/core/ast/extension/ExtensionTranslator.java b/src/org/eventb/internal/core/ast/extension/ExtensionTranslator.java
index 67c63b8..6ead336 100644
--- a/src/org/eventb/internal/core/ast/extension/ExtensionTranslator.java
+++ b/src/org/eventb/internal/core/ast/extension/ExtensionTranslator.java
@@ -1,5 +1,5 @@
/*******************************************************************************
- * Copyright (c) 2014 Systerel and others.
+ * Copyright (c) 2014, 2016 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
@@ -10,17 +10,21 @@
*******************************************************************************/
package org.eventb.internal.core.ast.extension;
+import static org.eventb.core.ast.Formula.CPROD;
import static org.eventb.core.ast.Formula.EQUAL;
import static org.eventb.core.ast.Formula.FUNIMAGE;
import static org.eventb.core.ast.Formula.MAPSTO;
+import static org.eventb.core.ast.Formula.RELIMAGE;
import static org.eventb.core.ast.Formula.TRUE;
import org.eventb.core.ast.Expression;
import org.eventb.core.ast.Formula;
import org.eventb.core.ast.FormulaFactory;
import org.eventb.core.ast.FreeIdentifier;
+import org.eventb.core.ast.GivenType;
import org.eventb.core.ast.Predicate;
import org.eventb.core.ast.RelationalPredicate;
+import org.eventb.core.ast.Type;
/**
* Common implementation of a translator for an extension instance. Instances
@@ -30,53 +34,57 @@ import org.eventb.core.ast.RelationalPredicate;
*/
public abstract class ExtensionTranslator {
- protected final FreeIdentifier function;
- protected final FormulaFactory factory;
+ public static class IdentExtTranslator extends ExtensionTranslator {
- public ExtensionTranslator(FreeIdentifier function) {
- this.function = function;
- this.factory = function.getFactory();
- }
+ protected final FreeIdentifier function;
+ protected final FormulaFactory factory;
- protected Expression makeFunApp(Expression[] newChildExprs,
- Predicate[] newChildPreds) {
- Expression param = null;
- for (final Expression expr : newChildExprs) {
- param = join(param, expr);
- }
- for (final Predicate pred : newChildPreds) {
- param = join(param, makeExprOfPred(pred));
- }
- if (param == null) {
- // Atomic extension
- return function;
+ public IdentExtTranslator(FreeIdentifier function) {
+ this.function = function;
+ this.factory = function.getFactory();
}
- return factory.makeBinaryExpression(FUNIMAGE, function, param, null);
- }
+ protected Expression makeFunApp(Expression[] newChildExprs,
+ Predicate[] newChildPreds) {
+ Expression param = null;
+ for (final Expression expr : newChildExprs) {
+ param = join(param, expr);
+ }
+ for (final Predicate pred : newChildPreds) {
+ param = join(param, makeExprOfPred(pred));
+ }
+ if (param == null) {
+ // Atomic extension
+ return function;
+ }
+ return factory.makeBinaryExpression(FUNIMAGE, function, param,
+ null);
- private Expression makeExprOfPred(Predicate pred) {
- if (pred.getTag() == Formula.EQUAL) {
- final RelationalPredicate relPred = (RelationalPredicate) pred;
- if (relPred.getRight().getTag() == Formula.TRUE) {
- return relPred.getLeft();
+ }
+
+ private Expression makeExprOfPred(Predicate pred) {
+ if (pred.getTag() == Formula.EQUAL) {
+ final RelationalPredicate relPred = (RelationalPredicate) pred;
+ if (relPred.getRight().getTag() == Formula.TRUE) {
+ return relPred.getLeft();
+ }
}
+ return factory.makeBoolExpression(pred, null);
}
- return factory.makeBoolExpression(pred, null);
- }
- /*
- * Joins the given expressions with a maplet, unless the first is null.
- */
- private Expression join(Expression left, Expression right) {
- if (left == null) {
- return right;
+ /*
+ * Joins the given expressions with a maplet, unless the first is null.
+ */
+ private Expression join(Expression left, Expression right) {
+ if (left == null) {
+ return right;
+ }
+ return factory.makeBinaryExpression(MAPSTO, left, right, null);
}
- return factory.makeBinaryExpression(MAPSTO, left, right, null);
+
}
- public static class PredicateExtTranslator extends
- ExtensionTranslator {
+ public static class PredicateExtTranslator extends IdentExtTranslator {
private final Expression btrue;
@@ -96,8 +104,7 @@ public abstract class ExtensionTranslator {
}
- public static class ExpressionExtTranslator extends
- ExtensionTranslator {
+ public static class ExpressionExtTranslator extends IdentExtTranslator {
public ExpressionExtTranslator(FreeIdentifier function) {
super(function);
@@ -110,4 +117,66 @@ public abstract class ExtensionTranslator {
}
+ public static class TypeConstructorTranslator extends ExpressionExtTranslator {
+
+ public TypeConstructorTranslator(FreeIdentifier relation) {
+ super(relation);
+ }
+
+ @Override
+ public Expression translate(Expression[] newChildExprs,
+ Predicate[] newChildPreds) {
+ return makeRelApp(newChildExprs, newChildPreds);
+ }
+
+ private Expression makeRelApp(Expression[] newChildExprs,
+ Predicate[] newChildPreds) {
+ Expression param = null;
+ for (final Expression expr : newChildExprs) {
+ param = joinProd(param, expr);
+ }
+ assert newChildPreds.length == 0;
+ if (param == null) {
+ // Atomic extension
+ return function;
+ }
+ if (param.isATypeExpression()) {
+ return function.getType().getTarget().toExpression();
+ }
+ return factory.makeBinaryExpression(RELIMAGE, function, param,
+ null);
+ }
+
+ /*
+ * Joins the given expressions with a Cartesian product, unless the
+ * first is null.
+ */
+ private Expression joinProd(Expression left, Expression right) {
+ if (left == null) {
+ return right;
+ }
+ return factory.makeBinaryExpression(CPROD, left, right, null);
+ }
+
+ }
+
+ /**
+ * Translator for a parametric type. The translation class has allocated a
+ * given type that corresponds to the parametric type instance and we just
+ * return this given type (there are no type polymorphism in plain Event-B).
+ */
+ public static class TypeExtTranslator extends ExtensionTranslator {
+
+ private final Type type;
+
+ public TypeExtTranslator(GivenType type) {
+ this.type = type;
+ }
+
+ public Type translate() {
+ return type;
+ }
+
+ }
+
}
diff --git a/src/org/eventb/internal/core/ast/extension/FunctionalTypeBuilder.java b/src/org/eventb/internal/core/ast/extension/FunctionalTypeBuilder.java
new file mode 100644
index 0000000..6620f63
--- /dev/null
+++ b/src/org/eventb/internal/core/ast/extension/FunctionalTypeBuilder.java
@@ -0,0 +1,91 @@
+/*******************************************************************************
+ * Copyright (c) 2014, 2016 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.internal.core.ast.extension;
+
+import org.eventb.core.ast.FormulaFactory;
+import org.eventb.core.ast.Type;
+import org.eventb.internal.core.ast.TypeRewriter;
+
+/**
+ * A class which allows to build the type of a function or constant that
+ * replaces a mathematical extension.
+ *
+ * @author Thomas Muller
+ * @author Laurent Voisin
+ */
+public class FunctionalTypeBuilder {
+
+ // How to rewrite the types coming from the source language.
+ private final TypeRewriter rewriter;
+
+ // The formula factory of the target language
+ private final FormulaFactory factory;
+
+ public FunctionalTypeBuilder(TypeRewriter rewriter) {
+ this.rewriter = rewriter;
+ this.factory = rewriter.getFactory();
+ }
+
+ public Type makeFunctionalType(Type[] children, int numberOfPredicates,
+ Type range) {
+ final Type trgDomain = makeDomainType(children, numberOfPredicates);
+ final Type trgRange = rewriter.rewrite(range);
+ if (trgDomain == null) {
+ // Atomic operator
+ return trgRange;
+ }
+ return factory.makeRelationalType(trgDomain, trgRange);
+ }
+
+ public Type makeRelationalType(Type[] children, Type range) {
+ final Type trgDomain = makeRelDomainType(children);
+ final Type trgRange = rewriter.rewrite(range);
+ if (trgDomain == null) {
+ // Atomic operator
+ return trgRange;
+ }
+ final Type trgBase = trgRange.getBaseType();
+ assert trgBase != null;
+ return factory.makeRelationalType(trgDomain, trgBase);
+ }
+
+ private Type makeDomainType(Type[] children, int numberOfPredicates) {
+ Type result = null;
+ for (Type child : children) {
+ final Type trgChild = rewriter.rewrite(child);
+ result = join(result, trgChild);
+ }
+ final Type boolType = factory.makeBooleanType();
+ for (int i = 0; i < numberOfPredicates; i++) {
+ result = join(result, boolType);
+ }
+ return result;
+ }
+
+ private Type makeRelDomainType(Type[] children) {
+ Type result = null;
+ for (final Type child : children) {
+ final Type base = child.getBaseType();
+ assert base != null;
+ final Type trgChild = rewriter.rewrite(base);
+ result = join(result, trgChild);
+ }
+ return result;
+ }
+
+ private Type join(Type left, Type right) {
+ if (left == null) {
+ return right;
+ }
+ return factory.makeProductType(left, right);
+ }
+
+}
\ No newline at end of file
diff --git a/src/org/eventb/internal/core/ast/extension/TranslatorRegistry.java b/src/org/eventb/internal/core/ast/extension/TranslatorRegistry.java
index 3164013..371d01a 100644
--- a/src/org/eventb/internal/core/ast/extension/TranslatorRegistry.java
+++ b/src/org/eventb/internal/core/ast/extension/TranslatorRegistry.java
@@ -1,5 +1,5 @@
/*******************************************************************************
- * Copyright (c) 2014 Systerel and others.
+ * Copyright (c) 2014, 2016 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
@@ -14,10 +14,13 @@ import java.util.HashMap;
import java.util.Map;
import org.eventb.core.ast.FreeIdentifier;
+import org.eventb.core.ast.GivenType;
import org.eventb.internal.core.ast.extension.ExtensionSignature.ExpressionExtSignature;
import org.eventb.internal.core.ast.extension.ExtensionSignature.PredicateExtSignature;
import org.eventb.internal.core.ast.extension.ExtensionTranslator.ExpressionExtTranslator;
import org.eventb.internal.core.ast.extension.ExtensionTranslator.PredicateExtTranslator;
+import org.eventb.internal.core.ast.extension.ExtensionTranslator.TypeConstructorTranslator;
+import org.eventb.internal.core.ast.extension.ExtensionTranslator.TypeExtTranslator;
/**
* Maintains a map between extension signatures and extension translations. Two
@@ -28,7 +31,7 @@ import org.eventb.internal.core.ast.extension.ExtensionTranslator.PredicateExtTr
*/
public abstract class TranslatorRegistry<S extends ExtensionSignature, T extends ExtensionTranslator> {
- private final ExtensionTranslation translation;
+ protected final ExtensionTranslation translation;
private final Map<S, T> translators = new HashMap<S, T>();
@@ -39,14 +42,13 @@ public abstract class TranslatorRegistry<S extends ExtensionSignature, T extends
public T get(S signature) {
T result = translators.get(signature);
if (result == null) {
- final FreeIdentifier function = translation.makeFunction(signature);
- result = newTranslator(function);
+ result = newTranslator(signature);
translators.put(signature, result);
}
return result;
}
- protected abstract T newTranslator(FreeIdentifier function);
+ protected abstract T newTranslator(S signature);
public static class PredTranslatorRegistry extends
TranslatorRegistry<PredicateExtSignature, PredicateExtTranslator> {
@@ -56,7 +58,9 @@ public abstract class TranslatorRegistry<S extends ExtensionSignature, T extends
}
@Override
- protected PredicateExtTranslator newTranslator(FreeIdentifier function) {
+ protected PredicateExtTranslator newTranslator(
+ PredicateExtSignature signature) {
+ final FreeIdentifier function = translation.makeFunction(signature);
return new PredicateExtTranslator(function);
}
@@ -70,10 +74,32 @@ public abstract class TranslatorRegistry<S extends ExtensionSignature, T extends
}
@Override
- protected ExpressionExtTranslator newTranslator(FreeIdentifier function) {
+ protected ExpressionExtTranslator newTranslator(
+ ExpressionExtSignature signature) {
+ final FreeIdentifier function = translation.makeFunction(signature);
+ if (signature.isATypeConstructor()) {
+ return new TypeConstructorTranslator(function);
+ }
return new ExpressionExtTranslator(function);
}
}
+ public static class TypeTranslatorRegistry extends
+ TranslatorRegistry<ExpressionExtSignature, TypeExtTranslator> {
+
+ public TypeTranslatorRegistry(ExtensionTranslation translation) {
+ super(translation);
+ }
+
+ @Override
+ protected TypeExtTranslator newTranslator(
+ ExpressionExtSignature signature) {
+ assert (signature.isATypeConstructor());
+ final GivenType type = translation.makeType(signature);
+ return new TypeExtTranslator(type);
+ }
+
+ }
+
}
diff --git a/src/org/eventb/internal/core/parser/SubParsers.java b/src/org/eventb/internal/core/parser/SubParsers.java
index d15bedc..2ea5a18 100644
--- a/src/org/eventb/internal/core/parser/SubParsers.java
+++ b/src/org/eventb/internal/core/parser/SubParsers.java
@@ -1,5 +1,5 @@
/*******************************************************************************
- * Copyright (c) 2010, 2014 Systerel and others.
+ * Copyright (c) 2010, 2016 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
@@ -958,6 +958,36 @@ public class SubParsers {
}
}
+ public static class ExtendedRelationalPredicateParser extends BinaryLedExprParser<ExtendedPredicate> {
+
+ public ExtendedRelationalPredicateParser(int kind, int tag) {
+ super(kind, tag);
+ }
+
+ @Override
+ protected void checkValue(ParserContext pc,
+ Expression left, Expression right)
+ throws SyntaxError {
+ EXTENDED_PRED.check(pc, tag, asList(left, right));
+ }
+
+ @Override
+ protected ExtendedPredicate makeValue(FormulaFactory factory,
+ Expression left, Expression right, SourceLocation loc) throws SyntaxError {
+ return EXTENDED_PRED.make(factory, tag, asList(left, right), loc);
+ }
+
+ @Override
+ protected Expression getLeft(ExtendedPredicate parent) {
+ return parent.getChildExpressions()[0];
+ }
+
+ @Override
+ protected Expression getRight(ExtendedPredicate parent) {
+ return parent.getChildExpressions()[1];
+ }
+ }
+
public static abstract class LedImage extends BinaryLedExprParser<BinaryExpression> {
public LedImage(int kind, int tag) {
@@ -1065,6 +1095,29 @@ public class SubParsers {
}
}
+ public static class ExtendedBinaryPredicateParser extends BinaryLedPredParser<ExtendedPredicate> {
+
+ public ExtendedBinaryPredicateParser(int kind, int tag) {
+ super(kind, tag);
+ }
+
+ @Override
+ protected ExtendedPredicate makeValue(FormulaFactory factory, Predicate left,
+ Predicate right, SourceLocation loc) throws SyntaxError {
+ return EXTENDED_PRED.make(factory, tag, asList(left, right), loc);
+ }
+
+ @Override
+ protected Predicate getLeft(ExtendedPredicate parent) {
+ return parent.getChildPredicates()[0];
+ }
+
+ @Override
+ protected Predicate getRight(ExtendedPredicate parent) {
+ return parent.getChildPredicates()[1];
+ }
+ }
+
public static class QuantifiedPredicateParser extends QuantifiedParser<QuantifiedPredicate> {
public QuantifiedPredicateParser(int kind, int tag) {
--
GitLab