import

src/org/eventb/core/ast/Assignment.java

+/*******************************************************************************
+ * Copyright (c) 2005, 2013 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
+ * http://www.eclipse.org/legal/epl-v10.html
+ *
+ * Contributors:
+ *     ETH Zurich - initial API and implementation
+ *     Systerel - generalised getPositions() into inspect()
+ *     Systerel - added child indexes
+ *     Systerel - add given sets to free identifier cache
+ *     Systerel - store factory used to build a formula
+ *******************************************************************************/
+package org.eventb.core.ast;
+
+import static org.eventb.internal.core.ast.FormulaChecks.ensureMinLength;
+
+import java.util.Arrays;
+
+import org.eventb.internal.core.ast.FindingAccumulator;
+import org.eventb.internal.core.ast.ITypeCheckingRewriter;
+import org.eventb.internal.core.ast.IntStack;
+import org.eventb.internal.core.typecheck.TypeUnifier;
+
+/**
+ * Common implementation for event-B assignments.
+ * <p>
+ * There are various kinds of assignments which are implemented in sub-classes
+ * of this class. The commonality between these assignments is that they are
+ * formed of two parts: a left-hand side and a right hand-side. The left-hand side,
+ * that is a list of free identifiers, is implemented in this class, while the
+ * right-hand side is implemented in subclasses.
+ * </p>
+ * <p>
+ * This class is not intended to be subclassed by clients.
+ * </p>
+ * 
+ * @author Laurent Voisin
+ * @since 1.0
+ * @noextend This class is not intended to be subclassed by clients.
+ */
+public abstract class Assignment extends Formula<Assignment> {
+
+	protected final FreeIdentifier[] assignedIdents;
+	
+	/**
+	 * Creates a new assignment with the given arguments.
+	 * 
+	 * @param tag node tag of this expression
+	 * @param ff the formula factory used to build this assignment
+	 * @param location source location of this expression
+	 * @param hashCode combined hash code for children
+	 * @param assignedIdents array of free identifiers that constitute the left-hand side
+	 * @since 3.0
+	 */
+	protected Assignment(int tag, FormulaFactory ff,
+			SourceLocation location, int hashCode,
+			FreeIdentifier[] assignedIdents) {
+		super(tag, ff, location, combineHashCodes(
+				combineHashCodes(assignedIdents), hashCode));
+		ensureMinLength(assignedIdents, 1);
+		this.assignedIdents = assignedIdents;
+		ensureSameFactory(this.assignedIdents);
+	}
+
+	protected final void appendAssignedIdents(StringBuilder result) {
+		boolean comma = false;
+		for (FreeIdentifier ident : assignedIdents) {
+			if (comma)
+				result.append(',');
+			comma = true;
+			result.append(ident.getName());
+		}
+	}
+	
+	@Override
+	protected final void solveType(TypeUnifier unifier) {
+		if (isTypeChecked()) {
+			return;
+		}
+		solveChildrenTypes(unifier);
+		for (FreeIdentifier ident: assignedIdents) {
+			ident.solveType(unifier);
+		}
+		synthesizeType();
+	}
+
+	/**
+	 * @since 3.0
+	 */
+	// Calls recursively solveType on each child of this node.
+	protected abstract void solveChildrenTypes(TypeUnifier unifier);
+
+	/**
+	 * Return the left-hand side of this assignment.
+	 * 
+	 * @return an array of the free identifiers that make up the left-hand side
+	 *         of this assignment
+	 */
+	public final FreeIdentifier[] getAssignedIdentifiers() {
+		return assignedIdents.clone();
+	}
+	
+	protected final String getSyntaxTreeLHS(String[] boundNames, String tabs) {
+		StringBuilder builder = new StringBuilder();
+		for (FreeIdentifier ident: assignedIdents) {
+			builder.append(ident.getSyntaxTree(boundNames, tabs));
+		}
+		return builder.toString();
+	}
+		
+	@Override
+	protected final Assignment getTypedThis() {
+		return this;
+	}
+
+	protected final boolean hasSameAssignedIdentifiers(Assignment other) {
+		return Arrays.equals(assignedIdents, other.assignedIdents);
+	}
+
+	@Override
+	public final Assignment rewrite(IFormulaRewriter rewriter) {
+		throw new UnsupportedOperationException("Assignments cannot be rewritten");
+	}
+
+	@Override
+	protected final Assignment rewrite(ITypeCheckingRewriter rewriter) {
+		throw new UnsupportedOperationException("Assignments cannot be rewritten");
+	}
+	
+	/**
+	 * Returns the (flattened) feasibility predicate of this assignment. An
+	 * exception is thrown if this assignment was not type checked.
+	 * 
+	 * @return Returns the feasibility predicate
+	 * @since 3.0
+	 */
+	public final Predicate getFISPredicate() {
+		assert isTypeChecked();
+		return getFISPredicateRaw().flatten();
+	}
+	
+	/**
+	 * @since 3.0
+	 */
+	protected abstract Predicate getFISPredicateRaw();
+	
+	/**
+	 * Returns the (flattened) before-after predicate of this assignment. An
+	 * exception is thrown if this assignment was not type checked.
+	 * 
+	 * @return Returns the before-after predicate of this assignment
+	 * @since 3.0
+	 */
+	public final Predicate getBAPredicate() {
+		assert isTypeChecked();
+		return getBAPredicateRaw().flatten();
+	}
+	
+	/**
+	 * @since 3.0
+	 */
+	protected abstract Predicate getBAPredicateRaw();
+
+	
+	/**
+	 * Returns an array of the free identifiers that occur on the right-hand
+	 * side of this assignment. The free identifiers are extracted using
+	 * {@link Formula#getFreeIdentifiers()} applied to all formulas that are
+	 * part of the right-hand side of this assignment.
+	 * 
+	 * @return all free identifiers that occur in the right-hand side of this
+	 *         assignment.
+	 */
+	public abstract FreeIdentifier[] getUsedIdentifiers();
+	
+	/**
+	 * @since 3.0
+	 */
+	protected abstract void synthesizeType();
+
+	@Override
+	protected final <F> void inspect(FindingAccumulator<F> acc) {
+		throw new UnsupportedOperationException(
+				"Assignments cannot be rewritten");
+	}
+
+	@Override
+	public final Formula<?> getChild(int index) {
+		throw new UnsupportedOperationException(
+				"Assignments cannot be rewritten");
+	}
+
+	@Override
+	public final int getChildCount() {
+		throw new UnsupportedOperationException(
+				"Assignments cannot be rewritten");
+	}
+
+	@Override
+	protected final IPosition getDescendantPos(SourceLocation sloc,
+			IntStack indexes) {
+		throw new UnsupportedOperationException(
+				"Assignments cannot be rewritten");
+	}
+
+	@Override
+	protected final Assignment rewriteChild(int index, SingleRewriter rewriter) {
+		throw new UnsupportedOperationException(
+				"Assignments cannot be rewritten");
+	}
+
+	@Override
+	protected final Assignment getCheckedReplacement(SingleRewriter rewriter) {
+		throw new UnsupportedOperationException(
+				"Assignments cannot be rewritten");
+	}
+
+}

src/org/eventb/core/ast/AssociativeExpression.java

+/*******************************************************************************
+ * Copyright (c) 2005, 2013 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
+ * http://www.eclipse.org/legal/epl-v10.html
+ *
+ * Contributors:
+ *     ETH Zurich - initial API and implementation
+ *     Systerel - added accept for ISimpleVisitor
+ *     Systerel - fixed bug in synthesizeType()
+ *     Systerel - mathematical language v2
+ *     Systerel - added support for predicate variables
+ *     Systerel - generalised getPositions() into inspect()
+ *     Systerel - externalized wd lemmas generation
+ *     Systerel - added child indexes
+ *     Systerel - store factory used to build a formula
+ *******************************************************************************/
+package org.eventb.core.ast;
+
+import static org.eventb.core.ast.AssociativeHelper.getSyntaxTreeHelper;
+import static org.eventb.core.ast.extension.StandardGroup.ARITHMETIC;
+import static org.eventb.core.ast.extension.StandardGroup.BINOP;
+import static org.eventb.internal.core.ast.FormulaChecks.ensureMinLength;
+import static org.eventb.internal.core.ast.FormulaChecks.ensureTagInRange;
+
+import java.util.ArrayList;
+import java.util.Arrays;
+import java.util.LinkedHashSet;
+import java.util.Set;
+
+import org.eventb.core.ast.extension.StandardGroup;
+import org.eventb.internal.core.ast.FindingAccumulator;
+import org.eventb.internal.core.ast.ITypeCheckingRewriter;
+import org.eventb.internal.core.ast.IdentListMerger;
+import org.eventb.internal.core.ast.IntStack;
+import org.eventb.internal.core.ast.LegibilityResult;
+import org.eventb.internal.core.ast.Position;
+import org.eventb.internal.core.ast.extension.IToStringMediator;
+import org.eventb.internal.core.ast.extension.KindMediator;
+import org.eventb.internal.core.parser.BMath;
+import org.eventb.internal.core.parser.GenParser.OverrideException;
+import org.eventb.internal.core.parser.IOperatorInfo;
+import org.eventb.internal.core.parser.IParserPrinter;
+import org.eventb.internal.core.parser.SubParsers.AssociativeExpressionInfix;
+import org.eventb.internal.core.typecheck.TypeCheckResult;
+import org.eventb.internal.core.typecheck.TypeUnifier;
+import org.eventb.internal.core.typecheck.TypeVariable;
+
+/**
+ * AssociativeExpression is the AST type for associative expressions in an
+ * event-B formula.
+ * <p>
+ * It can have several children which can only be Expression objects. Can only
+ * accept {BUNION, BINTER, BCOMP, FCOMP, OVR, PLUS, MUL}.
+ * </p>
+ * 
+ * @author François Terrier
+ * @since 1.0
+ * @noextend This class is not intended to be subclassed by clients.
+ */
+public class AssociativeExpression extends Expression {
+
+	// offset of the corresponding tag-interval in Formula
+	private static final int FIRST_TAG = Formula.FIRST_ASSOCIATIVE_EXPRESSION;
+	
+	/**
+	 * @since 2.0
+	 */
+	public static final String BINTER_ID = "Binary Intersection";
+	/**
+	 * @since 2.0
+	 */
+	public static final String BUNION_ID = "Binary Union";
+	/**
+	 * @since 2.0
+	 */
+	public static final String BCOMP_ID = "Backward Composition";
+	/**
+	 * @since 2.0
+	 */
+	public static final String FCOMP_ID = "Forward Composition";
+	/**
+	 * @since 2.0
+	 */
+	public static final String OVR_ID = "Overload";
+	/**
+	 * @since 2.0
+	 */
+	public static final String MUL_ID = "mul";
+	/**
+	 * @since 2.0
+	 */
+	public static final String PLUS_ID = "plus";
+
+	private static enum Operators implements IOperatorInfo<AssociativeExpression> {
+		OP_BUNION("\u222a", BUNION_ID, BINOP, BUNION),
+		OP_BINTER("\u2229", BINTER_ID, BINOP, BINTER),
+		OP_BCOMP("\u2218", BCOMP_ID, BINOP, BCOMP),
+		OP_FCOMP(";", FCOMP_ID, BINOP, FCOMP), 
+		OP_OVR("\ue103", OVR_ID, BINOP, OVR), 
+		OP_PLUS("+", PLUS_ID, ARITHMETIC, PLUS), 
+		OP_MUL("\u2217", MUL_ID, ARITHMETIC, MUL), 
+		;
+		
+		private final String image;
+		private final String id;
+		private final String groupId;
+		private final int tag;
+		
+		private Operators(String image, String id, StandardGroup group, int tag) {
+			this.image = image;
+			this.id = id;
+			this.groupId = group.getId();
+			this.tag = tag;
+		}
+
+		@Override
+		public String getImage() {
+			return image;
+		}
+		
+		@Override
+		public String getId() {
+			return id;
+		}
+		
+		@Override
+		public String getGroupId() {
+			return groupId;
+		}
+
+		@Override
+		public IParserPrinter<AssociativeExpression> makeParser(int kind) {
+			return new AssociativeExpressionInfix(kind, tag);
+		}
+		
+		@Override
+		public boolean isSpaced() {
+			return false;
+		}
+	}
+	
+	// For testing purposes
+	public static final int TAGS_LENGTH = Operators.values().length;
+	
+	/**
+	 * @since 2.0
+	 */
+	// FIXME just before merging the branch back to trunk, make this class an
+	// interface then move this code to a non published area
+	public static void init(BMath grammar) {
+		try {
+			for(Operators operInfo: Operators.values()) {
+				grammar.addOperator(operInfo);
+			}
+		} catch (OverrideException e) {
+			// TODO Auto-generated catch block
+			e.printStackTrace();
+		}
+	}
+	
+	// The children of this associative expression.
+	// Is never null and contains at least two elements by construction.
+	private final Expression[] children;
+	
+	/**
+	 * Must never be called directly: use the factory method instead.
+	 * 
+	 * @see FormulaFactory#makeAssociativeExpression(int, Expression[],
+	 *      SourceLocation)
+	 * @see FormulaFactory#makeAssociativeExpression(int, java.util.Collection,
+	 *      SourceLocation)
+	 */
+	protected AssociativeExpression(Expression[] children, int tag,
+			SourceLocation location, FormulaFactory ff) {
+		super(tag, ff, location, combineHashCodes(children));
+		this.children = children;
+		ensureTagInRange(tag, FIRST_TAG, TAGS_LENGTH);
+		ensureMinLength(children, 2);
+		ensureSameFactory(this.children);
+		setPredicateVariableCache(this.children);
+		synthesizeType(null);
+	}
+
+	@Override
+	protected void synthesizeType(Type givenType) {
+		// No need to add free identifiers of given sets since it has been done
+		// in children and we merge here
+		IdentListMerger freeIdentMerger = mergeFreeIdentifiers(children);
+		this.freeIdents = freeIdentMerger.getFreeMergedArray();
+
+		IdentListMerger boundIdentMerger = mergeBoundIdentifiers(children);
+		this.boundIdents = boundIdentMerger.getBoundMergedArray();
+
+		if (freeIdentMerger.containsError() || boundIdentMerger.containsError()) {
+			// Incompatible type environments, don't bother going further.
+			return;
+		}
+		
+		// Fast exit if first child is not typed
+		// (the most common case where type synthesis can't be done)
+		if (! children[0].isTypeChecked()) {
+			return;
+		}
+		
+		Type resultType;
+		Type partType, sourceType, targetType;
+		final int last = children.length - 1;
+		final FormulaFactory ff = getFactory();
+		switch (getTag()) {
+		case Formula.BUNION:
+		case Formula.BINTER:
+			resultType = children[0].getType();
+			if (! (resultType instanceof PowerSetType)) {
+				return;
+			}
+			for (int i = 1; i <= last; i++) {
+				if (! resultType.equals(children[i].getType())) {
+					return;
+				}
+			}
+			break;
+		case Formula.BCOMP:
+			partType = children[0].getType().getSource();
+			if (partType == null) {
+				return;
+			}
+			for (int i = 1; i <= last; i++) {
+				final Type childType = children[i].getType();
+				if (childType == null) {
+					return;
+				}
+				if (! partType.equals(childType.getTarget())) {
+					return;
+				}
+				partType = childType.getSource();
+			}
+			sourceType = children[last].getType().getSource();
+			targetType = children[0].getType().getTarget();
+			resultType = ff.makeRelationalType(sourceType, targetType);
+			break;
+		case Formula.FCOMP:
+			partType = children[0].getType().getTarget();
+			if (partType == null) {
+				return;
+			}
+			for (int i = 1; i <= last; i++) {
+				final Type childType = children[i].getType();
+				if (childType == null) {
+					return;
+				}
+				if (! partType.equals(childType.getSource())) {
+					return;
+				}
+				partType = childType.getTarget();
+			}
+			sourceType = children[0].getType().getSource();
+			targetType = children[last].getType().getTarget();
+			resultType = ff.makeRelationalType(sourceType, targetType);
+			break;
+		case Formula.OVR:
+			resultType = children[0].getType();
+			if (! resultType.isRelational()) {
+				return;
+			}
+			for (int i = 1; i <= last; i++) {
+				if (! resultType.equals(children[i].getType())) {
+					return;
+				}
+			}
+			break;
+		case Formula.PLUS:
+		case Formula.MUL:
+			resultType = children[0].getType();
+			for (Expression child: children) {
+				final Type childType = child.getType();
+				if (! (childType instanceof IntegerType)) {
+					return;
+				}
+			}
+			break;
+		default:
+			assert false;
+			return;
+		}
+		setFinalType(resultType, givenType);
+	}
+	
+	/**
+	 * Returns the children of this node.
+	 * 
+	 * @return the children of this node. Can never be <code>null</code> or
+	 *         empty.
+	 */
+	public Expression[] getChildren() {
+		return children.clone();
+	}
+
+	private String getOperatorImage() {
+		return getOperator().getImage();
+	}
+
+	private Operators getOperator() {
+		return Operators.values()[getTag()-FIRST_TAG];
+	}
+
+	@Override
+	boolean equalsInternalExpr(Expression expr) {
+		final AssociativeExpression other = (AssociativeExpression) expr;
+		return Arrays.equals(children, other.children);
+	}
+
+	@Override
+	protected void typeCheck(TypeCheckResult result, BoundIdentDecl[] quantifiedIdentifiers) {
+		final Type resultType;
+		switch (getTag()) {
+		case Formula.BUNION:
+		case Formula.BINTER:
+			TypeVariable alpha = result.newFreshVariable(null);
+			resultType = result.makePowerSetType(alpha);
+			for (int i = 0; i < children.length; i++) {
+				children[i].typeCheck(result,quantifiedIdentifiers);
+				result.unify(children[i].getType(), resultType, this);
+			}
+			break;
+		case Formula.BCOMP:
+			TypeVariable[] tv = new TypeVariable[children.length+1];
+			tv[0] = result.newFreshVariable(null);
+			for (int i = 0; i < children.length; i++) {
+				tv[i+1] = result.newFreshVariable(null);
+				children[i].typeCheck(result,quantifiedIdentifiers);
+				result.unify(children[i].getType(), result.makeRelationalType(tv[i+1], tv[i]), this);
+			}
+			resultType = result.makeRelationalType(tv[children.length], tv[0]);
+			break;
+		case Formula.FCOMP:
+			tv = new TypeVariable[children.length+1];
+			tv[0] = result.newFreshVariable(null);
+			for (int i = 0; i < children.length; i++) {
+				tv[i+1] = result.newFreshVariable(null);
+				children[i].typeCheck(result,quantifiedIdentifiers);
+				result.unify(children[i].getType(), result.makeRelationalType(tv[i], tv[i+1]), this);
+			}
+			resultType = result.makeRelationalType(tv[0], tv[children.length]);
+			break;
+		case Formula.OVR:
+			alpha = result.newFreshVariable(null);
+			TypeVariable beta = result.newFreshVariable(null);
+			resultType = result.makeRelationalType(alpha, beta);
+			for (int i = 0; i < children.length; i++) {
+				children[i].typeCheck(result,quantifiedIdentifiers);
+				result.unify(children[i].getType(), resultType, this);
+			}
+			break;
+		case Formula.PLUS:
+		case Formula.MUL:
+			resultType = result.makeIntegerType();
+			for (int i = 0; i < children.length; i++) {
+				children[i].typeCheck(result,quantifiedIdentifiers);
+				result.unify(children[i].getType(), resultType, this);
+			}
+			break;
+		default:
+			assert false;
+			return;
+		}
+		setTemporaryType(resultType, result);
+	}
+	
+	@Override
+	protected void solveChildrenTypes(TypeUnifier unifier) {
+		for (Expression child : children) {
+			child.solveType(unifier);
+		}
+	}
+
+	/**
+	 * @since 2.0
+	 */
+	@Override
+	protected void isLegible(LegibilityResult result) {
+		AssociativeHelper.isLegibleList(children, result);	
+	}
+	
+	@Override
+	protected void toString(IToStringMediator mediator) {
+		final Operators operator = getOperator();
+		final int kind = mediator.getKind();
+		
+		operator.makeParser(kind).toString(mediator, this);
+	}
+
+	@Override
+	protected int getKind(KindMediator mediator) {
+		return mediator.getKind(getOperatorImage());
+	}
+	
+	@Override
+	protected String getSyntaxTree(String[] boundNames, String tabs) {
+		return getSyntaxTreeHelper(boundNames, tabs,
+				children, getOperatorImage(), getTypeName(), this.getClass()
+						.getSimpleName());
+	}
+
+	@Override
+	protected void collectFreeIdentifiers(LinkedHashSet<FreeIdentifier> freeIdentSet) {
+		for (Expression child: children) {
+			child.collectFreeIdentifiers(freeIdentSet);
+		}
+	}
+
+	@Override
+	protected void collectNamesAbove(Set<String> names, String[] boundNames, int offset) {
+		for (Expression child: children) {
+			child.collectNamesAbove(names, boundNames, offset);
+		}
+	}
+
+	@Override
+	public boolean accept(IVisitor visitor) {
+		boolean goOn = true;
+
+		switch (getTag()) {
+		case BUNION: goOn = visitor.enterBUNION(this); break;
+		case BINTER: goOn = visitor.enterBINTER(this); break;
+		case BCOMP:  goOn = visitor.enterBCOMP(this);  break;
+		case FCOMP:  goOn = visitor.enterFCOMP(this);  break;
+		case OVR:    goOn = visitor.enterOVR(this);    break;
+		case PLUS:   goOn = visitor.enterPLUS(this);   break;
+		case MUL:    goOn = visitor.enterMUL(this);    break;
+		default:     assert false;
+		}
+
+		for (int i = 0; goOn && i < children.length; i++) {
+			if (i != 0) {
+				switch (getTag()) {
+				case BUNION: goOn = visitor.continueBUNION(this); break;
+				case BINTER: goOn = visitor.continueBINTER(this); break;
+				case BCOMP:  goOn = visitor.continueBCOMP(this);  break;
+				case FCOMP:  goOn = visitor.continueFCOMP(this);  break;
+				case OVR:    goOn = visitor.continueOVR(this);    break;
+				case PLUS:   goOn = visitor.continuePLUS(this);   break;
+				case MUL:    goOn = visitor.continueMUL(this);    break;
+				default:     assert false;
+				}
+			}
+			if (goOn) {
+				goOn = children[i].accept(visitor);
+			}
+		}
+		
+		switch (getTag()) {
+		case BUNION: return visitor.exitBUNION(this);
+		case BINTER: return visitor.exitBINTER(this);
+		case BCOMP:  return visitor.exitBCOMP(this);
+		case FCOMP:  return visitor.exitFCOMP(this);
+		case OVR:    return visitor.exitOVR(this);
+		case PLUS:   return visitor.exitPLUS(this);
+		case MUL:    return visitor.exitMUL(this);
+		default:     return true;
+		}
+	}
+
+	@Override
+	public void accept(ISimpleVisitor visitor) {
+		visitor.visitAssociativeExpression(this);		
+	}
+
+	@Override
+	protected Expression rewrite(ITypeCheckingRewriter rewriter) {
+		final boolean flatten = rewriter.autoFlatteningMode();
+		final ArrayList<Expression> newChildren = new ArrayList<Expression>(
+				children.length + 11);
+		boolean changed = false;
+		for (Expression child : children) {
+			final Expression newChild = child.rewrite(rewriter);
+			if (flatten && getTag() == newChild.getTag()) {
+				final Expression[] grandChildren = ((AssociativeExpression) newChild).children;
+				newChildren.addAll(Arrays.asList(grandChildren));
+				changed = true;
+			} else {
+				newChildren.add(newChild);
+				changed |= newChild != child;
+			}
+		}
+		final AssociativeExpression before;
+		if (! changed) {
+			before = this;
+		} else {
+			before = rewriter.getFactory().makeAssociativeExpression(getTag(),
+					newChildren, getSourceLocation());
+		}
+		return rewriter.rewrite(this, before);
+	}
+
+	@Override
+	protected final <F> void inspect(FindingAccumulator<F> acc) {
+		acc.inspect(this);
+		if (acc.childrenSkipped()) {
+			return;
+		}
+		acc.enterChildren();
+		for (Expression child: children) {
+			child.inspect(acc);
+			if (acc.allSkipped()) {
+				break;
+			}
+			acc.nextChild();
+		}
+		acc.leaveChildren();
+	}
+
+	@Override
+	public Expression getChild(int index) {
+		checkChildIndex(index);
+		return children[index];
+	}
+
+	@Override
+	public int getChildCount() {
+		return children.length;
+	}
+
+	@Override
+	public IPosition getDescendantPos(SourceLocation sloc, IntStack indexes) {
+		indexes.push(0);
+		for (Expression child: children) {
+			IPosition pos = child.getPosition(sloc, indexes);
+			if (pos != null)
+				return pos;
+			indexes.incrementTop();
+		}
+		indexes.pop();
+		return new Position(indexes);
+	}
+
+	@Override
+	protected Expression rewriteChild(int index, SingleRewriter rewriter) {
+		if (index < 0 || children.length <= index) 
+			throw new IllegalArgumentException("Position is outside the formula");
+		Expression[] newChildren = children.clone();
+		newChildren[index] = rewriter.rewrite(children[index]);
+		return getFactory().makeAssociativeExpression(
+				getTag(), newChildren, getSourceLocation());
+	}
+
+	@Override
+	public boolean isWDStrict() {
+		return true;
+	}
+
+}

src/org/eventb/core/ast/AssociativeHelper.java

+/*******************************************************************************
+ * Copyright (c) 2005, 2013 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
+ * http://www.eclipse.org/legal/epl-v10.html
+ *
+ * Contributors:
+ *     ETH Zurich - initial API and implementation
+ *     Systerel - added helper method for extensions
+ *******************************************************************************/
+package org.eventb.core.ast;
+
+import org.eventb.internal.core.ast.LegibilityResult;
+
+/**
+ * Helper class for implementing associative formulae of event-B.
+ * <p>
+ * Provides methods which implement common behavior of classes
+ * <code>AssociativePredicate</code> and <code>AssociativeExpression</code>.
+ * </p>
+ * 
+ * @author Laurent Voisin
+ */
+/* package */ class AssociativeHelper {
+
+	protected static String getSyntaxTreeHelper(String[] boundNames,
+			String tabs, Formula<?>[] children, String tagOperator,
+			String typeName, String className) {
+		StringBuilder str = new StringBuilder();
+		str.append(tabs + className + " [" + tagOperator + "]" + typeName
+				+ "\n");
+		String childIndent = tabs + "\t";
+		for (Formula<?> child : children) {
+			str.append(child.getSyntaxTree(boundNames, childIndent));
+		}
+		return str.toString();
+	}
+
+	// Disable default constructor.
+	private AssociativeHelper() {
+		assert false;
+	}
+
+	/*
+	 * Helper for computing well-formedness for a list of formulae.
+	 * 
+	 * @param formulae
+	 *            an array of formulae
+	 * @param result
+	 *            result of this operation
+	 * @param quantifiedIdents
+	 *            a list of currently bound identifiers
+	 */
+	protected static <T extends Formula<T>> void isLegibleList(T[] formulae, LegibilityResult result) {
+		for (T formula : formulae) {
+			formula.isLegible(result);
+		}
+	}
+	
+}

src/org/eventb/core/ast/AssociativePredicate.java

+/*******************************************************************************
+ * Copyright (c) 2005, 2013 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
+ * http://www.eclipse.org/legal/epl-v10.html
+ *
+ * Contributors:
+ *     ETH Zurich - initial API and implementation
+ *     Systerel - added accept for ISimpleVisitor
+ *     Systerel - added support for predicate variables
+ *     Systerel - generalised getPositions() into inspect()
+ *     Systerel - externalized wd lemmas generation
+ *     Systerel - added child indexes
+ *     Systerel - store factory used to build a formula
+ *******************************************************************************/
+package org.eventb.core.ast;
+
+import static org.eventb.core.ast.extension.StandardGroup.LOGIC_PRED;
+import static org.eventb.internal.core.ast.FormulaChecks.ensureMinLength;
+import static org.eventb.internal.core.ast.FormulaChecks.ensureTagInRange;
+
+import java.util.ArrayList;
+import java.util.Arrays;
+import java.util.LinkedHashSet;
+import java.util.Set;
+
+import org.eventb.core.ast.extension.StandardGroup;
+import org.eventb.internal.core.ast.FindingAccumulator;
+import org.eventb.internal.core.ast.ITypeCheckingRewriter;
+import org.eventb.internal.core.ast.IdentListMerger;
+import org.eventb.internal.core.ast.IntStack;
+import org.eventb.internal.core.ast.LegibilityResult;
+import org.eventb.internal.core.ast.Position;
+import org.eventb.internal.core.ast.extension.IToStringMediator;
+import org.eventb.internal.core.ast.extension.KindMediator;
+import org.eventb.internal.core.parser.BMath;
+import org.eventb.internal.core.parser.GenParser.OverrideException;
+import org.eventb.internal.core.parser.IOperatorInfo;
+import org.eventb.internal.core.parser.IParserPrinter;
+import org.eventb.internal.core.parser.SubParsers.AssociativePredicateInfix;
+import org.eventb.internal.core.typecheck.TypeCheckResult;
+import org.eventb.internal.core.typecheck.TypeUnifier;
+
+/**
+ * AssociativePredicate is the AST class for the associative predicates in an
+ * event-B formula.
+ * <p>
+ * It can have several children which can only be Predicate objects. Can only
+ * accept {LAND, LOR}.
+ * </p>
+ * 
+ * @author François Terrier
+ * @since 1.0
+ * @noextend This class is not intended to be subclassed by clients.
+ */
+public class AssociativePredicate extends Predicate {
+	
+	// The children of this associative predicate.
+	// Is never null and contains at least two elements by construction.
+	private final Predicate[] children;
+	
+	// offset of the corresponding interval in Formula
+	private static int FIRST_TAG = FIRST_ASSOCIATIVE_PREDICATE;
+
+	/**
+	 * @since 2.0
+	 */
+	public static final String LOR_ID = "lor";
+
+	/**
+	 * @since 2.0
+	 */
+	public static final String LAND_ID = "land";
+
+	private static enum Operators implements IOperatorInfo<AssociativePredicate> {
+		OP_LAND("\u2227", LAND_ID, LOGIC_PRED, LAND),
+		OP_LOR("\u2228", LOR_ID, LOGIC_PRED, LOR),
+		;
+		
+		private final String image;
+		private final String id;
+		private final String groupId;
+		private final int tag;
+		
+		private Operators(String image, String id, StandardGroup group, int tag) {
+			this.image = image;
+			this.id = id;
+			this.groupId = group.getId();
+			this.tag = tag;
+		}
+
+		@Override
+		public String getImage() {
+			return image;
+		}
+		
+		@Override
+		public String getId() {
+			return id;
+		}
+		
+		@Override
+		public String getGroupId() {
+			return groupId;
+		}
+
+		@Override
+		public IParserPrinter<AssociativePredicate> makeParser(int kind) {
+			return new AssociativePredicateInfix(kind, tag);
+		}
+
+		@Override
+		public boolean isSpaced() {
+			return false;
+		}
+	}
+
+	// For testing purposes
+	public static final int TAGS_LENGTH = Operators.values().length;
+	
+	/**
+	 * @since 2.0
+	 */
+	public static void init(BMath grammar) {
+		try {
+			for(Operators operInfo: Operators.values()) {
+				grammar.addOperator(operInfo);
+			}
+		} catch (OverrideException e) {
+			// TODO Auto-generated catch block
+			e.printStackTrace();
+		}
+	}
+	
+	/**
+	 * Must never be called directly: use the factory method instead.
+	 * 
+	 * @see FormulaFactory#makeAssociativePredicate(int, Predicate[],
+	 *      SourceLocation)
+	 * @see FormulaFactory#makeAssociativePredicate(int, java.util.Collection,
+	 *      SourceLocation)
+	 */
+	protected AssociativePredicate(Predicate[] children, int tag,
+			SourceLocation location, FormulaFactory ff) {
+		super(tag, ff, location, combineHashCodes(children));
+		this.children = children;
+		ensureTagInRange(tag, FIRST_TAG, TAGS_LENGTH);
+		ensureMinLength(children, 2);
+		ensureSameFactory(this.children);
+		setPredicateVariableCache(this.children);
+		synthesizeType();
+	}
+
+	@Override
+	protected void synthesizeType() {
+		IdentListMerger freeIdentMerger = mergeFreeIdentifiers(children);
+		this.freeIdents = freeIdentMerger.getFreeMergedArray();
+
+		IdentListMerger boundIdentMerger = mergeBoundIdentifiers(children);
+		this.boundIdents = boundIdentMerger.getBoundMergedArray();
+
+		if (freeIdentMerger.containsError() || boundIdentMerger.containsError()) {
+			// Incompatible type environments, don't bother going further.
+			return;
+		}
+		
+		for (Predicate child: children) {
+			if (! child.isTypeChecked()) {
+				return;
+			}
+		}
+		typeChecked = true;
+	}
+	
+	/**
+	 * Returns the children of this node.
+	 * 
+	 * @return the children of this node. Can never be <code>null</code> or
+	 *         empty.
+	 */
+	public Predicate[] getChildren() {
+		return children.clone();
+	}
+
+	private Operators getOperator() {
+		return Operators.values()[getTag()-FIRST_TAG];
+	}
+
+	private String getOperatorImage() {
+		return getOperator().getImage();
+	}
+
+	@Override
+	protected boolean equalsInternal(Formula<?> formula) {
+		final AssociativePredicate other = (AssociativePredicate) formula;
+		return Arrays.equals(children, other.children);
+	}
+
+	@Override
+	protected void typeCheck(TypeCheckResult result, BoundIdentDecl[] quantifiedIdentifiers) {
+		for (Predicate child: children) {
+			child.typeCheck(result,quantifiedIdentifiers);
+		}
+	}
+	
+	@Override
+	protected void solveChildrenTypes(TypeUnifier unifier) {
+		for (Predicate child: children) {
+			child.solveType(unifier);
+		}
+	}
+
+	@Override
+	protected void toString(IToStringMediator mediator) {
+		final Operators operator = getOperator();
+		final int kind = mediator.getKind();
+		
+		operator.makeParser(kind).toString(mediator, this);
+	}
+
+	@Override
+	protected int getKind(KindMediator mediator) {
+		return mediator.getKind(getOperatorImage());
+	}
+
+	@Override
+	protected String getSyntaxTree(String[] boundNames, String tabs) {
+		return AssociativeHelper
+				.getSyntaxTreeHelper(boundNames, tabs, children,
+						getOperatorImage(), "", this.getClass().getSimpleName());
+	}
+
+	/**
+	 * @since 2.0
+	 */
+	@Override
+	protected void isLegible(LegibilityResult result) {
+		AssociativeHelper.isLegibleList(children, result);
+	}
+
+	@Override
+	protected void collectFreeIdentifiers(LinkedHashSet<FreeIdentifier> freeIdentSet) {
+		for (Predicate child: children) {
+			child.collectFreeIdentifiers(freeIdentSet);
+		}
+	}
+
+	@Override
+	protected void collectNamesAbove(Set<String> names, String[] boundNames, int offset) {
+		for (Predicate child: children) {
+			child.collectNamesAbove(names, boundNames, offset);
+		}
+	}
+
+	@Override
+	public boolean accept(IVisitor visitor) {
+		boolean goOn = true;
+
+		switch (getTag()) {
+		case LAND: goOn = visitor.enterLAND(this); break;
+		case LOR:  goOn = visitor.enterLOR(this);  break;
+		default:   assert false;
+		}
+
+		for (int i = 0; goOn && i < children.length; i++) {
+			if (i != 0) {
+				switch (getTag()) {
+				case LAND: goOn = visitor.continueLAND(this); break;
+				case LOR:  goOn = visitor.continueLOR(this);  break;
+				default:     assert false;
+				}
+			}
+			if (goOn) {
+				goOn = children[i].accept(visitor);
+			}
+		}
+		
+		switch (getTag()) {
+		case LAND: return visitor.exitLAND(this);
+		case LOR:  return visitor.exitLOR(this);
+		default:   assert false; return true;
+		}
+	}
+
+	@Override
+	public void accept(ISimpleVisitor visitor) {
+		visitor.visitAssociativePredicate(this);
+	}
+
+	@Override
+	protected Predicate rewrite(ITypeCheckingRewriter rewriter) {
+		final boolean flatten = rewriter.autoFlatteningMode();
+		final ArrayList<Predicate> newChildren = new ArrayList<Predicate>(
+				children.length + 11);
+		boolean changed = false;
+		for (Predicate child : children) {
+			Predicate newChild = child.rewrite(rewriter);
+			if (flatten && getTag() == newChild.getTag()) {
+				final Predicate[] grandChildren = ((AssociativePredicate) newChild).children;
+				newChildren.addAll(Arrays.asList(grandChildren));
+				changed = true;
+			} else {
+				newChildren.add(newChild);
+				changed |= newChild != child;
+			}
+		}
+		final AssociativePredicate before;
+		if (!changed) {
+			before = this;
+		} else {
+			before = rewriter.getFactory().makeAssociativePredicate(getTag(),
+					newChildren, getSourceLocation());
+		}
+		return rewriter.rewrite(this, before);
+	}
+
+	@Override
+	protected final <F> void inspect(FindingAccumulator<F> acc) {
+		acc.inspect(this);
+		if (acc.childrenSkipped()) {
+			return;
+		}
+		acc.enterChildren();
+		for (Predicate child: children) {
+			child.inspect(acc);
+			if (acc.allSkipped()) {
+				break;
+			}
+			acc.nextChild();
+		}
+		acc.leaveChildren();
+	}
+
+	@Override
+	public Predicate getChild(int index) {
+		checkChildIndex(index);
+		return children[index];
+	}
+
+	@Override
+	public int getChildCount() {
+		return children.length;
+	}
+
+	@Override
+	protected IPosition getDescendantPos(SourceLocation sloc, IntStack indexes) {
+		indexes.push(0);
+		for (Predicate child: children) {
+			IPosition pos = child.getPosition(sloc, indexes);
+			if (pos != null)
+				return pos;
+			indexes.incrementTop();
+		}
+		indexes.pop();
+		return new Position(indexes);
+	}
+
+	@Override
+	protected Predicate rewriteChild(int index, SingleRewriter rewriter) {
+		if (index < 0 || children.length <= index) 
+			throw new IllegalArgumentException("Position is outside the formula");
+		Predicate[] newChildren = children.clone();
+		newChildren[index] = rewriter.rewrite(children[index]);
+		return getFactory().makeAssociativePredicate(
+				getTag(), newChildren, getSourceLocation());
+	}
+
+	@Override
+	public boolean isWDStrict() {
+		return false;
+	}
+
+}

src/org/eventb/core/ast/AtomicExpression.java

+/*******************************************************************************
+ * Copyright (c) 2005, 2013 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
+ * http://www.eclipse.org/legal/epl-v10.html
+ *
+ * Contributors:
+ *     ETH Zurich - initial API and implementation
+ *     Systerel - added accept for ISimpleVisitor
+ *     Systerel - mathematical language v2
+ *     Systerel - added support for predicate variables
+ *     Systerel - generalised getPositions() into inspect()
+ *     Systerel - externalized wd lemmas generation
+ *     Systerel - added child indexes
+ *     Systerel - add given sets to free identifier cache
+ *     Systerel - store factory used to build a formula
+ *******************************************************************************/
+package org.eventb.core.ast;
+
+import static org.eventb.core.ast.extension.StandardGroup.ATOMIC_EXPR;
+import static org.eventb.internal.core.ast.FormulaChecks.ensureHasType;
+import static org.eventb.internal.core.ast.FormulaChecks.ensureTagInRange;
+import static org.eventb.internal.core.ast.GivenTypeHelper.getGivenTypeIdentifiers;
+
+import java.util.LinkedHashSet;
+import java.util.Set;
+
+import org.eventb.core.ast.extension.StandardGroup;
+import org.eventb.internal.core.ast.FindingAccumulator;
+import org.eventb.internal.core.ast.ITypeCheckingRewriter;
+import org.eventb.internal.core.ast.IntStack;
+import org.eventb.internal.core.ast.LegibilityResult;
+import org.eventb.internal.core.ast.Position;
+import org.eventb.internal.core.ast.extension.IToStringMediator;
+import org.eventb.internal.core.ast.extension.KindMediator;
+import org.eventb.internal.core.parser.BMath;
+import org.eventb.internal.core.parser.GenParser.OverrideException;
+import org.eventb.internal.core.parser.IOperatorInfo;
+import org.eventb.internal.core.parser.IParserPrinter;
+import org.eventb.internal.core.parser.SubParsers.AtomicExpressionParser;
+import org.eventb.internal.core.typecheck.TypeCheckResult;
+import org.eventb.internal.core.typecheck.TypeUnifier;
+import org.eventb.internal.core.typecheck.TypeVariable;
+
+/**
+ * AtomicExpression is the class for all atomic expressions in an event-B
+ * formula.
+ * <p>
+ * It is a terminal expression and therefore has no children. It can only accept
+ * {INTEGER, NATURAL, NATURAL1, BOOL, TRUE, FALSE, EMPTYSET, KPRED, KSUCC,
+ * KPRJ1_GEN, KPRJ2_GEN, KID_GEN}.
+ * </p>
+ * 
+ * @author François Terrier
+ * @since 1.0
+ * @noextend This class is not intended to be subclassed by clients.
+ */
+public class AtomicExpression extends Expression {
+	
+	// offset of the corresponding tag-interval in Formula
+	private static final int FIRST_TAG = FIRST_ATOMIC_EXPRESSION;
+	
+	// For testing purposes
+	public static final int TAGS_LENGTH = Operators.values().length;
+	
+	private static final String INTEGER_ID = "Integer";
+	private static final String NATURAL_ID = "Natural";
+	private static final String NATURAL1_ID = "Natural1";
+	private static final String BOOL_ID = "Bool Type";
+	private static final String TRUE_ID = "True";
+	private static final String FALSE_ID = "False";
+	private static final String EMPTYSET_ID = "Empty Set";
+	private static final String KPRED_ID = "Predecessor";
+	private static final String KSUCC_ID = "Successor";
+	private static final String KPRJ1_GEN_ID = "Projection 1";
+	private static final String KPRJ2_GEN_ID = "Projection 2";
+	private static final String KID_GEN_ID = "Identity";
+
+	private static enum Operators implements IOperatorInfo<AtomicExpression> {
+		OP_INTEGER("\u2124", INTEGER_ID, ATOMIC_EXPR, INTEGER),
+		OP_NATURAL("\u2115", NATURAL_ID, ATOMIC_EXPR, NATURAL),
+		OP_NATURAL1("\u21151", NATURAL1_ID, ATOMIC_EXPR, NATURAL1),
+		OP_BOOL("BOOL", BOOL_ID, ATOMIC_EXPR, BOOL),
+		OP_TRUE("TRUE", TRUE_ID, ATOMIC_EXPR, TRUE),
+		OP_FALSE("FALSE", FALSE_ID, ATOMIC_EXPR, FALSE),
+		OP_EMPTYSET("\u2205", EMPTYSET_ID, ATOMIC_EXPR, EMPTYSET),
+		OP_KPRED("pred", KPRED_ID, ATOMIC_EXPR, KPRED),
+		OP_KSUCC("succ", KSUCC_ID, ATOMIC_EXPR, KSUCC),
+		OP_KPRJ1_GEN("prj1", KPRJ1_GEN_ID, ATOMIC_EXPR, KPRJ1_GEN),
+		OP_KPRJ2_GEN("prj2", KPRJ2_GEN_ID, ATOMIC_EXPR, KPRJ2_GEN),
+		OP_KID_GEN("id", KID_GEN_ID, ATOMIC_EXPR, KID_GEN),
+		;
+		
+		private final String image;
+		private final String id;
+		private final String groupId;
+		private final int tag;
+		
+		private Operators(String image, String id, StandardGroup group, int tag) {
+			this.image = image;
+			this.id = id;
+			this.groupId = group.getId();
+			this.tag = tag;
+		}
+
+		@Override
+		public String getImage() {
+			return image;
+		}
+		
+		@Override
+		public String getId() {
+			return id;
+		}
+		
+		@Override
+		public String getGroupId() {
+			return groupId;
+		}
+
+		@Override
+		public IParserPrinter<AtomicExpression> makeParser(int kind) {
+			return new AtomicExpressionParser(kind, tag);
+		}
+
+		@Override
+		public boolean isSpaced() {
+			return false;
+		}
+	}
+	
+	/**
+	 * @since 2.0
+	 */
+	public static void initV1(BMath grammar) {
+		try {
+			grammar.addOperator(Operators.OP_INTEGER);
+			grammar.addOperator(Operators.OP_NATURAL);
+			grammar.addOperator(Operators.OP_NATURAL1);
+			grammar.addOperator(Operators.OP_BOOL);
+			grammar.addOperator(Operators.OP_TRUE);
+			grammar.addOperator(Operators.OP_FALSE);
+			grammar.addOperator(Operators.OP_EMPTYSET);
+			grammar.addOperator(Operators.OP_KPRED);
+			grammar.addOperator(Operators.OP_KSUCC);
+		} catch (OverrideException e) {
+			// TODO Auto-generated catch block
+			e.printStackTrace();
+		}
+		
+	}
+
+	/**
+	 * @since 2.0
+	 */
+	public static void initV2(BMath grammar) {
+		try {
+			initV1(grammar);
+			grammar.addOperator(Operators.OP_KPRJ1_GEN);
+			grammar.addOperator(Operators.OP_KPRJ2_GEN);
+			grammar.addOperator(Operators.OP_KID_GEN);
+		} catch (OverrideException e) {
+			// TODO Auto-generated catch block
+			e.printStackTrace();
+		}
+	}
+
+	/**
+	 * Must never be called directly: use the factory method instead.
+	 * 
+	 * @see FormulaFactory#makeAtomicExpression(int, SourceLocation)
+	 * @see FormulaFactory#makeAtomicExpression(int, SourceLocation, Type)
+	 */
+	protected AtomicExpression(int tag, SourceLocation location, Type type,
+			FormulaFactory ff) {
+		super(tag, ff, location, 0);
+		ensureTagInRange(tag, FIRST_TAG, TAGS_LENGTH);
+		ensureSameFactory(type);
+		setPredicateVariableCache();
+		synthesizeType(type);
+		ensureHasType(this, type);
+	}
+	
+	@Override
+	protected void synthesizeType(Type givenType) {
+		// May change at the end of this method
+		this.freeIdents = NO_FREE_IDENT;
+		this.boundIdents = NO_BOUND_IDENT;
+
+		final FormulaFactory ff = getFactory();
+		final Type resultType;
+		switch (getTag()) {
+		case Formula.INTEGER:
+		case Formula.NATURAL:
+		case Formula.NATURAL1:
+			resultType = ff.makePowerSetType(ff.makeIntegerType());
+			break;
+		case Formula.BOOL:
+			resultType = ff.makePowerSetType(ff.makeBooleanType());
+			break;
+		case Formula.TRUE:
+		case Formula.FALSE:
+			resultType = ff.makeBooleanType();
+			break;
+		case Formula.EMPTYSET:
+			if (!isEmptySetType(givenType)) {
+				return;
+			}
+			resultType = givenType;
+			break;
+		case Formula.KPRED:
+		case Formula.KSUCC:
+			resultType = ff.makeRelationalType(
+					ff.makeIntegerType(),
+					ff.makeIntegerType()
+			);
+			break;
+		case Formula.KPRJ1_GEN:
+			if (!isPrjType(givenType, true)) {
+				return;
+			}
+			resultType = givenType;
+			break;
+		case Formula.KPRJ2_GEN:
+			if (!isPrjType(givenType, false)) {
+				return;
+			}
+			resultType = givenType;
+			break;
+		case Formula.KID_GEN:
+			if (!isIdType(givenType)) {
+				return;
+			}
+			resultType = givenType;
+			break;
+		default:
+			assert false;
+			return;
+		}
+		if (resultType != null) {
+			this.freeIdents = getGivenTypeIdentifiers(resultType);
+			setFinalType(resultType, givenType);
+		}
+	}
+
+	private boolean isEmptySetType(Type proposedType) {
+		return proposedType instanceof PowerSetType;
+	}
+
+	private static boolean isPrjType(Type proposedType, boolean left) {
+		if (proposedType == null) {
+			// Type not specified
+			return false;
+		}
+		final Type source = proposedType.getSource();
+		final Type target = proposedType.getTarget();
+		if (!(source instanceof ProductType)) {
+			// Wrong shape of type
+			return false;
+		}
+		final ProductType pSource = (ProductType) source;
+		final Type child = left ? pSource.getLeft() : pSource.getRight();
+		return child.equals(target);
+	}
+
+	private static boolean isIdType(Type proposedType) {
+		if (proposedType == null) {
+			// Type not specified
+			return false;
+		}
+		final Type source = proposedType.getSource();
+		final Type target = proposedType.getTarget();
+		return source != null && source.equals(target);
+	}
+
+	/**
+	 * @since 2.0
+	 */
+	@Override
+	protected void isLegible(LegibilityResult result) {
+		return;
+	}
+
+	@Override
+	boolean equalsInternalExpr(Expression expr) {
+		return true;
+	}
+
+	@Override
+	protected void typeCheck(TypeCheckResult result,
+			BoundIdentDecl[] quantifiedIdentifiers) {
+
+		final TypeVariable alpha, beta;
+		final Type srcType;
+		final Type resultType;
+		switch (getTag()) {
+		case Formula.INTEGER:
+		case Formula.NATURAL:
+		case Formula.NATURAL1:
+			resultType = result.makePowerSetType(result.makeIntegerType());
+			break;
+		case Formula.BOOL:
+			resultType = result.makePowerSetType(result.makeBooleanType());
+			break;
+		case Formula.TRUE:
+		case Formula.FALSE:
+			resultType = result.makeBooleanType();
+			break;
+		case Formula.EMPTYSET:
+			alpha = result.newFreshVariable(getSourceLocation());
+			resultType = result.makePowerSetType(alpha);
+			break;
+		case Formula.KPRED:
+		case Formula.KSUCC:
+			resultType = result.makeRelationalType(
+					result.makeIntegerType(),
+					result.makeIntegerType()
+			);
+			break;
+		case Formula.KPRJ1_GEN:
+			alpha = result.newFreshVariable(getSourceLocation());
+			beta = result.newFreshVariable(getSourceLocation());
+			srcType = result.makeProductType(alpha, beta);
+			resultType = result.makeRelationalType(srcType, alpha);
+			break;
+		case Formula.KPRJ2_GEN:
+			alpha = result.newFreshVariable(getSourceLocation());
+			beta = result.newFreshVariable(getSourceLocation());
+			srcType = result.makeProductType(alpha, beta);
+			resultType = result.makeRelationalType(srcType, beta);
+			break;
+		case Formula.KID_GEN:
+			alpha = result.newFreshVariable(getSourceLocation());
+			resultType = result.makeRelationalType(alpha, alpha);
+			break;
+		default:
+			assert false;
+			return;
+		}
+		setTemporaryType(resultType, result);
+		result.analyzeExpression(this);
+	}
+	
+	@Override
+	protected void solveChildrenTypes(TypeUnifier unifier) {
+		// No child
+	}
+
+	@Override
+	protected void toString(IToStringMediator mediator) {
+		final Operators operator = getOperator();
+		final int kind = mediator.getKind();
+		
+		operator.makeParser(kind).toString(mediator, this);
+	}
+
+	@Override
+	protected int getKind(KindMediator mediator) {
+		return mediator.getKind(getOperatorImage());
+	}
+
+	private String getOperatorImage() {
+		return getOperator().getImage();
+	}
+
+	private Operators getOperator() {
+		return Operators.values()[getTag()-FIRST_TAG];
+	}
+
+	@Override
+	protected String getSyntaxTree(String[] boundNames, String tabs) {
+		final String typeName = getType()!=null?" [type: "+getType().toString()+"]":"";
+		return tabs + this.getClass().getSimpleName() + " ["
+				+ getOperatorImage() + "]"  + typeName + "\n";
+	}
+
+	@Override
+	protected void collectFreeIdentifiers(LinkedHashSet<FreeIdentifier> freeIdentSet) {
+		// Nothing to do
+	}
+
+	@Override
+	protected void collectNamesAbove(Set<String> names, String[] boundNames, int offset) {
+		// Nothing to do
+	}
+	
+	@Override
+	public boolean accept(IVisitor visitor) {
+		switch (getTag()) {
+		case INTEGER:  return visitor.visitINTEGER(this);
+		case NATURAL:  return visitor.visitNATURAL(this);
+		case NATURAL1: return visitor.visitNATURAL1(this);
+		case BOOL:     return visitor.visitBOOL(this);
+		case TRUE:     return visitor.visitTRUE(this);
+		case FALSE:    return visitor.visitFALSE(this);
+		case EMPTYSET: return visitor.visitEMPTYSET(this);
+		case KPRED:    return visitor.visitKPRED(this);
+		case KSUCC:    return visitor.visitKSUCC(this);
+		case KPRJ1_GEN:return visitor.visitKPRJ1_GEN(this);
+		case KPRJ2_GEN:return visitor.visitKPRJ2_GEN(this);
+		case KID_GEN:  return visitor.visitKID_GEN(this);
+		default:       return true;
+		}
+	}
+
+	@Override
+	public void accept(ISimpleVisitor visitor) {
+		visitor.visitAtomicExpression(this);
+	}
+
+	@Override
+	protected Expression rewrite(ITypeCheckingRewriter rewriter) {
+		return rewriter.rewrite(this);
+	}
+
+	@Override
+	public boolean isATypeExpression() {
+		int tag = getTag();
+		return tag == INTEGER || tag == BOOL;
+	}
+
+	@Override
+	public Type toType() {
+		final FormulaFactory factory = getFactory();
+		switch (getTag()) {
+		case INTEGER:
+			return factory.makeIntegerType();
+		case BOOL:
+			return factory.makeBooleanType();
+		default:
+			return super.toType();
+		}
+	}
+
+	@Override
+	protected final <F> void inspect(FindingAccumulator<F> acc) {
+		acc.inspect(this);
+		if (acc.childrenSkipped()) {
+			return;
+		}
+	}
+
+	@Override
+	public Formula<?> getChild(int index) {
+		throw invalidIndex(index);
+	}
+
+	@Override
+	public int getChildCount() {
+		return 0;
+	}
+
+	@Override
+	protected IPosition getDescendantPos(SourceLocation sloc, IntStack indexes) {
+		return new Position(indexes);
+	}
+
+	@Override
+	protected Expression rewriteChild(int index, SingleRewriter rewriter) {
+		throw new IllegalArgumentException("Position is outside the formula");
+	}
+
+	@Override
+	public boolean isWDStrict() {
+		return true;
+	}
+
+}

src/org/eventb/core/ast/BecomesEqualTo.java

+/*******************************************************************************
+ * Copyright (c) 2005, 2013 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
+ * http://www.eclipse.org/legal/epl-v10.html
+ *
+ * Contributors:
+ *     ETH Zurich - initial API and implementation
+ *     Systerel - added accept for ISimpleVisitor
+ *     Systerel - added support for predicate variables
+ *     Systerel - externalized wd lemmas generation
+ *     Systerel - add given sets to free identifier cache
+ *     Systerel - store factory used to build a formula
+ *******************************************************************************/
+package org.eventb.core.ast;
+
+import static org.eventb.core.ast.extension.StandardGroup.INFIX_SUBST;
+import static org.eventb.internal.core.ast.FormulaChecks.ensureSameLength;
+
+import java.util.Arrays;
+import java.util.LinkedHashSet;
+import java.util.Set;
+
+import org.eventb.internal.core.ast.IdentListMerger;
+import org.eventb.internal.core.ast.LegibilityResult;
+import org.eventb.internal.core.ast.extension.IToStringMediator;
+import org.eventb.internal.core.ast.extension.KindMediator;
+import org.eventb.internal.core.parser.BMath;
+import org.eventb.internal.core.parser.GenParser.OverrideException;
+import org.eventb.internal.core.parser.IOperatorInfo;
+import org.eventb.internal.core.parser.IParserPrinter;
+import org.eventb.internal.core.parser.MainParsers;
+import org.eventb.internal.core.typecheck.TypeCheckResult;
+import org.eventb.internal.core.typecheck.TypeUnifier;
+
+/**
+ * Implements the deterministic assignment, where an expression is given for
+ * each assigned identifier.
+ * 
+ * @author Laurent Voisin
+ * @since 1.0
+ * @noextend This class is not intended to be subclassed by clients.
+ */
+public class BecomesEqualTo extends Assignment {
+
+	private static final String BECEQ_ID = "Becomes Equal To";
+	
+	/**
+	 * @since 2.0
+	 */
+	public static final IOperatorInfo<BecomesEqualTo> OP_BECEQ = new IOperatorInfo<BecomesEqualTo>() {
+		
+		@Override
+		public IParserPrinter<BecomesEqualTo> makeParser(int kind) {
+			return new MainParsers.BecomesEqualToParser(kind);
+		}
+
+		@Override
+		public String getImage() {
+			return "\u2254";
+		}
+		
+		@Override
+		public String getId() {
+			return BECEQ_ID;
+		}
+		
+		@Override
+		public String getGroupId() {
+			return INFIX_SUBST.getId();
+		}
+		
+		@Override
+		public boolean isSpaced() {
+			return true;
+		}
+	};
+
+	/**
+	 * @since 2.0
+	 */
+	public static void init(BMath grammar) {
+		try {		
+			grammar.addOperator(OP_BECEQ);
+		} catch (OverrideException e) {
+			// TODO Auto-generated catch block
+			e.printStackTrace();
+		}
+	}
+	
+	private final Expression[] values;
+	
+	/**
+	 * Must never be called directly: use the factory method instead.
+	 * 
+	 * @see FormulaFactory#makeBecomesEqualTo(FreeIdentifier, Expression,
+	 *      SourceLocation)
+	 * @see FormulaFactory#makeBecomesEqualTo(FreeIdentifier[], Expression[],
+	 *      SourceLocation)
+	 * @see FormulaFactory#makeBecomesEqualTo(java.util.Collection,
+	 *      java.util.Collection, SourceLocation)
+	 */
+	protected BecomesEqualTo(FreeIdentifier[] assignedIdents, Expression[] values,
+			SourceLocation location, FormulaFactory ff) {
+		super(BECOMES_EQUAL_TO, ff, location, combineHashCodes(values), assignedIdents);
+		this.values = values;
+		ensureSameLength(assignedIdents, values);
+		ensureSameFactory(this.values);
+		setPredicateVariableCache(this.values);
+		synthesizeType();
+	}
+
+	@Override
+	protected void synthesizeType() {
+		final int length = assignedIdents.length;
+		final Expression[] children = new Expression[length * 2];
+		System.arraycopy(assignedIdents, 0, children, 0, length);
+		System.arraycopy(values, 0, children, length, length);
+		
+		IdentListMerger freeIdentMerger = mergeFreeIdentifiers(children);
+		this.freeIdents = freeIdentMerger.getFreeMergedArray();
+
+		IdentListMerger boundIdentMerger = mergeBoundIdentifiers(children);
+		this.boundIdents = boundIdentMerger.getBoundMergedArray();
+
+		if (freeIdentMerger.containsError() || boundIdentMerger.containsError()) {
+			// Incompatible type environments, don't bother going further.
+			return;
+		}
+
+		// Check equality of types
+		for (int i = 0; i < length; i++) {
+			final Type type = assignedIdents[i].getType();
+			if (type == null || ! type.equals(values[i].getType())) {
+				return;
+			}
+		}
+		typeChecked = true;
+	}
+	
+	/**
+	 * Returns the expressions that occur in the right-hand side of this
+	 * assignment.
+	 * 
+	 * @return an array containing the expressions on the right-hand side of
+	 *         this assignment
+	 */
+	public Expression[] getExpressions() {
+		return values.clone();
+	}
+
+	@Override
+	protected void collectFreeIdentifiers(LinkedHashSet<FreeIdentifier> freeIdentSet) {
+		for (FreeIdentifier ident: assignedIdents) {
+			ident.collectFreeIdentifiers(freeIdentSet);
+		}
+		for (Expression value: values) {
+			value.collectFreeIdentifiers(freeIdentSet);
+		}
+	}
+
+	@Override
+	protected void collectNamesAbove(Set<String> names, String[] boundNames,
+			int offset) {
+		
+		for (FreeIdentifier ident: assignedIdents) {
+			ident.collectNamesAbove(names, boundNames, offset);
+		}
+		for (Expression value: values) {
+			value.collectNamesAbove(names, boundNames, offset);
+		}
+	}
+	
+	private String getOperatorImage() {
+		return OP_BECEQ.getImage();
+	}
+
+	@Override
+	protected void toString(IToStringMediator mediator) {
+		final int kind = mediator.getKind();
+		OP_BECEQ.makeParser(kind).toString(mediator, this);
+	}
+
+	@Override
+	protected int getKind(KindMediator mediator) {
+		return mediator.getKind(getOperatorImage());
+	}
+
+	/* (non-Javadoc)
+	 * @see org.eventb.core.ast.Formula#getSyntaxTree(java.lang.String[], java.lang.String)
+	 */
+	@Override
+	protected String getSyntaxTree(String[] boundNames, String tabs) {
+		final String childTabs = tabs + '\t';
+		
+		final StringBuilder result = new StringBuilder();
+		result.append(tabs);
+		result.append(this.getClass().getSimpleName());
+		result.append(" [:=]\n");
+		for (FreeIdentifier ident: assignedIdents) {
+			result.append(ident.getSyntaxTree(boundNames, childTabs));
+		}
+		for (Expression value: values) {
+			result.append(value.getSyntaxTree(boundNames, childTabs));
+		}
+		return result.toString();
+	}
+
+	@Override
+	protected boolean equalsInternal(Formula<?> formula) {
+		final BecomesEqualTo other = (BecomesEqualTo) formula;
+		return this.hasSameAssignedIdentifiers(other)
+				&& Arrays.equals(values, other.values);
+	}
+
+	@Override
+	protected void typeCheck(TypeCheckResult result, BoundIdentDecl[] boundAbove) {
+		for (int i = 0; i < values.length; i++) {
+			assignedIdents[i].typeCheck(result, boundAbove);
+			values[i].typeCheck(result, boundAbove);
+			result.unify(assignedIdents[i].getType(), values[i].getType(), this);
+		}
+	}
+
+	@Override
+	protected void isLegible(LegibilityResult result) {
+		for (FreeIdentifier ident: assignedIdents) {
+			ident.isLegible(result);
+		}
+		for (Expression value: values) {
+			value.isLegible(result);
+		}
+	}
+
+	@Override
+	protected void solveChildrenTypes(TypeUnifier unifier) {
+		for (Expression value: values) {
+			value.solveType(unifier);
+		}
+	}
+
+	@Override
+	public boolean accept(IVisitor visitor) {
+		boolean goOn = visitor.enterBECOMES_EQUAL_TO(this);
+
+		for (int i = 0; goOn && i < assignedIdents.length; ++i) {
+			goOn = assignedIdents[i].accept(visitor);
+			if (goOn) {
+				goOn = visitor.continueBECOMES_EQUAL_TO(this);
+			}
+		}
+		
+		for (int i = 0; goOn && i < values.length; i++) {
+			if (i != 0) {
+				goOn = visitor.continueBECOMES_EQUAL_TO(this);
+			}
+			if (goOn) {
+				goOn = values[i].accept(visitor);
+			}
+		}
+
+		return visitor.exitBECOMES_EQUAL_TO(this);
+	}
+
+	@Override
+	public void accept(ISimpleVisitor visitor) {
+		visitor.visitBecomesEqualTo(this);
+	}
+
+	@Override
+	protected Predicate getFISPredicateRaw() {
+		return getFactory().makeLiteralPredicate(BTRUE, getSourceLocation());
+	}
+
+	@Override
+	protected Predicate getBAPredicateRaw() {
+		final FormulaFactory ff = getFactory();
+		final SourceLocation loc = getSourceLocation();
+		final int length = assignedIdents.length;
+		final Predicate[] predicates = new Predicate[length];
+		for (int i=0; i<length; i++) {
+			predicates[i] = 
+				ff.makeRelationalPredicate(EQUAL, 
+						assignedIdents[i].withPrime(),
+						values[i], 
+						loc);
+		}
+		if (predicates.length > 1)
+			return ff.makeAssociativePredicate(LAND, predicates, loc);
+		else
+			return predicates[0];
+	}
+
+	@Override
+	public FreeIdentifier[] getUsedIdentifiers() {
+		if (values.length == 1) {
+			return values[0].getFreeIdentifiers();
+		}
+
+		// More than one value, we need to merge the free identifiers of every
+		// child
+		IdentListMerger freeIdentMerger = mergeFreeIdentifiers(values);
+		FreeIdentifier[] idents = freeIdentMerger.getFreeMergedArray();
+
+		// Need to clone the array, as it can be maximal for one child (and then
+		// we would expose an internal array to clients)
+		return idents.clone();
+	}
+
+	@Override
+	public boolean isWDStrict() {
+		return true;
+	}
+
+}

src/org/eventb/core/ast/BecomesMemberOf.java

+/*******************************************************************************
+ * Copyright (c) 2005, 2013 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
+ * http://www.eclipse.org/legal/epl-v10.html
+ *
+ * Contributors:
+ *     ETH Zurich - initial API and implementation
+ *     Systerel - added accept for ISimpleVisitor
+ *     Systerel - added support for predicate variables
+ *     Systerel - externalized wd lemmas generation
+ *     Systerel - add given sets to free identifier cache
+ *     Systerel - store factory used to build a formula
+ *******************************************************************************/
+package org.eventb.core.ast;
+
+import static org.eventb.core.ast.extension.StandardGroup.INFIX_SUBST;
+
+import java.util.LinkedHashSet;
+import java.util.Set;
+
+import org.eventb.internal.core.ast.IdentListMerger;
+import org.eventb.internal.core.ast.LegibilityResult;
+import org.eventb.internal.core.ast.extension.IToStringMediator;
+import org.eventb.internal.core.ast.extension.KindMediator;
+import org.eventb.internal.core.parser.BMath;
+import org.eventb.internal.core.parser.GenParser.OverrideException;
+import org.eventb.internal.core.parser.IOperatorInfo;
+import org.eventb.internal.core.parser.IParserPrinter;
+import org.eventb.internal.core.parser.MainParsers;
+import org.eventb.internal.core.typecheck.TypeCheckResult;
+import org.eventb.internal.core.typecheck.TypeUnifier;
+
+/**
+ * Implements the set-based assignment, where a set expression is given for
+ * the assigned identifier.
+ * 
+ * @author Laurent Voisin
+ * @since 1.0
+ * @noextend This class is not intended to be subclassed by clients.
+ */
+public class BecomesMemberOf extends Assignment {
+
+	private static final String BECMO_ID = "Becomes Member Of";
+
+	/**
+	 * @since 2.0
+	 */
+	public static final IOperatorInfo<BecomesMemberOf> OP_BECMO = new IOperatorInfo<BecomesMemberOf>() {
+		
+		@Override
+		public IParserPrinter<BecomesMemberOf> makeParser(int kind) {
+			return new MainParsers.BecomesMemberOfParser(kind);
+		}
+
+		@Override
+		public String getImage() {
+			return ":\u2208";
+		}
+		
+		@Override
+		public String getId() {
+			return BECMO_ID;
+		}
+		
+		@Override
+		public String getGroupId() {
+			return INFIX_SUBST.getId();
+		}
+
+		@Override
+		public boolean isSpaced() {
+			return true;
+		}
+	};
+
+	/**
+	 * @since 2.0
+	 */
+	public static void init(BMath grammar) {
+		try {		
+			grammar.addOperator(OP_BECMO);
+		} catch (OverrideException e) {
+			// TODO Auto-generated catch block
+			e.printStackTrace();
+		}
+	}
+	
+	private final Expression setExpr;
+	
+	/**
+	 * Must never be called directly: use the factory method instead.
+	 * 
+	 * @see FormulaFactory#makeBecomesMemberOf(FreeIdentifier, Expression,
+	 *      SourceLocation)
+	 */
+	protected BecomesMemberOf(FreeIdentifier assignedIdent, Expression setExpr,
+			SourceLocation location, FormulaFactory ff) {
+		super(BECOMES_MEMBER_OF, ff, location, setExpr.hashCode(),
+				new FreeIdentifier[] { assignedIdent });
+		this.setExpr = setExpr;
+		ensureSameFactory(this.setExpr);
+		setPredicateVariableCache(this.setExpr);
+		synthesizeType();
+	}
+
+	@Override
+	protected void synthesizeType() {
+		// assignedIdents contains only one element since it is guaranteed by
+		// constructor
+		IdentListMerger freeIdentMerger = IdentListMerger.makeMerger(
+					assignedIdents[0].freeIdents, setExpr.freeIdents);
+		this.freeIdents = freeIdentMerger.getFreeMergedArray();
+
+		IdentListMerger boundIdentMerger = IdentListMerger.makeMerger(
+					assignedIdents[0].boundIdents, setExpr.boundIdents);
+		this.boundIdents = boundIdentMerger.getBoundMergedArray();
+
+		if (freeIdentMerger.containsError() || boundIdentMerger.containsError()) {
+			// Incompatible type environments, don't bother going further.
+			return;
+		}
+
+		if (! setExpr.isTypeChecked())
+			return;
+
+		// Check equality of types
+		final Type type = assignedIdents[0].getType();
+		if (type == null || ! type.equals(setExpr.getType().getBaseType())) {
+			return;
+		}
+		typeChecked = true;
+	}
+
+	/**
+	 * Returns the set that occurs in the right-hand side of this assignment.
+	 * 
+	 * @return the set on the right-hand side of this assignment
+	 */
+	public Expression getSet() {
+		return setExpr;
+	}
+
+	@Override
+	protected void collectFreeIdentifiers(LinkedHashSet<FreeIdentifier> freeIdentSet) {
+		for (FreeIdentifier ident: assignedIdents) {
+			ident.collectFreeIdentifiers(freeIdentSet);
+		}
+		setExpr.collectFreeIdentifiers(freeIdentSet);
+	}
+
+	@Override
+	protected void collectNamesAbove(Set<String> names, String[] boundNames,
+			int offset) {
+
+		for (FreeIdentifier ident: assignedIdents) {
+			ident.collectNamesAbove(names, boundNames, offset);
+		}
+		setExpr.collectNamesAbove(names, boundNames, offset);
+	}
+
+	@Override
+	protected void toString(IToStringMediator mediator) {
+		final int kind = mediator.getKind();
+		OP_BECMO.makeParser(kind).toString(mediator, this);
+	}
+
+	@Override
+	protected int getKind(KindMediator mediator) {
+		return mediator.getKind(OP_BECMO.getImage());
+	}
+
+	@Override
+	protected String getSyntaxTree(String[] boundNames, String tabs) {
+		final String childTabs = tabs + '\t';
+		
+		final StringBuilder result = new StringBuilder();
+		result.append(tabs);
+		result.append(this.getClass().getSimpleName());
+		result.append(" [:\u2208]\n");
+		for (FreeIdentifier ident: assignedIdents) {
+			result.append(ident.getSyntaxTree(boundNames, childTabs));
+		}
+		result.append(setExpr.getSyntaxTree(boundNames, childTabs));
+		return result.toString();
+	}
+
+	@Override
+	protected boolean equalsInternal(Formula<?> formula) {
+		final BecomesMemberOf other = (BecomesMemberOf) formula;
+		return this.hasSameAssignedIdentifiers(other)
+				&& setExpr.equals(other.setExpr);
+	}
+
+	@Override
+	protected void typeCheck(TypeCheckResult result, BoundIdentDecl[] boundAbove) {
+		final FreeIdentifier lhs = assignedIdents[0];
+		lhs.typeCheck(result, boundAbove);
+		setExpr.typeCheck(result, boundAbove);
+		result.unify(setExpr.getType(), result.makePowerSetType(lhs.getType()), this);
+	}
+
+	/* (non-Javadoc)
+	 * @see org.eventb.core.ast.Formula#isLegible(org.eventb.internal.core.ast.LegibilityResult, org.eventb.core.ast.BoundIdentDecl[])
+	 */
+	@Override
+	protected void isLegible(LegibilityResult result) {
+		for (FreeIdentifier ident: assignedIdents) {
+			ident.isLegible(result);
+		}
+		setExpr.isLegible(result);
+	}
+
+	@Override
+	protected void solveChildrenTypes(TypeUnifier unifier) {
+		setExpr.solveType(unifier);
+	}
+
+	@Override
+	public boolean accept(IVisitor visitor) {
+		boolean goOn = visitor.enterBECOMES_MEMBER_OF(this);
+
+		if (goOn) {
+			goOn = assignedIdents[0].accept(visitor);
+		}
+		if (goOn) {
+			goOn = visitor.continueBECOMES_MEMBER_OF(this);
+		}
+		if (goOn) {
+			goOn = setExpr.accept(visitor);
+		}
+		return visitor.exitBECOMES_MEMBER_OF(this);
+	}
+
+	@Override
+	public void accept(ISimpleVisitor visitor) {
+		visitor.visitBecomesMemberOf(this);
+	}
+
+
+	@Override
+	protected Predicate getFISPredicateRaw() {
+		final FormulaFactory ff = getFactory();
+		final SourceLocation loc = getSourceLocation();
+		final Expression emptySet = ff.makeEmptySet(setExpr.getType(), null);
+		return ff.makeRelationalPredicate(NOTEQUAL, setExpr, emptySet, loc);
+	}
+
+	@Override
+	protected Predicate getBAPredicateRaw() {
+		final FormulaFactory ff = getFactory();
+		final SourceLocation loc = getSourceLocation();
+		final FreeIdentifier primedIdentifier = 
+			assignedIdents[0].withPrime();
+		return ff.makeRelationalPredicate(IN, primedIdentifier, setExpr, loc);
+	}
+
+	@Override
+	public FreeIdentifier[] getUsedIdentifiers() {
+		return setExpr.getFreeIdentifiers();
+	}
+
+	@Override
+	public boolean isWDStrict() {
+		return true;
+	}
+
+}

src/org/eventb/core/ast/BecomesSuchThat.java

+/*******************************************************************************
+ * Copyright (c) 2005, 2013 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
+ * http://www.eclipse.org/legal/epl-v10.html
+ *
+ * Contributors:
+ *     ETH Zurich - initial API and implementation
+ *     Systerel - added accept for ISimpleVisitor
+ *     Systerel - added support for predicate variables
+ *     Systerel - externalized wd lemmas generation
+ *     Systerel - bug #3574162: AST does not compare bound ident decl types
+ *     Systerel - add given sets to free identifier cache
+ *     Systerel - store factory used to build a formula
+ *******************************************************************************/
+package org.eventb.core.ast;
+
+import static org.eventb.core.ast.QuantifiedHelper.areEqualDecls;
+import static org.eventb.core.ast.QuantifiedHelper.getBoundIdentsAbove;
+import static org.eventb.core.ast.QuantifiedHelper.getSyntaxTreeQuantifiers;
+import static org.eventb.core.ast.QuantifiedUtil.catenateBoundIdentLists;
+import static org.eventb.core.ast.extension.StandardGroup.INFIX_SUBST;
+import static org.eventb.internal.core.ast.FormulaChecks.ensureSameLength;
+
+import java.util.LinkedHashSet;
+import java.util.Set;
+
+import org.eventb.internal.core.ast.BoundIdentSubstitution;
+import org.eventb.internal.core.ast.IdentListMerger;
+import org.eventb.internal.core.ast.LegibilityResult;
+import org.eventb.internal.core.ast.Substitution;
+import org.eventb.internal.core.ast.extension.IToStringMediator;
+import org.eventb.internal.core.ast.extension.KindMediator;
+import org.eventb.internal.core.parser.BMath;
+import org.eventb.internal.core.parser.GenParser.OverrideException;
+import org.eventb.internal.core.parser.IOperatorInfo;
+import org.eventb.internal.core.parser.IParserPrinter;
+import org.eventb.internal.core.parser.MainParsers;
+import org.eventb.internal.core.typecheck.TypeCheckResult;
+import org.eventb.internal.core.typecheck.TypeUnifier;
+
+/**
+ * Implements the most general assignment, where a predicate is given on the
+ * before and after values of assigned identifiers.
+ * <p>
+ * In event-B, the after values of the assigned identifiers are denoted by a
+ * primed identifier whose prefix is the assigned identifier. These primed
+ * identifiers are implemented as bound identifiers, whose (implicit)
+ * declaration is stored in instances of this class.
+ * </p>
+ * <p>
+ * For instance, the assignment <code>x :| x &lt; x'</code> is represented in the
+ * following way:
+ * <ul>
+ * <li>the assigned identifier is <code>x</code>.</li>
+ * <li>the bound primed identifier is <code>x'</code>.</li>
+ * <li>the condition is <code>x &lt; [[0]]</code>, where <code>[[0]]</code>
+ * denotes an occurrence of the bound identifier <code>x'</code>.</li>
+ * </ul>
+ * 
+ * @author Laurent Voisin
+ * @since 1.0
+ * @noextend This class is not intended to be subclassed by clients.
+ */
+public class BecomesSuchThat extends Assignment {
+
+	private static final String BECST_ID = "Becomes Such That";
+	
+	/**
+	 * @since 2.0
+	 */
+	public static final IOperatorInfo<BecomesSuchThat> OP_BECST = new IOperatorInfo<BecomesSuchThat>() {
+		
+		@Override
+		public IParserPrinter<BecomesSuchThat> makeParser(int kind) {
+			return new MainParsers.BecomesSuchThatParser(kind);
+		}
+
+		@Override
+		public String getImage() {
+			return ":\u2223";
+		}
+		
+		@Override
+		public String getId() {
+			return BECST_ID;
+		}
+		
+		@Override
+		public String getGroupId() {
+			return INFIX_SUBST.getId();
+		}
+
+		@Override
+		public boolean isSpaced() {
+			return true;
+		}
+	};
+
+	/**
+	 * @since 2.0
+	 */
+	public static void init(BMath grammar) {
+		try {
+			grammar.addOperator(OP_BECST);
+		} catch (OverrideException e) {
+			// TODO Auto-generated catch block
+			e.printStackTrace();
+		}
+	}
+	
+	// Quantified primed identifiers
+	private BoundIdentDecl[] primedIdents;
+	
+	// Post-condition of this assignment
+	private final Predicate condition;
+	
+	/**
+	 * Must never be called directly: use the factory method instead.
+	 * 
+	 * @see FormulaFactory#makeBecomesSuchThat(FreeIdentifier, BoundIdentDecl,
+	 *      Predicate, SourceLocation)
+	 * @see FormulaFactory#makeBecomesSuchThat(FreeIdentifier[],
+	 *      BoundIdentDecl[], Predicate, SourceLocation)
+	 * @see FormulaFactory#makeBecomesSuchThat(java.util.Collection,
+	 *      java.util.Collection, Predicate, SourceLocation)
+	 */
+	protected BecomesSuchThat(FreeIdentifier[] assignedIdents,
+			BoundIdentDecl[] primedIdents, Predicate condition,
+			SourceLocation location,
+			FormulaFactory ff) {
+		// Note: primedIdents must not be part of hash-code as their name is
+		// not relevant for equality
+		super(Formula.BECOMES_SUCH_THAT, ff, location, condition.hashCode(), assignedIdents);
+		this.condition = condition;
+		this.primedIdents = primedIdents;
+		ensureSameLength(assignedIdents, primedIdents);
+		ensureSameFactory(this.primedIdents);
+		ensureSameFactory(this.condition);
+		setPredicateVariableCache(this.condition);
+		synthesizeType();
+	}
+
+	@Override
+	protected void synthesizeType() {
+		final int length = assignedIdents.length;
+		final Formula<?>[] children = new Formula[2 * length + 1];
+		System.arraycopy(assignedIdents, 0, children, 0, length);
+		System.arraycopy(primedIdents, 0, children, length, length);
+		children[2 * length] = condition;
+		
+		IdentListMerger freeIdentMerger = mergeFreeIdentifiers(children);
+		this.freeIdents = freeIdentMerger.getFreeMergedArray();
+
+		final BoundIdentifier[] boundIdentsBelow = condition.boundIdents; 
+		this.boundIdents = getBoundIdentsAbove(boundIdentsBelow, primedIdents,
+				getFactory());
+
+		if (freeIdentMerger.containsError()) {
+			// Incompatible type environments, don't bother going further.
+			return;
+		}
+		
+		if (! condition.isTypeChecked()) {
+			return;
+		}
+
+		// Check equality of types
+		for (int i = 0; i < length; i++) {
+			final Type type = assignedIdents[i].getType();
+			if (type == null || ! type.equals(primedIdents[i].getType())) {
+				return;
+			}
+		}
+		typeChecked = true;
+	}
+
+	/**
+	 * Returns the declaration of the primed identifiers created for each
+	 * assigned identifier.
+	 * 
+	 * @return an array of bound identifier declaration
+	 */
+	public BoundIdentDecl[] getPrimedIdents() {
+		return primedIdents.clone();
+	}
+
+	/**
+	 * Returns the post-condition that appears in the right-hand side of this
+	 * assignment.
+	 * 
+	 * @return the post-condition of this assignment
+	 */
+	public Predicate getCondition() {
+		return condition;
+	}
+
+	@Override
+	protected void collectFreeIdentifiers(LinkedHashSet<FreeIdentifier> freeIdentSet) {
+		for (FreeIdentifier ident: assignedIdents) {
+			ident.collectFreeIdentifiers(freeIdentSet);
+		}
+		condition.collectFreeIdentifiers(freeIdentSet);
+	}
+
+	@Override
+	protected void collectNamesAbove(Set<String> names, String[] boundNames, int offset) {
+		for (FreeIdentifier ident: assignedIdents) {
+			ident.collectNamesAbove(names, boundNames, offset);
+		}
+		final int newOffset = offset + primedIdents.length;
+		condition.collectNamesAbove(names, boundNames, newOffset);
+	}
+
+	@Override
+	protected void toString(IToStringMediator mediator) {
+		final int kind = mediator.getKind();
+		OP_BECST.makeParser(kind).toString(mediator, this);
+	}
+
+	@Override
+	protected int getKind(KindMediator mediator) {
+		return mediator.getKind(OP_BECST.getImage());
+	}
+
+	@Override
+	protected String getSyntaxTree(String[] boundNames, String tabs) {
+		final String childTabs = tabs + '\t';
+		final String[] boundNamesBelow = catenateBoundIdentLists(boundNames, primedIdents);
+		return tabs
+			+ this.getClass().getSimpleName()
+			+ " [:\u2223]\n"
+		    + getSyntaxTreeLHS(boundNames, childTabs)
+		    + getSyntaxTreeQuantifiers(boundNamesBelow, childTabs, primedIdents)
+		    + condition.getSyntaxTree(boundNamesBelow, childTabs);
+	}
+
+	@Override
+	protected boolean equalsInternal(Formula<?> formula) {
+		final BecomesSuchThat other = (BecomesSuchThat) formula;
+		return hasSameAssignedIdentifiers(other)
+				&& areEqualDecls(primedIdents, other.primedIdents)
+				&& condition.equals(other.condition);
+	}
+
+	@Override
+	protected void typeCheck(TypeCheckResult result, BoundIdentDecl[] boundAbove) {
+		for (int i = 0; i < primedIdents.length; i++) {
+			assignedIdents[i].typeCheck(result, boundAbove);
+			primedIdents[i].typeCheck(result, boundAbove);
+			result.unify(assignedIdents[i].getType(), primedIdents[i].getType(), this);
+		}
+		BoundIdentDecl[] boundBelow = catenateBoundIdentLists(boundAbove, primedIdents);
+		condition.typeCheck(result, boundBelow);
+	}
+
+	@Override
+	protected void isLegible(LegibilityResult result) {
+		for (FreeIdentifier ident: assignedIdents) {
+			ident.isLegible(result);
+		}
+		for (BoundIdentDecl decl: primedIdents) {
+			decl.isLegible(result);
+		}
+		condition.isLegible(result);
+	}
+
+	@Override
+	protected void solveChildrenTypes(TypeUnifier unifier) {
+		for (BoundIdentDecl ident : primedIdents) {
+			ident.solveType(unifier);
+		}
+		condition.solveType(unifier);
+	}
+
+	@Override
+	public boolean accept(IVisitor visitor) {
+		boolean goOn = visitor.enterBECOMES_SUCH_THAT(this);
+
+		for (int i = 0; goOn && i < assignedIdents.length; ++i) {
+			goOn = assignedIdents[i].accept(visitor);
+			if (goOn) {
+				goOn = visitor.continueBECOMES_SUCH_THAT(this);
+			}
+		}
+		
+		for (int i = 0; goOn && i < primedIdents.length; ++i) {
+			goOn = primedIdents[i].accept(visitor);
+			if (goOn) {
+				goOn = visitor.continueBECOMES_SUCH_THAT(this);
+			}
+		}
+		
+		if (goOn) {
+			goOn = condition.accept(visitor);
+		}
+
+		return visitor.exitBECOMES_SUCH_THAT(this);
+	}
+
+	@Override
+	public void accept(ISimpleVisitor visitor) {
+		visitor.visitBecomesSuchThat(this);
+	}
+
+	@Override
+	protected Predicate getFISPredicateRaw() {
+		final SourceLocation loc = getSourceLocation();
+		return QuantifiedHelper.getWDSimplifyQ(getFactory(), EXISTS,
+				primedIdents, condition, loc);
+	}
+
+	@Override
+	protected Predicate getBAPredicateRaw() {
+		final FormulaFactory ff = getFactory();
+		ITypeEnvironmentBuilder typeEnvironment = ff.makeTypeEnvironment();
+		FreeIdentifier[] freshIdents = 
+				typeEnvironment.makeFreshIdentifiers(primedIdents);
+		Substitution subst = 
+			new BoundIdentSubstitution(primedIdents, freshIdents, ff);
+		return condition.rewrite(subst);
+	}
+
+	@Override
+	public FreeIdentifier[] getUsedIdentifiers() {
+		return condition.getFreeIdentifiers();
+	}
+
+	@Override
+	public boolean isWDStrict() {
+		return true;
+	}
+
+}

src/org/eventb/core/ast/BinaryPredicate.java

+/*******************************************************************************
+ * Copyright (c) 2005, 2013 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
+ * http://www.eclipse.org/legal/epl-v10.html
+ *
+ * Contributors:
+ *     ETH Zurich - initial API and implementation
+ *     Systerel - added accept for ISimpleVisitor
+ *     Systerel - added support for predicate variables
+ *     Systerel - generalised getPositions() into inspect()
+ *     Systerel - externalized wd lemmas generation
+ *     Systerel - added child indexes
+ *     Systerel - store factory used to build a formula
+ *******************************************************************************/
+package org.eventb.core.ast;
+
+import static org.eventb.core.ast.extension.StandardGroup.INFIX_PRED;
+import static org.eventb.internal.core.ast.FormulaChecks.ensureTagInRange;
+
+import java.util.LinkedHashSet;
+import java.util.Set;
+
+import org.eventb.core.ast.extension.StandardGroup;
+import org.eventb.internal.core.ast.FindingAccumulator;
+import org.eventb.internal.core.ast.ITypeCheckingRewriter;
+import org.eventb.internal.core.ast.IdentListMerger;
+import org.eventb.internal.core.ast.IntStack;
+import org.eventb.internal.core.ast.LegibilityResult;
+import org.eventb.internal.core.ast.Position;
+import org.eventb.internal.core.ast.extension.IToStringMediator;
+import org.eventb.internal.core.ast.extension.KindMediator;
+import org.eventb.internal.core.parser.BMath;
+import org.eventb.internal.core.parser.GenParser.OverrideException;
+import org.eventb.internal.core.parser.IOperatorInfo;
+import org.eventb.internal.core.parser.IParserPrinter;
+import org.eventb.internal.core.parser.SubParsers.BinaryPredicateParser;
+import org.eventb.internal.core.typecheck.TypeCheckResult;
+import org.eventb.internal.core.typecheck.TypeUnifier;
+
+/**
+ * BinaryPredicate is the base class for all binary predicates in an event-B
+ * formula.
+ * <p>
+ * It can only accept {LIMP, LEQV}.
+ * </p>
+ * 
+ * @author François Terrier
+ * @since 1.0
+ * @noextend This class is not intended to be subclassed by clients.
+ */
+public class BinaryPredicate extends Predicate {
+	
+	// offset of the corresponding tag-interval in Formula
+	private final static int FIRST_TAG = FIRST_BINARY_PREDICATE;
+
+	private static final String LIMP_ID = "Logical Implication";
+	private static final String LEQV_ID = "Equivalent";
+	
+	private static enum Operators implements IOperatorInfo<BinaryPredicate> {
+		OP_LIMP("\u21d2", LIMP_ID, INFIX_PRED, LIMP),
+		OP_LEQV("\u21d4", LEQV_ID, INFIX_PRED, LEQV),
+		;
+		
+		private final String image;
+		private final String id;
+		private final String groupId;
+		private final int tag;
+		
+		private Operators(String image, String id, StandardGroup group, int tag) {
+			this.image = image;
+			this.id = id;
+			this.groupId = group.getId();
+			this.tag = tag;
+		}
+
+		@Override
+		public String getImage() {
+			return image;
+		}
+		
+		@Override
+		public String getId() {
+			return id;
+		}
+		
+		@Override
+		public String getGroupId() {
+			return groupId;
+		}
+
+		@Override
+		public IParserPrinter<BinaryPredicate> makeParser(int kind) {
+			return new BinaryPredicateParser(kind, tag);
+		}
+
+		@Override
+		public boolean isSpaced() {
+			return false;
+		}
+	}
+
+	/**
+	 * @since 2.0
+	 */
+	public static void init(BMath grammar) {
+		try {
+			for(Operators operInfo: Operators.values()) {
+				grammar.addOperator(operInfo);
+			}
+		} catch (OverrideException e) {
+			// TODO Auto-generated catch block
+			e.printStackTrace();
+		}
+	}
+
+	// Left and right children.
+	// Are never null by construction.
+	private final Predicate left;
+	private final Predicate right;
+	
+	// For testing purposes
+	public static final int TAGS_LENGTH = Operators.values().length;
+	
+	/**
+	 * Must never be called directly: use the factory method instead.
+	 * 
+	 * @see FormulaFactory#makeBinaryPredicate(int, Predicate, Predicate,
+	 *      SourceLocation)
+	 */
+	protected BinaryPredicate(Predicate left, Predicate right, int tag,
+			SourceLocation location, FormulaFactory ff) {
+		super(tag, ff, location, combineHashCodes(left.hashCode(), right.hashCode()));
+		this.left = left;
+		this.right = right;
+		ensureTagInRange(tag, FIRST_TAG, TAGS_LENGTH);
+		ensureSameFactory(this.left, this.right);
+		setPredicateVariableCache(this.left, this.right);
+		synthesizeType();
+	}
+	
+	@Override
+	protected void synthesizeType() {
+		IdentListMerger freeIdentMerger = 
+			IdentListMerger.makeMerger(left.freeIdents, right.freeIdents);
+		this.freeIdents = freeIdentMerger.getFreeMergedArray();
+
+		IdentListMerger boundIdentMerger = 
+			IdentListMerger.makeMerger(left.boundIdents, right.boundIdents);
+		this.boundIdents = boundIdentMerger.getBoundMergedArray();
+
+		if (freeIdentMerger.containsError() || boundIdentMerger.containsError()) {
+			// Incompatible type environments, don't bother going further.
+			return;
+		}
+		
+		if (left.isTypeChecked() && right.isTypeChecked()) {
+			typeChecked = true;
+		}
+	}
+
+	private String getOperatorImage() {
+		return getOperator().getImage();
+	}
+
+	private Operators getOperator() {
+		return Operators.values()[getTag()-FIRST_TAG];
+	}
+
+	@Override
+	protected int getKind(KindMediator mediator) {
+		return mediator.getKind(getOperatorImage());
+	}
+	
+	@Override
+	protected boolean equalsInternal(Formula<?> formula) {
+		final BinaryPredicate other = (BinaryPredicate) formula;
+		return left.equals(other.left) && right.equals(other.right);
+	}
+
+	@Override
+	protected void typeCheck(TypeCheckResult result, BoundIdentDecl[] quantifiedIdentifiers) {
+		left.typeCheck(result, quantifiedIdentifiers);
+		right.typeCheck(result, quantifiedIdentifiers);
+	}
+	
+	@Override
+	protected void solveChildrenTypes(TypeUnifier unifier) {
+		left.solveType(unifier);
+		right.solveType(unifier);
+	}
+
+	@Override
+	protected void toString(IToStringMediator mediator) {
+		final Operators operator = getOperator();
+		final int kind = mediator.getKind();
+		
+		operator.makeParser(kind).toString(mediator, this);
+	}
+
+	@Override
+	protected String getSyntaxTree(String[] boundNames, String tabs) {
+		return tabs + this.getClass().getSimpleName() + " [" + getOperatorImage() + "]\n"
+				+ left.getSyntaxTree(boundNames, tabs + "\t")
+				+ right.getSyntaxTree(boundNames, tabs + "\t");
+	}
+
+	/**
+	 * @since 2.0
+	 */
+	@Override
+	protected void isLegible(LegibilityResult result) {
+		left.isLegible(result);
+		right.isLegible(result);
+	}
+
+	/**
+	 * Returns the predicate on the left-hand side of this node.
+	 * 
+	 * @return the predicate on the left-hand side
+	 */
+	public Predicate getLeft() {
+		return left;
+	}
+
+	/**
+	 * Returns the predicate on the right-hand side of this node.
+	 * 
+	 * @return the predicate on the right-hand side
+	 */
+	public Predicate getRight() {
+		return right;
+	}
+
+	@Override
+	protected void collectFreeIdentifiers(LinkedHashSet<FreeIdentifier> freeIdentSet) {
+		left.collectFreeIdentifiers(freeIdentSet);
+		right.collectFreeIdentifiers(freeIdentSet);
+	}
+
+	@Override
+	protected void collectNamesAbove(Set<String> names, String[] boundNames, int offset) {
+		left.collectNamesAbove(names, boundNames, offset);
+		right.collectNamesAbove(names, boundNames, offset);
+	}
+	
+	@Override
+	public boolean accept(IVisitor visitor) {
+		boolean goOn = true;
+
+		switch (getTag()) {
+		case LIMP: goOn = visitor.enterLIMP(this); break;
+		case LEQV: goOn = visitor.enterLEQV(this); break;
+		default:   assert false;
+		}
+
+		if (goOn) goOn = left.accept(visitor);
+		
+		if (goOn) {
+			switch (getTag()) {
+			case LIMP: goOn = visitor.continueLIMP(this); break;
+			case LEQV: goOn = visitor.continueLEQV(this); break;
+			default:   assert false;
+			}
+		}
+		
+		if (goOn) goOn = right.accept(visitor);
+		
+		switch (getTag()) {
+		case LIMP: return visitor.exitLIMP(this);
+		case LEQV: return visitor.exitLEQV(this);
+		default:   return true;
+		}
+	}
+
+	@Override
+	public void accept(ISimpleVisitor visitor) {
+		visitor.visitBinaryPredicate(this);
+	}
+
+	@Override
+	protected Predicate rewrite(ITypeCheckingRewriter rewriter) {
+		final Predicate newLeft = left.rewrite(rewriter);
+		final Predicate newRight = right.rewrite(rewriter);
+		final BinaryPredicate before;
+		if (newLeft == left && newRight == right) {
+			before = this;
+		} else {
+			before = rewriter.getFactory().makeBinaryPredicate(getTag(),
+					newLeft, newRight, getSourceLocation());
+		}
+		return rewriter.rewrite(this, before);
+	}
+
+	@Override
+	protected final <F> void inspect(FindingAccumulator<F> acc) {
+		acc.inspect(this);
+		if (acc.childrenSkipped()) {
+			return;
+		}
+		acc.enterChildren();
+		left.inspect(acc);
+		if (acc.allSkipped()) {
+			return;
+		}
+		acc.nextChild();
+		right.inspect(acc);
+		acc.leaveChildren();
+	}
+
+	@Override
+	public Predicate getChild(int index) {
+		switch (index) {
+		case 0:
+			return left;
+		case 1:
+			return right;
+		default:
+			throw invalidIndex(index);
+		}
+	}
+
+	@Override
+	public int getChildCount() {
+		return 2;
+	}
+
+	@Override
+	protected IPosition getDescendantPos(SourceLocation sloc, IntStack indexes) {
+		IPosition pos;
+		indexes.push(0);
+		pos = left.getPosition(sloc, indexes);
+		if (pos != null)
+			return pos;
+		indexes.incrementTop();
+		pos = right.getPosition(sloc, indexes);
+		if (pos != null)
+			return pos;
+		indexes.pop();
+		return new Position(indexes);
+	}
+
+	@Override
+	protected Predicate rewriteChild(int index, SingleRewriter rewriter) {
+		Predicate newLeft = left;
+		Predicate newRight = right;
+		switch (index) {
+		case 0:
+			newLeft = rewriter.rewrite(left);
+			break;
+		case 1:
+			newRight = rewriter.rewrite(right);
+			break;
+		default:
+			throw new IllegalArgumentException("Position is outside the formula");
+		}
+		return getFactory().makeBinaryPredicate(getTag(), newLeft, newRight,
+				getSourceLocation());
+	}
+
+	@Override
+	public boolean isWDStrict() {
+		return getTag() == LEQV;
+	}
+
+}

src/org/eventb/core/ast/BooleanType.java

+/*******************************************************************************
+ * Copyright (c) 2005, 2013 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
+ * http://www.eclipse.org/legal/epl-v10.html
+ *
+ * Contributors:
+ *     ETH Zurich - initial API and implementation
+ *     Systerel - add type visitor
+ *     Systerel - store factory used to build a type
+ *******************************************************************************/
+package org.eventb.core.ast;
+
+import java.util.Set;
+
+/**
+ * Denotes the predefined boolean type which corresponds to the set of boolean values.
+ * 
+ * @author Laurent Voisin
+ * @since 1.0
+ * @noextend This class is not intended to be subclassed by clients.
+ */
+public class BooleanType extends Type {
+
+	private static String NAME = "BOOL";
+	private static int HASH_CODE = NAME.hashCode();
+	
+	/**
+	 * Must never be called directly: use the factory method instead.
+	 * 
+	 * @see FormulaFactory#makeBooleanType()
+	 * @since 3.0
+	 */
+	protected BooleanType(FormulaFactory ff) {
+		super(ff, true);
+	}
+
+	@Override
+	protected void addGivenTypes(Set<GivenType> set) {
+		// Nothing to do
+	}
+	
+	@Override
+	protected Expression buildExpression(FormulaFactory factory) {
+		return factory.makeAtomicExpression(Formula.BOOL, null);
+	}
+
+	@Override
+	protected void buildString(StringBuilder buffer) {
+		buffer.append(NAME);
+	}
+
+	@Override
+	public boolean equals(Object o) {
+		if (this == o) return true;
+		return (o instanceof BooleanType);
+	}
+	
+	@Override
+	public int hashCode() {
+		return HASH_CODE;
+	}
+
+	@Override
+	public void accept(ITypeVisitor visitor) {
+		visitor.visit(this);
+	}
+
+}