package typedLambda.model.util;

import java.io.PrintStream;

import typedLambda.model.term.Abstraction;
import typedLambda.model.type.FunctionType;
import typedLambda.model.util.exception.NotInNormalFormException;

/*
 * The TypeAssigner assigns types to combinators, à la Curry.
 * 
 * If the combinator A is typed by (T1 -> T2)
 * 	and the combinator B is typed by T1
 *  then the combinator AB is typed by T2.
 */
public interface TypeAssigner {

	/*
	 * Assigns a FunctionType to a combinator and returns this FunctionType.
	 * Returns null if the combinator cannot be typed, such as "λa.aa".
	 * 
	 * The combinator must be in normal form.
	 * 
	 * If the reasoning PrintStream is not null
	 * 	then produced the reasoning of assignment on this PrintStream.
	 */
	public FunctionType assignType(Abstraction combinatorHand, PrintStream reasoning)
			throws NotInNormalFormException;

	/*
	 * Type assignment without reasoning PrintStream.
	 */
	public FunctionType assignType(Abstraction combinatorHand)
			throws NotInNormalFormException;
	
	/*
	 * Returns the step count in applying the application rule
	 * 	during the last normalization.
	 */
	public int  getLastStepCount();
	
	/*
	 * Returns the Pair update count in applying the application rule
	 * 	during the last normalization.
	 */
	public int getLastPairUpdateCount();
}