SortExpression.java 

// 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

Copyright:  © by the author
Author:  Hassan Aït-Kaci
Version:  Last modified on Wed May 01 06:21:32 2019 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 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 <tt>SortExpression</tt> to the
    //  * specified argument (a <tt>BitCode</tt>).
    //  *
    //  * @params code a <tt>BitCode</tt>
    //  * @return this <tt>Sort</tt>
    //  */
    // 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();
    }
    /* ************************************************************************ */
  }

This file was generated on Mon Sep 09 09:18:00 PDT 2019 from file SortExpression.java
by the hlt.language.tools.Hilite Java tool written by Hassan Aït-Kaci