package code.subst.visitor;

import code.subst.*;
import code.term.*;
import java.util.Hashtable;

/**
 * This class defines a few operations on substitutions.
 * They are bundled together because they are small and
 * similar, hence easily coded by cut and paste.
 *
 * @author Sergio Antoy
 * @since April 22, 2005
 */

public class SubstOps {

    public static final SubstOps instance = new SubstOps();

    private SubstOps() {}

    // ------------------------------------------------------------------
    /**
     * Return a printable representation of a substitution.
     * Substitutions to be presented to user at the end of
     * a computation should undergo selfApply and filterAnon
     * first
     */

    public String toString(Subst subst) {
	return subst.accept(toStringVisitor, null);
    }

    private ToStringVisitor toStringVisitor = new ToStringVisitor();

    private class ToStringVisitor implements SubstVisitor<String,Object> {
        public String visit(IdSubst s, Object ignore) { return ""; }
        public String visit(VarSubst s, Object ignore) {
	    return s.variable.toString() +
                   "=" +
                   s.binding.toString() +
                   "; " +
	           s.next.accept(this, ignore);
        }
    }

    // ------------------------------------------------------------------
    /**
     * Remove bound variables from the codomain of a substitution
     * by replacing them with their bindings.  E.g., given:
     * <PRE>
     *     _34=zero; Y=_33; X=succ(_34)
     * </PRE>
     * return
     * <PRE>
     *     _34=zero; Y=_33; X=succ(zero)
     * </PRE>
     *
     */

    public Subst selfApply(Subst subst) {
	return subst.accept(selfApplyVisitor, subst);
    }

    private SelfApplyVisitor selfApplyVisitor = new SelfApplyVisitor();

    private class SelfApplyVisitor implements SubstVisitor<Subst,Subst> {
        public Subst visit(IdSubst s, Subst subst) { return s; }
        public Subst visit(VarSubst s, Subst subst) {
	    Variable variable = s.variable;
	    Term binding = s.binding;
	    Subst newNext = s.next.accept(this, subst);
	    Term newBinding = binding.cloneWithSubst(subst);
	    Subst newSubst = new VarSubst(variable, newBinding, newNext);
	    return newSubst;
        }
    }

    // ------------------------------------------------------------------
    /**
     * Remove anon variables from the domain of a substitution.
     * E.g., given:
     * <PRE>
     *     _34=zero; Y=_33; X=succ(_34)
     * </PRE>
     * return
     * <PRE>
     *     Y=_33; X=succ(_34)
     * </PRE>
     *
     */

    public Subst filterAnon(Subst subst) {
	return subst.accept(filterAnonVisitor, subst);
    }

    private FilterAnonVisitor filterAnonVisitor = new FilterAnonVisitor();

    private class FilterAnonVisitor implements SubstVisitor<Subst,Object> {
        public Subst visit(IdSubst s, Object ignore) { return s; }
        public Subst visit(VarSubst s, Object ignore) {
	    Subst newNext = s.next.accept(this, ignore);
	    if (s.variable.getName().startsWith(Variable.autoVarPrefix)) {
		return newNext;
	    } else {
		return new VarSubst(s.variable, s.binding, newNext);
	    }
        }
    }
}