package JavaAgent.resource.fopl;


import java.util.*;

/** 
** This class is an Enumerator for sub-Terms in a Vector of Terms. The first
** element of the Vector as this is usually the function or predicate Term.
** The Enumerator gets all arguments in sequence. However, if a Term thus
** enumerated is a FunctTerm then all of its sub-Terms will be enumerated
** before the next argument but after the FunctTerm itself.
** @see Literal
** @see FunctTerm
*/

public class SubTermEnum implements Enumeration {

  /**
  ** This constructor takes a Vector of Terms to enumerate. The first Term
  ** will be ignored.
  */
  public SubTermEnum(Vector terms) {
    tEnums = new Stack();
    Enumeration te = terms.elements();
    te.nextElement();
    tEnums.push(te);
  }

  /**
  ** This function tests whether there are more sub-Terms.
  ** @return whether there are more sub-Terms
  */
  public boolean hasMoreElements() {
    return (! tEnums.isEmpty());
  }

  /**
  ** This function returns the next sub-Term in this Enumeration.
  ** @return next sub-Term
  */
  public Object nextElement() {
    Enumeration e = (Enumeration)tEnums.peek();
    Term result = (Term)e.nextElement();
    if (result instanceof FunctTerm)
      tEnums.push(((FunctTerm)result).arguments());
    else while ((! tEnums.isEmpty()) && (! e.hasMoreElements())) {
      tEnums.pop();
      if (! tEnums.isEmpty())
	e = (Enumeration)tEnums.peek();
    }
    return result;
  }

  /**
  ** a Stack of Enumerations for the Terms
  */
  Stack tEnums;
}
