package JavaAgent.resource.fopl;


import java.util.*;


/** 
 ** This class implements symbolic variables in Java. Like Symbols, Variables
 ** are memory-unique objects, i.e. they are equal if and only if the handles
 ** are the same. This allows the creation of multiple variables with the 
 ** same name that are not equal. It also allows for efficient equality 
 ** testing. The unique index could also be used to compare variables.
 ** <p> The class also maintains some aids that should facilitate parsing.
 ** A set of global and a set of local Variables are used by the function 
 ** <tt>get()</tt>. The variable <tt>newLocal</tt> determines what
 ** <tt>get()</tt> will return. The function <tt>newVars()</tt> dismisses all
 ** local and global variables, i.e. future calls to <tt>get()</tt> cannot
 ** return them.
 */

public class Variable {

  /** 
  ** This Java variable determines how <tt>get()</tt> looks for the symbolic
  ** Variable to be returned. If <tt>false</tt> (the default), an existing
  ** Variable is searched for. If set to <tt>true</tt>, the Variable will 
  ** always be created as a new local Variable.
  */
  public static boolean newLocal = false;

  /** 
  ** This Java variable indicates how symbolic Variables are to be
  ** printed. If <tt>true</tt>, the default, symbolic Variables are printed 
  ** with their index. Printing Variables without index is useful when the
  ** expression they occur in is to be parsed again. This will avoid 
  ** multiple indices but may lead to ambiguities.
  */ 
  public static boolean printWithIndex = true;

  /** 
  ** This function must be used to get hold of Variables with the given 
  ** name. It effectively replaces a public constructor. For example,
  ** <p> <tt>Variable myVar = Variable.get("?x");</tt>
  ** <p> will return a Variable with the given name. The '?' in the variable 
  ** name is not necessary. If the Variable has been defined previously 
  ** the same Variable will be returned (unless <tt>newVars()</tt> has been 
  ** called). The function first searches the
  ** variable stack (local variables) and then the global variables. If
  ** the given name isn't found in either, the Variable is created as 
  ** a new global. This behaviour can be changed by setting the static
  ** varibale <tt>newLocal</tt> to true. In this case a new local Variable 
  ** will be created no matter whether one with this name existed. 
  ** @param aName the name of the Variable
  ** @return a Variable with the given name (see above)
  ** @exception IllegalArgumentException An exception will occur if the 
  ** supplied String is empty or null.
  ** @exception OutOfMemoryError An error can occur if the unique indices for 
  ** Variables have run out.
  */
  public static Variable get(String aName) throws IllegalArgumentException {
    if ((aName == null) || aName.equals(""))
      throw new IllegalArgumentException(
          "Attempt to get Variable without name!");

    if (newLocal) {
      // create a new local Variable on the stack:
      Variable newVar = new Variable(aName);
      localVars.addElement(newVar);
      return newVar;
    }

    // search from top of stack downwards:
    for (int i=localVars.size()-1; i>=0; i--)
      if (aName.equals(((Variable)localVars.elementAt(i)).theName))
	return (Variable)localVars.elementAt(i);

    // search the global variables:
    for (Enumeration e=globalVars.elements(); e.hasMoreElements(); ) {
      Variable thisVar = (Variable)e.nextElement();
      if (aName.equals(thisVar.theName))
	return thisVar;
    }

    // create a new global variable:
    Variable newVar = new Variable(aName);
    globalVars.addElement(newVar);
    return newVar;
  }

  /**
  ** Cloning a Variable returns a new Variable with the same name and
  ** type but with a different index. The new Variable will not be 
  ** equal to the original (using the <tt>equals()</tt> test).
  ** @return an (unequal) copy of this Variable
  ** @exception OutOfMemoryError An error can occur if the unique indices for 
  ** Variables have run out.
  */
  public Object clone() {
    Variable newVar = new Variable(theName);
    newVar.theType = theType;
    return newVar;
  }

  /**
  ** This function removes all Variables from the static memory. Future
  ** calls to <tt>get()</tt> (or the constructor) will return new Variables 
  ** even if the given names have been used before.
  */
  public static void newVars() {
    globalVars = new Vector(30, 20);
    localVars = new Vector(30, 20);
  }

  /** 
  ** This function can be used to remove the last <tt>n</tt> local Variables 
  ** from the stack. Subsequent calls to <tt>get()</tt> which could have 
  ** otherwise returned one of these Variables will not find them anymore 
  ** and thus, look for either previously defined local or global Variables 
  ** that might have been hidden by the Variables now removed here.
  ** @param n the number of variables to be removed from the stack
  ** @exception IllegalArgumentException An exception will occur if the number
  ** of local Variables currently in the static stack is less than the given 
  ** number.
  */
  public static void removeLocals(int n) throws IllegalArgumentException {
    if (localVars.size() < n)
      throw new IllegalArgumentException ("Cannot remove " + n + 
          " elements from " + localVars.toString());
    int lastToRemove = localVars.size()-n;
    for (int i=localVars.size()-1; i>=lastToRemove; i--)
      localVars.removeElementAt(i);
  }

  /** 
  ** This function sets the type of the variable to the given Symbol (or null).
  ** If the Variable already had a different type then this will be 
  ** overwritten.
  ** @param aSy the (new) type of this Variable
  */
  public void setType(Symbol aSy) {
    theType = aSy;
  }

  /**
  ** This function returns the Symbol that represents the type 
  ** of this Variable. It may be null if the type was undefined.
  ** @return the type of this Variable
  */
  public Symbol getType() {
    return theType;
  }

  /** 
  ** This function tests for variable equality. Two Variables are 
  ** considered equal only if they are the same object in memory.
  ** @param otherVar the Object this one is compared to
  ** @return whether the other Object is the same as this
  */
  public boolean equals(Object otherVar) {
    return this == otherVar;
  }

  /** 
  ** This function returns the name of this Variable.
  ** @return the name of this Variable without the index
  */
  public String getName() {
    return theName;
  }

  /**
  ** It is possible to reuse Variables with this function. The given 
  ** Variable is stored as a global Variable and should a Variable of that
  ** name be seeked with <tt>get(String)</tt> then this Variable will be 
  ** returned.
  ** @param var the Variable to be used as global
  */
  public static void useVariable(Variable var) {
    globalVars.addElement(var);
  }

  /** 
  ** A Variable is printed as the String that is its name and its index if
  ** <tt>printWithIndex</tt> is <tt>true</tt>.
  ** @return the print-name of this Variable (depends on 
  ** <tt>printWithIndex</tt>)
  */
  public String toString() {
    if (printWithIndex)
      return theName + '_' + index;
    return theName;
  }

  /** 
  ** The hashCode() of a Variable is the unique index of this variable.
  ** @return the index of this Variable
  */
  public int hashCode() {
    return index;
  }

  /**
  ** It is allowed to create Variables directly with this constructor. 
  ** However, the static function get() should normally be used. A 
  ** Variable created with the constructor will not be stored as global
  ** or local.
  ** @param aName the name of the Variable
  ** @exception IllegalArgumentException An exception will occur if the 
  ** supplied String is empty or null.
  ** @exception OutOfMemoryError An error can occur if the unique indices for 
  ** Variables have run out.
  */
  protected Variable(String aName) throws IllegalArgumentException {
    if ((aName == null) || aName.equals(""))
      throw new IllegalArgumentException(
          "Attempt to create Variable without name!");
    theName = new String(aName);
    index = varIndex++;
    if (varIndex == Integer.MAX_VALUE)
      throw new OutOfMemoryError("Variable index overflow!");
  }

  /**
  ** This function returns the first Variable from the given Vector of 
  ** Variables that has the given String as its name (ignoring the index).
  ** If no such Variable exists the function returns null.
  ** @param name the name of the seeked Variable
  ** @param vars the Vector of Variables
  ** @return the first Variable from the given Vector with the given name
  */
  static public Variable get(String name, Vector vars) {
    for (Enumeration ve=vars.elements(); ve.hasMoreElements(); ) {
      Variable nv = (Variable)ve.nextElement();
      if (name.equals(nv.theName))
	return nv;
    }
    return null;
  }

  /** the name of this Variable */
  protected String theName;
  /** the Symbol that is the type of this Variable (by default null) */
  protected Symbol theType = null;

  private int index;

  private static int varIndex = 0;
  private static Vector globalVars = new Vector(30, 20);
  private static Vector localVars = new Vector(30, 20);

}
