package edu.kit.iti.formal.pse.worthwhile.prover;

import edu.kit.iti.formal.pse.worthwhile.model.ast.Expression;
import edu.kit.iti.formal.pse.worthwhile.model.ast.VariableDeclaration;
import edu.kit.iti.formal.pse.worthwhile.model.ast.VariableReference;

/**
 * Substitute {@link VariableReference}s in an {@link Expression} with another {@link Expression}.
 * 
 * @see VariableReferenceSubstitution#substitute(VariableDeclaration, Expression)
 * @author fabian
 * 
 */
class VariableReferenceSubstitution extends SubstitutionVisitor<Expression> {
	/**
	 * Substitutes occurrences of a {@link VariableDeclaration} in an {@link Expression} with another
	 * <code>Expression</code>.
	 * 
	 * A clone of the <code>substitute</code> is used for substitution.
	 * 
	 * @param expression
	 *                the <code>Expression</code> to search for occurrences of <code>variable</code>
	 * @param variable
	 *                the <code>VariableDeclaration</code> the substituted {@link VariableReference}s have to be
	 *                occurrences of
	 * @param substitute
	 *                the <code>Expression</code> occurrences of <code>variable</code> are substituted with
	 * @return the substituted <code>expression</code>, which differs from the passed <code>expression</code> when
	 *         the <code>expression</code> itself was an occurrence of <code>variable</code>
	 */
	public static Expression substitute(final Expression expression, final VariableDeclaration variable,
	                final Expression substitute) {
		final VariableReferenceSubstitution substitutor = new VariableReferenceSubstitution(variable,
		                substitute);
		expression.accept(substitutor);
		if (substitutor.getFound()) {
			substitutor.setFound(false);
			return substitutor.getSubstitute();
		}
		return expression;
	}

	/**
	 * The {@link VariableDeclaration} the substituted {@link VariableReference}s have to be occurrences of.
	 */
	private VariableDeclaration variable;

	/**
	 * 
	 * @param variable
	 *                the {@link VariableDeclaration} the substituted {@link VariableReference}s have to be
	 *                occurrences of
	 * @param substitute
	 *                the {@link Expression} occurrences of {@link VariableReferenceSubstitution#variable} are
	 *                substituted with
	 */
	VariableReferenceSubstitution(final VariableDeclaration variable, final Expression substitute) {
		super(substitute);
		this.variable = variable;
	}

	@Override
	public void visit(final VariableReference variableReference) {
		if (variableReference.getVariable() == this.variable) {
			this.setFound(true);
		}
	}
}

@@ -248,16 +248,94 @@
 ference;
+%0Aimport edu.kit.iti.formal.pse.worthwhile.model.ast.util.AstNodeCreatorHelper;
 %0A%0A/**%0A *
@@ -2050,16 +2050,170 @@
 iable;%0A%0A
+%09/**%0A%09 * The %7B@link Expression%7D occurrences of %7B@link VariableReferenceSubstitution#variable%7D are substituted with.%0A%09 */%0A%09private Expression substitute;%0A%0A
 %09/**%0A%09 *
@@ -2650,26 +2650,20 @@
 %09%09super(
-substitute
+null
 );%0A%09%09thi
@@ -2685,16 +2685,48 @@
 riable;%0A
+%09%09this.substitute = substitute;%0A
 %09%7D%0A%0A%09@Ov
@@ -2802,63 +2802,389 @@
 %7B%0A%09%09
-if (variableReference.getVariable() == this.variable) %7B
+final VariableDeclaration referencedVariable = variableReference.getVariable();%0A%0A%09%09if (referencedVariable == this.variable) %7B%0A%09%09%09final Expression index = variableReference.getIndex();%0A%09%09%09if (index != null) %7B%0A%09%09%09%09this.setSubstitute(AstNodeCreatorHelper.createArrayFunctionAccess(index,%0A%09%09%09%09                this.substitute));%0A%09%09%09%7D else %7B%0A%09%09%09%09this.setSubstitute(this.substitute);%0A%09%09%09%7D
 %0A%09%09%09

Fix VariableReferenceSubstitution ignores index access