package typedLambda.model.term;

/*
 * A Term object represents a term of lambda calculus i.e. either a variable,
 *	 an abstraction or an application.
 *
 * Assemblies of terms make Term trees.
 * 
 * A combinator is a closed Term tree in normal form.
 */
public interface Term {

	/*
	 * The parent of a Term is the Term it belongs to.
	 * 
	 * A Term with no parent is said free.
	 * A Term with no child is said unlinked.
	 */
	public Term getParent();
	
	/*
	 * A Leaf object represents a variable in lambda calculus.
	 */
	public boolean isLeaf();
	
	/*
	 * An Abstraction object represents an abstraction in lambda calculus.
	 */
	public boolean isAbstraction();
	
	/*
	 * A Pair object represents an application in lambda calculus.
	 */
	public boolean isPair();
	
	/*
	 * Breaks links with eventual children.
	 * 
	 * Two cleared abstractions, two cleared leaves, two cleared terms
	 * 	are completely equivalent.
	 */
	public void clear();
	
	/*
	 * Return true if links with children are all broken.
	 */
	public boolean isCleared();
	
	/*
	 * Return true if a link with a child is broken.
	 */
	public boolean isBroken();
	
	/*
	 * Return the Term using the De Bruijn notation.
	 */
	public String toDeBruijnString();
	
	/*
	 * Return the Term using a detailed De Bruijn notation.
	 * 
	 * If a redex is given then its position is indicated.
	 */
	public String toDetailedDeBruijnString(Pair redex);
}