package com.naveensundarg.shadow.prover.representations.method;

import com.naveensundarg.shadow.prover.core.Logic;
import com.naveensundarg.shadow.prover.representations.ErrorPhrase;
import com.naveensundarg.shadow.prover.representations.Phrase;
import com.naveensundarg.shadow.prover.representations.formula.Formula;
import java.util.List;
import java.util.Set;

/**
 * Created by naveensundarg on 8/28/17.
 */
public final class Absurd extends PrimitiveMethod {

    private static final Absurd INSTANCE;

    static {
        INSTANCE = new Absurd();
    }

    private Absurd() {

    }

    public static Absurd getInstance() {

        return INSTANCE;
    }

    @Override
    public Phrase apply(Set<Formula> assumptionBase, List<Phrase> args) {

        if (args.size() == 2) {

            Phrase P1 = args.get(0);
            Phrase P2 = args.get(1);

            if (P1 instanceof Formula) {


                if (P2 instanceof Formula) {


                    if (assumptionBase.contains(P1)) {

                        if (assumptionBase.contains(P2)) {

                            if(P1.equals(Logic.negated((Formula) P2))|| P2.equals(Logic.negated((Formula)P1))){


                                return Logic.getFalseFormula();


                            }
                            else {

                                return new ErrorPhrase("absurd: pattern matching failed");
                            }


                        } else {

                            return new ErrorPhrase("absurd: the assumption base does not contain " + P2);
                        }

                    } else {

                        return new ErrorPhrase("absurd: the assumption base does not contain " + P1);
                    }


                } else {

                    return new ErrorPhrase("absurd: the first input is not a formula, got " + P2 + " of class " + P2.getClass());
                }

            } else {

                return new ErrorPhrase("absurd: the first input is not a formula, got " + P1 + " of class " + P1.getClass());
            }

        } else

        {

            return new ErrorPhrase("absurd takes exactly two inputs but got: " + args);
        }

    }

    @Override
    public String toString() {
        return "absurd";
    }
}
