package typedLambda.model.util;

import typedLambda.model.term.Abstraction;
import typedLambda.model.term.Pair;
import typedLambda.model.term.Term;
import typedLambda.model.type.FunctionType;
import typedLambda.model.type.Type;
import typedLambda.model.type.exception.UntypedTermException;
import typedLambda.model.util.exception.NotInNormalFormException;

/*
 * An Inferencer infers about type assignment on the Term nodes of a Term tree.
 * 
 * The Term tree must be in normal form.
 * 
 * The tree nodes are indexed.
 * First are the abstractions, next the pairs.
 * 
 * Leaves are not represented as tree nodes.
 * The Type of a Leaf is the Type of the bound Abstraction.
 */
public interface Inferencer{

	/*
	 * Returns the hand (or root term) of the combinator to be typed.
	 */
	public Abstraction getHand();
	
	/*
	 * Returns the count of the abstractions of the combinator to be typed.
	 */
	public int getAbstractionCount();
	
	/*
	 * Returns the count of the nodes of the Term tree.
	 */
	public int getNodeCount();
	
	/*
	 * Returns the node Term with the given node index.
	 */
	public Term getNode(int nodeIndex);
	
	/*
	 * Returns the Type of the node Term with the given node index.
	 * 
	 * It is a variable,
	 * 	that may takes different values before a possible stabilization.
	 */
	public Type getNodeType(int nodeIndex);
	
	/*
	 * Evaluates the type of a function
	 * 	whose argument	Type and result Type are given by a Pair.
	 */
	public FunctionType evaluatePairFunctionType(Pair pair);
	
	/*
	 * Executes a step in applying the application rules.
	 * 
	 * Returns true if this step is the last one.
	 * Returns false if more steps are required.
	 * 
	 * An untypable combinator throws an UntypedTermException.
	 */
	public boolean applyApplicationRules()
		throws NotInNormalFormException, UntypedTermException;

	/*
	 * Returns true if the node type with the given node index
	 * 	has been updated during the last application rule step,
	 * 	false elsewhere.
	 */
	public boolean isNodeTypeUpdated(int nodeIndex);
	
	/*
	 * Apply the abstraction rules
	 * 	and returns the type assigned to the combinator.
	 */
	public FunctionType applyAbstractionRules();
}