// FILE. . . . . /home/hak/hlt/src/hlt/osfv1/base/SortExpression.java
// EDIT BY . . . Hassan Ait-Kaci
// ON MACHINE. . Hak-Laptop
// STARTED ON. . Mon Sep 02 09:16:41 2013
/**
* This is the mother class of all OSF sort expressions to be
* interpreted in a given context of a sort ordering. It is instantiated
* by specific classes corresponding to specific expressions.
*
* @version Last modified on Mon Sep 16 12:30:49 2013 by hak
* @author Hassan Aït-Kaci
* @copyright © by the author
*/
package hlt.osf.base;
import java.util.HashSet;
import java.util.Iterator;
import hlt.osf.exec.Context;
import hlt.osf.util.BitCode;
import hlt.osf.util.Decoded;
import hlt.osf.io.DisplayManager;
/**
* This is the class of all OSF sort expressions, which are special kinds of
* instances of OsfExpression. It
* will always evaluate as a code, which then can be retrieved as an explicit
* sort or a disjunctive sort.
*/
abstract public class SortExpression extends OsfExpression
{
/* ************************************************************************ */
/**
* This returns the type of a sort expression, which is one of:
*
*
* -
* Context.SYM() if it is an atomic sort symbol, i.e.,
* an instance of the class Sort;
*
*
* -
* Context.DIS() if it is a disjunction of atomic sort
* symbols, i.e., an instance of the class DisjunctiveSortExpression;
*
*
* -
* Context.NOT() if it is a negated sort expression,
* i.e., an instance of the class NotSortExpression;
*
*
* -
* Context.AND() if it is a sort-expression conjunction,
* i.e., an instance of the class AndSortExpression;
*
*
* -
* Context.OR () if it is a sort-expression disjunction,
* i.e., an instance of the class OrSortExpression
* (N.B.: this is not to be confused with a DisjunctiveSortExpression,
* which is a disjunction of atomic sort symbols, while this is
* a disjunction or arbitrary sort expressions);
*
*
* -
* Context.BNT() if this is a sort-expression complementation,
* i.e., an instance of the class ButnotSortExpression.
*
*
*
*
* The three last types of sort expressions are for instances of BinarySortExpression.
*/
abstract public byte type ();
/* ************************************************************************ */
public boolean isConstant ()
{
return type() == Context.CON();
}
public boolean isSymbol ()
{
return type() == Context.SYM();
}
public boolean isDisjunction ()
{
return type() == Context.DIS();
}
public boolean isNot ()
{
return type() == Context.NOT();
}
public boolean isAnd ()
{
return type() == Context.AND();
}
public boolean isOr ()
{
return type() == Context.OR();
}
public boolean isButnot ()
{
return type() == Context.BNT();
}
/* ************************************************************************ */
/**
* This is this sort expression's bit code in its context.
*/
private BitCode _value;
/**
* Returns this sort expression's bit code in its context.
*/
public BitCode value ()
{
return _value == null
? (_value = _context.evaluate(this))
: _value;
}
/* ************************************************************************ */
/**
* Returns the string form of this sort expression's maximal lower bound
* after it has been evaluated in its context.
*/
public String maxLowerBound ()
{
Decoded decoded = decoded();
if (decoded.sort() != null)
return decoded.sort().toString();
int size = 0;
HashSet mlbs = decoded.mlbs();
StringBuffer buf = new StringBuffer("{ ");
for (Iterator it=mlbs.iterator();it.hasNext();)
{
if (++size == Decoded.enumSize())
{
buf.append("...");
break;
}
buf.append(it.next());
if (it.hasNext())
buf.append(" ; ");
}
buf.append(" }");
return buf.toString();
}
/* ************************************************************************ */
private Decoded _decoded;
/**
* Returns a Decoded object corresponding to the value of this
* sort expression.
*/
public Decoded decoded ()
{
return _decoded == null
? (_decoded = _context.decodedValue(value()))
: _decoded;
}
/* ************************************************************************ */
/**
* This is a flag indicating whether this expression is parenthesized or not.
* This is used for rendering its original string form.
*/
private boolean _isParenthesized = false;
/**
* This returns whether or not this expression is parenthesized.
* This is used for rendering its original string form.
*/
public boolean isParenthesized ()
{
return _isParenthesized;
}
/**
* This sets whether or not this expression is to be parenthesized.
* This is used for rendering its original string form.
*/
public SortExpression setParenthesized (boolean value)
{
_isParenthesized = value;
return this;
}
/* ************************************************************************ */
public String toString ()
{
return displayForm();
}
/* ************************************************************************ */
}