package G4ip;

import java.util.Vector;
import G4ip.Form.*;

/** Context acts as a multiset.<p>
  * Typical contexts in logical rules are Gamma, Delta, etc.
  * @author      Christian Urban
  */
public class Context extends Vector {
  
  public Context() { super(); }

  public Context(Context init_context) {
    super();
    for (int i=0;i<init_context.size();i++) {
      addElement(init_context.elementAt(i));
    }
  }

  /** should be toString, but this is a "final" method in Vector 
    */
  public String makeString() {
    String s = new String();
    int i;                      // size()-1 because the last formula
    for (i=0;i<size()-1;i++) {  // should be printed without a comma
      s=s.concat(elementAt(i).toString());
      s=s.concat(", ");
    }
    if (size() > 0) {           // add last formula 
      s=s.concat(elementAt(i).toString()); 
    }
    return s;
  }

  /** returns a context with one additional formula at the beginning 
    * @param   new_formula    a formula
    */
  public Context add(Form new_formula) {
    Context new_c = new Context(this);
    new_c.insertElementAt(new_formula,0);
    return new_c;
  }

  /** returns a context with two additional formulae at the beginning 
    * @param new_formula1,new_formula2    two formulae
    */
  public Context add(Form new_formula1, Form new_formula2) {
    Context new_c = new Context(this);
    new_c.insertElementAt(new_formula1,0);
    new_c.insertElementAt(new_formula2,0);
    return new_c;
  }

  /** tests whether a context contains a specific atom 
    * @param a a formula
    */
  public boolean includes(Form a) {
    if (a instanceof Atm) {
      for (int i=0;i<size();i++) {
        switch((Form)elementAt(i)) {
        case Atm(String c):
          if (c.compareTo(((Atm)a).c) == 0) return true; break;
        }
      }
    }
    return false;
  }

}