package de.tla2b.translation;

import java.util.ArrayList;
import util.UniqueString;

import tla2sany.semantic.ASTConstants;
import tla2sany.semantic.ExprNode;
import tla2sany.semantic.FormalParamNode;
import tla2sany.semantic.LetInNode;
import tla2sany.semantic.OpApplNode;
import tla2sany.semantic.OpDefNode;
import tlc2.tool.BuiltInOPs;
import tlc2.tool.ToolGlobals;
import de.tla2b.analysis.AbstractASTVisitor;
import de.tla2b.analysis.BOperation;
import de.tla2b.analysis.SpecAnalyser;
import de.tla2b.global.BBuiltInOPs;
import de.tla2b.global.BBuildIns;
import de.tla2b.global.TranslationGlobals;

public class OperationsFinder extends AbstractASTVisitor implements
		ASTConstants, ToolGlobals, TranslationGlobals {
	private final SpecAnalyser specAnalyser;

	private String currentName;
	private ArrayList<OpApplNode> exists;
	// a list containing all existential quantifier which will be parameters in
	// the resulting B Maschine

	private final ArrayList<BOperation> bOperations;

	public OperationsFinder(SpecAnalyser specAnalyser) {
		this.specAnalyser = specAnalyser;
		this.bOperations = new ArrayList<BOperation>();
		if (specAnalyser.getNext() != null) {

			currentName = "Next";
			exists = new ArrayList<OpApplNode>();
			visitExprNode(specAnalyser.getNext());
		}
	}

	
	public void visitExprNode(ExprNode n) {
		switch (n.getKind()) {
		case OpApplKind: {
			visitOpApplNode((OpApplNode) n);
			return;
		}
		case NumeralKind: {
			throw new RuntimeException(String.format(
					"Expected an action (instead of a number).%n%s", n.getLocation().toString()));
		}
		case StringKind: {
			throw new RuntimeException(String.format(
					"Expected an action (instead of a string).%n%s", n.getLocation().toString()));
		}
		case SubstInKind: {
			throw new RuntimeException(String.format(
					"Expected an action.%n%s", n.getLocation().toString()));
		}
		case AtNodeKind: { // @
			throw new RuntimeException(String.format(
					"Expected an action.%n%s", n.getLocation().toString()));
		}
		case LetInKind: {
			// we do not visit the local definitions
			visitExprNode(((LetInNode) n).getBody());
			return;
		}
		}
	}
	
	public void visitUserDefinedNode(OpApplNode n) {
		OpDefNode def = (OpDefNode) n.getOperator();
		if (BBuiltInOPs.contains(def.getName())) {
			BOperation op = new BOperation(def.getName().toString(), n, exists,
					specAnalyser);
			bOperations.add(op);
			return;
		}

		for (int i = 0; i < def.getParams().length; i++) {
			FormalParamNode param = def.getParams()[i];
			param.setToolObject(SUBSTITUTE_PARAM, n.getArgs()[i]);
		}
		currentName = def.getName().toString();
		visitExprNode(def.getBody());
	}

	@Override
	public void visitBuiltInNode(OpApplNode n) {
	    UniqueString opname = n.getOperator().getName();
		int opcode = BuiltInOPs.getOpCode(opname);
		switch (opcode) {
		case OPCODE_dl: // DisjList: split action further
		{
			if (n.getArgs().length == 1) {
				visitExprOrOpArgNode(n.getArgs()[0]);
				return;
			} else {
				String oldName = currentName;
				ArrayList<OpApplNode> oldExists = new ArrayList<OpApplNode>(
						exists);

				for (int i = 0; i < n.getArgs().length; i++) {
					exists = new ArrayList<OpApplNode>(oldExists);
					currentName = oldName + i;
					visitExprOrOpArgNode(n.getArgs()[i]);
				}
				return;
			}
		}
		case OPCODE_lor: { // logical or: split action further
			String oldName = currentName;
			ArrayList<OpApplNode> oldExists = new ArrayList<OpApplNode>(exists);

			for (int i = 0; i < n.getArgs().length; i++) {
				exists = new ArrayList<OpApplNode>(oldExists);
				currentName = oldName+ i;
				visitExprOrOpArgNode(n.getArgs()[i]);
			}
			return;
		}
		case OPCODE_be: { // BoundedExists
			exists.add(n);
			visitExprOrOpArgNode(n.getArgs()[0]);
			return;
		}

		case OPCODE_unchanged:
		case OPCODE_eq: // =
		case OPCODE_noteq: // /=, #
		case OPCODE_neg: // Negation
		case OPCODE_lnot: // Negation
		case OPCODE_cl: // $ConjList
		case OPCODE_land: // \land
		case OPCODE_equiv: // \equiv
		case OPCODE_implies: // =>
		case OPCODE_bf: // \A x \in S : P
		case OPCODE_in: // \in
		case OPCODE_notin: // \notin
		case OPCODE_subseteq: // \subseteq - subset or equal
		case OPCODE_fa: // $FcnApply f[1]
		case OPCODE_ite: // IF THEN ELSE
		case OPCODE_case: {
		   // no further decomposing: create a B operation
			BOperation op = new BOperation(currentName, n, exists, specAnalyser);
			bOperations.add(op);
			return;
		}

		}
		//System.out.println("OPCODE of " + opname + " = "+ opcode);
		
		if (opname == BBuildIns.OP_false ||  // FALSE: always disabled
		    opname == BBuildIns.OP_true) {  // TRUE: CHAOS
			BOperation op = new BOperation(currentName, n, exists, specAnalyser);
			bOperations.add(op);
			return;
		}
		throw new RuntimeException(String.format(
				"Expected an action at '%s' :%n%s", n.getOperator().getName()
						.toString(), n.getLocation().toString()));

	}

	public ArrayList<BOperation> getBOperations() {
		return bOperations;
	}

}