// 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 /** * @version Last modified on Fri Aug 23 12:28:19 2019 by hak * @author Hassan Aït-Kaci * @copyright © by the author */ 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. * * @param code a BitCode object * @return 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 ({t1 ; ... ; tn}). */ 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. * *

*/ 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(); } /* ************************************************************************ */ }