package typedLambda.model.util;

import typedLambda.model.term.Abstraction;
import typedLambda.model.term.Pair;
import typedLambda.model.term.Term;
import typedLambda.model.term.exception.AbstractionNotFoundException;
import typedLambda.model.util.exception.reduce.TooMuchBetaReductionException;

/*
 * The Reducer proposes the beta reduction of a lambda Term in its tree representation.
 * 
 * A limit may be fixed to the count of beta reductions required for a normalization.
 */
public interface Reducer {

	/*
	 * This method  verify the closure of a combinator.
	 */
	public void verifyClosure(Abstraction hand, Abstraction before)
			throws AbstractionNotFoundException;
	
	/*
	 * This method duplicates a lambda term.
	 */
	public <T extends Term> T cloneTerm(T container);
	
	/*
	 * This method returns the leftmost normalizable Pair of a lambda Term
	 * 	if any, null elsewhere.
	 */
	public Pair leftmostNormalizablePair(Term container);
	
	/*
	 * This method proposes the beta reduction of a redex within a container.
	 * 
	 * Returns the substitution count.
	 */
	public int reduceRedex(Abstraction container, Pair redex);

	/*
	 * This method proposes the beta reduction of a free redex.
	 * 
	 * Returns the reduced Term.
	 */
	public Term reduceRedex(Pair redex);
	
	/*
	 * This method proposes the normalization of an Abstraction.
	 * 
	 * Normalization includes beta reductions and Abstraction going up.
	 */
	public NormalizationStatistics normalize(Abstraction container)
			throws TooMuchBetaReductionException;

	/*
	 * This method proposes the normalization of a Pair.
	 * 
	 * Normalization includes beta reductions and Abstraction going up.
	 */
	public Term normalize(Pair container)
			throws TooMuchBetaReductionException;
	
	/*
	 * Returns the characteristics of the last normalization.
	 */
	public NormalizationStatistics lastNormalization();
}