package JavaAgent.resource.fopl;


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

import JavaAgent.resource.cdl.KRSentence;

/**
** A FOPLFormula is a rather ugly side effect necessary to allow the
** inheritance from the JAT Language class. Formula cannot directly inherit 
** from the Language class because Formula is an abstract class. Hence,
** this class, FOPLFormula, inherits from Language and contains only 
** exactly one object, a Formula.
** @see JavaAgent.resource.Language
** @see Formula
*/

public class FOPLFormula extends JavaAgent.resource.Language 
    implements JavaAgent.resource.cdl.Parsable, KRSentence {

  /**
  ** This constructor creates an empty instance of a FOPLFormula.
  */
  public FOPLFormula() {
    theForm = null;
  }
    
  /**
  ** This constructor for a FOPLFormula parses the given String and
  ** creates the according Formula.
  ** @param input The string to be parsed.
  ** @exception ParseException An Exception can occur if parsing fails.
  */
  public FOPLFormula(String input) throws java.text.ParseException {
    theForm = Formula.parse(input);
  }

  /** 
  ** This function generates a copy of this FOPLFormula. The copy will contain
  ** a clone of the Formula contained in this one.
  ** @return an equal copy of this FOPLFormula
  */
  public Object clone() {
    FOPLFormula res = new FOPLFormula();
    res.theForm = (Formula)theForm.clone();
    return res;
  }

  /** 
  ** Returns a copy of this Formula 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 
  ** Formula 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 Formula.
  ** @param s the Substitution that tells us how to replace Variables
  ** @return a new FOPLFormula that is an instance of this FOPLFormula; 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.
  */
  public FOPLFormula clone(Substitution s) 
      throws IllegalArgumentException {
    FOPLFormula res = new FOPLFormula();
    res.theForm = theForm.clone(s);
    return res;
  }

  /**
  ** This function returns the Formula embedded in this FOPLFormula.
  ** @return the Formula embedded in this FOPLFormula
  */
  protected Formula getFormula() {
    return theForm;
  }

  /**
  ** This function tests whether this and the given Object are equal. In
  ** general, two FOPLFormulae are equal if they contain equal Formulae.
  ** @param otherForm the FOPLFormula 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 Formula)
      return theForm.equals(otherForm);
    if (! (otherForm instanceof FOPLFormula))
      return false;
    return theForm.equals(((FOPLFormula)otherForm).theForm);
  }

  /**
  ** This function returns the String that represents this FOPLFormula.
  */
  public String toString() {
    return theForm.toString();
  }

  /**
  ** This function returns a FOPLFormula that represents a conjunction of
  ** the KRSentences in the given Vector.
  ** @param conjuncts a Vector of FOPLFormulas
  ** @return a FOPLFormula containing the conjunction of the given 
  **   FOPLFormulas
  */
  static public KRSentence getConjunction(Vector conjuncts) {
    if (conjuncts.size() < 2)
      return (KRSentence)conjuncts.firstElement();
    MultiConFormula res = new MultiConFormula(
        YYtokentypes.AND.intValue(), conjuncts.size()+1);
    for (Enumeration fe = conjuncts.elements(); fe.hasMoreElements(); )
      res.addFormula(((FOPLFormula)fe.nextElement()).theForm);
    FOPLFormula result = new FOPLFormula();
    result.theForm = res;
    return result;
  }

  /**
  ** This function returns the Class that implements KnowledgeBase for
  ** this KRSentence Class.
  */
  static public Class getKBClass() {
    try {
      return Class.forName("JavaAgent.resource.fopl.FormulaSet");
    } catch (ClassNotFoundException cnfe) {
      throw new UnknownError("Failed to find class FormulaSet!");
    }
  }

  /**
  ** This function returns the premise of this implication.
  */
  public FOPLFormula getPremise() {
    FOPLFormula res = new FOPLFormula();
    res.theForm = ((BinConFormula)theForm).getPremise();
    return res;
  }

  /**
  ** This function returns the conclusion of this implication.
  */
  public FOPLFormula getConclusion() {
    FOPLFormula res = new FOPLFormula();
    res.theForm = ((BinConFormula)theForm).getConclusion();
    return res;
  }

  /**
  ** This function should only be used on empty instances of a FOPLFormula.
  ** It will parse the given String and create the according Formula to
  ** be kept in this FOPLFormaula.
  ** @param input The string to be parsed.
  */
  public void parseString(String input) {
    try {
      theForm = Formula.parse(input);
    }
    catch (ParseException pe) {
      // Language.parseString does not allow the throwing of exceptions!
    }
  }

  /**
  ** This function can be used to parse a given String that represents a 
  ** FOPLFormula. The syntax is as for a Formula.
  ** @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 FOPLFormula parse(String s) 
      throws IllegalArgumentException, ParseException {
    FOPLFormula res = new FOPLFormula();
    res.theForm = Formula.parse(s);
    return res;
  }

  /**
  ** This function can be used to parse a given InputStream that represents 
  ** a Formula. The syntax is as for a Formula.
  */
  public static FOPLFormula parse(InputStream ist) 
      throws IllegalArgumentException, IOException, ParseException {
    FOPLFormula res = new FOPLFormula();
    res.theForm = Formula.parse(ist);
    return res;
  }

  /**
  ** The Formula contained in this FOPLFormula.
  */
  protected Formula theForm;

}
