CommonRegularRangeExpression.java

package dev.civl.mc.model.common.expression;

import java.util.Arrays;
import java.util.HashSet;
import java.util.Set;

import dev.civl.mc.model.IF.CIVLSource;
import dev.civl.mc.model.IF.Scope;
import dev.civl.mc.model.IF.expression.ConditionalExpression;
import dev.civl.mc.model.IF.expression.Expression;
import dev.civl.mc.model.IF.expression.RegularRangeExpression;
import dev.civl.mc.model.IF.type.CIVLType;
import dev.civl.mc.model.IF.variable.Variable;
import dev.civl.sarl.IF.SymbolicUniverse;
import dev.civl.sarl.IF.ValidityResult.ResultType;
import dev.civl.sarl.IF.expr.BooleanExpression;
import dev.civl.sarl.IF.expr.NumericExpression;
import dev.civl.sarl.IF.expr.SymbolicExpression;
import dev.civl.sarl.IF.type.SymbolicTupleType;

public class CommonRegularRangeExpression extends CommonExpression
		implements
			RegularRangeExpression {

	private Expression low;
	private Expression high;
	private Expression step;

	public CommonRegularRangeExpression(CIVLSource source, Scope hscope,
			Scope lscope, CIVLType type, Expression low, Expression high,
			Expression step) {
		super(source, hscope, lscope, type);
		this.low = low;
		this.high = high;
		this.step = step;
	}

	@Override
	public ExpressionKind expressionKind() {
		return ExpressionKind.REGULAR_RANGE;
	}

	@Override
	public Set<Variable> variableAddressedOf(Scope scope) {
		Set<Variable> variableSet = new HashSet<>();
		Set<Variable> operandResult = low.variableAddressedOf(scope);

		if (operandResult != null)
			variableSet.addAll(operandResult);
		operandResult = high.variableAddressedOf(scope);
		if (operandResult != null)
			variableSet.addAll(operandResult);
		operandResult = step.variableAddressedOf(scope);
		if (operandResult != null)
			variableSet.addAll(operandResult);
		return variableSet;
	}

	@Override
	public Set<Variable> variableAddressedOf() {
		Set<Variable> variableSet = new HashSet<>();
		Set<Variable> operandResult = low.variableAddressedOf();

		if (operandResult != null)
			variableSet.addAll(operandResult);
		operandResult = high.variableAddressedOf();
		if (operandResult != null)
			variableSet.addAll(operandResult);
		operandResult = step.variableAddressedOf();
		if (operandResult != null)
			variableSet.addAll(operandResult);
		return variableSet;
	}

	@Override
	public Expression getLow() {
		return this.low;
	}

	@Override
	public Expression getHigh() {
		return this.high;
	}

	@Override
	public Expression getStep() {
		return this.step;
	}

	@Override
	public String toString() {
		StringBuffer string = new StringBuffer();

		string.append(low);
		string.append("..");
		string.append(high);
		string.append("#");
		string.append(step);
		return string.toString();
	}

	@Override
	public void calculateConstantValueWork(SymbolicUniverse universe) {
		SymbolicExpression lowValue, highValue, stepValue;
		BooleanExpression claim;
		ResultType validity;
		boolean negativeStep = false;

		low.calculateConstantValue(universe);
		high.calculateConstantValue(universe);
		step.calculateConstantValue(universe);
		lowValue = low.constantValue();
		highValue = high.constantValue();
		stepValue = step.constantValue();
		if (lowValue == null || highValue == null || stepValue == null)
			return;
		claim = universe.equals(universe.zeroInt(), stepValue);
		validity = universe.reasoner(universe.trueExpression()).valid(claim)
				.getResultType();
		if (validity == ResultType.YES)
			return;
		claim = universe.lessThan(universe.zeroInt(),
				(NumericExpression) stepValue);
		validity = universe.reasoner(universe.trueExpression()).valid(claim)
				.getResultType();
		if (validity == ResultType.NO)
			negativeStep = true;
		if (negativeStep) {
			SymbolicExpression tmp = lowValue;

			lowValue = highValue;
			highValue = tmp;
		}
		constantValue = universe.tuple(
				(SymbolicTupleType) this.expressionType
						.getDynamicType(universe),
				Arrays.asList(lowValue, highValue, stepValue));
	}

	@Override
	protected boolean expressionEquals(Expression expression) {
		RegularRangeExpression that = (RegularRangeExpression) expression;

		return this.low.equals(that.getLow())
				&& this.high.equals(that.getHigh())
				&& this.step.equals(that.getStep());
	}

	@Override
	public Expression replaceWith(ConditionalExpression oldExpression,
			Expression newExpression) {
		CommonRegularRangeExpression result = null;
		Expression newLow = low.replaceWith(oldExpression, newExpression);
		Expression newHigh = high.replaceWith(oldExpression, newExpression);
		Expression newStep = step.replaceWith(oldExpression, newExpression);

		if (newLow != null || newHigh != null || newStep != null) {
			return new CommonRegularRangeExpression(getSource(),
					expressionScope(), lowestScope(), expressionType,
					newLow != null ? newLow : low,
					newHigh != null ? newHigh : high,
					newStep != null ? newStep : step);
		}
		return result;
	}

	@Override
	protected void addFreeVariables(Set<Variable> result) {
		if (high != null)
			((CommonExpression) high).addFreeVariables(result);
		if (low != null)
			((CommonExpression) low).addFreeVariables(result);
		if (step != null)
			((CommonExpression) step).addFreeVariables(result);
	}

}