package aspectjhw.lambda;
import java.util.*;

/** Application terms in the lambda calculus. */
public class Application implements Term {
    /** The operator and operand expressions. */
    protected final Term[] exps;
    //@ protected invariant \nonnullelements(exps);

    /** Initialize this to be an application of e0 to e1. */
    //@ requires e0 != null && e1 != null;
    public Application(Term e0, Term e1) {
        exps = new Term[] { e0, e1 };
    }

    // doc comment inherited
    public Term reduce1Step() {
        Term oper = exps[0].reduce1Step();
        if (oper != exps[0]) {
            return new Application(oper, exps[1]);
        } else if (oper instanceof Lambda) {
            return ((Lambda) oper).apply(exps[1]);
        } else {
            return this;
        }
    }

    // doc comment inherited
    public Set freeVars() {
        Set s = new HashSet();
        for (int i = 0; i < 2; i++) {
            s.addAll(exps[i].freeVars());
        }
        return s;
    }

    // doc comment and specification inherited
    public Term substituteFor(String var, Term arg) {
        Term substituted[] = new Term[2];
        for (int i = 0; i < 2; i++) {
            substituted[i] = exps[i].substituteFor(var, arg);
        }
        return new Application(substituted[0], substituted[1]);
    }

    // doc comment inherited
    public String toString() { return "(" + exps[0].toString() + " " + exps[1].toString() + ")"; }

    // doc comment inherited
    public boolean equals(Object o) {
        return (o instanceof Application) && exps[0].equals(((Application) o).exps[0])
            && exps[1].equals(((Application) o).exps[1]);
    }

    // doc comment inherited
    public int hashCode() { return exps[0].hashCode() + exps[1].hashCode(); }
}