package JavaAgent.resource.fopl;


import java.util.*;

/** 
** This class allows to build structured Terms that consist of a function
** symbol and a number of arguments. There must be at least one argument,
** otherwise this FunctTerm is a ConstTerm and should be represented 
** as such.
** @see ConstTerm
*/

public class FunctTerm extends Term {

  /**
  ** This constructor for a FunctTerm takes a Symbol (the function symbol) 
  ** and a Vector of arguments. All elements of the Vector must be Terms!
  ** @param aSy the function symbol
  ** @param someTerms the Vector of argument terms
  ** @exception IllegalArgumentException An exception will occur if the 
  ** given Symbol is null, the given Vector is null or empty, or one of the 
  ** elements of the Vector is not a Term.
  */
  public FunctTerm(Symbol aSy, Vector someTerms) 
      throws IllegalArgumentException{
    if (aSy == null)
      throw new IllegalArgumentException(
          "Attempt to create FunctTerm without function symbol.");
    theTerms = new Vector(someTerms.size()+2);
    theTerms.addElement(new ConstTerm(aSy));
    if ((someTerms == null) || someTerms.isEmpty())
      throw new IllegalArgumentException(
          "Attempt to create FunctTerm without arguments.");
    for (Enumeration e=someTerms.elements(); e.hasMoreElements(); ) {
      Object ne = e.nextElement();
      if (ne instanceof Term)
	theTerms.addElement((Term)ne);
      else 
	throw new IllegalArgumentException(
            "FunctTerm argument " + ne + " is not a Term as expected.");
    }
  }

  /** 
  ** Returns a copy of this FunctTerm. Variables and Symbols in the
  ** copy will be the same as the original ones. The function uses 
  ** <tt>clone()</tt> again to generate the copies of all the agrument 
  ** Terms in this FunctTerm. 
  ** @return an equal copy of this FunctTerm
  */
  public Object clone() {
    try {
      FunctTerm newFT = new FunctTerm();
      for (Enumeration e=theTerms.elements(); e.hasMoreElements(); )
	newFT.theTerms.addElement(((Term)e.nextElement()).clone());
      return newFT;
    }
    catch (Exception e) {
      throw new UnknownError(
          "Attempt to clone FunctTerm failed: " + e.getMessage());
    }
  }

  /** 
  ** Returns a copy of this FunctTerm with Variables replaced according to 
  ** the given Substitution. Symbols in the copy will be the same 
  ** as the original ones but Variables will be repalced by the respective 
  ** Terms in the given Substitution. A Variable not occurring in the 
  ** Substitution will be replaced by a new (different) Variable with the 
  ** same name. The given Substitution will be extended to include the 
  ** mappings of old Variables to new ones.
  ** <p> This function can also be used to generate a copy of this 
  ** FunctTerm that contains a new set of Variables. The given Substitution 
  ** should be a new, empty Substitution in this case. Otherwise cloning
  ** can be seen as instantiating this FunctTerm.
  ** @param s the Substitution that tells us how to replace Variables
  ** @return a new FunctTerm that is an instance of this FunctTerm; the 
  ** Substitution <tt>s</tt> will extended with any new Variable 
  ** replacements introduced
  ** @exception IllegalArgumentException An exception can occur if the given
  ** Substitution is null. In this case <tt>clone()</tt> (above) should be
  ** used.
  */
  public Term clone(Substitution s) throws IllegalArgumentException {
    try {
      FunctTerm newFT = new FunctTerm();
      for (Enumeration e=theTerms.elements(); e.hasMoreElements(); )
	newFT.theTerms.addElement(((Term)e.nextElement()).clone(s));
      return newFT;
    }
    catch (IllegalArgumentException iae) {
      throw iae;
    }
    catch (Exception e) {
      throw new UnknownError(
          "Attempt to clone FunctTerm failed: " + e.getMessage());
    }
  }

  /** 
  ** Returns a copy of this FunctTerm with Variables replaced according to 
  ** the given Substitution and the first Term replaced by the second. Apart
  ** from the Term replacement this function is just like 
  ** <tt>clone(Substitution)</tt> above. However if this is the first given 
  ** then an instance of the second given Term under the given Substitution 
  ** will be returned.
  ** @param s the Substitution that tells us how to replace Variables
  ** @param t the sub-Term to be replaced
  ** @param rTerm the (uninstantiated) replacement Term
  ** @return a new Term that is, apart from the replaced Term, an instance 
  ** of this Term; the Substitution <tt>s</tt> will extended with any new 
  ** Variable replacements introduced
  ** @exception IllegalArgumentException An exception can occur if the given
  ** Substitution is null. 
  */
  protected Term clone(Substitution s, Term t, Term rTerm) 
      throws IllegalArgumentException {
    if (this == t)
      return rTerm.clone(s);
    FunctTerm newFT = new FunctTerm();
    for (Enumeration e=theTerms.elements(); e.hasMoreElements(); )
      newFT.theTerms.addElement(((Term)e.nextElement()).clone(s, t, rTerm));
    return newFT;
  }

  /**
  ** This function adds the Variables in this FunctTerm to the given Vector. No
  ** Variable is added twice though.
  ** @param vars a Vector of Variables that will be extended
  ** @exception IllegalArgumentException An exception can occur if the given
  ** Vector is null.
  */
  public void getVars(Vector vars) throws IllegalArgumentException {
    for (Enumeration e=theTerms.elements(); e.hasMoreElements(); )
      ((Term)e.nextElement()).getVars(vars);
  }

  /**
  ** This function attempts to extend the given Substitution so that this 
  ** FunctTerm and the given Term are unified. It returns <tt>true</tt> if 
  ** and only if this is possible. If the other Term is a FunctTerm then 
  ** unification succeeds only if the two function symbols are equal and the
  ** Substitution can be extended to unify all arguments. If 
  ** the other Term is a VarTerm then unification succeeds only if the 
  ** given Substitution can be extended accordingly.
  ** @param other the other Term this FunctTerm is to be unified with
  ** @param s the Substitution to be extended for the unification
  ** @return whether a unifying extension of the given Substitution was 
  ** possible
  ** @exception IllegalArgumentException An exception will occur if the given
  ** Term or the given Substitution are null.
  ** @exception UnificationException An exception will occur if the given
  ** Substitution was already finshed.
  */
  public boolean unify(Term other, Substitution s)
      throws IllegalArgumentException, UnificationException {
    if (s == null)
      throw new IllegalArgumentException(
          "Attempt to extend null Substitution.");
    if (other == null)
      throw new IllegalArgumentException(
          "Attempt to unify " + this + " with null.");
    if (other instanceof VarTerm)
      return s.unify(((VarTerm)other).getVar(), this);
    if (other instanceof FunctTerm) {
      Vector otherTerms = ((FunctTerm)other).theTerms;
      if (theTerms.size() != otherTerms.size())
	return false;
      Enumeration e1=theTerms.elements();
      for (Enumeration e2=otherTerms.elements(); e2.hasMoreElements(); )
	if (!((Term)e1.nextElement()).
	        unify((Term)e2.nextElement(), s))
	  return false;
      return true;
    }
    return false;
  }

  /**
  ** This function tests whether one of the Variables in the given set of 
  ** variables occurs in this FunctTerm taking the given Substitution into 
  ** account.
  ** @param theVars the Variables to be tested whether they occur in this 
  ** FunctTerm
  ** @param s the Substitution under which the test takes place
  ** @return <tt>true</tt> if and only if a Variable in the given Vector is
  ** contained in this FunctTerm under the given Substitution
  */
  protected boolean contains(Vector theVars, Substitution s, Vector okVars) {
    for (Enumeration e=theTerms.elements(); e.hasMoreElements(); )
      if (((Term)e.nextElement()).contains(theVars, s, okVars))
	return true;
    return false;
  }

  /**
  ** This function returns an Enumeration over the arguments of this
  ** FunctTerm.
  ** @return an Enumeration over the arguments of this FunctTerm
  */
  public Enumeration arguments() {
    Enumeration e = theTerms.elements();
    e.nextElement();
    return e;
  }

  /**
  ** This function returns an Enumeration over all sub-terms in this FunctTerm.
  ** Note that this is not an Enumeration over the arguments but every 
  ** sub-Term within this FunctTerm.
  ** @return an Enumeration over all sub-Terms in this FunctTerm
  */
  public Enumeration allSubTerms() {
    return new SubTermEnum(theTerms);
  }

  /**
  ** A FunctTerm is printed as ( &lt;constant&gt; &lt;term&gt;+ )
  ** @return the String that represents this FunctTerm
  */
  public String toString() {
    String result = new String("(");
    result += theTerms.elementAt(0);
    for (int i=1; i<theTerms.size(); i++)
      result += " " + theTerms.elementAt(i).toString();
    return result + ')';
  }

  /** 
  ** A FunctTerm is equal to any other FunctTerm that consists
  ** of an equal function symbol followed by an equal number of equal Terms.
  ** @param otherTerm the Object this FunctTerm is compared to
  ** @return whether the given Object equals this FunctTerm
  */
  public boolean equals(Object otherTerm) {
    if (otherTerm == null)
      return false;
    if (! (otherTerm instanceof FunctTerm))
      return false;
    FunctTerm ft = (FunctTerm)otherTerm;
    if (ft.theTerms.size() != theTerms.size())
      return false;
    Enumeration e1=theTerms.elements();
    for (Enumeration e2=ft.theTerms.elements(); e2.hasMoreElements(); )
      if (! e1.nextElement().equals(e2.nextElement()))
	return false;
    return true;
  }

  private FunctTerm() {
    theTerms = new Vector();
  }

  /** 
  ** the Vector of Terms in this FunctTerm; the first of these should be a 
  ** ConstTerm containing the function symbol
  */
  private Vector theTerms;
}
