package org.mandarax.reference;

/*
 * Copyright (C) 1999-2004 <a href="mailto:mandarax@jbdietrich.com">Jens Dietrich</a>
 *
 * This library is free software; you can redistribute it and/or
 * modify it under the terms of the GNU Lesser General Public
 * License as published by the Free Software Foundation; either
 * version 2 of the License, or (at your option) any later version.
 *
 * This library is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 * Lesser General Public License for more details.
 *
 * You should have received a copy of the GNU Lesser General Public
 * License along with this library; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

import org.mandarax.kernel.*;

import java.util.ArrayList;
import java.util.Hashtable;
import java.util.Iterator;
import java.util.List;

/**
 * Utility to clone facts and to rename variables.
 * The renaming can be retrieved using <code>getRenamings()</code>.
 *
 * @author <A HREF="mailto:mandarax@jbdietrich.com">Jens Dietrich</A>
 * @author <A HREF="mailto:a.kozlenkov@city.ac.uk">Alex Kozlenkov</A>
 * @version 3.3.1 <9 August 2004>
 * @since 1.0
 *        Prova re-integration modifications
 */
public final class VariableRenaming {

	public static String GENERATED_VAR_PREFIX = "@@";
	private int counter = 0;
	private Hashtable recentRenamings = new java.util.Hashtable();
	// added in order to keep track of all replacements made during a derivation
	private Hashtable allRenamings = new java.util.Hashtable();
	private LogicFactory lFactory = LogicFactory.getDefaultFactory();

	/**
	 * Clone a constant term.
	 *
	 * @param original the term to be cloned
	 * @return the cloned term
	 */
	private Term clone( ConstantTerm original ) {
		return lFactory.createConstantTerm(original.getObject());
	}

	/**
	 * Clone a clause and rename all variables.
	 *
	 * @param original the original clause
	 * @return the cloned clause
	 */
	public Clause cloneAndRenameVars( Clause original ) {

		// first reset the var name server to clean its existing associations
		reset();

		List posLit = original.getPositiveLiterals();
		List negLit = original.getNegativeLiterals();
		List clonedPosLiterals = new ArrayList(posLit.size());

		for( Iterator it = posLit.iterator(); it.hasNext(); ) {
			clonedPosLiterals.add(cloneAndRenameVars((Fact) it.next()));
		}

		List clonedNegLiterals = new ArrayList(negLit.size());

		for( Iterator it = negLit.iterator(); it.hasNext(); ) {
			clonedNegLiterals.add(cloneAndRenameVars((Fact) it.next()));
		}

		return new TmpClause(clonedPosLiterals, clonedNegLiterals);
	}

	/**
	 * Clone the head in a clause and rename all variables.
	 *
	 * @param original the original clause
	 * @return the cloned clause
	 */
	public TmpClause cloneAndRenameVarsInHead( Clause original ) {

		// first reset the var name server to clean its existing associations
		reset();

		List posLit = original.getPositiveLiterals();
		List negLit = original.getNegativeLiterals();
		List clonedPosLiterals = new ArrayList(posLit.size());

		for( Iterator it = posLit.iterator(); it.hasNext(); ) {
			clonedPosLiterals.add(cloneAndRenameVars((Fact) it.next()));
		}

		return new TmpClause(clonedPosLiterals, negLit);
	}

	/**
	 * Clone the head in a clause and rename all variables.
	 *
	 * @param original the original clause
	 * @return the cloned clause
	 */
	public TmpClause cloneAndRenameVarsInBody( TmpClause original ) {
		List negLit = original.getNegativeLiterals();

		List clonedNegLiterals = new ArrayList(negLit.size());

		for( Iterator it = negLit.iterator(); it.hasNext(); ) {
			clonedNegLiterals.add(cloneAndRenameVars((Fact) it.next()));
		}

		original.negativeLiterals = clonedNegLiterals;
		return original;
	}

	/**
	 * Clone a complex term and rename all variables.
	 *
	 * @param original the original term
	 * @return the cloned term
	 */
	private Term cloneAndRenameVars( ComplexTerm original ) {
		Term[] subterms = original.getTerms();
		Term[] copiedSubterms = new Term[subterms.length];

		for( int i = 0; i < subterms.length; i++ ) {
			copiedSubterms[i] = cloneAndRenameVars(subterms[i]);
		}

		return lFactory.createComplexTerm(original.getFunction(),
		        copiedSubterms);
	}

	/**
	 * Clone a fact and rename all variables.
	 *
	 * @param original the original fact
	 *                 Prova: "extra" should be cloned as well.
	 * @return the cloned fact
	 */
	public Fact cloneAndRenameVars( Fact original ) {
		Term[] t = original.getTerms();
		Fact f = null;
		if( original instanceof Prerequisite ) {
			f = lFactory.createPrerequisite(original.getPredicate(),
			        new Term[t.length],
			        original.isNegatedAF());
			((Prerequisite) f).setExtra(((Prerequisite) original).getExtra());
		} else
			f =
			        lFactory.createFact(original.getPredicate(),
			                new Term[t.length]);
		for( int i = 0; i < t.length; i++ ) {
			f.setTerm(cloneAndRenameVars(t[i]), i);
		}
		return f;
	}

	/**
	 * Clone a term and rename all variables.
	 *
	 * @param original the original term
	 * @return the cloned term
	 */
	private Term cloneAndRenameVars( Term original ) {
		if( original instanceof ConstantTerm ) {
			// a.kozlenkov@city.ac.uk: Why do we need to create a new constant term?
			return original; //clone((ConstantTerm) original);
		}

		if( original instanceof VariableTerm ) {
			return cloneAndRenameVars((VariableTerm) original);
		}

		if( original instanceof ComplexTerm ) {
			return cloneAndRenameVars((ComplexTerm) original);
		}

		return original;
	}

	/**
	 * Clone and rename a variable term. The new name is a generated temporary session name.
	 *
	 * @param original the original term
	 * @return the cloned term with the renamed variables
	 */
	private org.mandarax.kernel.VariableTerm cloneAndRenameVars( org.mandarax.kernel.VariableTerm original ) {
		org.mandarax.kernel.VariableTerm replacement =
		        (org.mandarax.kernel.VariableTerm) recentRenamings.get(original);

		if( replacement == null ) {
			// if there is no association in the cache generate and assign a new name
			counter = counter + 1;
			String aName = GENERATED_VAR_PREFIX + String.valueOf(counter);
			replacement = lFactory.createVariableTerm(aName, original.getType());
			recentRenamings.put(original, replacement);
			allRenamings.put(original, replacement);
		}

		return replacement;
	}

	/**
	 * Get the recent renamings.
	 *
	 * @return a hashtable containing renamings (term -> term associations)
	 */
	public Hashtable getRecentRenamings() {
		return recentRenamings;
	}

	/**
	 * Get all renamings made.
	 *
	 * @return a hashtable containing renamings (term -> term associations)
	 */
	public Hashtable getAllRenamings() {
		return allRenamings;
	}

	/**
	 * Reset the cache.
	 */
	private void reset() {
		recentRenamings = new Hashtable();
	}
}
