package code.term.visitor;

import code.term.*;
import code.subst.*;
import code.subst.visitor.SubstVisitor;
import code.stuff.Pair;

import java.util.Hashtable;
import java.util.HashSet;

/**
 * Rename anonymous variables of a term and subst expression so that
 * the names in a left-to-right traversal are "_1", "_2", ...
 *
 * @author David Shapiro
 * @since April 18, 2005
 */


public class VariableNormalizer  {

    /**
     *  Store variables that have been introduced by the normalization
     *  and hance should be left untouched.
     */
    private HashSet<Variable> introduced = new HashSet<Variable>();

    /** 
     *  Map anonymous variables in a term to new anonymous
     *  variables with normalized names
     */
    private Hashtable<Variable,Variable> varRenaming
	= new Hashtable<Variable,Variable>();
    private int counter;

    /** 
     *  Map subterms of a term to subterms that have been replaced
     *  so that sharing is preserved.
     */
    private Hashtable<Term,Term> correspondence
	= new Hashtable<Term,Term>();

    private Worker worker = new Worker();

    public VariableNormalizer() {}

    public Pair<Term,Subst> doit(Term inTerm, Subst inSubst) {
	introduced.clear();
	varRenaming.clear();
	counter = 1;
	correspondence.clear();
	Term outTerm = new Term
	    (inTerm.getRepresentation().accept(worker, null));
	Subst outSubst = inSubst.accept(substNormalizer, null);
	return new Pair<Term,Subst>(outTerm, outSubst);
    }

    private SubstNormalizer substNormalizer = new SubstNormalizer();

    private class SubstNormalizer implements SubstVisitor<Subst,Object> {
        public Subst visit(IdSubst s, Object ignore) { return s; }
        public Subst visit(VarSubst s, Object ignore) {
	    Variable variable = s.variable;
	    Term binding = s.binding;
	    Variable newVariable = (Variable) variable.accept(worker, null);
	    Term newBinding = new Term(binding.getRepresentation().accept
				      (worker, null));
	    Subst newSubst = s.next.accept(this,null);
	    return new VarSubst(newVariable, newBinding, newSubst);
        }
    }

    private class Worker implements TermVisitor<TermImpl,Object> {

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

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

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

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

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

        public TermImpl visit(Variable t, Object ignore) {
	    if (introduced.contains(t)) {
		return t;
	    } else {
		String name = t.getName();
		if (name.startsWith(Variable.autoVarPrefix)) {
		    Variable newVariable = varRenaming.get(t);
		    if (newVariable == null) {
			newVariable
			    = new Variable(Variable.autoVarPrefix + counter++);
			introduced.add(newVariable);
			varRenaming.put(t,newVariable);
		    }
		    return newVariable;
		} else {
		    return t;
		}
	    }
	}

	// This method is the same as in CloneWithSubstTermVisitor
	// It should be factorized.
        public TermImpl visit(TermImplUser t, Object ignore) {
	    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 = correspondence.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, null);
		    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]);
			correspondence.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;
        }
    }

}