package code.subst;

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

/**
 * Abstract base class of all substitutions. A substitution is a
 * mapping from variables to terms. The mapping is computed
 * incrementally.
 *
 * @author Sergio Antoy
 * @since June 17, 2003
 */

public abstract class Subst {
    /**
     * Identity substitution. It is a static constant since there is only one
     * identity. The constructor of identity substitutions is protected, thus
     * this constant is the only device to obtain an identity substitution.
     */
    public final static IdSubst id = new IdSubst();

    /**
     * Return the binding of a variable.
     *
     * @param variable The variable to tell the binding
     * @return The binding of the argument.
     */
    public abstract Term getBinding(Variable variable);

    public abstract <R,T> R accept(SubstVisitor<R,T> v, T o);

}