Context.html

Context.java

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

Copyright: © by the author

Author: Hassan Aït-Kaci

Version: Last modified on Fri Aug 23 12:28:19 2019 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;

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 storing, accessing, compiling, and evaluating OSF forms.


public class Context
{
  /* ************************************************************************ */
  // Context object components, getters, and setters

The initial size of this context's taxonomy.


  private int _SORT_CODE_ARRAY_SIZE = Custom.SORT_CODE_ARRAY_SIZE;

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;
    }

  /* ************************************************************************ */
  // Context object constructors

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);
  }
  
  /* ************************************************************************ */
  // Context's error logger

  private ErrorLogger _errorLogger = new ErrorLogger();

This is this Context's error logger. It controls where to log error messages.


  public ErrorLogger errorLogger ()
  {
    return _errorLogger;
  }

  /* ************************************************************************ */
  // Context's oft-used methods

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 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 Decoded objects.


  private HashMap _codeCache = new HashMap(_CODE_CACHE_TABLE_SIZE);

Returns this OSF context's table associating a bit code to the unique Decoded object it denotes if there is one. Defined sorts are registered at (re-)initialization.


  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();
    //    System.out.println(">>> Getting sort: "+name);

    if (name == Custom.TOP_STRING)
      return top();
    
    if (name == Custom.BOT_STRING)
      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 == Custom.TOP_STRING)
      return top().bitcode();
    // no need to pay the price of a hash search
    if (name == Custom.BOT_STRING)
      return bottom().bitcode();

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

    if (sort == null)
      throw new UndefinedSymbolException("Undefined sort symbol: "+name);
    
    return sort.bitcode();
  }
  
  /* ************************************************************************ */

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 have been previously 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.

Parameters:

code - a BitCode object

Returns: a string listing the GLBs of the given code


  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 = decode(code);

    // For debugging purposes we may need to use this instead of just
    // the GLBs: a 3-line string listing: (1) the ancestors, (2) the
    // sort symbol with this code (if there is one), (3) the
    // descendants:
    //
    // return decodedObject.toString();

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

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

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

This returns a Decoded object for the specified code. It checks the code cache in case this code has 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 decode (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 = _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 == Custom.BOT_STRING)
      	throw new AnomalousSituationException("Cannot declare a supersort of "+Custom.BOT_STRING+" - in "+location);
      
      if (s2 == Custom.BOT_STRING)
      	throw new AnomalousSituationException("Cannot declare a subsort of "+Custom.BOT_STRING+" - in "+location);

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

      if (s2 == Custom.TOP_STRING)
	{
	  _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.bitcode().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();

This is this Context's display manager. It controls where to output the display.


  public DisplayManager displayManager ()
  {
    return _displayManager;
  }

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

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

  // expression indentifying codes:

  static private final byte _CON = 0; // identifies a constant
  static private final byte _SYM = 1; // identifies a symbol
  static private final byte _DIS = 2; // identifies a disjunctive sort ({t_1 ; ... ; t_n})
  static private final byte _NOT = 3; // identifies a negation (unary not)
  static private final byte _AND = 4; // identifies a conjunction (binary and)
  static private final byte _OR  = 5; // identifies a disjunction (binary or)
  static private final byte _BNT = 6; // identifies a relative complementation (binary butnot)
  static private final byte _BAD = 7; // identifies a bad expression

  // Public accessors of the above (BAD not needed):

Identifies a constant.


  static public final byte CON () { return _CON; }

Identifies a symbol.


  static public final byte SYM () { return _SYM; }

Identifies a disjunctive sort ({t₁ ; ... ; t_n}).


  static public final byte DIS () { return _DIS; }

Identifies a negation (unary not).


  static public final byte NOT () { return _NOT; }

Identifies a conjunction (binary and).


  static public final byte AND () { return _AND; }

Identifies a disjunction (binary or).


  static public final byte OR  () { return _OR;  }

Identifies a relative complementation (binary butnot).


  static public final byte BNT () { return _BNT; }

  // The following are the only basic operations on bit vectors needed
  // to implement the above:

  static final private Byte _NOT_OP = Byte.valueOf(_NOT);
  static final private Byte _AND_OP = Byte.valueOf(_AND);
  static final private Byte _OR_OP  = Byte.valueOf(_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 the value of its bitcode().


  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, then returns the BitCode resulting from the evaluation.


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

    System.err.println(">>> Expression to be compiled and evaluated: "+expression);

    _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;

Toggles timing on/off.


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

Returns true iff timing is on.


  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;

Toggles tracing on/off. Tracing steps through a SortExpression's evaluation. Usefule for debugging or demo purposes.


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

Returns true iff tracing is on.


  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));
    // System.err.println("code = "+code);
    
    // for debugging purposes, the following prints:
    // - all ancestor sorts
    System.err.println("\tancestors = "+code.decoded().ancestors(_taxonomy));
    // - the lub sorts
    System.err.println("\tlubs = "+code.decoded().lubs());
    // - the sort for this code if there is one
    Sort sort = code.decoded().sort();
    System.err.println("\tsort = "+(sort==null?"":sort));
    // - the glb sorts
    System.err.println("\tglbs = "+code.decoded().glbs());
    // - all descendant sorts
    System.err.println("\tdescendants = "+code.decoded().descendants(_taxonomy));
    // - all unrelated sorts
  }

  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 trigger 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, OR). The DIS operation is compiled using ORs, and the BNT operation is compiled 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 and ⊤, if one of them is ⊤, then the result is the constant; otherwise, 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
  {
    System.err.println(">>> Compiling expression "+e);

    ArrayList dis = null; // to store the elements of a disjunctive set of sorts
    int size = 0; // used to record the size of the above (see case _DIS below)

    switch (e.type())
      {
      case _SYM: // this is a sort symbol: push its bitcode as the generated instruction
	_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().bitcode());
	    return;
	  }
	// a 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 ()
  {

    System.err.println(">>> Evaluating the stack");
    
    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));
	      negativeQuery = true;
	      if (_isTracing)
		System.err.println(">>> Setting negative query flag");
	      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 Mon Sep 09 09:18:00 PDT 2019 from file Context.java
by the hlt.language.tools.Hilite Java tool written by Hassan Aït-Kaci