|
Context.java
|
// FILE. . . . . /home/hak/hlt/src/hlt/osfv1/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 an
sort ordering context for accessing, compiling, and evaluating OSF forms.
|
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 ORs, 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. Such a sort expression can only be conjoined—no union nor negation can be applied to it. Regarding evaluation of a constant sort or conjunction with a constant sort, there are several possible cases depending on whether the expression to evaluate is:
|
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 Thu Sep 19 11:57:09 CEST 2013 from file Context.java
by the hlt.language.tools.Hilite Java tool written by Hassan Aït-Kaci