// 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.
 *
 * @version     Last modified on Tue Jan 21 08:05:58 2014 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 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 <tt><a href="OsfExpression.html">OsfExpression</a></tt>. 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:
     * <ul>
     *
     * <p><li>
     *    <tt>Context.SYM()</tt> if it is an atomic sort symbol, <i>i.e.</i>,
     *    an instance of the class <tt><a href="Sort.html">Sort</a></tt>;
     * </li></p>
     *
     * <p><li>
     *    <tt>Context.DIS()</tt> if it is a disjunction of atomic sort
     *    symbols, <i>i.e.</i>, an instance of the class <tt><a
     *    href="DisjunctiveSortExpression.html">DisjunctiveSortExpression</a></tt>;
     * </li></p>
     *
     * <p><li>
     *    <tt>Context.NOT()</tt> if it is a negated sort expression,
     *   <i>i.e.</i>, an instance of the class <tt><a
     *   href="NotSortExpression.html">NotSortExpression</a></tt>;
     * </li></p>
     *
     * <p><li>
     *    <tt>Context.AND()</tt> if it is a sort-expression conjunction,
     *    <i>i.e.</i>, an instance of the class <tt><a
     *    href="AndSortExpression.html">AndSortExpression</a></tt>;
     * </li></p>
     *
     * <p><li>
     *    <tt>Context.OR ()</tt> if it is a sort-expression disjunction,
     *    <i>i.e.</i>, an instance of the class <tt><a
     *    href="OrSortExpression.html">OrSortExpression</a></tt>
     *    (<b>N.B.</b>: this is not to be confused with a <tt><a
     *    href="DisjunctiveSortExpression.html">DisjunctiveSortExpression</a></tt>,
     *    which is a disjunction of <i>atomic sort symbols</i>, while this is
     *    a disjunction or <i>arbitrary sort expressions</i>);
     * </li></p>
     *
     * <p><li>
     *    <tt>Context.BNT()</tt> if this is a sort-expression complementation,
     *    <i>i.e.</i>, an instance of the class <a
     *    href="ButnotSortExpression.html"><tt>ButnotSortExpression</tt></a>.
     * </li></p>
     *
     * </ul>
     *
     * The three last types of sort expressions are for instances of <tt><a
     * href="BinarySortExpression.html">BinarySortExpression</a></tt>.
     */
    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 <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();
    }
    /* ************************************************************************ */
  }
