Context.html

`Context.java`

    // FILE. . . . . /home/hak/hlt/src/hlt/osf/exec/Context.java
    // EDIT BY . . . Hassan Ait-Kaci
    // ON MACHINE. . Hp-Dv7
    // STARTED ON. . Mon Nov 05 19:13:27 2012

This is the class gathering the data structures and resources used for the interpretation of OSF constraints. It can be viewed as an sort ordering context for accessing, compiling, and evaluating OSF forms.
Author: |  | Hassan Aït-Kaci
Copyright: |  | © by the author
Version: |  | Last modified on Mon Jan 21 09:45:34 2013 by hak

    package hlt.osf.exec;

    import hlt.osf.io.*;
    import hlt.osf.base.*;
    import hlt.osf.util.*;

    import hlt.language.tools.Debug;

    import hlt.language.util.Error;
    import hlt.language.util.Stack;
    import hlt.language.util.Locatable;
    import hlt.language.util.ArrayList;

    import java.util.HashMap;
    import java.util.Iterator;

    public class Context
    {
      /* ************************************************************************ */

Constructs a new sort ordering context.

      public Context ()
      {
        _taxonomy.setContext(this);
      }

Constructs a new sort ordering context with the specified sort code array size.

      public Context (int sortCodeArraySize)
      {
        this(sortCodeArraySize,2,3);
      }

Constructs a new sort ordering context with the specified sort code array size, the named sort table's size factor, and the code cache's size. These factors set the corresponding tables' sizes as multiple of the size of the sort code array.

      public Context (int sortCodeArraySize, float namedSortTableFactor, float cachCodeTableFactor)
      {
        this();
        _SORT_CODE_ARRAY_SIZE = sortCodeArraySize;
        _NAMED_SORTS_TABLE_SIZE = Math.round(namedSortTableFactor * sortCodeArraySize);
        _CODE_CACHE_TABLE_SIZE = Math.round(cachCodeTableFactor * sortCodeArraySize);
      }

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

The initial size of this context's taxonomy (defaults to `50`).

      private int _SORT_CODE_ARRAY_SIZE = 50;

The array of sorts to encode.

      private Taxonomy _taxonomy = new Taxonomy(_SORT_CODE_ARRAY_SIZE);

Returns this OSF context's array where sorts are recorded.

      public Taxonomy taxonomy ()
        {
          return _taxonomy;
        }

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

      private ErrorLogger _errorLogger = new ErrorLogger();

      public ErrorLogger errorLogger ()
      {
        return _errorLogger;
      }

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

Returns the top sort symbol. This is safe only if the taxonomy has been encoded.

      static public Sort top () throws LockedCodeArrayException
      {
        return Sort.top();
      }

Returns the bottom sort symbol. This is safe only if the taxonomy has been encoded.

      static public Sort bottom () throws LockedCodeArrayException
      {
        return Sort.bottom();
      }

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

This the least available index in this context's taxonomy. It is equal to `0` if there are no built-in sorts. Defining new built-in sorts increase this value so that built-in sorts remain untouched in the array upon resetting.

      private int _MIN_SORT_INDEX = 0;

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

Resets this sort ordering context to a "virginal" state, preserving only built-in sorts.

      public void reset ()
      {
        // clear all sorts except built-in sorts:
        _taxonomy.reset(_MIN_SORT_INDEX);

        if (_taxonomy.isLocked())
          {
    	// reset the children of top:
    	top().resetChildren();
    	// reset the height of top:
    	top().resetHeight();
    	// reset the parents of bottom:
    	bottom().resetParents();
          }

        // clear the named sort and code cache tables, and re-register the
        // built-in sort names - except for top and bottom, which will get
        // re-registered at when re-locking the sort code array:
        _namedSorts.clear();
        _codeCache.clear();

        for (int i = _MIN_SORT_INDEX; i-->0;)
          {
    	Sort sort = (Sort)_taxonomy.get(i);
    	_namedSorts.put(sort.name,sort);
          }

        // resets the last evaluated expression to null:
        _lastExpression = null;

        // unlock the defined sorts:
        _taxonomy.unlock();
      }

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

The initial size of this context's named sort table (defaults to twice the `_SORT_CODE_ARRAY_SIZE`).

      private int _NAMED_SORTS_TABLE_SIZE = 2 * _SORT_CODE_ARRAY_SIZE;

The table associating names to sorts.

      private HashMap _namedSorts = new HashMap(_NAMED_SORTS_TABLE_SIZE);

Returns this OSF context's table associating a name to the sort it denotes.

      public HashMap namedSorts ()
        {
          return _namedSorts;
        }

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

The initial size of this context's code cache table (defaults to three times the `_SORT_CODE_ARRAY_SIZE`).

      private int _CODE_CACHE_TABLE_SIZE = 3 * _SORT_CODE_ARRAY_SIZE;

The table associating bit codes to sorts.

      private HashMap _codeCache = new HashMap(_CODE_CACHE_TABLE_SIZE);

Returns this OSF context's table associating a bit code to the sort it denotes if there is one, or the set of sorts that are its maximal lower bounds as an array or sorts.

      public HashMap codeCache ()
        {
          return _codeCache;
        }

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

If the specified name is an undefined sort, this defines the sort with this name initializing it in the sort array. Returns the defined sort with its context set to this one.

      public Sort getSort (String sortName) throws UndefinedSymbolException
      {
        String name = sortName.intern();

        if (name == "@")
          return top();

        if (name == "{}")
          return bottom();

        Sort sort = (Sort)_namedSorts.get(name);

        if (sort == null) // this is a new sort
          {
    	if (_taxonomy.isLocked())
    	  throw new UndefinedSymbolException("Undefined sort symbol: "+sortName);

    	BitCode code = new BitCode();
    	int index = _taxonomy.size();

    	code.set(index);
    	sort = new Sort(index,name,code);
    	_taxonomy.add(sort);
    	_namedSorts.put(name,sort);
          }

        return sort.setContext(this);
      }

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

This returns the bit code of the sort bearing the specified name.

      public BitCode getSortCode (String name) throws LockedCodeArrayException, UndefinedSymbolException
      {
        if (!_taxonomy.isLocked())
          throw new LockedCodeArrayException("Attempt to perform an operation requiring prior sort encoding");

        // no need to pay the price of a hash search
        if (name == "@")
          return top().code;
        // no need to pay the price of a hash search
        if (name == "{}")
          return bottom().code;

        Sort sort = (Sort)_namedSorts.get(name);

        if (sort == null)
          throw new UndefinedSymbolException("Undefined sort symbol: "+name);

        return sort.code;
      }

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

This returns a string form of the sorts whose codes are maximal lower bounds of the specified code. It is empty, this is bottom. If its cardinality is equal to the number of defined sorts, this is top. Otherwise, it checks the code cache in case this code had already been decoded before. Otherwise, it compute its maximal lower bounds and records it in the code cache before returning is display form.

      public String decodedString (BitCode code)
      {
        DisplayFormManager dfm  = _displayManager.displayFormManager();

        int cardinality = code.cardinality();

        if (cardinality == 0)
          // this is bottom:
          return dfm.displayBottomForm();

        if (cardinality == _taxonomy.size())
          // this is top:
          return dfm.displayTopForm();

        // check the code cache:
        Object mlbs = decode(code);

        if (mlbs instanceof Sort)
          return dfm.displaySortForm((Sort)mlbs);

        // return the MLBs code's string form:
        return dfm.displaySortsForm((BitCode)mlbs,_taxonomy);
      }

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

Given a bit code, this returns the object that it corresponds to in the current taxonomy. This object may be either a sort, or a disjunctive set of its maximal subsorts represented as a bit code set of these subsorts' indices.

      public Object decode (BitCode code)
      {
        // check the code cache:
        Object mlbs = _codeCache.get(code);

        if (mlbs == null)
          // this code has not been seen before compute its MLBs and cache it:
          _codeCache.put(code,mlbs=_taxonomy.maxLowerBounds(code));

        return mlbs;
      }

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

This declares that the sort named `s1` is a subsort of the sort named `s2`. This assumes that the sort ordering has not been encoded yet.

      public void declareIsa (String s1, String s2, Locatable where)
        throws LockedCodeArrayException, CyclicSortOrderingException
        {
          if (_taxonomy.isLocked())
    	throw new LockedCodeArrayException("Attempt to modify an already encoded sort taxonomy "+where);

          if (s1 == "{}")
    	throw new CyclicSortOrderingException("Cannot declare a supersort of {} "+where);

          if (s2 == "@")
    	throw new CyclicSortOrderingException("Cannot declare a subsort of @ "+where);

          Sort s_1 = getSort(s1);
          Sort s_2 = getSort(s2);

          if (!s_1.addIsaDeclaration(s2))
          	_errorLogger.recordError(new Error()
    				 .makeWarning()
    				 .setLabel("Warning: ")
    				 .setMsg("redundant subsort declaration: "+s1+" <| "+s2)
    				 .setExtent(where));

          // no need to declare a subsort of top or a supersort of bottom:
          if (s1 == "{}" || s2 == "@")
    	return;

          s_2.code.set(s_1.index);
        }

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

Encodes all the sorts of this sort ordering context's taxonomy.

      public void encodeSorts () throws AnomalousSituationException
      {
        _taxonomy.encodeSorts();
      }

Encodes the sorts between index first and index last (both inclusive) of this sort ordering context's taxonomy.

      public void encodeSorts (int first, int last) throws AnomalousSituationException
      {
        _taxonomy.encodeSorts(first,last);
      }

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

      private DisplayManager _displayManager = new DisplayManager();

      public DisplayManager displayManager ()
      {
        return _displayManager;
      }

      public void setDisplayManager (DisplayManager displayManager)
      {
        _displayManager = displayManager;
      }

      /* ************************************************************************ */
      /*                       SORT EXPRESSION EVALUATION                         */
      /* ************************************************************************ */

      static private final byte _SYM = 0;
      static private final byte _DIS = 1;
      static private final byte _NOT = 2;
      static private final byte _AND = 3;
      static private final byte _OR  = 4;
      static private final byte _BNT = 5;
      static private final byte _BAD = 6;

      static public final byte SYM () { return _SYM; }
      static public final byte DIS () { return _DIS; }
      static public final byte NOT () { return _NOT; }
      static public final byte AND () { return _AND; }
      static public final byte OR  () { return _OR;  }
      static public final byte BNT () { return _BNT; }

      static final private Byte _NOT_OP = new Byte(_NOT);
      static final private Byte _AND_OP = new Byte(_AND);
      static final private Byte _OR_OP  = new Byte(_OR);

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

This is a stack used to compile a sort expression into postfix form to be evaluated.

      private Stack _exprStack = new Stack();

This is a stack used to evaluate a sort expression that has been compiled into postfix form in _exprStack.

      private Stack _evalStack = new Stack();

This is the last expression that was evaluated in this context. Its bit code is its `value()`.

      private SortExpression _lastExpression;

Returns the last sort expression evaluated in this context.

      public SortExpression lastExpression () throws LockedCodeArrayException, AnomalousSituationException
      {
        if (!_taxonomy.isLocked())
          throw new LockedCodeArrayException("Attempt to perform an operation requiring prior sort encoding");

        if (_lastExpression == null)
          throw new AnomalousSituationException("No expression has been evaluated yet");

        return _lastExpression;
      }

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

Compiles and evaluates the specified sort expression.

      public BitCode evaluate (SortExpression expression) throws LockedCodeArrayException
      {
        if (!_taxonomy.isLocked())
          throw new LockedCodeArrayException("Attempt to evaluate a sort expression with a non-encoded sort taxonomy");

        _exprStack.clear();
        _evalStack.clear();
        _lastExpression = expression;
        _compile(expression);
        return _evaluate();
      }

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

      // These are used for tracing to step through a sort expression's
      // evaluation (essentially for debugging purposes).

      private static boolean _isTracing = false;

      public static void toggleTracing ()
      {
        _isTracing = !_isTracing;
      }

      public static boolean isTracing ()
      {
        return _isTracing;
      }

      private void _showStack (Stack stack)
      {
        for (int i = stack.size(); i-->0;)
          _printStackElt(stack.get(i));
      }

      private void _printStackElt (Object o)
      {
        if (o instanceof Byte)
          System.err.println(_opToString((Byte)o));
        else
          System.err.println(decodedString((BitCode)o));
      }

      private void _showSortStack (Stack stack)
      {
        for (int i = stack.size(); i-->0;)
          _printSortStackElt((BitCode)stack.get(i));
      }

      private void _printSortStackElt (BitCode code)
      {
        System.err.println("code = "+code+"\tmaximal subsort = "+decodedString(code));
      }

      private String _opToString (Byte op)
      {
        switch (op.byteValue())
          {
          case _AND:
    	return "AND";
          case _OR:
    	return "OR";
          case _NOT:
    	return "NOT";
          }
        return "UNKNOWN_OP";
      }

      private void _trace ()
      {
        System.err.println("*****************");
        System.err.println("EVALUATION STACK:");
        System.err.println("*****************");
        _showSortStack(_evalStack);

        System.err.println();

        System.err.println("*****************");
        System.err.println("EXPRESSION STACK:");
        System.err.println("*****************");
        _showStack(_exprStack);

        if (_NUM_OF_CODES_COPIED != _CODE_COPIES_SO_FAR)
          {
    	int newCopies = _NUM_OF_CODES_COPIED - _CODE_COPIES_SO_FAR;
    	System.err.println("\nMade "+(newCopies)+" new code cop"+(newCopies == 1 ? "y" : "ies"));
    	_CODE_COPIES_SO_FAR = _NUM_OF_CODES_COPIED;
          }

        Debug.step();
      }

      private static int _NUM_OF_CODES_COPIED;
      private static int _CODE_COPIES_SO_FAR;

      public static void tallyCodeCopy ()
      {
        _NUM_OF_CODES_COPIED++;
      }

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

This compiles the current sort expression into the expression stack in postfix form of bit codes and Boolean operators. Only three Boolean operators are used for compiling all types of sort expressions: one unary (`NOT`) and two binary (`AND`, `NOT`). The `DIS` operation compiles using `OR`s, and the `BNT` using `AND` and `NOT`.

      private void _compile (SortExpression e) throws UndefinedSymbolException
      {
        ArrayList dis = null;
        int size = 0;

        switch (e.type())
          {
    	case _SYM:
    	_exprStack.push(getSortCode(((SymbolSortExpression)e).name()));
    	return;

    	case _DIS:
    	dis = ((DisjunctiveSortExpression)e).names();
    	size = dis.size();

    	if (size == 0)
    	  { // an empty sort disjunction is compiled as bottom:
    	    _exprStack.push(bottom().code);
    	    return;
    	  }
    	// an non-empty sort disjunction is compiled as a sequence of ORs
    	// or simply just the first symbol if a singleton:
    	for (int i=size; i-->1;)
    	  {
    	    _exprStack.push(_OR_OP);
    	    _exprStack.push(getSortCode((String)dis.get(i)));
    	  }
    	_exprStack.push(getSortCode((String)dis.get(0)));
    	return;

    	case _NOT:
    	_exprStack.push(_NOT_OP);
    	_compile(((NotSortExpression)e).arg());
    	return;

    	case _AND:
    	_exprStack.push(_AND_OP);
    	_compile(((AndSortExpression)e).rhs());
    	_compile(((AndSortExpression)e).lhs());
    	return;

    	case _OR:
    	_exprStack.push(_OR_OP);
    	_compile(((OrSortExpression)e).rhs());
    	_compile(((OrSortExpression)e).lhs());
    	return;

    	case _BNT: // compiled as: lhs and not(rhs)
    	_exprStack.push(_AND_OP);
    	_exprStack.push(_NOT_OP);
    	_compile(((ButnotSortExpression)e).rhs());
    	_compile(((ButnotSortExpression)e).lhs());
    	return;
          }
      }

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

This evaluates a compiled expression stack `_exprStack` consisting of a postfix form of bit codes and Boolean operators using the evaluation stack `_evalStack`.

      private BitCode _evaluate ()
      {
        Object elt = null;
        BitCode arg1 = null;
        BitCode arg2 = null;

        if (_isTracing)
          {
    	_NUM_OF_CODES_COPIED = 0;
    	_CODE_COPIES_SO_FAR = 0;
          }

        while (!_exprStack.empty())
          {
    	if (_isTracing)
    	  _trace();

    	elt = _exprStack.pop();

    	if (elt instanceof BitCode)
    	  _evalStack.push(elt);
    	else
    	  // elt must be a Byte operator:
    	  switch (((Byte)elt).byteValue())
    	    {
    	    case _NOT:
    	      arg1 = (BitCode)_evalStack.pop();
    	      _evalStack.push(BitCode.not(arg1));
    	      break;
    	    case _AND:
    	      arg1 = (BitCode)_evalStack.pop();
    	      arg2 = (BitCode)_evalStack.pop();
    	      _evalStack.push(BitCode.and(arg1,arg2));
    	      break;
    	    case _OR:
    	      arg1 = (BitCode)_evalStack.pop();
    	      arg2 = (BitCode)_evalStack.pop();
    	      _evalStack.push(BitCode.or(arg1,arg2));
    	      break;
    	    }
          }

        if (_isTracing)
          {
    	_trace();
    	System.err.println("\nTotal number of code copying in this run: "+
    			   _NUM_OF_CODES_COPIED);
          }

        return ((BitCode)_evalStack.pop()).lock();
      }

      /* ************************************************************************ */
    }

This file was generated on Wed Jan 30 13:26:29 CET 2013 from file `Context.java`
by the `hlt.language.tools.Hilite` Java tool written by Hassan Aït-Kaci