package code.term.visitor;

import code.term.*;

import java.util.*;

/**
 * This class performs a clone of a term after replacing a subterm
 * with another.  The subterm being replace is intended to be a redex
 * with non-deterministic replacements, otherwise the replacement
 * should be in place, i.e., a destructive update.
 *
 * @author Sergio Antoy
 * @since Apr 7, 2005
 * 
 */
public class CloneWithReplaceTerm {

    /** 
     *  This table maps terms that have been cloned.
     *  This is essential to preserve sharing of subterms in a term.
     *  It is the term identity that is mapped in the table.
     */
    private Hashtable<Term, Term> table = new Hashtable<Term, Term>();

    public Term doit(Term top, Term out, Term in) {
        if (top.getRepresentation() == out.getRepresentation()) {
	    // Since we always check this, there is no
	    // need to map "out -> in" in the table
            return in;
        } else {
            boolean rebuild = false;
            Term[] argument = top.getArgument();
            int length = argument.length;
            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
		    newArg[i] = newTerm;
		    rebuild = true;
		} else {
		    newTerm = doit(oldTerm, out, in);
		    if (newTerm != oldTerm) {
			// oldTerm has been clone now for the first time
			table.put(oldTerm,newTerm);
			rebuild = true;
			newArg[i] = newTerm;
		    } else {
			// oldTerm has not been cloned
			newArg[i] = oldTerm;
		    }
		}
            }
	    // If one argument has been cloned
	    // then we are on a spine and must re-construct
	    return rebuild ? new Term(top.getRoot(), newArg) : top;
        }
    }
}