// FILE. . . . . /home/hak/hlt/src/hlt/osfv1/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 ψ-term tags as explained in the specification. 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 "free" whenever it
* is not the tag of any ψ-term (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 Wed Sep 11 12:32:12 2013 by hak
* @author Hassan Aït-Kaci
* @copyright © by the author
*/
package hlt.osf.base;
import java.util.HashMap;
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 #_n, where n 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;
}
/**
* 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 Tag.getTag(String name).
*/
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.e., 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 propagates sharing information between the two tags.
*/
public Tag bind (Tag value)
{
if (_isShared)
value.markAsShared();
else
if (value.isShared())
markAsShared();
_ref = value;
return this;
}
/**
* Returns true iff this tag is bound.
*/
public boolean isBound ()
{
return _ref != this;
}
/**
* Returns true iff this tag is unbound.
*/
public boolean isUnbound ()
{
return _ref == this;
}
/* ************************************************************************ */
/**
* This is true iff this tag occurs more than once in a ψ-term.
*/
private boolean _isShared = false;
/**
* Returns true iff this tag occurs more than once in a ψ-term.
*/
public boolean isShared ()
{
return _isShared;
}
/**
* Mark this tag as shared (i.e., reoccurring at distinct
* positions) and returns this tag.
*/
public Tag markAsShared ()
{
_isShared = true;
return this;
}
/* ************************************************************************ */
/**
* This is the ψ-term to which this tag belongs, unless it is free, in
* which case it is null.
*/
private PsiTerm _term = null;
/**
* Returns the ψ-term to which this tag belongs if it is not free, or
* null otherwise.
*/
public PsiTerm term ()
{
return _term;
}
/**
* Set this tag's term to the specified ψ-term, and returns this tag.
*/
public Tag setTerm (PsiTerm term)
{
_term = term;
return this;
}
/**
* Returns true iff this tag is free - i.e. it does not
* belong to any ψ-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 distinct 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();
}
/* ************************************************************************ */
}