package ilog.language.design.types;

/**
 * @version     Last modified on Mon Sep 02 10:24:38 2002 by hak
 * @author      <a href="mailto:hak@ilog.fr">Hassan A&iuml;t-Kaci</a>
 * @copyright   &copy; 2001 <a href="http://www.ilog.fr/">ILOG, S.A.</a>
 */

import ilog.language.design.kernel.Expression;
import ilog.language.design.kernel.Application;
import ilog.language.design.kernel.Scope;

import ilog.language.util.Locatable;
import ilog.language.util.Extent;
import ilog.language.util.Stack;
import ilog.language.tools.Misc;
import java.util.ArrayList;
import java.util.Iterator;


/**
 * A <tt>TypeChecker</tt> is a backtracking prover that establishes
 * <a href="Goal.html"><tt>Goal</tt></a> objects.  * A <tt>Goal</tt>
 * is anything that may be established and undone by a <tt>TypeChecker</tt>,
 * and may be:
 * <ul>
 * <li> a <a href="TypingGoal.html"><tt>TypingGoal</tt></a>;
 * <li> a <a href="UnifyGoal.html"><tt>UnifyGoal</tt></a>;
 * <li> a <a href="BaseTypeGoal.html"><tt>BaseTypeGoal</tt></a>.
 * </ul>
 * A <a href="TypingGoal.html"><tt>TypingGoal</tt></a> object is a pair
 * consisting of an expression and a type.  Proving a typing goal
 * amounts to unifying its expression component's type with its
 * type component. Such goals are spawned by the type checking method of
 * expressions as per their type checking rules. Some globally defined
 * symbols having multiple types, it is necessary to keep choices of
 * these and backtrack to alternative types upon failure. Thus, a
 * <tt>TypeChecker</tt> object maintains all the necessary structures
 * for undoing the effects that happened since the last choice
 * point. These effects are:
 *
 * <ol>
 * <li> type variable binding,
 * <li> function type currying,
 * <li> application expression currying.
 * </ol>
 *
 * In addition, it is also necessary to remember all <tt>Goal</tt>s
 * that were proven since the last choice point in order to
 * prove them anew upon backtracking to an alternative choice. This is
 * necessary because the goals are spawned by <tt>typeCheck</tt> method
 * of expressions that may be exited long before a failure occurs. Then,
 * all the original typing goals that were spawned in the mean time since
 * the current choice point's goal must be reestablished. In order for this
 * to work, any choice points that were associated to these original goals
 * must also be recovered. To enable this, when a choice point is created
 * for a <a href="../kernel/Global.html"><tt>Global</tt></a> symbol, choices
 * are linked in the reverse order (<i>i.e.</i>, ending in the original goal)
 * to enable reinstating all choices that were tried for this goal.
 *
 * <p>
 *
 * In order to coordinate type proving, a typechecker object is passed
 * to all type checking and unification methods as an argument in order
 * to record any effect in the appropriate trail.
 *
 * <p>
 *
 * To recapitulate, the structures of a <tt>TypeChecker</tt> object are:
 *
 * <ul>
 * <li> a <i>goal stack</i> containing <tt>Goal</tt> objects that
 *      are yet to be proven;<p>
 * <li> a <i>binding trail stack</i> containing type variables and boxing
 *      masks to reset to "unbound" upon backtracking;<p>
 * <li> a <i>function type currying trail</i> containing 4-tuples of
 *      the form (function type, previous domains, previous range, previous
 *      boxing mask) for resetting the function type to the recorded domains,
 *      range, and mask upon backtracking;<p>
 * <li> an <i>application currying trail</i> containing triples of
 *      the form (application type, previous function, previous arguments)
 *      for resetting the application to the recorded function and arguments
 *      upon backtracking;<p>
 * <li> a <i>goal trail</i> containing <tt>Goal</tt> objects that
 *      have been proven since the last choice point, and must be reproven
 *      upon backtracking;<p>
 * <li> a <i>choice-point stack</i> whose entries consists of:
 *      <p>
 *      <ul>
 *      <li> a queue of <tt>TypingGoalEntry</tt> objects wherefrom to
 *           constructs new <tt>TypingGoal</tt> objects to try upon failure;
 *      <li> pointers to all trails up to which to undo effects.
 *      </ul>
 * </ul>
 */

public class TypeChecker implements GoalProver
{
  /**
   * This is the goal stack - it contains the goals remaining to be proved.
   */
  private Stack _goalStack = new Stack();
  /**
   * This is the choice-point stack - it contains the alternative choices
   * remaining to be made.
   */
  private Stack _chptStack = new Stack();
  /**
   * This stack records the bindable objects that have been affected.
   */
  private Stack _bindTrail = new Stack();
  /**
   * This stack records the components of function types affected by currying.
   */
  private Stack _typeTrail = new Stack();
  /**
   * This stack records the components of application expressions affected by
   * currying.
   */
  private Stack _applTrail = new Stack();
  /**
   * This stack records the goals that have been proven up to now.
   */
  private Stack _goalTrail = new Stack();

  /**
   * This stack records the exitable scopes that have been entered/exited.
   */
  private Stack _exitableStack = new Stack();


  /**
   * Checks that the specified extent is within an axitable scope, and if
   * it is returns that scope. Otherwise, tiggers a typing error.
   */
  final Scope checkExitable (Locatable extent) throws TypingErrorException
    {
      if (_exitableStack.isEmpty())
        error(new TypingErrorException("not within an exitable scope"),extent);

      return (Scope)_exitableStack.peek();
    }

  /**
   * Pushes the specified exitable scope onto the exitable scope stack.
   */
  final void pushExitable (Scope scope)
    {
      _exitableStack.push(scope);
    }

  /**
   * Pops the latest exitable scope .
   */
  final void popExitable ()
    {
      _exitableStack.pop();
    }

  private static final TypingErrorException _GENERIC_ERROR = new TypingErrorException("ill-typed form");
  private StaticSemanticsErrorException _currentError, _actualError;
  private Locatable _currentExtent;

  public final void error (StaticSemanticsErrorException error) throws StaticSemanticsErrorException
    {
      _currentError = error.setExtent(_currentExtent);

      if (_actualError == null || Misc.precedes(_actualError.extent(),_currentExtent))
        _actualError = _currentError;

      throw _currentError;
    }

  public final void error (StaticSemanticsErrorException error, Locatable locatable)
    throws StaticSemanticsErrorException
    {
      _currentExtent = locatable;
      error(error);
    }

  public final void reportError () throws StaticSemanticsErrorException
    {
      StaticSemanticsErrorException error = _actualError;
      reset();
      
      if (error != null)
        throw(error);
      else
        throw _GENERIC_ERROR;
    }    

  public final TypeChecker reset ()
    {
      _GENERIC_ERROR.setExtent(_currentExtent);
      _currentExtent = null;
      _currentError = _actualError = null;
      return this;
    }

  public final void trail (Bindable bindable)
    {
      //if (_chptStack.isEmpty()) return;

      _bindTrail.push(bindable);
    }

  final void trail (FunctionType type, Type[] domains, Type range, BoxingMask mask)
    {
      //if (_chptStack.isEmpty()) return;

      _typeTrail.push(mask);
      _typeTrail.push(range);
      _typeTrail.push(domains);
      _typeTrail.push(type);
    }

  public final void trail (Application application, Expression function, Expression[] arguments)
    {
      //if (_chptStack.isEmpty()) return;

      _applTrail.push(arguments);      
      _applTrail.push(function);      
      _applTrail.push(application);      
    }

  public final void trail (Goal goal)
    {
      //if (_chptStack.isEmpty()) return;

      _goalTrail.push(goal);      
    }

  public final void unify (Type t1, Type t2) throws TypingErrorException
    {
      _goalStack.push(new UnifyGoal(t1,t2));
      typeCheck();
    }

  public final void typeCheck (Goal goal) throws TypingErrorException
    {
      _goalStack.push(goal);
      if (goal instanceof TypingGoal)
        {
          Expression expression = ((TypingGoal)goal).expression();
          if (expression.otherTypes() != null)
            checkOtherTypes(expression);
        }
      typeCheck();
    }

  public final void typeCheck (Expression expression, Type type) throws TypingErrorException
    {
      typeCheck(new TypingGoal(expression,type));
    }

  public final void checkOtherTypes (Expression expression)
    {
      for (Iterator i=expression.otherTypes().iterator(); i.hasNext();)
        _goalStack.push(new TypingGoal(expression,(Type)i.next()));
    }

  public final void typeCheck () throws TypingErrorException
    {
      while (!_goalStack.isEmpty())
        {
          Goal goal = (Goal)_goalStack.pop();
          _currentExtent = goal.extent();

          try
            {
              goal.prove(this);
            }
          catch (FailedUnificationException error)
            {
              _backtrack();
            }
        }
    }

  final public void prove (Goal goal)
    {
      typeCheck(goal);
    }

  final public void debugProve (Goal goal)
    {
      ilog.language.tools.Debug.step("Proving goal: "+goal+
                                     "\n\tChoicepoint stack: "+_chptStack+
                                     "\n\t       Goal stack: "+_goalStack+
                                     "\n\t       Goal trail: "+_goalTrail);
    }

  public final ArrayList allTypes (Expression expression)
    {
      ArrayList types = new ArrayList();

      try
        {
          expression.typeCheck(this);
          types.add(expression.type().copy());
          //ilog.language.tools.Debug.step("Types so far: " + types);
        }
      catch (TypingErrorException error)
        {
          //ilog.language.tools.Debug.step(error.msg());
          return types;
        }

      for (;;)
        try
          {
            //ilog.language.tools.Debug.step("Backtracking to find more types...");
            _backtrack();
            typeCheck();
            types.add(expression.type().copy());
            //ilog.language.tools.Debug.step("Types so far: " + types);
          }
        catch (TypingErrorException error)
          {
            //ilog.language.tools.Debug.step(error.msg());
          return types;
          }
    }      

  public final ArrayList remainingTypes (Expression expression, ArrayList types)
    {
      for (;;)
        try
          {
            _backtrack();
            typeCheck();
            Type type = expression.type().copy();
            types.add(type);
          }
        catch (TypingErrorException error)
          {
            return types;
          }
    }

  final void pushChoicePoint (ChoicePoint choicePoint)
    {
      _chptStack.push(choicePoint.stamp(_goalStack.size(),
                                        _chptStack.size(),
                                        _bindTrail.size(),
                                        _typeTrail.size(),
                                        _applTrail.size(),
                                        _goalTrail.size()));
    }

  private final void _backtrack () throws TypingErrorException
    {
      if (_chptStack.isEmpty())
        {
          _clearAllStacks();       
          reportError();
        }

      ChoicePoint chpt = (ChoicePoint)_chptStack.peek();
      TypingGoal goal = ((TypingGoalEntry)chpt.goalEntries().pop()).getTypingGoal();
      
      _unwindBindTrail(chpt.bindTrailPoint());
      _unwindTypeTrail(chpt.typeTrailPoint());
      _unwindApplTrail(chpt.applTrailPoint());
      _unwindGoalTrail(chpt.goalTrailPoint(),goal);

      if (chpt.goalEntries().isEmpty())
        _chptStack.pop();
    }

  private final void _clearAllStacks ()
    {
      _goalStack.clear();
      _chptStack.clear();
      _exitableStack.clear();
      _goalTrail.clear();
      _unwindBindTrail();
      _unwindTypeTrail();
      _unwindApplTrail();
    }

  private final void _unwindBindTrail ()
    {
      _unwindBindTrail(0);
    }

  private final void _unwindBindTrail (int point)
    {
      while (_bindTrail.size() > point)
        ((Bindable)_bindTrail.pop()).unbind();
    }

  private final void _unwindTypeTrail ()
    {
      _unwindTypeTrail(0);
    }

  private final void _unwindTypeTrail (int point)
    {
      while (_typeTrail.size() > point)
        {
          FunctionType type = (FunctionType)_typeTrail.pop();
          type.setDomains((Type[])_typeTrail.pop());
          type.setRange((Type)_typeTrail.pop());
          type.setMask((BoxingMask)_typeTrail.pop());
        }
    }

  private final void _unwindApplTrail ()
    {
      _unwindApplTrail(0);
    }

  private final void _unwindApplTrail (int point)
    {
      while (_applTrail.size() > point)
        {
          Application application = (Application)_applTrail.pop();
          application.setFunction((Expression)_applTrail.pop());
          application.setArguments((Expression[])_applTrail.pop());
        }
    }

  /**
   * Recovers the goal stack from the goal trail up to the specified
   * point, at which point it replaces the oldest (to that point) trailed
   * goal with the specified one.
   */
  private final void _unwindGoalTrail (int point,TypingGoal newChoice)
    {
      while (_goalTrail.size() > point+1)
        {
          Goal goal = (Goal)_goalTrail.pop();
          if (goal instanceof TypingGoal)
            goal = _recoverChoices((TypingGoal)goal);
          _goalStack.push(goal);
        }

      _goalTrail.pop();
      _goalStack.push(newChoice);      
    }

  /**
   * Recovers the original initial typing goal and choice point corresponding to the
   * given typing goal. Returns the recovered original initial typing goal.
   */
  private final TypingGoal _recoverChoices (TypingGoal goal)
    {
      if (goal.previousChoice() != null)
        {
          ChoicePoint choicePoint = goal.getChoicePoint();

          while (goal.previousChoice() != null)
            {
              choicePoint.unpop(goal.goalEntry());
              goal = goal.previousChoice();
            }
        }

      return goal;
    }

}