package code.subst;

import code.term.Term;
import code.term.Variable;
import code.subst.visitor.*;

/**
 * This class represents a non-identity substitution. It consists of a
 * mapping from a variable to a term followed by another, possibly
 * identity substitution.
 *
 * @author Sergio Antoy
 * @since June 17, 2003
 */

public class VarSubst extends Subst {
    /** The variable being bound. */
    public final Variable variable;
    /* The binding of the variable being bound.*/
    public final Term binding;
    /** The rest of this substitution. */
    public final Subst next;

    /**
     * Construct an instance of a bound variable of an incremental
     * substitution.
     *
     * @param variable The variable being bound
     * @param binding The binding of the variable
     * @param next The remaining substitution.
     */
    public VarSubst(Variable variable, Term binding, Subst next) {
	this.variable = variable ;
	this.binding = binding;
        this.next = next;
    }

    public Term getBinding(Variable variable) {
	return this.variable == variable 
	    ? binding : next.getBinding(variable);
    }

    public <R,T> R accept(SubstVisitor<R,T> v, T o)  {
	return v.visit(this, o);
    }
}