package JavaAgent.resource.fopl;


import java.util.*;

/** 
** The most basic Term is a ConstTerm that is represented by a Symbol. 
** ConstTerms or constants are usually used in logic to represent named 
** individuals or concepts.
** @see Symbol
*/

public class ConstTerm extends Term {

  /** 
  ** This constructor just takes the Symbol that is this Term. Note that 
  ** there is only one Symbol (in memory) with this name, but there may 
  ** well be several ConstTerms containing this Symbol.
  ** @param aSy the Symbol that is this Term
  ** @exception IllegalArgumentException An exception will occur if the 
  ** given Symbol is null.
  */
  public ConstTerm(Symbol aSy) throws IllegalArgumentException {
    if (aSy == null)
      throw new IllegalArgumentException(
          "Attempt to create ConstTerm without Symbol.");
    theSy = aSy;
  }

  /** 
  ** This constructor takes a String that is interpreted as the name of a 
  ** Symbol. This constructor will not check whether the given name is a 
  ** legal Symbol name (e.g. does not contain spaces).
  ** @param aName the name of the Symbol that is this Term
  ** @exception IllegalArgumentException An exception will occur if the 
  ** supplied String is empty or null.
  */
  public ConstTerm(String aName) throws IllegalArgumentException {
    theSy = Symbol.get(aName);
  }

  /**
  ** Cloning a ConstTerm returns another ConstTerm that contains 
  ** the same Symbol.
  ** @return a new ConstTerm containing the same Symbol
  */
  public Object clone() {
    try {
      return new ConstTerm(theSy);
    }
    catch (IllegalArgumentException iae) {
      throw new UnknownError("Attempt to clone ConstTerm without Symbol.");
    }
  }

  /**
  ** Cloning a ConstTerm under a given Substitution returns another 
  ** ConstTerm that contains the same Symbol. Since a ConstTerm cannot 
  ** contain Variables the Substitution will be ignored.
  ** @param s a Substitution (will be ignored)
  ** @return a new ConstTerm containing the same Symbol
  */
  public Term clone(Substitution s) {
    try {
      return new ConstTerm(theSy);
    }
    catch (IllegalArgumentException iae) {
      throw new UnknownError("Attempt to clone ConstTerm without Symbol.");
    }
  }

  /**
  ** Cloning a ConstTerm under a given Substitution returns another 
  ** ConstTerm that contains the same Symbol or an instance of the second
  ** given Term if this is the first given Term. 
  ** @param s a Substitution
  ** @param t the Term to be replaced
  ** @param rTerm the (uninstantiated) replacement Term
  ** @return a new ConstTerm containing the same Symbol or an instance of
  ** rTerm if this Term is the given Term t
  */
  protected Term clone(Substitution s, Term t, Term rTerm)
      throws IllegalArgumentException {
    if (this == t)
      return rTerm.clone(s);
    return new ConstTerm(theSy);
  }

  /**
  ** This function adds the Variables in this Term to the given Vector. 
  ** However, as ConstTerms do not contain Variables this function 
  ** effectively does nothing.
  ** @param vars a Vector of Variables (will be ignored)
  */
  public void getVars(Vector vars) {
  }

  /**
  ** This function attempts to extend the given Substitution so that this 
  ** Term and the given Term are unified. It returns <tt>true</tt> if and 
  ** only if this is possible. If the other Term is a ConstTerm then 
  ** unification succeeds only if the two contained Symbols are equal. 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 ConstTerm 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 ((other == null) || (s == null))
      throw new IllegalArgumentException(
          "Attempt to unify ConstTerm with null argument");
    if (other instanceof ConstTerm) 
      return theSy == ((ConstTerm)other).theSy;
    if (other instanceof VarTerm)
      return s.unify(((VarTerm)other).getVar(), this);
    return false;
  }

  /**
  ** This function tests whether one of the Variables in the given set of 
  ** variables occurs in this Term taking the given Substitution into account.
  ** Since ConstTerms don't contain any Variables this is always false and 
  ** this function effectively does nothing.
  ** @param theVars the Variables to be tested whether they occur in this Term 
  ** (will be ignored)
  ** @param s the Substitution under which the test takes place (will be 
  ** ignored)
  ** @return <tt>false</tt> 
  */
  public boolean contains(Vector theVars, Substitution s) {
    return false;
  }

  /**
  ** Like <tt>contains(Vector, Substitution)</tt>, this function tests whether 
  ** one of the variables in the first given Vector occurs in this Term 
  ** taking the given substitution into account. Normally, the public version 
  ** of <tt>contains</tt> (above) should be used. For ConstTerms the effect
  ** is identical though, i.e. there is no effect.
  ** @param theVars the Variables to be tested whether they occur in this Term 
  ** (will be ignored)
  ** @param s the Substitution under which the test takes place (will be 
  ** ignored)
  ** @param okVars some Variables in this Term that have already been tested
  ** (will be ignored)
  ** @return <tt>false</tt> 
  */
  protected boolean contains(Vector theVars, Substitution s, Vector okVars) {
    return false;
  }

  /**
  ** A ConstTerm is printed as the Symbol it holds.
  ** @return the String for the contained Symbol
  */
  public String toString() {
    return theSy.toString();
  }

  /** 
  ** A ConstTerm is equal to any other ConstTerm that holds
  ** the same Symbol. It never equals a VarTerm or any other kind 
  ** of Term.
  ** @param otherTerm the Object this Term is compared to
  ** @return whether the given Object equals this ConstTerm
  */
  public boolean equals(Object otherTerm) {
    if (otherTerm == null)
      return false;
    return (otherTerm instanceof ConstTerm) && 
        (theSy == ((ConstTerm)otherTerm).theSy);
  }

  /**
  ** This function can be used to extract the Symbol contained in this 
  ** ConstTerm.
  ** @return the Symbol contained in this ConstTerm
  */
  public Symbol getSymbol() {
    return theSy;
  }

  /**
  ** the Symbol contained in this ConstTerm
  */
  private Symbol theSy;
}
