package JavaAgent.resource.fopl;


import java.util.*;

/**
** This kind of Term represents a symbolic Variable (as opposed to a Java 
** variable). Variables again can be mapped to other Terms by a Substitution.
** Note that several differnent VarTerms can share a Variable.
** @see Substitution
** @see Variable
*/

public class VarTerm extends Term {

  /**
  ** This constructor just takes a Variable that is this Term. Note that 
  ** several VarTerms may share a Variable, but other VarTerms
  ** might contain a different Variable with the same name.
  ** @param aVar the Variable that is this Term
  ** @exception IllegalArgumentException An exception will occur if the 
  ** given Variable is null.
  */
  public VarTerm(Variable aVar) throws IllegalArgumentException {
    if (aVar == null)
      throw new IllegalArgumentException(
          "Attempt to create VarTerm without Variable.");
    theVar = aVar;
  }

  /** 
  ** This constructor takes a String that is interpreted as the name of a 
  ** Variable. This constructor will not check whether the given name is a 
  ** legal Variable name (e.g. does not contain spaces). It it uses the 
  ** static function <tt>get</tt> of the class Variable to get the Variable 
  ** in this VarTerm.
  ** @param aName the name of the Variable that is this Term
  ** @exception IllegalArgumentException An exception will occur if the 
  ** supplied String is empty or null.
  */
  public VarTerm(String aName) throws IllegalArgumentException {
    theVar = Variable.get(aName);
  }

  /**
  ** Cloning a VarTerm returns a new VarTerm with the same Variable. Use
  ** <tt>clone(Substitution)</tt> with an appropriate Substitution to 
  ** to get a copy with VarTerms replaced by other Terms.
  ** @return a VarTerm containing the same Variable as this one
  */
  public Object clone() {
    try {
      return new VarTerm(theVar);
    }
    catch (IllegalArgumentException iae) {
      throw new UnknownError("Attempt to clone VarTerm without Variable.");
    }
  }

  /**
  ** Cloning a VarTerm with a given Substitution returns a new Term which
  ** is determined by the given Substitution. Thus, the returned Term is 
  ** not necessarily a VarTerm. The function <tt>getValue(Variable)</tt> of
  ** the Substitution class is used to generate the returned Term. A 
  ** Variable not occurring in the Substitution will be replaced by a new 
  ** (different) Variable with the same name. The given Susbtitution will 
  ** be extended to include the mappings of old Variables to new ones.
  ** <p> To generate a new VarTerm with a new Variable with the same name 
  ** as this one (unlike <tt>clone()</tt>) this function can be called with 
  ** an empty Substitution.
  ** @param s the Substitution that tells us how to replace Variables
  ** @return a new Term that is 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. In this case <tt>clone()</tt> (above) should be
  ** used.
  */
  public Term clone(Substitution s) throws IllegalArgumentException {
    if (s == null)
      throw new IllegalArgumentException(
          "Attempt to instantiate " + theVar + " under null Substitution.");
    return s.getValue(theVar);
  }

  /**
  ** Cloning a VarTerm with a given Substitution and Term replacements 
  ** returns a new Term which is either an instantiation of the Variable 
  ** under the given Substitution or an instance of the replacement Term. 
  ** If this Term is the first given Term the result will be an instance of 
  ** the second given Term. Otherwise the function 
  ** <tt>getValue(Variable)</tt> of the Substitution class is used to 
  ** generate the returned Term. A Variable not occurring in the Substitution 
  ** will be replaced by a new (different) Variable with the same name. The 
  ** given Susbtitution will be extended to include the mappings of old 
  ** Variables to new ones.
  ** @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);
    return s.getValue(theVar);
  }

  /**
  ** This function adds the Variable in this VarTerm to the given Vector. If 
  ** the Variable in this VarTerm is already in the Vector nothing is added.
  ** @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 {
    if (vars == null)
      throw new IllegalArgumentException(
          "Attempt to add Variable to null Vector.");
    if (! vars.contains(theVar))
      vars.addElement(theVar);
  }

  /**
  ** 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. A VarTerm can in principle be unified with 
  ** any other kind of Term. Whether this succeeds depends entirely on 
  ** whether the given Substitution can be extended accordingly.
  ** @param other the other Term this VarTerm 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 " + theVar + " with null.");
    if (other instanceof VarTerm)
      return s.unify(theVar, ((VarTerm)other).theVar);
    return s.unify(theVar, other);
  }

  /**
  ** Like <tt>contains(Vector, Substitution)</tt>, this function tests whether 
  ** one of the variables in the first given Vector occurs in this VarTerm 
  ** taking the given Substitution into account. Normally, the public version 
  ** of <tt>contains</tt> (in class Term) should be used. The difference is 
  ** the third argument which must be a Vector of Variables that have
  ** already been tested for occurance, i.e. if the Variable in this VarTerm
  ** is in the latter Vector it has been tested before. 
  ** @param theVars the Variables to be tested whether they occur in this Term
  ** @param s the Substitution under which the test takes place
  ** @param okVars some Variables in this Term that have already been tested
  ** @return <tt>true</tt> if and only if a Variable in the given Vector is
  ** contained in this Term under the given Substitution
  */
  protected boolean contains(Vector theVars, Substitution s, Vector okVars) {
    if ((theVars == null) || (s == null) || (okVars == null))
      throw new UnknownError("Unexpected error in occurs check!");
    if (okVars.contains(theVar))
      return false;
    if (theVars.contains(theVar))
      return true;
    okVars.addElement(theVar);
    Term bTerm = s.getTerm(theVar);
    if (bTerm == null)
      return false;
    return bTerm.contains(theVars, s, okVars);
  }

  /**
  ** A VarTerm is printed as the Variable it holds. Note that this can be 
  ** changed in the class Variable.
  ** @return the String that represents the contained Variable
  */
  public String toString() {
    return theVar.toString();
  }

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

  /**
  ** This function can be used to extract the Variable contained in this 
  ** VarTerm.
  ** @return the Variable contained in this VarTerm
  */
  public Variable getVar() {
    return theVar;
  }

  /**
  ** the Variable contained in this VarTerm
  */
  private Variable theVar;
}
