// 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.
 *
 * @version     Last modified on Tue Jan 21 08:48:56 2014 by hak
 * @author      <a href="mailto:hak@acm.org">Hassan A&iuml;t-Kaci</a>
 * @copyright   &copy; <a href="http://www.hassan-ait-kaci.net/">by the author</a>
 */

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
   * <tt>50</tt>).
   */
  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 <tt>_SORT_CODE_ARRAY_SIZE</tt>).
   */
  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 <tt>_SORT_CODE_ARRAY_SIZE</tt>).
   */
  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
   * <tt>Decoded</tt> 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 <tt>Decoded</tt> 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 <tt>Decoded</tt> object
   * associated to this code in the cache. If the code has not been seen
   * before, it constructs a new <tt>Decoded</tt> 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 <tt>s1</tt> is a subsort of the
   * sort named <tt>s2</tt>.  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 <tt>value()</tt>.
   */
  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
   * <tt>decode(BitCode)</tt> 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 (<tt>NOT</tt>) and two binary (<tt>AND</tt>, <tt>NOT</tt>). The
   * <tt>DIS</tt> operation compiles using <tt>OR</tt>s, and the
   * <tt>BNT</tt> using <tt>AND</tt> and <tt>NOT</tt>.
   *
   * <p>
   *
   * There must be special care taken for compiling (and evaluating an
   * expression containing) a <tt>ConstantSortExpression</tt>. Indeed, a
   * constant sort expression is in fact a pair of objects consisting of a
   * built-in sort and a value.
   *
   * <p>
   *
   * Regarding evaluation, there are several possible cases depending on
   * whether the expression to evaluate is as described below.
   *
   * <ul>
   *
   * <li>A constant sort expression&mdash;it is evaluated as its sort, keeping
   * its value associated.</li>
   *
   * <li>A sort conjunction, one of whose argument is a constant&mdash;both
   * sorts are conjoined. Since the sort of a constant is only compatible
   * with itself, there are three possibilities:
   *
   *	<ul>
   *
   *	<li>if the two sorts are different, then the result is bottom;
   *	otherwise,</li>
   *
   *	<li>if both arguments are constants with different values, then the
   *	result is bottom; otherwise,</li>
   *
   *	<li> the result is the constant (its sort with its associated
   *	value).</li>
   *
   *	</ul>
   * 
   * </ul>
   */
  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 <tt>_exprStack</tt>
   * consisting of a postfix form of bit codes and Boolean operators
   * using the evaluation stack <tt>_evalStack</tt>.
   */
  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();
  }

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