// FILE. . . . . d:/hak/hlt/src/hlt/fot/Variable.java
// EDIT BY . . . Hassan Ait-Kaci
// ON MACHINE. . Hak-Laptop
// STARTED ON. . Sat Jul 14 07:24:10 2018

package hlt.fot;

/**
 * This is a class for variables that may appear in first-order
 * terms. It implements the interface <a
 * href="FirstOrderTerm.html"><tt>FirstOrderTerm</tt></a>.
 *
 * @see         FirstOrderTerm
 *
 * @version     Last modified on Thu Aug 16 05:50:56 2018 by hak
 * @author      <a href="mailto:hak@acm.org">Hassan A&iuml;t-Kaci</a>
 * @copyright   &copy; <a href="http://www.hassan-ait-kaci.net/">by the author</a>
 */

import java.util.HashMap;
import java.util.ArrayList;

public class Variable implements FirstOrderTerm
{
  /* ************************************************************************ */
  // Fields and accessors:
  /* ************************************************************************ */

  private String name;
  private boolean isAnonymous = false;

  public String name ()
  {
    return name;
  }

  public boolean isAnonymous ()
  {
    return isAnonymous;
  }

  /* ************************************************************************ */
  // Constructors: they are all private to ensure that only this class
  // may use them; the public method getVariable(String) is the one to
  // use to access a registered variable or create it and register it;
  /* ************************************************************************ */

  private Variable ()
  {
    this(anonymousVariableName(),true);
  }

  private Variable (String name)
  {
    this.name = name;
    registeredVariableNames.add(name);
    registeredVariableTable.put(name,this);
  }

  private Variable (String name, boolean isAnonymous)
  {
    this(name);
    this.isAnonymous = isAnonymous;
  }

  /* ************************************************************************ */
  // Methods:
  /* ************************************************************************ */

  /**
   * Returns <tt>true</tt>. This implements the <tt>FirstOrderTerm</tt>
   * interface's method identifying <tt>this</tt> as a variable.
   */
  final public boolean isVariable ()
  {
    return true;
  }

  /**
   * Returns <tt>true</tt> iff this variable occurs in the specified term.
   */
  public boolean occursIn (FirstOrderTerm term)
  {
    if (term.isVariable())
      return this == ((Variable)term).deref();

    FirstOrderTermStructure t = (FirstOrderTermStructure)term;

    for (int i = 1; i <= t.functor().arity(); i++)
      if (this.occursIn(t.argument(i)))
	return true;

    return false;
  }

  /* ************************************************************************ */
  // Static structures and methods:
  /* ************************************************************************ */

  /**
   * This is a <tt>String</tt> &rarr; <tt>Variable</tt> association
   * table where all variables are uniquely represented and identified
   * by their names.
   */
  public static HashMap registeredVariableTable = new HashMap();

  /**
   * This is an ordered list of the names of all the registered
   * variables in the order of creation (upon initial registration).
   */
  public static ArrayList registeredVariableNames = new ArrayList();

  /**
   * Returns the variable uniquely associated to this name if it exists,
   * or creates it and returns it.
   */
  public static Variable getVariable (String name)
  {
    Variable variable = (Variable)registeredVariableTable.get(name);

    if (variable == null)
      variable = new Variable(name);

    return variable;
  }

  /**
   * This is the count of anomymous variables.
   */
  private static int anomymousVarCount = 0;

  /**
   * Erases all existing variables.
   */
  public static void resetRegisteredVariables ()
  {
    registeredVariableNames.clear();
    registeredVariableTable.clear();
    anomymousVarCount = 0;
  }

  private static String anonymousVariableName ()
  {
    return "_"+(anomymousVarCount++);
  }

  /**
   * Returns a new anonymous variable.
   */
  public static Variable anonymousVariable ()
  {
    return new Variable(anonymousVariableName(),true);
  }

  /* ************************************************************************ */
  // VARIABLE DEREFERENCING & BINDING
  /* ************************************************************************ */

  private FirstOrderTerm deref = this;

  public FirstOrderTerm deref ()
  {
    if (deref == this)
      return this;

    if (deref.isVariable())
      return ((Variable)deref).deref();

    return deref;
  }

  public boolean isBound ()
  {
    return deref() != this;
  }

  public boolean isUnbound ()
  {
    return deref() == this;
  }

  public void bind (FirstOrderTerm term)
  {
    deref = term;
  }

  /* ************************************************************************ */
  // STRING FORM
  /* ************************************************************************ */

  /**
   * Returns the string form of this variable.
   */
  public String toString ()
  {
    return name();
  }

  /**
   * Returns the string form of this variable taking into account its
   * eventual binding. Overrrides the equivalent but less efficient
   * default in <tt>FirstOrderTerm</tt>.
   */
  public String derefToString ()
  {
    FirstOrderTerm term = deref();

    if (term.isVariable())
      return term.toString();

    return term.derefToString();
  }

  /* ************************************************************************ */
  // EQUALITY
  /* ************************************************************************ */

  /**
   * Returns <tt>true</tt> if the specified term is this variable.
   * Because a variable is uniquely represented, they must be the same
   * individual.
   */
  public boolean equal (FirstOrderTerm term)
  {
    return this == term;
  }

}