// 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 Fri Sep 06 08:17:59 2013 by hak
 * @author      <a href="mailto:hak@acm.org">Hassan A&iuml;t-Kaci</a>
 * @copyright   &copy; <a href="http://www.hassan-ait-kaci.net/">by the author</a>
 */

package hlt.osf.base;

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. 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 Boolean expression of this sort expression; one
     * of:
     * <ul>
     *    <li><tt>Context.SYM()</tt> if this is a sort symbol;</li>
     *    <li><tt>Context.DIS()</tt> if this is a disjunctive sort;</li>
     *    <li><tt>Context.NOT()</tt> if this is a negated sort expression;</li>
     *    <li><tt>Context.AND()</tt> if this is a sort-expression conjunction;</li>
     *    <li><tt>Context.OR ()</tt> if this is a sort-expression disjunction;</li>
     *    <li><tt>Context.BNT()</tt> if this is a sort-expression complementation.</li>
     * </ul>
     */
    abstract public byte type ();

    /* ************************************************************************ */

    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's maximal lower bound after
     * it has been evaluated in its context.
     */
    public String maxLowerBound ()
    {
      return decoded().mlbs().toString();
    }

    /* ************************************************************************ */

    private Decoded _decoded;
    
    /**
     * Returns a <tt>Decoded</tt> 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();
    }
    /* ************************************************************************ */
  }