package JavaAgent.resource.fopl;


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

/** 
** A Literal is one of the most basic building blocks for a Formula.
** It consists of a predicate symbol followed by one or more arguments
** which must be Terms. The predicate represents a relation between the 
** arguments. A Literal may also have a sign which indicates whether it is 
** negated or not.
** @see Proposition
** @see Term
*/

public class Literal extends Formula
    implements JavaAgent.resource.cdl.Parsable {

  /**
  ** This constructor for a Literal takes a Symbol and a list of 
  ** arguments. All elements of the given Vector must be Terms!
  ** @param aSy the predicate 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 Literal(Symbol aSy, Vector someTerms) 
      throws IllegalArgumentException {
    negated = false;
    if (aSy == null)
      throw new IllegalArgumentException(
          "Attempt to create Literal without predicate symbol.");
    theTerms = new Vector(someTerms.size()+2);
    theTerms.addElement(new ConstTerm(aSy));
    if ((someTerms == null) || someTerms.isEmpty())
      throw new IllegalArgumentException(
          "Attempt to create Literal 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(
            "Literal argument " + ne + " is not a Term as expected.");
    }
  }

  /**
  ** This protected constructor for a Literal takes a boolean indecating 
  ** whether the Literal is negated, a Symbol (the predicate) and two Terms 
  ** which are the two arguments.
  ** @param neg the sign of this Literal
  ** @param aSy the predicate Symbol
  ** @param t1 the first argument Term
  ** @param t2 the second argument Term
  ** @exception IllegalArgumentException An exception will occur if the 
  ** given Symbol or one of the given Terms is null.
  */
  public Literal(boolean neg, Symbol aSy, Term t1, Term t2) 
      throws IllegalArgumentException {
    negated = neg;
    if ((t1 == null) || (t2 == null))
      throw new IllegalArgumentException(
          "Attempt to create Literal with null argument.");
    theTerms = new Vector(4);
    theTerms.addElement(new ConstTerm(aSy));
    theTerms.addElement(t1);
    theTerms.addElement(t2);
  }

  /**
  ** This protected constructor creates an empty Literal. The Vector must 
  ** be filled before anything else should be done with the Literal.
  */
  protected Literal() {
    negated = false;
    theTerms = null;
  }

  /** 
  ** Cloning a Literal returns a new Literal consisting of the same 
  ** predicate symbol and a clone of each argument. Symbols and Variables
  ** in the copy will be the same as in the original.
  ** @return an equal copy of this Literal
  */
  public Object clone() {
    Literal newLit = new Literal();
    newLit.negated = negated;
    newLit.theTerms = new Vector(theTerms.size()+1);
    for (Enumeration e=theTerms.elements(); e.hasMoreElements(); )
      newLit.theTerms.addElement(((Term)e.nextElement()).clone());
    return newLit;
  }

  /** 
  ** Cloning a Literal returns a new Literal consisting of the same 
  ** predicate symbol and a clone of each argument with the given 
  ** Substitution. That is, Variables occuring in the argument Terms will
  ** be replaced by Terms they are mapped to in the 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.
  ** @param s the Substitution that tells us how to replace Variables
  ** @return a new Literal that is an instance of this Literal; 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 Formula clone(Substitution s) {
    if (s == null)
      throw new IllegalArgumentException(
          "Attempt to clone Literal with null Substitution.");
    Literal newLit = new Literal();
    newLit.negated = negated;
    newLit.theTerms = new Vector(theTerms.size()+1);
    for (Enumeration e=theTerms.elements(); e.hasMoreElements(); )
      newLit.theTerms.addElement(((Term)e.nextElement()).clone(s));
    return newLit;
  }

  /** 
  ** Cloning a Literal returns a new Literal consisting of the same 
  ** predicate symbol and a clone of each argument with the given 
  ** Substitution but with the first given sub-Term replaced by the second 
  ** given Term. Apart from the Term replacement this function is just like
  ** <tt>clone(Substitution)</tt> above.
  ** @param s the Substitution that tells us how to replace Variables
  ** @param t the sub-Term in this Literal to be replaced
  ** @param rTerm the (uninstantiated) replacement Term
  ** @return a new Literal that is, apart from the replaced Term, an instance 
  ** of this Literal; the Substitution <tt>s</tt> will extended with any new 
  ** Variable replacements introduced
  ** @exception IllegalArgumentException An exception can occur if the given
  ** Substitution or either of the given Terms is null.
  */
  protected Literal clone(Substitution s, Term t, Term rTerm) {
    if ((s == null) || (t == null) || (rTerm == null))
      throw new IllegalArgumentException(
          "Attempt to clone Literal with null argument.");
    Literal newLit = new Literal();
    newLit.negated = negated;
    newLit.theTerms = new Vector(theTerms.size()+1);
    for (Enumeration e=theTerms.elements(); e.hasMoreElements(); )
      newLit.theTerms.addElement(((Term)e.nextElement()).clone(s, t, rTerm));
    return newLit;
  }

  /**
  ** This function adds the Variables in this Literal 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 returns a new Literal which is a copy of this Literal. 
  ** The given Substitution and the given Vector of Variables will 
  ** be ignored here. Finally, the given boolean indicates whether the 
  ** Literal is to be negated, i.e. its sign to be reversed.
  ** @param s a Substitution (will be ignored)
  ** @param allQuantVars the Vector of universally quantified Variables 
  ** (will be ignored)
  ** @param isNegated whether the Literal has to be negated
  ** @return a new Literal with the given boolean worked into the sign
  */
  protected Formula toSkolemizedAndOrForm(
      Substitution s, Vector allQuantVars, boolean isNegated) {
    Literal newLit = (Literal)clone();
    newLit.negated = (negated && !isNegated) || (!negated && isNegated);
    return newLit;
  }

  /**
  ** This function tests whether this is a positive Literal.
  ** @return whether this Literal is positive, i.e. not negated
  */
  public boolean isPositive() {
    return (! negated);
  }

  /**
  ** This function tests whether this Literal represents an equality or
  ** inequality. Use <tt>isPositive()</tt> above to find out which one 
  ** it is.
  ** @return whether the predicate in this Literal is "="
  */
  public boolean isEquality() {
    try {
      return eqTerm.equals((Term)theTerms.firstElement());
    } catch (NoSuchElementException nsee) {
      throw new UnknownError("No predicate found in Literal!");
    }
  }

  /**
  ** This function returns the n-th argument to this Literal. The first 
  ** argument has the index 1.
  ** @param n the index of the argument Term to be retrieved
  ** @return the n-th argument
  ** @exception ArrayIndexOutOfBoundsException An exception will occur if 
  ** the given index specifies a not existing argument.
  */
  public Term nthArgument(int n) throws ArrayIndexOutOfBoundsException {
    return (Term)theTerms.elementAt(n);
  }

  /**
  ** This function can be used to change the sign of this Literal.
  */
  public void negate() {
    negated = (! negated);
  }

  /**
  ** This function attempts to extend the given Substitution so that this 
  ** Literal and the given Literal are unified. It returns <tt>true</tt> if 
  ** and only if this is possible. The sign of the two Literals is ignored
  ** for this purpose.
  ** @param other the other Literal this Literal 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
  ** Literal or the given Substitution are null.
  ** @exception UnificationException An exception can occur if the given
  ** Substitution was already finshed.
  */
  public boolean unify(Literal 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 (theTerms.size() != other.theTerms.size())
      return false;
    Enumeration e1=theTerms.elements();
    for (Enumeration e2=other.theTerms.elements(); e2.hasMoreElements(); )
      if (!((Term)e1.nextElement()).unify((Term)e2.nextElement(), s))
	return false;
    return true;
  }

  /**
  ** This function attempts to extend the given Substitution so that this 
  ** Literal and the given Literal are unified. It returns <tt>true</tt> if 
  ** and only if this is possible. The sign of the two Literals must be 
  ** identical for this purpose.
  ** @param other the other Literal this Literal 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
  ** Literal or the given Substitution are null.
  ** @exception UnificationException An exception can occur if the given
  ** Substitution was already finshed.
  */
  public boolean signedUnify(Literal other, Substitution s)
      throws IllegalArgumentException, UnificationException {
    return ((negated == other.negated) && unify(other, s));
  }

  /** 
  ** This function tests whether this and the given Literal completmentary. 
  ** This will be the case if they have the same predicte and all the 
  ** argument Terms are equal, but the signs are different.
  ** @param otherLit the Literal this one is to be compared to
  ** @return whether the given Literal is complemetary to this one
  */
  public boolean complements(Literal otherLit) {
    if ((otherLit == null) || (negated == otherLit.negated) ||
	(theTerms.size() != otherLit.theTerms.size()))
      return false;
    Enumeration e1=theTerms.elements();
    for (Enumeration e2=otherLit.theTerms.elements(); e2.hasMoreElements(); )
      if (! e1.nextElement().equals(e2.nextElement()))
	return false;
    return true;
  }

  /** 
  ** This function attempts to extend the given Substitution so that this 
  ** Literal and the given Literal are complementary. It returns 
  ** <tt>true</tt> if and only if this is possible. The sign of the two 
  ** Literals must be different for this purpose.
  ** @param other the other Literal this Literal 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 and the two signs are complementary
  ** @exception IllegalArgumentException An exception will occur if the given
  ** Literal or the given Substitution are null.
  ** @exception UnificationException An exception can occur if the given
  ** Substitution was already finshed.
  */
  public boolean complements(Literal other, Substitution s) 
      throws IllegalArgumentException, UnificationException {
    return ((negated != other.negated) && unify(other, s));
  }

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

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

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

  /** 
  ** This function tests whether this and the given Object are equal. In
  ** general, two Literals are equal if they have the same sign, predicte,
  ** and all the argument Terms are equal.
  ** @param otherForm the Formula this one is to be compared to
  ** @return whether the given Object is equal to this one
  */
  public boolean equals(Object otherForm) {
    if (otherForm == null)
      return false;
    if (! (otherForm instanceof Literal))
      return false;
    Literal lit = (Literal)otherForm;
    if ((negated != lit.negated) || (lit.theTerms.size() != theTerms.size()))
      return false;
    Enumeration e1=theTerms.elements();
    for (Enumeration e2=lit.theTerms.elements(); e2.hasMoreElements(); )
      if (! e1.nextElement().equals(e2.nextElement()))
	return false;
    return true;
  }

  /**
  ** This function can be used to parse a given String that represents a 
  ** Literal. The syntax in BNF is as follows:
  ** <pre>
  ** &lt;signedlit&gt; ::= &lt;literal&gt; | ( not &lt;literal&gt; )
  ** &lt;literal&gt;    ::= &lt;constant&gt; | 
  **                  ( = &lt;term&gt; &lt;term&gt; )
  **                  ( &lt;constant&gt; &lt;term&gt;+ )
  **
  ** &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 Literal parseLit(String s) 
      throws IllegalArgumentException, ParseException {
    if ((s == null) || s.equals(""))
      throw new IllegalArgumentException("Attempt to parse empty String!");
    try {
      YYparse parser = new YYparse("literal " + s);
      return (Literal)parser.parseResult;
    } catch (IOException ioe) {
      throw new ParseException("I/O problem while parsing (" + 
          ioe.getMessage() + ')', 0);
    } catch (Exception e) {
      throw new ParseException("Parse error in Literal " + s + 
          " (" + e.getMessage() + ')', 0);
    }
  }

  /**
  ** This function can be used to parse a given InputStream that represents
  ** a Literal. The syntax in BNF is as above except that the first token
  ** should be the word <tt>LITERAL</tt> so that the generic parser knows what
  ** it has to expect. This is added automatically when parsing a String.
  ** @exception IllegalArgumentException An exception will occur if the 
  ** supplied InputStream is null.
  ** @exception IOException An exception can occur if there are problems 
  ** reading from the given InputStream.
  ** @exception ParseException An exception can occur if parsing failed.
  ** Potential reasons include a syntax error.
  */
  public static Literal parseLit(InputStream ist) 
      throws IllegalArgumentException, IOException, ParseException {
    if (ist == null)
      throw new IllegalArgumentException("Attempt to parse null Stream!");
    try {
      YYparse parser = new YYparse(ist);
      return (Literal)parser.parseResult;
    } catch (IOException ioe) {
      throw ioe;
    } catch (Exception e) {
      throw new ParseException("Parse error in Literal: (" + 
          e.getMessage() + ')', 0);
    }
  }

  /**
  ** This variable indicates whether this Literal is negated.
  */
  protected boolean negated;

  /**
  ** This Vector of Terms contains the predicate and the agument Terms in this
  ** Literal. The first Term should be a ConstTerm containing the Symbol that
  ** represents the predicate.
  */
  protected Vector theTerms;

  /**
  ** for quick acces and to avoid the need to construct it all the time
  */
  private ConstTerm eqTerm = new ConstTerm(Symbol.get("="));
}
