package code.term.visitor;

import code.lang.SuccessModule;
import code.table.ModuleTable;
import code.term.*;

/**
 * @author Stephen Johnson
 * @since Jul 6, 2004
 */
public class EqSuccessTermVisitor implements TermVisitor<Term,TermImpl> {

    public static final EqSuccessTermVisitor singleton
        = new EqSuccessTermVisitor();

    // private static final String successModuleName = "$Success";
    private static final String successModuleName = "Prelude";
    private static int parallelAndId
	= ModuleTable.sureGetId(successModuleName,"&");
    private static int eqSuccessId
	= ModuleTable.sureGetId(successModuleName,"=:=");

    private EqSuccessTermVisitor() {};

    public Term visit(TermImplChar t, TermImpl right) {
        if (right instanceof TermImplChar) {
            char rightValue = ((TermImplChar) right).value;
            return t.value == rightValue
                    ? SuccessModule.successTerm
                    : SuccessModule.termFail;
        } else {
            throw new RuntimeException("Type inconsistency " + right);
        }
    }

    public Term visit(TermImplFloat t, TermImpl right) {
        if (right instanceof TermImplFloat) {
            float rightValue = ((TermImplFloat) right).value;
            return t.value == rightValue
                    ? SuccessModule.successTerm
                    : SuccessModule.termFail;
        } else {
            throw new RuntimeException("Type inconsistency " + right);
        }
    }

    public Term visit(TermImplInt t, TermImpl right) {
        if (right instanceof TermImplInt) {
            int rightValue = ((TermImplInt) right).value;
            return t.value == rightValue
                    ? SuccessModule.successTerm
                    : SuccessModule.termFail;
        } else {
            throw new RuntimeException("Type inconsistency " + right);
        }
    }

    public Term visit(TermImplString t, TermImpl right) {
        if (right instanceof TermImplString) {
            String rightValue = ((TermImplString) right).value;
            return t.value.equals(rightValue)
                    ? SuccessModule.successTerm
                    : SuccessModule.termFail;
        } else {
            throw new RuntimeException("Type inconsistency " + right);
        }
    }

    public Term visit(TermImplOpaque t, TermImpl right) {
        if (right instanceof TermImplOpaque) {
            return t.opaque.equals(((TermImplOpaque) right).opaque)
                    ? SuccessModule.successTerm
                    : SuccessModule.termFail;
        } else {
            throw new RuntimeException("Type inconsistency " + right);
        }
    }


    /** It assumes that both sides of =:= are non-variable HNFs */
    public Term visit(TermImplUser t, TermImpl right) {
        int rightRoot = right.getRoot();
        if (t.getRoot() == rightRoot) {
            Term[] leftArg = t.getArgument();
            Term[] rightArg = right.getArgument();
            if (leftArg.length == rightArg.length) {
                Term reduct;
                if (leftArg.length == 0) {
                    reduct = SuccessModule.successTerm;
                } else {
                    int i = leftArg.length - 1;
                    reduct = new Term(eqSuccessId,
                            new Term[]{leftArg[i],
                                       rightArg[i], });
                    while (--i >= 0) {
                        reduct = new Term(parallelAndId,
                                new Term[]{
                                    new Term(eqSuccessId,
                                            new Term[]{leftArg[i],
                                                       rightArg[i], }),
                                    reduct, });
                    }
                }
                return reduct;
            } else {
                throw new RuntimeException("Type inconsistency #arg");
            }
        }
        return SuccessModule.termFail;
    }

    public Term visit(Variable v, TermImpl right) {
        throw new IllegalStateException("Improper call for =:= of a variable");
    }
}