package lambdaKit.model.term;

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

/*
 * An Abstraction object represents an abstraction in the lambda calculus.
 */
public interface Abstraction extends Term {

	/*
	 * Returns an identifier of this Abstraction.
	 */
	public int getId();
	
	/*
	 * Returns the body of the abstraction.
	 */
	public Term getBody();
	
	/*
	 * Set the body of the abstraction.
	 * 
	 * The abstraction must have no body.
	 * The body must have no parent.
	 */
	public void setBody(Term body)
			throws ClearFirstException, NotAFreeTermException;

	/*
	 * Breaks the body link.
	 */
	public void clearBody();
}