// FILE. . . . . /home/hak/hlt/src/hlt/osfv2/base/Tag.java
// EDIT BY . . . Hassan Ait-Kaci
// ON MACHINE. . Hak-Laptop
// STARTED ON. . Mon Sep 02 09:16:55 2013

/**
 * This is the class of &psi;-term tags as explained in the <a
 * href="../specs/basic.html#Tags">specification</a>. Tags are uniquely
 * identified by their names. That means that two tag instances with the
 * same name are in fact the same object. This is ensure thanks to a
 * global hash map associating an interned string name to the unique tag
 * baring this name. A tag will be said to be "<i>free</i>" whenever it
 * is not the tag of any <tt>&psi;-term</tt> (although it may be bound
 * to one that is).  By convention, any tag name will start with the '#'
 * character, even if the name it is given does not - in which case it
 * is prepended with '#'. All tag names are interned striing.
 *
 * @version     Last modified on Tue Jan 21 08:06:03 2014 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>
 */

package hlt.osf.base;

import java.util.HashMap;
import java.util.Iterator;

public class Tag
  {
    /* ************************************************************************ */

    /**
     * This is a global counter used to generate new tag names.
     */
    private static int _tagNumber = 0;

    /**
     * Returns a newly generated tag name. Generated tags are of the
     * form <tt>#_<i>n</i></tt>, where <tt><i>n</i></tt> is an integer,
     * Since it could be possible that such a tag name may have be
     * already specified as an explicitly named tag, care must be taken
     * not to return such an already recorded tag.
     */
    public static String newTagName ()
      {
	String tagName = ("#_"+(_tagNumber++)).intern();

	if (_knownTags.get(tagName) != null)
	  // can't use this name as it already exists as an explicitly named tag
	  return newTagName();
	
	return tagName;
      }

    /* ************************************************************************ */

    /**
     * This is a global hash map associating a tag name to the unique
     * tag bearing this name.
     */
    private static HashMap _knownTags = new HashMap();

    /**
     * Resets the know tags and the tag numbering.
     */
    public static void clearKnownTags ()
      {
	_knownTags.clear();
	_tagNumber = 0;
      }

    public static void tallyTags ()
    {
      if (!_knownTags.isEmpty())
	{
	  System.out.println("----------");
	  System.out.println("Known Tags:");
	  System.out.println("----------");
	  for (Iterator it = _knownTags.values().iterator(); it.hasNext();)
	    {
	      Tag tag = (Tag)it.next();
	      System.out.println(tag+(tag.isShared() ? "\t(shared)" : ""));
	    }
	  System.out.println("----------");
	}
    }

    /**
     * This static method returns the tag uniquely identified with the given
     * name. If the given name is null, a new tag is created and a newly
     * generated name associated to it. Therefore, this class has no public
     * constructor: the only way to access or make a tag is by invoking the
     * method <tt>Tag.getTag(String name)</tt>.
     */
    public static Tag getTag (String name)
      {
	Tag tag = null;
	  
	if (name == null)
	  {
	    tag = new Tag();
	    _knownTags.put(tag.name(),tag);
	    return tag;
	  }

	name = name.intern();

	tag = (Tag)_knownTags.get(name);

	if (tag == null)
	  {
	    tag = new Tag(name);
	    _knownTags.put(tag.name(),tag);
	  }

	return tag;
      }

    public static Tag newTag ()
    {
      return getTag(null);
    }

    /* ************************************************************************ */

    /**
     * Constructs an unbound free tag with an automatically generated name.
     */
    private Tag ()
      {
        _name = newTagName();
      }

    /**
     * Constructs an unbound free tag with the specified name.
     */
    private Tag (String name)
      {
        setName(name);
      }

    /* ************************************************************************ */

    /**
     * This is the tag this is bound too. By default a tag is unbound -
     * that is, it is bound to itself.
     */
    private Tag _ref = this;

    /**
     * This returns the immediate tag this is bound to.
     */
    public Tag ref ()
      {
	return _ref;
      }

    /**
     * Ths returns the ultimate tag this is bound to; <i>i.e.</i>, its
     * binding's binding's ... binding.  This is the most important method for
     * a tag as its real identity is always that of its dereferenced tag
     * (which may be itself if it is unbound).
     */
    public Tag deref ()
      {
	Tag value = _ref;

	while (value.ref() != value)
	  value = value.ref();

	return value;
      }

    /**
     * This binds this tag to the specified one and returns this
     * tag. Binding also sets this tag's term to the other's and
     * propagates sharing information between the two tags.
     */
    public Tag bind (Tag value)
      {
	if (_isShared)
	  value.markAsShared();
	else
	  if (value.isShared())
	    markAsShared();
	  
	_ref = value;

	// _term = value.deref().term();

	return this;
      }

    /**
     * Returns <tt>true</tt> iff this tag is bound.
     */
    public boolean isBound ()
      {
	return _ref != this;
      }

    /**
     * Returns <tt>true</tt> iff this tag is unbound.
     */
    public boolean isUnbound ()
      {
	return _ref == this;
      }

    /* ************************************************************************ */

    /**
     * This is <tt>true</tt> iff this tag occurs more than once in a &psi;-term.
     */
    private boolean _isShared = false;

    /**
     * Returns <tt>true</tt> iff this tag occurs more than once in a &psi;-term.
     */
    public boolean isShared ()
      {
	return _isShared;
      }

    /**
     * Mark this tag as shared (<i>i.e.</i>, reoccurring at distinct
     * positions) and returns this tag.
     */
    public Tag markAsShared ()
      {
	_isShared = true;
	return this;
      }

    /* ************************************************************************ */

    /**
     * This is the &psi;-term to which this tag belongs, unless it is free, in
     * which case it is <tt>null</tt>.
     */
    private PsiTerm _term = null;

    /**
     * Returns the &psi;-term to which this tag belongs if it is not free, or
     * <tt>null</tt> otherwise.
     */
    public PsiTerm term ()
      {
	return _term;
      }

    /**
     * Set this tag's term to the specified &psi;-term, and returns this tag.
     */
    public Tag setTerm (PsiTerm term)
      {
	_term = term;
	return this;
      }

    /**
     * Returns <tt>true</tt> iff this tag is free - <i>i.e.</i> it does not
     * belong to any &psi;-term (although it may be bound to one that is not
     * free).
     */
    public boolean isFree ()
      {
	return _term == null;
      }

    /* ************************************************************************ */

    /**
     * This is this tag's name.
     */
    private String _name;

    /**
     * Returns the name of this tag.
     */
    public String name ()
      {
	return _name == null ? _name = newTagName() : _name;
      }

    /**
     * This gives the specified name to this his tag and returns this
     * tag.  If the specified String does not start with a '#', one will
     * be prepended. Note, because equality of tags is object equality,
     * giving an explicit name to a tag may mean that if another tag
     * bears the same name, it will still be a <i>distinct</t> tag. For
     * explicitly named tags, it is therefore recommended to use a
     * global name manager ensuring unique names for all tags.
     */
    public Tag setName (String name)
      {
	if (name == null)
	  _name = newTagName();
	else
	  _name = (name.charAt(0) == '#' ? name : "#"+name).intern();
	return this;
      }

    /* ************************************************************************ */

    /**
     * Return a string value for this tag, which is its name.
     */
    public String toString ()
      {
	return name();
      }

    /* ************************************************************************ */

    // It is not necessary to change the equals method: we can let it
    // remain == since equals tags are always uniquely identified.

    // /**
    //  * Return true iff this tag has the same name as the supplied one.
    //  */
    // public equals (Object other)
    // {
    //   return other instantceof Tag && name() == ((Tag)other).name();
    // }

    public int hashCode ()
      {
    	return name().hashCode();
      }

    /* ************************************************************************ */
  }
