package JavaAgent.resource.fopl;


import java.util.*;
import java.text.ParseException;

/**
** A Term represents an object in a conceptualization of some domain. Terms 
** are mostly used in logical expressions. Currently, there are several 
** kinds of Terms implemented.
** @see ConstTerm
** @see VarTerm
** @see FunctTerm
** @see Substitution
*/

public abstract class Term implements JavaAgent.resource.cdl.Parsable {

  /**
  ** Returns a copy of this Term. Variables and Symbols in the
  ** copy will be the same as the original ones.
  ** @return an equal copy of this Term
  */
  abstract public Object clone();

  /**
  ** Returns a copy of this Term 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 
  ** Term 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 the Term.
  ** @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 be 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.
  */
  abstract public Term clone(Substitution s) throws IllegalArgumentException;

  /**
  ** Returns a copy of this Term with Variables replaced according to the 
  ** given Substitution and the first given Term replaced by the second.
  ** This function works just like <tt>clone(Substitution)</tt> except that
  ** it also replaces a Term. Notice that the replacement Term will be an
  ** instance of the second Term under the given Substitution.
  ** @param s the Substitution that tells us how to replace Variables
  ** @param t the Term to be replaced
  ** @param rTerm the replacement Term
  ** @return a new Term that is an instance of this Term with the replaced 
  ** sub-Term; the Substitution <tt>s</tt> will be extended with any new 
  ** Variable replacements introduced
  ** @exception IllegalArgumentException An exception can occur if the given
  ** Substitution or one of the given Terms is null.
  */
  abstract protected Term clone(Substitution s, Term t, Term rTerm) 
      throws IllegalArgumentException;

  /**
  ** This function adds the Variables in this Term 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.
  */
  abstract public void getVars(Vector vars) throws IllegalArgumentException;

  /**
  ** 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. For example, if <tt>t1</tt> and <tt>t2</tt> 
  ** are Terms then:
  ** <p> <tt>Substitution subst = new Substitution();</tt>
  ** <br> <tt>boolean unif = t1.unify(t2, subst);</tt>
  ** <br> <tt>Term uniTerm = t1.clone(subst);</tt>
  ** <p> will firstly create a new, empty Substitution <tt>subst</tt>. This 
  ** will be modified in the call to <tt>unify</tt>. If unification was 
  ** possible <tt>unif</tt> will contain the value <tt>true</tt> and 
  ** <tt>subst</tt> will be the unifying Substitution. Otherwise it will have
  ** an undefined value. In the latter case the last line should not be 
  ** executed. If unification was successful though it is save and will set
  ** <tt>uniTerm</tt> to the expected value.
  ** @param other the other Term this one 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 can occur if the given
  ** Substitution was already finshed.
  */
  abstract public boolean unify(Term other, Substitution s) 
      throws IllegalArgumentException, UnificationException;

  /**
  ** This function tests whether one of the Variables in the given set of 
  ** Variables occurs in this Term taking the given Substitution into account.
  ** @param theVars the Variables to be tested whether they occur in this Term
  ** @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 Term under the given Substitution
  ** @exception IllegalArgumentException An exception can occur if the given
  ** Vector or the given Substitution are null.
  */
  public boolean contains(Vector theVars, Substitution s) 
      throws IllegalArgumentException {
    return contains(theVars, s, new Vector());
  }

  /**
  ** 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. The difference is the third 
  ** argument which must be a Vector of Variables in this Term that have
  ** already been tested for occurance. Variables in this Term that do not
  ** contain any Variable from the first set are added to the latter set.
  ** @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
  */
  abstract protected boolean contains(
      Vector theVars, Substitution s, Vector okVars);

  /**
  ** Tests whether this Term is equal to the given Object. This is only true
  ** if the structure as well as all of the components of this Term are equal
  ** to the given Term.
  ** @param otherTerm the Object this Term is compared to
  ** @return whether the given Object equals this Term
  */
  abstract public boolean equals(Object otherTerm);

  /**
  ** This function can be used to parse a given String that represents a 
  ** Term. The syntax in BNF is as follows:
  ** <pre>
  ** &lt;term&gt;       ::= &lt;constant&gt; | &lt;variable&gt; | 
  **                  ( &lt;constant&gt; &lt;term&gt;+ ) |
  ** &lt;variable&gt;   ::= ?&lt;name&gt;
  ** &lt;constant&gt;   ::= &lt;name&gt;
  ** </pre>
  ** @exception IllegalArgumentException An exception will occur if the 
  ** supplied String is empty or null.
  ** @exception ParseException An exception can occur if parsing failed.
  ** Potential reasons include a syntax error or an I/O problem.
  */
  public static Term parse(String s) 
      throws IllegalArgumentException, ParseException {
    if ((s == null) || s.equals(""))
      throw new IllegalArgumentException("Attempt to parse empty String!");
    try {
      YYparse parser = new YYparse("term " + s);
      return (Term)parser.parseResult;
    } catch (java.io.IOException ioe) {
      throw new ParseException("I/O problem while parsing (" + 
          ioe.getMessage() + ')', 0);
    } catch (Exception e) {
      throw new ParseException("Parse error in Term " + s + 
          " (" + e.getMessage() + ')', 0);
    }
  }
}
