// FILE. . . . . /home/hak/hlt/src/hlt/osf/base/SortExpression.java
// EDIT BY . . . Hassan Ait-Kaci
// ON MACHINE. . Hak-Laptop
// STARTED ON. . Mon Sep 02 09:16:41 2013
/**
* @version Last modified on Wed May 01 06:21:32 2019 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 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. These are
* special kinds of instances
* of OsfExpressions. 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
{
/* ************************************************************************ */
/**
* Returns the type of this sort expression as a byte. This
* may be one of:
*
* - Context.SYM() if this is an atomic sort symbol,
* i.e., an instance of the class Sort;
*
*
- Context.DIS() if this is a disjunction of atomic
* sort symbols, i.e., an instance of the class DisjunctiveSort;
*
*
- Context.NOT() if this is a negated sort
* expression, i.e., an instance of the class NotSortExpression;
*
*
- Context.AND() if this is a sort-expression
* conjunction, i.e., an instance of the class AndSortExpression;
*
*
- Context.OR () if this is a sort-expression
* disjunction, i.e., an instance of the class OrSortExpression
* (N.B.: this must not be confused with a DisjunctiveSort,
* 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 SortExpression's bit code after sort
* encoding.
*/
private BitCode _bitcode;
/**
* Returns this sort SortExpression's bit code after sort
* encoding by evaluating it in its context, but only if necessary.
*/
public BitCode bitcode ()
{
return _bitcode == null
? (_bitcode = _context.evaluate(this))
: _bitcode;
}
// /**
// * Sets the binary code of this SortExpression to the
// * specified argument (a BitCode).
// *
// * @params code a BitCode
// * @return this Sort
// */
// public SortExpression setBitcode (BitCode code)
// {
// _bitcode = code;
// return this;
// }
/* ************************************************************************ */
/**
* Returns the string form of this SortExpression's maximal
* lower bound after it has been evaluated in its context.
*/
public String maxLowerBound ()
{
Decoded decoded = decoded();
// System.err.println(">>> Decoded form of sort expression: \""+this+"\" is: "+decoded);
// System.err.println(">>> Its bit code is: "+decoded.bitcode());
if (decoded.isSort())
return decoded.sort().toString();
int size = 0;
HashSet glbs = decoded.glbs();
// System.err.println(">>> glbs = decoded.glbs() == "+glbs);
StringBuffer buf = new StringBuffer("{ ");
if (glbs != null)
for (Iterator it=glbs.iterator();it.hasNext();)
{
if (++size == Decoded.enumSize())
{
buf.append("...");
break;
}
buf.append(it.next());
if (it.hasNext())
buf.append(" ; ");
}
buf.append(" }");
// System.err.println(">>> glbs in string form == "+buf);
return buf.toString();
}
/* ************************************************************************ */
private Decoded _decoded;
/**
* Returns a Decoded object corresponding to the bitcode of this
* sort expression.
*/
public Decoded decoded ()
{
return _decoded == null
? (_decoded = _context.decode(bitcode()))
: _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();
}
/* ************************************************************************ */
}