package ilog.language.design.types;

/**
 * @version     Last modified on Wed Oct 16 15:21:20 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.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 one of the following:
 * <ul>
 * <li> <a href="EmptyGoal.html"><tt>EmptyGoal</tt>,
 * <li> <a href="TypingGoal.html"><tt>TypingGoal</tt>,
 * <li> <a href="GlobalTypingGoal.html"><tt>GlobalTypingGoal</tt>,
 * <li> <a href="PruningGoal.html"><tt>PruningGoal</tt>,
 * <li> <a href="PushExitableGoal.html"><tt>PushExitableGoal</tt>,
 * <li> <a href="PopExitableGoal.html"><tt>PopExitableGoal</tt>,
 * <li> <a href="CheckExitableGoal.html"><tt>CheckExitableGoal</tt>,
 * <li> <a href="ShadowUnifyGoal.html"><tt>ShadowUnifyGoal</tt>,
 * <li> <a href="UnifyGoal.html"><tt>UnifyGoal</tt>.
 * <li> <a href="BaseTypeGoal.html"><tt>BaseTypeGoal</tt>,
 * <li> <a href="UnifyBaseTypeGoal.html"><tt>UnifyBaseTypeGoal</tt>,
 * <li> <a href="ResiduatedGoal.html"><tt>ResiduatedGoal</tt>,
 * </ul>
 * The most common goal 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 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. 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:
 *      <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.
 *      </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).
   */
  static boolean GIVE_DETAILS = false;

  public TypeChecker ()
    {
    }

  public TypeChecker (boolean give_details)
    {
      GIVE_DETAILS = give_details;
    }

  /**
   * 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 (_exitStack.isEmpty())
        error(new TypingErrorException("not within an exitable scope"),extent);

      return (Scope)_exitStack.peek();
    }

  /**
   * 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;
      reset();
      
      throw error != null ? error : _GENERIC_ERROR;
    }    

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

  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
    {
      typeCheck(new UnifyGoal(t1,t2));
    }

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

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

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

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

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

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

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

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

      try
        {
          expression.typeCheck(this);
          types.add(expression.type().copy());
          _showStep("Types so far: " + types);
        }
      catch (TypingErrorException error)
        {
          return types;
        }

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

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

  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 ()
    {
      TypingState ctpt = popCutPoint();

      while (((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())
        {
          _clearAllStacks();       
          reportError();
        }

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

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

  private final void _clearAllStacks ()
    {
//      TimeStamp.reset();
      _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 goal = (Goal)_goalTrail.pop();
          _goalStack.push(goal);

          if (goal instanceof GlobalTypingGoal)
            ((GlobalTypingGoal)goal).deactivate();
          else
            if (goal instanceof PopExitableGoal)
              pushExitable(((PopExitableGoal)goal).scope());
            else
              if (goal instanceof PushExitableGoal)
                popExitable();
        }

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

  final private void _showState ()
    {
      _show(_showNonEmpty(_goalStack,"        Goal stack")+/*
            _showNonEmpty(_goalTrail,"        Goal trail")+
            _showNonEmpty(_exitStack,"        Exit 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)
    {
      if (_tracing) System.out.println(s);
    }

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

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

}