`SortExpression.java`

    // FILE. . . . . /home/hak/hlt/src/hlt/osfv2/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.
Author: |  | Hassan Aït-Kaci
Copyright: |  | © by the author
Version: |  | Last modified on Tue Jan 21 08:05:58 2014 by hak

    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();
        }
        /* ************************************************************************ */
      }

This file was generated on Tue Jan 21 09:56:10 CET 2014 from file `SortExpression.java`
by the `hlt.language.tools.Hilite` Java tool written by Hassan Aït-Kaci