package typedLambda.model.term;

import typedLambda.model.term.exception.ClearFirstException;
import typedLambda.model.term.exception.NotAFreeTermException;

/*
 * A Pair object represents an application in lambda calculus.
 */
public interface Pair extends Term {

	/*
	 * Returns the left part of the Pair, i.e. the function.
	 */
	public Term getLeft();
	
	/*
	 * Set the left part of the Pair, i.e. the function.
	 * 
	 * The Pair must have no left part.
	 * The left Term must have no parent.
	 */
	public void setLeft(Term left)
			throws ClearFirstException, NotAFreeTermException;
	
	/*
	 * Breaks the left part link.
	 */
	public void clearLeft();
	
	/*
	 * Returns the right part of the Pair, i.e. the argument.
	 */
	public Term getRight();
	
	/*
	 * Set the right part of the Pair, i.e. the argument.
	 * 
	 * The Pair must have no right part.
	 * The right Term must have no parent.
	 */
	public void setRight(Term right)
			throws ClearFirstException, NotAFreeTermException;
	
	/*
	 * Breaks the right part link.
	 */
	public void clearRight();
	
	/*
	 * A Pair is normalizable if its left part or its right part is an Abstraction.
	 * If its left part is an Abstraction then it is a redex.
	 * If its right part is an Abstraction then it is an Abstraction going up.
	 */
	public boolean isNormalizable();
}