package code.term.visitor;

import code.subst.Subst;
import code.term.*;
import code.term.Variable;

import java.util.*;

/**
 * This visitor performs a clone with a substition for a term.
 *
 * @author Stephen Johnson
 * @since Jul 6, 2004
 * 
 * Recoded by Sergio on Mon Apr  4 16:33:21 PDT 2005
 * to preserve sharing when a term is cloned.
 * Extended to generics on Mon Apr 11 10:37:06 PDT 2005.
 */
public class CloneWithSubstTermVisitor 
    implements TermVisitor<TermImpl,Subst> {

    /** 
     *  This table maps terms that have been cloned.
     *  Terms have an identity and can be shared
     */
    private Hashtable<Term, Term> table = new Hashtable<Term, Term>();

    public TermImpl visit(TermImplChar t, Subst ignore) { return t; }

    public TermImpl visit(TermImplFloat t, Subst ignore) { return t; }

    public TermImpl visit(TermImplInt t, Subst ignore) { return t; }

    public TermImpl visit(TermImplString t, Subst ignore) { return t; }

    public TermImpl visit(TermImplOpaque t, Subst ignore) { return t; }

    public TermImpl visit(TermImplUser t, Subst subst) {
        Term[] argument = t.getArgument();
        int length = argument.length;

        boolean rebuild = false;
        Term[] newArg = new Term[length];
        for (int i = 0; i < length; i++) {
            Term oldTerm = argument[i];
            Term newTerm = table.get(oldTerm);
            if (newTerm != null) {
                // oldTerm has been cloned before
                // System.err.println("- retrieving "+oldTerm);
                // System.err.println("  mapped to "+newTerm);
                newArg[i] = newTerm;
                rebuild = true;
            } else {
                TermImpl tmp = (TermImpl) 
                    oldTerm.getRepresentation().accept(this, subst);
                if (tmp != oldTerm.getRepresentation()) {
                    // oldTerm has just been cloned for the first time
                    newArg[i] = newTerm = new Term(tmp);
                    // System.err.println("- mapping "+oldTerm);
                    // System.err.println("  to "+newTerm]);
                    table.put(oldTerm,newTerm);
                    rebuild = true;
                } else {
                    // oldTerm has not been cloned
                    newArg[i] = oldTerm;
                }
            }
        }
        if (rebuild) return new TermImplUser(t.getRoot(), newArg);
        else return t;
    }

    public TermImpl visit(Variable v, Subst subst) {
        Term binding = subst.getBinding(v);
        if (binding == null) return v;
        else return binding.getRepresentation().accept(this, subst);
    }
}