package typedLambda.model.substitute;

import typedLambda.model.term.Term;

/*
 * Substitutions of terms are used by the beta reductions.
 * 
 * There are four types of substitution :
 * 	the BodySubstitution,
 * 	the LeftSubstitution,
 * 	the RightSubstitution,
 * 	the null substitution.
 * 
 * A BodySubstitution if a substitution whose the substituted Term
 * 	is the body of an Abstraction.
 * 
 * A LeftSubstitution is a substitution whose the substituted Term
 * 	is the left part of a Pair.
 * 
 * A RightSubstitution is a substitution whose the substituted Term
 * 	is the right part of a Pair.
 * 
 * The substitutions are organized in circular linked lists.
 * Each circular list contains exactly one null substitution.
 * This null substitution is both the head and the queue of the list.
 * 
 * Null substitutions are unchanged.
 * The other types of substitution are recycled after use.
 * 
 * Each beta reduction builds, processes and returns to factory
 * 	a list of substitution, with various types.
 * 
 * A list of substitution for reuse contains only one type of substitution
 * 	(the null substitution is excepted).
 * 
 * An empty list contains only the null substitution.
 */
public interface Substitution {

	/*
	 * True for the null substitution, exclusively.
	 */
	public boolean isNull();
	
	/*
	 * True for the body substitution, exclusively.
	 */
	public boolean isBodySubstitution();

	/*
	 * True for the left substitution, exclusively.
	 */
	public boolean isLeftSubstitution();

	/*
	 * True for the right substitution, exclusively.
	 */
	public boolean isRightSubstitution();

	/*
	 * To call before returning to factory.
	 * 
	 * Two body substitutions, two left substitutions, two right substitutions
	 * 	are completely equivalent.
	 */
	public void clear();
	
	/*
	 * Returns the previous substitution in the circular list it belongs to.
	 * 
	 * May returns the null substitution but never null.
	 */
	public Substitution getPrevious();
	
	/*
	 * This method is used for adding to or removing from the circular list.
	 */
	public void setPrevious(Substitution previous);
	
	/*
	 * Returns the parent Term of the substituted Term.
	 */
	public Term getParentTerm();
	
	/*
	 * Returns the binders count.
	 * 
	 * This is the count of the parent Abstraction of the substituted Term.
	 */
	public int bindersCount();

	/*
	 * Executes the substitution by substituting the substitutable Term
	 * 	by the given term.
	 * 
	 * The given Term takes the place of the substituted Term.
	 * 
	 * The given Term may be null.
	 * The substituted Term may be null.
	 * The substituted Term and the given Term may be the same.
	 */
	public void substituteBy(Term term);
}