package ilog.language.design.types;

/**
 * @version     Last modified on Tue Oct 08 18:40:28 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 java.util.Iterator;
import ilog.language.util.Locatable;
import ilog.language.design.kernel.Global;

public class GlobalTypingGoal extends Goal
{
  /**
   * The <a href="../kernel/Global.html"><tt>Global</tt></a> being type-checked.
   */
  private Global _global;

  private TypingGoal _currentGoal;
  private boolean _activated = false;
  private ChoicePoint _choicePoint;

  /**
   * Constructs a global typing goal with the specified <a href="../kernel/Global.html">
   * <tt>Global</tt></a>.
   */
  public GlobalTypingGoal (Global global)
    {
      _global = global;
    }

  final Locatable extent ()
    {
      return _global;
    }

  final void deactivate ()
    {
      _activated = false;
    }

  private final ChoicePoint _choicePoint ()
    {
      if (_choicePoint == null) _choicePoint = new ChoicePoint();
      return _choicePoint;
    }

  private final void _activate (TypeChecker typeChecker) throws FailedUnificationException
    {
      Iterator i = _global.viableTypes().iterator();

      if (!i.hasNext())
        {
          Type.resetNames();
          typeChecker.error(new TypeClashException("no type allowed for '"+_global+"' fits "+
                                                   _global.sieve().toQuantifiedString()),
                            _global);
        }

      _setCurrentGoal((CodeEntry)i.next());
      if (i.hasNext())
        {
          _choicePoint().setTimeStamp(this);
          while (i.hasNext())
            _choicePoint.push((CodeEntry)i.next());
          typeChecker.pushChoicePoint(_choicePoint);
        }

      _activated = true;
    }
  
  private final void _setCurrentGoal (CodeEntry entry)
    {
      _currentGoal = new TypingGoal(_global,entry.type().copy());
      _currentGoal.setIsTrailable(false);
      _currentGoal.setTimeStamp(this);
      _global.setCodeEntry(entry);
    }
  
  private final void _backtrack (TypeChecker typeChecker)
    {
      _setCurrentGoal(_choicePoint.pop());

      if (_choicePoint.isEmpty())
        {
          typeChecker.popChoicePoint();
          deactivate();
        }
    }
  
  final void prove (TypeChecker typeChecker) throws FailedUnificationException
    {
      trail(typeChecker);

      if (!_activated)
        _activate(typeChecker);
      else
        _backtrack(typeChecker);

      typeChecker.showGoal(_currentGoal);
      _currentGoal.prove(typeChecker);
    }

  /**
   * Returns a string form of this typing goal.
   */
  final public String toString ()
    {
      return _activated
           ? _currentGoal.toString()
           : super.toString() + ": (global) symbol => " + _global;
    }
}