//\\//\\//\\//\\//\\//\\//\\//\\//\\//\\//\\//\\//\\//\\//\\//\\//\\
// PLEASE DO NOT EDIT WITHOUT THE EXPLICIT CONSENT OF THE AUTHOR! \\
//\\//\\//\\//\\//\\//\\//\\//\\//\\//\\//\\//\\//\\//\\//\\//\\//\\

package ilog.language.design.types;

/**
 * @version     Last modified on Tue Nov 12 16:24:53 2002 by Hak
 * @author      <a href="mailto:hak@ilog.fr">Hassan A&iuml;t-Kaci</a>
 * @copyright   &copy; 2000-2002 <a href="http://www.ilog.fr/">ILOG, S.A.</a>
 */

import ilog.language.util.Locatable;
import ilog.language.design.kernel.Expression;

/**
 * A <tt>ArrayIndexTypeGoal</tt> encapsulates a pair consisting of an expression and
 * an array type. Such a goal is <i>proven</i> in the context of a <tt>TypeChecker</tt>
 * by unifying the type of the expression with the array type's index type.
 */

public class ArrayIndexTypeGoal extends Goal
{
  private Expression _expression;
  private ArrayType _type;

  public ArrayIndexTypeGoal (Expression expression, ArrayType type)
    {
      _expression = expression;
      _type = type;
    }

  final Locatable extent ()
    {
      return _expression;
    }

  final Expression expression ()
    {
      return _expression;
    }

  final Type arrayType ()
    {
      return _type;
    }

  final void prove (TypeChecker typeChecker) throws FailedUnificationException
    {
      trail(typeChecker);
      _expression.type().unify(_type.indexType(),typeChecker);
    }

  final public String toString ()
    {
      return super.toString() +
             ": (array index type) array type => " + _type.value() +
             ", expression => " + _expression;
    }
}