package lambdaKit.model.util;

import lambdaKit.model.term.Pair;
import lambdaKit.model.term.Term;
import lambdaKit.model.term.exception.NotAFreeTermException;

/*
 * The Reducer proposes the beta reduction of a lambda Term in its tree representation.
 */
public interface Reducer {

	/*
	 * This method duplicates a lambda term.
	 */
	public Term cloneTerm(Term container);
	
	/*
	 * This method proposes the beta reduction of a free redex.
	 * 
	 * Returns the reduced Term.
	 */
	public Term reduceFreeRedex(Pair redex)
			throws NotAFreeTermException;

	/*
	 * This method proposes the beta reduction of an internal redex.
	 */
	public void reduceInternalRedex(Pair redex);

	/*
	 * This method proposes a statistic on beta reductions.
	 */
	public NormalizationStatistics getNormalizationStatistics();
	
	/*
	 * this method resets the normalization statistics.
	 */
	public void resetNormalizationStatistics();
}