package JavaAgent.resource.fopl;


import java.util.*;

/** 
** A Substitution maps a set of Variables to a set of Terms. Each Variable 
** belongs to a set of Variables in the Substitution. Each set of Variables 
** might have a Term associated with it. Substitutions are mainly used for 
** unification of Terms or instantiation of Terms.
** @see Variable
** @see Term
** @see UnificationException
*/

public class Substitution {

  /**
  ** The constructor just initializes the Substituiton as empty. In an empty 
  ** Substitution no Variables are mapped to anything. 
  */
  public Substitution() {
    mappings = new Vector();
    finished = false;
  }

  /**
  ** This function returns a copy of this Substitution that will be identical 
  ** to this Substitution. Hoeever, modification to the new Substitution
  ** will not affect the original.
  */
  public Object clone() {
    Substitution res = new Substitution();
    res.finished = finished;
    for (Enumeration sce=mappings.elements(); sce.hasMoreElements(); )
      res.mappings.addElement(((SubstComp)sce.nextElement()).clone());
    return res;
  }

  /** 
  ** This function attempts to extend this Substitution such that the given 
  ** Variable and the given Term are unified and returns whether this 
  ** succeeded. Basically, this will succeed if: 
  ** <ul>
  ** <li> the Variable was not instantiated before and association with the 
  **   given Term does not introduce a circle into the substitution, or
  ** <li> the variable was instantiated before and old and new term are
  **   unifiable without causing circles.
  ** </ul>
  ** @param aVar the Variable the given Term is to be unified with
  ** @param aTerm the Term the given Variable will be mapped to
  ** @return whether successful extension of this Substitution was possible
  ** @exception IllegalArgumentException An exception will occor if the 
  ** given Variable or Term are null.
  ** @exception UnificationException An exception will occor if this
  ** Substitution has already been finished.
  */
  public boolean unify(Variable aVar, Term aTerm) 
      throws IllegalArgumentException, UnificationException {
    // test for exceptional conditions:
    if (aVar == null)
      throw new IllegalArgumentException(
          "Attempt to unify null Variable with a Term.");
    if (aTerm == null)
      throw new IllegalArgumentException(
          "Attempt to unify a Variable with null Term.");
    if (finished)
      throw new UnificationException(
	  "Attempt to extend Substitution that has been finished!", this);
    
    // if the term is a VarTerm:
    if (aTerm instanceof VarTerm)
      return unify(aVar, ((VarTerm)aTerm).getVar());

    int scIndex = getComp(aVar);
    if (scIndex < 0) {
      mappings.addElement(new SubstComp(aVar));
      scIndex = mappings.size()-1;
    }
    SubstComp sc = (SubstComp)mappings.elementAt(scIndex);
    if (aTerm.contains(sc.uniVars, this))
      return false;
    // the variable was not subtituted before:
    if (sc.theTerm == null) {
      sc.theTerm = aTerm;
      return true;
    }
    // the variable is bound to a term:
    return aTerm.unify(sc.theTerm, this);
  }

  /**
  ** This function attempts to extend this Substitution such that the given 
  ** Variables will be unified and returns <tt>true</tt> if this was 
  ** possible. This will be the case if:
  ** <ul>
  ** <li> both Variables have not been mapped to Terms in this Substitution
  **   previously, or
  ** <li> only one of the two given Variables has been mapped to a Term by 
  **   this Substitution previously and this Term does not contain the other
  **   Variable or any other Variable associated with it, or
  ** <li> both Variables had Terms associated with them and these Terms are
  **   unifyable without causing circles in this Substitution.
  ** </ul>
  ** @param var1 a Variable to be associated with the other given Variable
  ** @param var2 a Variable to be associated with the other given Variable
  ** @return whether successful extension of this Substitution was possible
  ** @exception IllegalArgumentException An exception will occor if either of
  ** the given Variables is null.
  ** @exception UnificationException An exception will occor if this
  ** Substitution has already been finished.
  */
  public boolean unify(Variable var1, Variable var2)
      throws IllegalArgumentException, UnificationException {
    // test for exceptional conditions:
    if ((var1 == null) || (var2 == null))
      throw new IllegalArgumentException(
          "Attempt to unify null Variable with other Variable.");
    if (finished)
      throw new UnificationException(
	  "Attempt to extend Substitution that has been finished!", this);
    
    // get the substitution components:
    int sc1Index = getComp(var1);
    int sc2Index = getComp(var2);

    // if both variables are new:
    if ((sc1Index < 0) && (sc2Index < 0)) {
      mappings.addElement(new SubstComp(var1, var2));
      return true;
    }

    // if only the first substitution component is new:
    if (sc1Index < 0)
      return ((SubstComp)mappings.elementAt(sc2Index)).addVar(var1, this);
      
    // if only the second substitution component is new:
    if (sc2Index < 0)
      return ((SubstComp)mappings.elementAt(sc1Index)).addVar(var2, this);
      
    // neither of the variables is new:
    // test if the variables are already unified:
    if (sc1Index == sc2Index)
      return true;
    // get the actual substitution components:
    SubstComp sc1 = (SubstComp)mappings.elementAt(sc1Index);
    SubstComp sc2 = (SubstComp)mappings.elementAt(sc2Index);

    // if both variables were unsubstituted before:
    if ((sc1.theTerm == null) && (sc2.theTerm == null)) {
      sc1.addVariables(sc2.uniVars);
      mappings.removeElementAt(sc2Index);
      return true;
    }

    // SC1 has an associated term but SC2 has not:
    if (sc2.theTerm == null) {
      if(sc1.theTerm.contains(sc2.uniVars, this))
	return false;
      sc1.addVariables(sc2.uniVars);
      mappings.removeElementAt(sc2Index);
      return true;
    }

    // SC2 has an associated term but SC1 has not:
    if (sc1.theTerm == null) {
      if(sc2.theTerm.contains(sc1.uniVars, this))
	return false;
      sc2.addVariables(sc1.uniVars);
      mappings.removeElementAt(sc1Index);
      return true;
    }

    // both variables have associated terms:
    if ((sc1.theTerm.contains(sc2.uniVars, this)) ||
        (sc2.theTerm.contains(sc1.uniVars, this)))
      return false;
    sc2.addVariables(sc1.uniVars);
    mappings.removeElementAt(sc1Index);
    return sc1.theTerm.unify(sc2.theTerm, this);
  }

  /**
  ** This function returns the Term the given Variable is mapped to. More 
  ** specifically, it returns:
  ** <ul>
  ** <li> a new VarTerm with a new Variable iff the Variable is not part 
  **   of the Substitution or has no Term associated with it; the new 
  **   VarTerm will be retained for future consistency;
  ** <li> a Term that is the instantiation of the associated Term under
  **   this Substitution iff there is an associated term;
  ** </ul>
  ** <p> Once this function has been called this Substitution can no
  ** longer be modified with calls to <tt>unify(...)</tt> above.
  ** @param aVar the Variable the Term is being seeked for
  ** @return the instantiated Term the given Variable is mapped to
  ** @exception IllegalArgumentException An exception will occor if
  ** the given Variable is null.
  */
  public Term getValue(Variable aVar) throws IllegalArgumentException {
    if (aVar == null)
      throw new IllegalArgumentException(
          "Attempt to get value of null Variable in Substitution.");
    finished = true;
    int scIndex = getComp(aVar);
    if (scIndex < 0) {
      VarTerm newVT = new VarTerm((Variable)aVar.clone());
      mappings.addElement(new SubstComp(aVar, newVT));
      return (VarTerm)newVT.clone();
    }
    SubstComp sc = (SubstComp)mappings.elementAt(scIndex);
    if (sc.theTerm == null)
      sc.theTerm = new VarTerm((Variable)aVar.clone());
    if (sc.theTerm instanceof VarTerm)
      return (VarTerm)sc.theTerm.clone();
    return (Term)sc.theTerm.clone(this);
  }

  /**
  ** This function can be used to make sure that a Variable that is not
  ** already mapped to a Term by this Substitution will not be touched.
  ** @param aVar the Variable to be locked
  ** @exception UnificationException An exception will occur if the given 
  **   Variable is already part of this Substitution.
  */
  public void lockVariable(Variable aVar) throws UnificationException {
    finished = true;
    int scIndex = getComp(aVar);
    if (scIndex >= 0)
      throw new UnificationException(
          "Cannot lock Variable " + aVar + "!", this);
    mappings.addElement(new SubstComp(aVar, new VarTerm(aVar)));
  }

  /**
  ** This function returns the Term associated with this Variable in this 
  ** Substitution or null if there is no such Term. The returned Term will
  ** be instantiated under this Substitution. Variables in the returned Term 
  ** are <b>not</b> replaced by other Terms in the Substitution. Use 
  ** <tt>getValue(Variable)</tt> (above) to get an instantiatied version
  ** of the Term associated with the given Variable.
  ** @param v the Variable the Term is being seeked for
  ** @return the <b>un</b>instantiated Term the given Variable is mapped to
  ** @exception IllegalArgumentException An exception will occor if
  ** the given Variable is null.
  */
  protected Term getTerm(Variable v) throws IllegalArgumentException {
    if (v == null)
      throw new IllegalArgumentException(
          "Attempt to get Term for null Variable in Substitution.");
    int scIndex = getComp(v);
    if (scIndex < 0)
      return null;
    return ((SubstComp)mappings.elementAt(scIndex)).theTerm;
  }

  /** 
  ** This function returns a Vector of all the Variables that are unified in
  ** this Substitution. It will not include new Variables old ones are being 
  ** mapped to.
  ** @return a Vector of all the Variables that are unified in
  ** this Substitution
  */
  public Vector getVars() {
    Vector res = new Vector();
    for (Enumeration e1=mappings.elements(); e1.hasMoreElements(); )
      for (Enumeration e2=((SubstComp)e1.nextElement()).uniVars.elements(); 
	   e2.hasMoreElements(); )
	res.addElement(e2.nextElement());
    return res;
  }

  /**
  ** This function renders this Substitution printable.
  ** @return the String representing this Substitution
  */
  public String toString() {
    String res = "[";
    Enumeration e=mappings.elements();
    if (e.hasMoreElements())
      res += ((SubstComp)e.nextElement()).toString();
    while (e.hasMoreElements())
      res += ", " + ((SubstComp)e.nextElement()).toString();
    return res + ']';
  }

  /** 
  ** returns the index of the substitution component of this substitution 
  ** that contains the given variable, returns -1 iff the variable does not 
  ** exist in this substitution 
  */
  private int getComp(Variable aVar) {
    for (int i=0; i<mappings.size(); i++)
      if (((SubstComp)mappings.elementAt(i)).uniVars.contains(aVar))
	return i;
    return -1;
  }

  /**
  **  a vector of SubstComps: 
  */
  private Vector mappings;
  /**
  ** whether the substitution has been finshed
  */
  private boolean finished;
}


class SubstComp {

  SubstComp(Variable aVar) {
    uniVars = new Vector();
    uniVars.addElement(aVar);
    theTerm = null;
  }

  SubstComp(Variable aVar, Term aTerm) {
    uniVars = new Vector();
    uniVars.addElement(aVar);
    theTerm = aTerm;
  }

  SubstComp(Variable var1, Variable var2) {
    uniVars = new Vector();
    uniVars.addElement(var1);
    if (var1 != var2)
      uniVars.addElement(var2);
    theTerm = null;
  }

  private SubstComp() {
  }

  public Object clone() {
    SubstComp res = new SubstComp();
    res.uniVars = (Vector)uniVars.clone();
    res.theTerm = theTerm;
    return res;
  }

  boolean addVar(Variable aVar, Substitution s) {
    uniVars.addElement(aVar);
    if (theTerm == null)
      return true;
    return (! (theTerm.contains(uniVars, s)));
  }

  void addVariables(Vector vars) {
    for (Enumeration e=vars.elements(); e.hasMoreElements(); )
      uniVars.addElement(e.nextElement());
  }

  public String toString() {
    if (theTerm == null)
      return uniVars.toString();
    return theTerm.toString() + "->" + uniVars.toString();
  }

  Vector uniVars;
  Term theTerm;
}
