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 Sun Mar 29 10:25:36 2015 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 DisjunctiveSort;

  • 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 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 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 Sun Mar 29 11:34:23 CEST 2015 from file SortExpression.java
by the hlt.language.tools.Hilite Java tool written by Hassan Aït-Kaci