package org.eclipse.cdt.codan.extension;

import org.eclipse.cdt.core.dom.ast.ASTVisitor;
import org.eclipse.cdt.core.dom.ast.IASTBinaryExpression;
import org.eclipse.cdt.core.dom.ast.IASTExpression;
import org.eclipse.cdt.core.dom.ast.IASTIdExpression;
import org.eclipse.cdt.core.dom.ast.IASTName;
import org.eclipse.cdt.core.dom.ast.IASTUnaryExpression;
import org.eclipse.cdt.core.dom.ast.IBinding;
import org.eclipse.cdt.core.dom.ast.IVariable;

public class ConditionalVisitor extends ASTVisitor {
	private ExecutionState es;
	private boolean value;

	public ConditionalVisitor(ExecutionState es, boolean value) {
		this.es = es;
		this.value = value;
		shouldVisitExpressions = true;
	}

	@Override
	public int visit(IASTExpression node) {
		int ret = PROCESS_CONTINUE;
		// Modify execution state according to branch condition
		ExecutionStateClause clause = null;
		// *N.B.* content for condition IBlock is condition expression itself
		if (node instanceof IASTBinaryExpression) { // TODO use visitor, nested BinaryExpressions
			// FIXME compound conditionals
			IASTBinaryExpression binExpr = (IASTBinaryExpression) node;
			int op = binExpr.getOperator();

			// FIXME other ops
			// Check operator is an equality operator
			if (op == IASTBinaryExpression.op_equals) { // if (x == 0)
				IASTExpression o1 = binExpr.getOperand1();
				if (o1 instanceof IASTIdExpression) {
					IASTName name = ((IASTIdExpression) o1).getName();
					clause = parseConditional(clause, name, binExpr.getOperand2(), value);
				}
			}
			else if (op == IASTBinaryExpression.op_notequals) { // if (x != 0)
				IASTExpression o1 = binExpr.getOperand1();
				if (o1 instanceof IASTIdExpression) {
					IASTName name = ((IASTIdExpression) o1).getName();
					clause = parseConditional(clause, name, binExpr.getOperand2(), !value); // Negation
				}
			}
		}
		else if (node instanceof IASTUnaryExpression) { // if (!x)
			IASTUnaryExpression uExpr = (IASTUnaryExpression) node;
			int op = uExpr.getOperator();
			
			// Check operator is a negation operator
			if (op == IASTUnaryExpression.op_not) {
				IASTExpression operand = uExpr.getOperand();
				if (operand instanceof IASTIdExpression) {
					IASTName name = ((IASTIdExpression) operand).getName();
					clause = parseConditional(clause, name, !value); // Negation
				}
			}
		}
		else if (node instanceof IASTIdExpression) { // if (x)
			IASTName name = ((IASTIdExpression) node).getName();
			clause = parseConditional(clause, name, value);
		}
		
		if (clause != null) {
			es.addClause(clause);
			// TODO Theorem Prover goes here! / Determine if branch is feasible
			es.bindTruthAssignments();
			ret = PROCESS_SKIP;
		}
		else {
			// FIXME Handle unresolvable case
		}
		return ret;
	}
	
	private ExecutionStateClause parseConditional(ExecutionStateClause clause, IASTName name, IASTExpression valueExpr, boolean branchTruth) {
		IBinding binding = name.resolveBinding();
		if (binding instanceof IVariable) {
			IVariable var = (IVariable) binding;
			Boolean truth = ASTParserUtil.getTruthValue(valueExpr);
			if (truth != null) {
				clause = new ExecutionStateClause(var, truth == branchTruth);
			}
		}
		return clause;
	}
	
	private ExecutionStateClause parseConditional(ExecutionStateClause clause, IASTName name, boolean branchTruth) {
		IBinding binding = name.resolveBinding();
		if (binding instanceof IVariable) {
			IVariable var = (IVariable) binding;
			clause = new ExecutionStateClause(var, branchTruth);
		}
		return clause;
	}
}