|
Tag.java
|
// FILE. . . . . /home/hak/hlt/src/hlt/osfv3/base/Tag.java // EDIT BY . . . Hassan Ait-Kaci // ON MACHINE. . Hak-Laptop // STARTED ON. . Mon Sep 02 09:16:55 2013
|
package hlt.osf.base; import java.util.HashMap; import java.util.Iterator;
| This is the class of ψ-term tags as explained in the specification. Tags are uniquely identified by their names. This means that two tag instances with the same name are in fact the same object. This is ensured thanks to a global hash map associating an interned (i.e. unique) 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 (i.e., unique) strings. |
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;
}
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 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 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 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();
}
/* ************************************************************************ */
}
This file was generated on Mon Sep 09 09:18:00 PDT 2019 from file Tag.java
by the hlt.language.tools.Hilite Java tool written by Hassan Aït-Kaci