package aspectjhw.lambda;
import java.util.*;
/** Lambda (i.e., function) terms. */
public class Lambda implements Term {
    /** The bound variable. */
    protected final /*@ non_null @*/ String var;
    /** The body. */
    protected final /*@ non_null @*/ Term body;

    /** Initialize this to have variable v and body b. */
    //@ requires v != null && b != null;
    public Lambda(String v, Term b) {
        var = v;
        body = b;
    }

    // doc comment inherited
    public Term reduce1Step() {
        return this;
    }

    // doc comment inherited
    public Set freeVars() {
        Set s = new HashSet();
        s.addAll(body.freeVars());
        s.remove(var);
        return s;
    }

    /** Apply this lambda abstraction to the argument. */
    //@ requires arg != null;
    public Term apply(Term arg) {
        return body.substituteFor(var, arg);
    }

    // doc comment and specification inherited
    public Term substituteFor(String var2, Term arg) {
        if (var2.equals(var)) {
            return this;
        } else if (arg.freeVars().contains(var)) {
            throw new SubstitutionException();
        } else {
            Term newBody = body.substituteFor(var2, arg);
            return new Lambda(var, newBody);
        }
    }

    /** Exception class used in substituteFor */
    public class SubstitutionException extends RuntimeException {
    }

    // doc comment inherited
    public String toString() {
        return "(\\ " + var + " -> " + body.toString() + ")"; 
    }

    // doc comment inherited
    public boolean equals(Object o) {
        return (o instanceof Lambda) && var.equals(((Lambda) o).var)
            && body.equals(((Lambda) o).body);
    }

    // doc comment inherited
    public int hashCode() { 
        return var.hashCode() + body.hashCode();
    }
}