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

package ilog.language.design.types;

/**
 * @version     Last modified on Thu Dec 12 16:21:05 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.design.kernel.Global;
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.ViewableStack;
import ilog.language.util.Stack;
import ilog.language.util.Queue;
import ilog.language.tools.Debug;
import ilog.language.tools.Misc;

import java.util.Iterator;
import java.util.AbstractList;

/**
 * A <tt>TypeChecker</tt> is a backtracking prover that establishes <a
 * href="Goal.html"><tt>Goal</tt></a> objects.  The most common goal is a <a
 * href="TypingGoal.html"><tt>TypingGoal</tt></a>, and consists 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.
 *
 * <p>
 *
 * Some globally defined symbols having multiple types, it is necessary to keep
 * choices of these and backtrack to alternative types upon failure. Therefore, a
 * special goal is used to handle the typing of a <a
 * href="../kernel/Global.html"><tt>Global</tt></a>: a <a
 * href="GlobalTypingGoal.html"><tt>GlobalTypingGoal</tt></a>. Thus, a
 * <tt>TypeChecker</tt> object maintains all the necessary structures for undoing
 * the effects that happened since the latest 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 latest 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. This is why we use a
 * <i>goal trail</i> that remembers the sequence of goals that was spawned.  In
 * order for this to work, any choice points that were associated to these original
 * goals must also be reinitialized. All this machinery (including choice point
 * stack pushing and popping) is appropriately set up and managed as it should be by
 * <a href="GlobalTypingGoal.html"><tt>GlobalTypingGoal</tt></a>s.
 *
 * <p>
 *
 * In order to maintain consistency of the effects of type checking, a typechecker
 * object is passed to all goal proving and type unification methods as an argument
 * to enable recording of any such effect in the appropriate trail. These effects
 * may then be appropriately undone upon backtracking by <i>unwinding</i> the trails
 * back to where the latest choice point indicates.
 *
 * <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 <a href="ChoicePoint.html">
 *      <tt>ChoicePoint</tt></a> objects containing:
 *      <p>
 *      <ul>
 *      <li> a queue of <tt>CodeEntry</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 (a <a href="TypingState.html">
 *           <tt>TypingState</tt></a>).
 *      </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 cut-point states of the type-checker before the latest
   * of which it will not backtrack.
   */
  private Stack _ctptStack = new Stack();
  /**
   * This stack records the exitable scopes that have been entered/exited.
   */
  private Stack _exitStack = new Stack();

  private boolean _tracing = false;

  public final boolean isTracing ()
    {
      return _tracing;
    }

  public final void setTracing (boolean flag)
    {
      if (flag) Type.resetNames();
      _tracing = flag;
    }

  public final void toggleTrace ()
    {
      setTracing(!_tracing);
    }

  /**
   * This is a static boolean switch to make type clash errors give the actual incompatible
   * types that it found. Due to backtracking over overloaded types, this information is often
   * wrong, and so it is not reported when this flag is <tt>false</tt> (default).
   */
  public static boolean GIVES_DETAILS = false;

//    /**
//     * This is a static boolean switch to dis/allow unification of int <i>vs.</i> real
//     * types; default is <tt>false</tt>.
//     */
//    public static boolean ALLOWS_LIBERAL_NUMBER_TYPING = false;

  /**
   * This is a boolean switch to dis/allow unification of position <i>vs.</i> named
   * tuple types; default is <tt>false</tt>.
   */
  public static boolean ALLOWS_POSITIONAL_NAMED_TUPLES = false;

  /**
   * This is a boolean switch to dis/allow unification of opaquely defined tuple types
   * against plain tuple types; default is <tt>false</tt>.
   */
  public static boolean ALLOWS_UNIFYING_OPAQUE_TUPLES = false;

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

      return (Scope)_exitStack.peek();
    }

  /**
   * Pushes the specified goal on the goal stack.
   */
  public final void pushGoal (Goal goal)
    {
      _goalStack.push(goal);
    }

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

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

  /**
   * Pushes the current typing state on the cut-point stack.
   */
  public final void pushCutPoint ()
    {
      _ctptStack.push(getTypingState());
    }

  /**
   * Pops and returns the latest typing state on the cut-point stack.
   */
  public final TypingState popCutPoint ()
    {
      return (TypingState)_ctptStack.pop();
    }

  private static final TypingErrorException _GENERIC_ERROR
    = new TypingErrorException("ill-typed form");
  private StaticSemanticsErrorException _error;
  private Goal _currentGoal;
  private Locatable _currentExtent;

  private final void _assessCulprit (StaticSemanticsErrorException error)
    {
      if (_error == null || _currentGoal.timeStamp() > _error.stamp())
        {
          _error = error.setExtent(_currentExtent);
          if (_currentGoal != null)
            _error.setStamp(_currentGoal.timeStamp());
        }
    }

  public final void error (StaticSemanticsErrorException error)
    throws StaticSemanticsErrorException
    {
      _assessCulprit(error);
      throw _error;
    }

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

  public final void reportError () throws StaticSemanticsErrorException
    {
      StaticSemanticsErrorException error = _error;

      //      if (_ctptStack.isEmpty()) reset();
      
      throw error != null ? error : _GENERIC_ERROR;
    }    

  public final void trail (Bindable bindable)
    {
      _bindTrail.push(bindable);
    }

  final void trail (FunctionType type, Type[] domains, Type range, BoxingMask mask)
    {
      _typeTrail.push(mask);
      _typeTrail.push(range);
      _typeTrail.push(domains);
      _typeTrail.push(type);
    }

  public final void trail (Application application, Expression function, Expression[] arguments)
    {
      _applTrail.push(arguments);
      _applTrail.push(function);
      _applTrail.push(application);
    }

  public final void trail (Goal goal)
    {
      _goalTrail.push(goal);
    }

  public final void unify (Type t1, Type t2) throws TypingErrorException
    {
      prove(new UnifyGoal(t1,t2));
    }

  public final void unify (Type t1, Type t2, Locatable extent) throws TypingErrorException
    {
      prove(new UnifyGoal(t1,t2,extent));
    }

  public final void prune (Global global, Type filter, Locatable extent) throws TypingErrorException
    {
      prove(new PruningGoal(global,filter,extent));
    }

  public final void residuate (Type type, Goal goal) throws TypingErrorException
    {
      ResiduatedGoal residuation = new ResiduatedGoal(goal);
      residuation.addTrigger(type);
      prove(goal);
    }

  public final void disallowVoid (Type type, Locatable extent, Object info) throws TypingErrorException
    {
      residuate(type,new NoVoidTypeGoal(type,extent,": "+info));
    }

  public final void prove (Goal goal) throws TypingErrorException
    {
      _goalStack.push(goal);
      typeCheck();
    }

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

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

          try
            {
              if (_tracing)
                {
                  if (!(_currentGoal instanceof GlobalTypingGoal)) showGoal(_currentGoal);
                  _showState();
                }
              _currentGoal.prove(this);
              if (_tracing) _showStep("Goal "+_currentGoal.timeStamp()+" succeeded; proceeding...");
            }
          catch (FailedUnificationException error)
            {
              if (_tracing) _showStep("Goal "+_currentGoal.timeStamp()+" failed: "+error.msg());
              _backtrack();
            }
        }
    }

  public final void allTypes (Expression expression, AbstractList types)
    {
      try
        {
          expression.typeCheck(this);
          types.add(expression.type().copy());
          if (_tracing) _showStep("Types so far: " + types);
        }
      catch (TypingErrorException error)
        {
          return;
        }

      for (;;)
        try
          {
            if (_tracing) _showStep("Backtracking to find more types...");
            _backtrack();
            typeCheck();
            types.add(expression.type().copy());
            if (_tracing) _showStep("Types so far: " + types);
          }
        catch (TypingErrorException error)
          {
            return;
          }
    }      

  public final void remainingTypes (Expression expression, AbstractList types)
    {
      for (;;)
        try
          {
            if (_tracing)
              _showStep("Found type "+expression.type()+"; looking for more types...");
            _backtrack();
            typeCheck();
            types.add( expression.type().copy());
            if (_tracing) _showStep("Types so far: " + types);
          }
        catch (TypingErrorException error)
          {
            return;
          }
    }

  public final TypingState getTypingState ()
    {
      return new TypingState().save(_goalStack.size(),_chptStack.size(),_bindTrail.size(),
                                    _typeTrail.size(),_applTrail.size(),_goalTrail.size());
    }

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

  final void popChoicePoint ()
    {
      _chptStack.pop();
    }

  private final ChoicePoint _getChoicePoint ()
    {
      return (ChoicePoint)_chptStack.peek();
    }

  private final TypingState _getCutPoint ()
    {
      return (TypingState)_ctptStack.peek();
    }

  public final void undoCutPoint ()
    {
      if (_tracing)
        {
          System.out.println("Undoing cut point from state:");
          _showState();
        }

      TypingState ctpt = popCutPoint();

      while (!_goalTrail.isEmpty() && ((Goal)_goalTrail.peek()).timeStamp() > ctpt.timeStamp())
        _goalTrail.pop();
      
      _unwindBindTrail(ctpt.bindTrailPoint());
      _unwindTypeTrail(ctpt.typeTrailPoint());
      _unwindApplTrail(ctpt.applTrailPoint());
    }

  private final boolean _noMoreChoices ()
    {
      return _chptStack.isEmpty()
          || !_ctptStack.isEmpty()
          && _getChoicePoint().timeStamp() < _getCutPoint().timeStamp();
    }

  private final void _backtrack () throws TypingErrorException
    {
      if (_noMoreChoices())
          reportError();

      ChoicePoint chpt = (ChoicePoint)_chptStack.peek();
      
      _unwindGoalTrail(chpt.timeStamp());
      _unwindBindTrail(chpt.bindTrailPoint());
      _unwindTypeTrail(chpt.typeTrailPoint());
      _unwindApplTrail(chpt.applTrailPoint());

      if (_tracing) _show("Retrying Goal " + chpt.timeStamp() + " ...");
    }

  public final TypeChecker reset ()
    {
//        TimeStamp.reset();
      _GENERIC_ERROR.setExtent(_currentExtent);
      _currentExtent = null;
      _error = null;
      _clearAllStacks();
      return this;
    }

  private final void _clearAllStacks ()
    {
      _goalStack.clear();
      _chptStack.clear();
      _exitStack.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());
        }
    }

  private final void _unwindGoalTrail (long stamp)
    {
      while (((Goal)_goalTrail.peek()).timeStamp() > stamp)
        ((Goal)_goalTrail.pop()).undo(this);

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

  final private void _showState ()
    {
      if (_tracing) _show(_showNonEmpty(_goalStack,"        Goal stack")+
                    _showNonEmpty(_goalTrail,"        Goal trail")+
                    _showNonEmpty(_exitStack,"        Exit stack")+
                    _showNonEmpty(_ctptStack,"   Cut point stack")+
                    _showNonEmpty(_chptStack,"Choice point stack")+
                    _showChoicePointEntries());
    }

  final private String _showNonEmpty (ViewableStack stack, String header)
    {
      return stack.isEmpty() ? "" : Misc.view(stack,header,0,100);
    }

  final private String _showChoicePointEntries ()
    {
      if (_chptStack.isEmpty()) return "";

      StringBuffer buf = new StringBuffer();
      
      for (int i=0; i < _chptStack.size(); i++)
        {
          ChoicePoint chpt = (ChoicePoint)_chptStack.get(i);
          buf.append(Misc.view(chpt.entries(),
                               "Next choices for goal "+chpt.timeStamp(),
                               0,86));
        }

      return buf.toString();
    }

  private final void _show (String s)
    {
      System.out.println(s);
    }

  private final void _showStep (String s)
    {
      Debug.step(s);
    }

  final void showGoal (Goal goal)
    {
      if (_tracing) _show(Misc.etc(120,"Currently attempting ==> "+goal));
    }

}