`Context.java`

    // FILE. . . . . /home/hak/hlt/src/hlt/osfv2/exec/Context.java
    // EDIT BY . . . Hassan Ait-Kaci
    // ON MACHINE. . Hak-Laptop
    // STARTED ON. . Mon Sep 02 15:34:40 2013

This is the class gathering the data structures and resources used for the interpretation of OSF constraints. It can be viewed as a context for accessing, compiling, and evaluating OSF forms.
Author: |  | Hassan Aït-Kaci
Copyright: |  | © by the author
Version: |  | Last modified on Tue Jan 21 08:48:56 2014 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 = 1000000; //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();
      }

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

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(Taxonomy.builtins.size());

        // 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 = Taxonomy.builtins.size(); 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);	// initialize the new sort's code by setting the bit corresponding to the sort's index
    	sort = new Sort(index,name,code);

    	_taxonomy.add(sort);
    	_namedSorts.put(name,sort);
          }

        return sort.setContext(this);
      }

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

Checks if there already exists a sort with the specified name; if so, does nothing; if not, declares it.

      private void _checkDeclaredSort (String sortName)
      {
        String name = sortName.intern();

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

        if (sort == null) // this is a new sort
          {
    	BitCode code = new BitCode();
    	int index = _taxonomy.size();

    	// initialize the new sort's code by setting the bit
    	// corresponding to the sort's index:
    	code.set(index);
    	sort = new Sort(index,name,code);

    	// install the new built-in sort as a child of top:
    	Sort.top().addChild(sort);
    	sort.addParent(Sort.top());
    	// install the new built-in sort as a parent of bottom:
    	Sort.bottom().addParent(sort);
    	sort.addChild(Sort.bottom());

    	// add the new sort to the taxonomy:
    	_taxonomy.add(sort);
    	_namedSorts.put(name,sort);

    	// set the new sort's context to this one:
    	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. If it is all 0's, this is bottom. If its cardinality is equal to the number of defined sorts, this is top. Otherwise, it computes its decoded value as a `Decoded` object (which may been saved in the cache, or a new one that gets cached), and returns the string form of either a sort or a set of maximal lower bounds as the case may be.

      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();

        // decode the code:
        Decoded decodedObject = decodedValue(code);

        if (decodedObject.isSort())
          // this is a sort
          return dfm.displaySortForm(decodedObject.sort());

        // return the MLBs code's string form:
        return dfm.displayForm(decodedObject.mlbs(),false);
      }

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

This returns a `Decoded` object for the specified code. It checks the code cache in case this code had already been decoded before, in which case it returns the `Decoded` object associated to this code in the cache. If the code has not been seen before, it constructs a new `Decoded` object for this code and records it in the code cache before returning it.

      public Decoded decodedValue (BitCode code)
      {
        long time = System.currentTimeMillis();

        // check the code cache:
        Decoded decoded = (Decoded)_codeCache.get(code);

        if (decoded == null)
          // no such decoded object in the cache; build a new one and cache it:
          // _codeCache.put(code,decoded = new Decoded(code,_taxonomy));
          _codeCache.put(code,decoded = _taxonomy.decode(code));

        time = System.currentTimeMillis() - time;
        if (_isTiming)
          System.out.println("*** Decoding time = "+time+" ms");

        return decoded;
      }

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

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)
        {
          String location = where.locationString();

          if (_taxonomy.isLocked())
          	throw new LockedCodeArrayException("Attempt to modify an already encoded sort taxonomy - in "+location);

          if (s1 == "{}")
          	throw new AnomalousSituationException("Cannot declare a supersort of {} - in "+location);

          if (s2 == "{}")
          	throw new AnomalousSituationException("Cannot declare a subsort of {} - in "+location);

          if (s1 == "@")
    	throw new AnomalousSituationException("Cannot declare @ as a subsort - in "+location);

          if (s2 == "@")
    	{
    	  _checkDeclaredSort(s1);
    	  return;
    	}

          if (s1 == s2)
    	{
    	  _errorLogger.recordError(new Error()
    				   .makeWarning()
    				   .setLabel("Warning: ")
    				   .setMsg("reflexive subsort declaration: "+s1+" <| "+s2+" (ignored)")
    				   .setExtent(where));
    	  return;
    	}

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

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

          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 _CON = 0;
      static private final byte _SYM = 1;
      static private final byte _DIS = 2;
      static private final byte _NOT = 3;
      static private final byte _AND = 4;
      static private final byte _OR  = 5;
      static private final byte _BNT = 6;
      static private final byte _BAD = 7;

      static public final byte CON () { return _CON; }
      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;
        long timeC = System.nanoTime();
        _compile(expression);
        timeC = System.nanoTime() - timeC;
        long timeV = System.nanoTime();
        BitCode value = _evaluate();
        timeV = System.nanoTime() - timeV;
        if (_isTiming)
          {
    	System.out.println("*** Expression compilation time = "+(((double)timeC)/1000000)+" ms");
    	System.out.println("*** Expression evaluation time = "+(((double)timeV)/1000000)+" ms");
    	System.out.println("*** Expression processing time = "+((double)(timeC+timeV)/1000000)+" ms");
          }
        return value;
      }

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

      private static boolean _isTiming = false;

      public static void toggleTiming ()
      {
        _isTiming = !_isTiming;
      }

      public static boolean isTiming ()
      {
        return _isTiming;
      }

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

      // 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 flag is used to detect whenever negation has been used (so as to skip computing "undesirables" when decoding - see method `decode(BitCode)` in Taxonomy.java).

      static boolean negativeQuery = false;

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`. There must be special care taken for compiling (and evaluating an expression containing) a `ConstantSortExpression`. Indeed, a constant sort expression is in fact a pair of objects consisting of a built-in sort and a value. Regarding evaluation, there are several possible cases depending on whether the expression to evaluate is as described below. A constant sort expression—it is evaluated as its sort, keeping its value associated. A sort conjunction, one of whose argument is a constant—both sorts are conjoined. Since the sort of a constant is only compatible with itself, there are three possibilities: if the two sorts are different, then the result is bottom; otherwise, if both arguments are constants with different values, then the result is bottom; otherwise, the result is the constant (its sort with its associated value).

      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 = ((DisjunctiveSort)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());
    	negativeQuery = true;
    	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 Tue Jan 21 09:56:10 CET 2014 from file `Context.java`
by the `hlt.language.tools.Hilite` Java tool written by Hassan Aït-Kaci