0001: /**************************************************************************/
0002: /* B O S S A */
0003: /* A simple imperative object-oriented research language */
0004: /* (c) Daniel Bonniot 1999 */
0005: /* */
0006: /* This program is free software; you can redistribute it and/or modify */
0007: /* it under the terms of the GNU General Public License as published by */
0008: /* the Free Software Foundation; either version 2 of the License, or */
0009: /* (at your option) any later version. */
0010: /* */
0011: /**************************************************************************/package mlsub.typing.lowlevel;
0012:
0013: import java.util.*;
0014:
0015: /**
0016: * Public interface to the lowlevel constraint implication checker.
0017: *
0018: * All accesses are done through this Engine.
0019: *
0020: * @author bonniot
0021: */
0022: public abstract class Engine {
0023: static {
0024: LowlevelUnsatisfiable.refinedReports = false;
0025: }
0026:
0027: /**
0028: * Enters a new typing context.
0029: * If an enter() completed successfully,
0030: * a matching leave() MUST be issued some time later by the caller.
0031: */
0032: public static void enter(boolean tentative) {
0033: if (dbg)
0034: Debug.println("Enter");
0035: floating.mark();
0036: soft.mark();
0037: formerFree.mark();
0038:
0039: // Once we are in existential mode, we don't mark/backtrack.
0040: if (!tentative && existentialLevel > 0)
0041: existentialLevel++;
0042: else {
0043: frozenLeqs.mark();
0044:
0045: for (Iterator i = constraints.iterator(); i.hasNext();) {
0046: Engine.Constraint k = (Engine.Constraint) i.next();
0047: k.mark();
0048: }
0049: }
0050: }
0051:
0052: /**
0053: * Rigidify the current constraint.
0054: * This means that no further assumptions will be made on it.
0055: *
0056: * @exception Unsatisfiable if the current context was not well kinded.
0057: */
0058: public static void implies() throws Unsatisfiable {
0059: assertFrozens();
0060:
0061: if (dbg)
0062: Debug.println("Implies");
0063:
0064: for (Iterator i = constraints.iterator(); i.hasNext();) {
0065: Engine.Constraint k = (Engine.Constraint) i.next();
0066: k.satisfy();
0067: k.rigidify();
0068: }
0069: }
0070:
0071: /**
0072: Used in Polytype.simplify().
0073: */
0074: public static void satisfy() throws Unsatisfiable {
0075: assertFrozens();
0076:
0077: for (Iterator i = constraints.iterator(); i.hasNext();) {
0078: Engine.Constraint k = (Engine.Constraint) i.next();
0079: k.satisfy();
0080: }
0081: }
0082:
0083: /**
0084: * Returns to the state we had before the last 'enter'.
0085: *
0086: * @exception Unsatisfiable if the constraint was not satisfiable.
0087: */
0088: public static void leave(boolean tentative, boolean commit)
0089: throws Unsatisfiable {
0090: // 'tentative' is only meaningful when in existential mode
0091: tentative &= existentialLevel > 0;
0092: // We only 'commit' in tentative mode
0093: commit &= tentative;
0094:
0095: boolean ok = false;
0096: try {
0097: assertFrozens();
0098:
0099: if (dbg)
0100: Debug.println("Leave");
0101:
0102: for (Iterator i = constraints.iterator(); i.hasNext();) {
0103: Engine.Constraint k = (Engine.Constraint) i.next();
0104: try {
0105: if (dbg)
0106: Debug.println("** Satisfying " + k);
0107:
0108: k.satisfy();
0109: } catch (Unsatisfiable e) {
0110: if (dbg)
0111: Debug.println("** Exception in " + k + e);
0112: throw e;
0113: }
0114: }
0115: ok = true;
0116: } finally {
0117: // Even if commit is true, if an error appeared during leaving
0118: // then we don't want to keep the changes.
0119: backtrack(tentative, ok && commit);
0120: }
0121: }
0122:
0123: public static void backtrack(boolean tentative, boolean commit) {
0124: floating.backtrack();
0125:
0126: if (existentialLevel <= 1 || tentative) {
0127: for (Iterator i = constraints.iterator(); i.hasNext();) {
0128: Engine.Constraint k = (Engine.Constraint) i.next();
0129: k.backtrack(commit);
0130: }
0131:
0132: if (!commit)
0133: frozenLeqs.backtrack();
0134:
0135: /*
0136: if (tentative && !commit)
0137: {
0138: // These type variables used to be free. Since we don't commit,
0139: // we must set them free again!
0140: try{
0141: for (Iterator i = formerFree.iterator(); i.hasNext();)
0142: {
0143: Element e = (Element) i.next();
0144: e.setKind(null);
0145: floating.add(e);
0146: }
0147: }
0148: finally{
0149: formerFree.endOfIteration();
0150: }
0151: }
0152: */
0153: }
0154:
0155: soft.backtrack();
0156: formerFree.backtrack();
0157:
0158: if (!tentative && existentialLevel > 0)
0159: existentialLevel--;
0160: }
0161:
0162: /** Marker used to know how deep we are inside existential mode, so that
0163: we know when to exit from it.
0164: */
0165: private static int existentialLevel = 0;
0166:
0167: public static void startSimplify() {
0168: for (Iterator i = constraints.iterator(); i.hasNext();) {
0169: Engine.Constraint k = (Engine.Constraint) i.next();
0170: k.startSimplify();
0171: }
0172: }
0173:
0174: public static void stopSimplify() {
0175: for (Iterator i = constraints.iterator(); i.hasNext();) {
0176: Engine.Constraint k = (Engine.Constraint) i.next();
0177: k.stopSimplify();
0178: }
0179: }
0180:
0181: /**
0182: * Iterates leq on two collections of Element.
0183: *
0184: * @param e1 the smaller elements
0185: * @param e2 the greater elements
0186: * @exception Unsatisfiable
0187: */
0188: public static void leq(Element[] e1, Element[] e2)
0189: throws Unsatisfiable {
0190: if (e1.length != e2.length)
0191: throw new IllegalArgumentException(
0192: "Bad size in Engine.leq(Element[])");
0193:
0194: for (int i = e1.length - 1; i >= 0; i--)
0195: leq(e1[i], e2[i]);
0196: }
0197:
0198: public static final void leq(Element e1, Element e2)
0199: throws Unsatisfiable {
0200: leq(e1, e2, false);
0201: }
0202:
0203: public static void setTop(Element top) {
0204: Engine.top = top;
0205: }
0206:
0207: private static Element top;
0208:
0209: /**
0210: Asserts that elements have some ordering relation.
0211:
0212: @param e1 a value of type 'Element'
0213: @param e2 a value of type 'Element'
0214: @exception Unsatisfiable if the constraint is not satisfiable.
0215: However this fact may also be discovered later.
0216: */
0217: public static final void leq(Element e1, Element e2, boolean initial)
0218: throws Unsatisfiable {
0219: if (e2 == top)
0220: return;
0221:
0222: Kind k1 = e1.getKind(), k2 = e2.getKind();
0223:
0224: // If e2 is Top, this is trivial.
0225: if (k2 == mlsub.typing.TopMonotype.TopKind.instance)
0226: return;
0227:
0228: if (k1 != null)
0229: if (k2 != null) {
0230: if (k1.equals(k2))
0231: k1.leq(e1, e2, initial);
0232: else {
0233: /* If a non-rigid type variable was previously compared to some
0234: rigid element, it will have its type.
0235: it is still possible for it to be greater than Top
0236: (and therefore equal to Top), provided it is "free upwards",
0237: that is, has no constraint to be smaller than another element.
0238: For this, we just need to forget its previous kind.
0239: */
0240: if (k1 == mlsub.typing.TopMonotype.TopKind.instance
0241: && e2 instanceof mlsub.typing.MonotypeVar
0242: && !isRigid(e2) && isFreeUpwards(e2)) {
0243: ((mlsub.typing.MonotypeVar) e2).resetKind(k1);
0244: return;
0245: }
0246:
0247: if (dbg) {
0248: Debug
0249: .println("Bad kinding discovered by Engine : "
0250: + k1
0251: + " != "
0252: + k2
0253: + "\nfor elements "
0254: + e1
0255: + " and " + e2);
0256: throw new LowlevelUnsatisfiable(
0257: "Bad Kinding for " + e1 + " and " + e2);
0258: } else
0259: throw LowlevelUnsatisfiable.instance;
0260: }
0261: } else {
0262: setKind(e2, k1);
0263: if (e2 instanceof mlsub.typing.MonotypeVar)
0264: ((mlsub.typing.MonotypeVar) e2)
0265: .allowUnknownTypeParameters();
0266: k1.leq(e1, e2, initial);
0267: }
0268: else if (k2 != null) {
0269: setKind(e1, k2);
0270: k2.leq(e1, e2, initial);
0271: } else // ie k1==null and k2==null
0272: {
0273: if (dbg) {
0274: Debug.println("Freezing " + e1 + " <: " + e2 + " ("
0275: + e1.getId() + " <: " + e2.getId() + ")");
0276: if (!(floating.contains(e1)))
0277: throw new InternalError(
0278: "Unknown floating element 1 : " + e1);
0279: if (!(floating.contains(e2)))
0280: throw new InternalError(
0281: "Unknown floating element 2 : " + e2);
0282: }
0283:
0284: frozenLeqs.add(new Leq(e1, e2));
0285: }
0286: }
0287:
0288: /****************************************************************
0289: * New nodes
0290: ****************************************************************/
0291:
0292: /**
0293: * Prepare a new Element to be used.
0294: */
0295: public static void register(Element e) {
0296: if (dbg)
0297: Debug.println("Registering " + e);
0298:
0299: if (e.isExistential())
0300: if (existentialLevel == 0)
0301: existentialLevel = 1;
0302:
0303: if (e.getKind() != null)
0304: e.getKind().register(e);
0305: else {
0306: e.setId(FLOATING);
0307: floating.add(e);
0308: }
0309: }
0310:
0311: public static final int INVALID = -1;
0312: private static final int FLOATING = -3;
0313: private static final int RIGID = -4;
0314:
0315: public static boolean isRigid(Element e) {
0316: if (e.getId() == FLOATING)
0317: return false;
0318:
0319: Kind kind = e.getKind();
0320: if (kind == null)
0321: throw new InternalError("null kind in Engine.isRigid for "
0322: + e);
0323: Engine.Constraint k = getConstraint(kind);
0324: if (k == null)
0325: throw new InternalError(
0326: "null constraint in Engine.isRigid for " + e);
0327: return k.isRigid(e);
0328: }
0329:
0330: static boolean isFreeUpwards(Element e) {
0331: if (e instanceof mlsub.typing.Monotype) {
0332: mlsub.typing.Monotype m = (mlsub.typing.Monotype) e;
0333:
0334: // If there is a constructed equivalent, it is the one that
0335: // has been getting the constraints (in particular its head).
0336: m = m.equivalent();
0337: if (m.head() != null)
0338: e = m.head();
0339: else
0340: e = m;
0341: }
0342:
0343: if (e.getId() == FLOATING)
0344: /// XXX check frozen leqs?
0345: return true;
0346:
0347: if (e.getId() < 0)
0348: return false;
0349:
0350: return getConstraint(e.getKind()).isFreeUpwards(e);
0351: }
0352:
0353: /****************************************************************
0354: * Simplification
0355: ****************************************************************/
0356:
0357: public static void tag(Element e, int variance) {
0358: Kind kind = e.getKind();
0359: if (kind == null)
0360: return;
0361: //throw new InternalError("null kind for "+e);
0362: Engine.Constraint k = getConstraint(kind);
0363: if (k == null)
0364: throw new InternalError("null constraint for " + e);
0365: k.tag(e, variance);
0366: }
0367:
0368: /**
0369: Return the simplified constraint.
0370: Must be surrounded by startSimplify and stopSimplify.
0371: */
0372: public static void simplify(final ArrayList binders,
0373: final ArrayList atoms) {
0374: for (Iterator it = constraints.iterator(); it.hasNext();) {
0375: final Engine.Constraint k = (Engine.Constraint) it.next();
0376: k.simplify();
0377:
0378: final int soft = k.k0.weakMarkedSize();
0379: final int n = k.k0.size();
0380: for (int b = soft; b < n; b++)
0381: binders.add(k.getElement(b));
0382:
0383: // add 'implements' constraints
0384: try {
0385: k.k0.implements Iter(new K0.ImplementsIterator() {
0386: protected void iter(int x, int iid) {
0387: if (x < soft)
0388: return;
0389:
0390: mlsub.typing.TypeConstructor tc = (mlsub.typing.TypeConstructor) k
0391: .getElement(x);
0392: atoms.add(new mlsub.typing.ImplementsCst(tc,
0393: ((mlsub.typing.Variance) tc.variance)
0394: .getInterface(iid)));
0395: }
0396: });
0397:
0398: // add every constraint, except between two rigid varaibles
0399: for (int b = soft; b < n; b++)
0400: for (int i = 0; i < n; i++)
0401: addIfLeq(b, i, k, atoms);
0402: for (int i = 0; i < soft; i++)
0403: for (int b = soft; b < n; b++)
0404: addIfLeq(i, b, k, atoms);
0405: } catch (Unsatisfiable ex) {
0406: }
0407: }
0408: }
0409:
0410: private static void addIfLeq(int i1, int i2, Engine.Constraint k,
0411: List atoms) {
0412: if (k.k0.wasEntered(i1, i2))
0413: atoms
0414: .add(k == variablesConstraint ? (mlsub.typing.AtomicConstraint) new mlsub.typing.MonotypeLeqCst(
0415: (mlsub.typing.MonotypeVar) k.getElement(i1),
0416: (mlsub.typing.MonotypeVar) k.getElement(i2))
0417: : new mlsub.typing.TypeConstructorLeqCst(
0418: (mlsub.typing.TypeConstructor) k
0419: .getElement(i1),
0420: (mlsub.typing.TypeConstructor) k
0421: .getElement(i2)));
0422: }
0423:
0424: /**
0425: Return the element e is equivalent to after simplification.
0426: */
0427: public static Element canonify(Element e) {
0428: Kind kind = e.getKind();
0429: if (kind == null)
0430: return e;
0431: //throw new InternalError("null kind for "+e);
0432: Engine.Constraint k = getConstraint(kind);
0433: if (k == null)
0434: throw new InternalError("null constraint for " + e);
0435:
0436: return k.getElement(e.getId());
0437: }
0438:
0439: /****************************************************************
0440: * Private
0441: ****************************************************************/
0442:
0443: private static class Leq {
0444: Leq(Element e1, Element e2) {
0445: this .e1 = e1;
0446: this .e2 = e2;
0447: }
0448:
0449: public String toString() {
0450: return e1 + " <: " + e2;
0451: }
0452:
0453: Element e1, e2;
0454: }
0455:
0456: private static final BackableList frozenLeqs = new BackableList();
0457:
0458: public static void setKind(Element element, Kind k)
0459: throws Unsatisfiable {
0460: boolean toTop = k == mlsub.typing.TopMonotype.TopKind.instance;
0461:
0462: Stack s = new Stack();
0463:
0464: s.push(element);
0465: while (!s.empty()) {
0466: Element e = (Element) s.pop();
0467:
0468: if (e.getKind() != null)
0469: if (e.getKind() == k)
0470: continue;
0471: else
0472: throw new LowlevelUnsatisfiable("Bad Kinding for "
0473: + e + ":\nhad: " + e.getKind() + "\nnew: "
0474: + k);
0475:
0476: if (e.isExistential())
0477: formerFree.add(e);
0478:
0479: // assert e.getKind()==null
0480: k.register(e);
0481: e.setKind(k);
0482:
0483: floating.remove(e);
0484: if (e.getId() == FLOATING)
0485: soft.add(e);
0486:
0487: // Propagates the kind to all comparable elements
0488: try {
0489: for (Iterator i = frozenLeqs.iterator(); i.hasNext();) {
0490: Leq leq = (Leq) i.next();
0491: if (leq.e1 == e)
0492: if (leq.e2.getKind() == null) {
0493: s.push(leq.e2);
0494: continue;
0495: } else {
0496: // General case later
0497: }
0498: else if (leq.e2 == e)
0499: // If e is Top, e1 <: e is trivial and can be discarded.
0500: if (toTop) {
0501: i.remove();
0502: continue;
0503: } else if (leq.e1.getKind() == null) {
0504: s.push(leq.e1);
0505: continue;
0506: } else {
0507: // General case later
0508: }
0509: else
0510: continue;
0511:
0512: // General case, add leq.e1 <: leq.e2
0513: if (leq.e1.getKind() != leq.e2.getKind())
0514: throw new InternalError(
0515: "Bad kinding in Engine.setKind");
0516:
0517: if (leq.e1 instanceof mlsub.typing.Monotype
0518: && leq.e2 instanceof mlsub.typing.Monotype) {
0519: mlsub.typing.Monotype e1 = (mlsub.typing.Monotype) leq.e1;
0520: mlsub.typing.Monotype e2 = (mlsub.typing.Monotype) leq.e2;
0521:
0522: if (e1.isUnknown())
0523: e2.setUnknown(false, true);
0524: else if (e2.isUnknown())
0525: e1.setUnknown(true, false);
0526: }
0527:
0528: i.remove();
0529: k.leq(leq.e1, leq.e2, initialContext);
0530: }
0531: } finally {
0532: frozenLeqs.endOfIteration();
0533: }
0534: }
0535: }
0536:
0537: /**
0538: * Doesn't check kinding.
0539: * Used in Typing.enumerate
0540: */
0541: public static void forceKind(Element element, Kind k)
0542: throws Unsatisfiable {
0543: Stack s = new Stack();
0544:
0545: s.push(element);
0546: while (!s.empty()) {
0547: Element e = (Element) s.pop();
0548:
0549: e.setKind(k);
0550: k.register(e);
0551:
0552: floating.remove(e);
0553:
0554: // Propagates the kind to all comparable elements
0555: try {
0556: for (Iterator i = frozenLeqs.iterator(); i.hasNext();) {
0557: Leq leq = (Leq) i.next();
0558: if (leq.e1 == e)
0559: if (leq.e2.getKind() == null)
0560: s.push(leq.e2);
0561: else {
0562: i.remove();
0563: k.leq(leq.e1, leq.e2);
0564: }
0565: else if (leq.e2 == e)
0566: if (leq.e1.getKind() == null)
0567: s.push(leq.e1);
0568: else {
0569: i.remove();
0570: k.leq(leq.e1, leq.e2);
0571: }
0572: }
0573: } finally {
0574: frozenLeqs.endOfIteration();
0575: }
0576: }
0577: }
0578:
0579: /**
0580: Enter all the 'floating' elements into the variablesConstraint
0581: and add their frozen constraints.
0582: */
0583: private static void assertFrozens() throws Unsatisfiable {
0584: try {
0585: for (Iterator i = soft.iterator(); i.hasNext();) {
0586: Element e = (Element) i.next();
0587: e.setId(RIGID);
0588: }
0589: } finally {
0590: soft.endOfIteration();
0591: }
0592: soft.clear();
0593:
0594: boolean more;
0595: do {
0596: more = false;
0597: try {
0598: for (Iterator i = frozenLeqs.iterator(); i.hasNext();) {
0599: Leq leq = (Leq) i.next();
0600: Element e1 = leq.e1;
0601: Element e2 = leq.e2;
0602:
0603: // If at least one of the two is existential, then we must
0604: // keep both frozen.
0605: if ((e1.isExistential() && !e2.isExistential())
0606: || (e2.isExistential() && !e1
0607: .isExistential())) {
0608: // Since we are marking an element as existential, we should
0609: // do one more pass to make sure all related elements are
0610: // marked
0611: more = true;
0612:
0613: if (e1.isExistential())
0614: ((mlsub.typing.MonotypeVar) e2)
0615: .setExistential();
0616: else if (e2.isExistential())
0617: ((mlsub.typing.MonotypeVar) e1)
0618: .setExistential();
0619: }
0620: }
0621: } finally {
0622: frozenLeqs.endOfIteration();
0623: }
0624: } while (more);
0625:
0626: try {
0627: for (Iterator i = floating.iterator(); i.hasNext();) {
0628: Element e = (Element) i.next();
0629:
0630: // useful for nullness head on monotype vars
0631: // we don't set existential in stone either, because they
0632: // might be put into a kind later on.
0633: if (e.getKind() != null || e.isExistential())
0634: continue;
0635:
0636: if (dbg)
0637: Debug.println("Registering variable " + e);
0638:
0639: e.setKind(variablesConstraint);
0640: variablesConstraint.register(e);
0641: i.remove();
0642: }
0643: } finally {
0644: floating.endOfIteration();
0645: }
0646:
0647: try {
0648: for (Iterator i = frozenLeqs.iterator(); i.hasNext();) {
0649: Leq leq = (Leq) i.next();
0650: Element e1 = leq.e1;
0651: Element e2 = leq.e2;
0652:
0653: // By the above code, if e2 is existential, e1 was marked as
0654: // existential too, so we don't need to test e2.
0655: if (e1.isExistential())
0656: continue;
0657:
0658: variablesConstraint.leq(leq.e1, leq.e2, initialContext);
0659: i.remove();
0660: }
0661: } finally {
0662: frozenLeqs.endOfIteration();
0663: }
0664: }
0665:
0666: /** Maps a Kind to its lowlevel constraint */
0667: private static HashMap kindsMap;
0668:
0669: public static Engine.Constraint getConstraint(Kind kind) {
0670: if (kind instanceof Engine.Constraint)
0671: return (Engine.Constraint) kind;
0672:
0673: Engine.Constraint res = (Engine.Constraint) kindsMap.get(kind);
0674: if (res != null)
0675: return res;
0676:
0677: if (dbg)
0678: Debug.println("Creating new Lowlevel constraint for "
0679: + kind);
0680:
0681: res = new Engine.Constraint("kind " + kind.toString());
0682: res.associatedKind = kind;
0683: // if the constraint is created after the initial context has been defined,
0684: // we have to change the state of the constraint here
0685: if (!initialContext)
0686: try {
0687: if (dbg)
0688: Debug
0689: .println("createInitialContext() and mark() called for new constraint");
0690: res.createInitialContext();
0691: res.mark();
0692: } catch (Unsatisfiable e) {
0693: throw new InternalError(
0694: "This shouldn't happen, Engine.Constraint is empty here !");
0695: }
0696: constraints.add(res);
0697: kindsMap.put(kind, res);
0698: return res;
0699: }
0700:
0701: /** The elements that have not yet been added to a Kind */
0702: private static final BackableList floating = new BackableList();
0703:
0704: /** The elements that have not yet been rigidified. */
0705: private static final BackableList soft = new BackableList();
0706:
0707: /** The elements that have been put into a kind since the last mark. */
0708: private static final BackableList formerFree = new BackableList();
0709:
0710: /** The constraint of monotype variables */
0711: public static Engine.Constraint variablesConstraint;
0712:
0713: /** The list of Constraints */
0714: private static ArrayList constraints;
0715:
0716: public static Iterator listConstraints() {
0717: return constraints.iterator();
0718: }
0719:
0720: /** Return to the initial virgin state. */
0721: public static void reset() {
0722: kindsMap = new HashMap();
0723: variablesConstraint = new Engine.Constraint("type variables",
0724: true);
0725: //kindsMap.put(variablesConstraint,variablesConstraint);
0726:
0727: constraints = new ArrayList(10);
0728: constraints.add(variablesConstraint);
0729:
0730: initialContext = true;
0731: }
0732:
0733: public static void createInitialContext() throws Unsatisfiable {
0734: for (Iterator i = constraints.iterator(); i.hasNext();) {
0735: Engine.Constraint k = (Engine.Constraint) i.next();
0736: k.createInitialContext();
0737: }
0738: initialContext = false;
0739: }
0740:
0741: public static void releaseInitialContext() {
0742: for (Iterator i = constraints.iterator(); i.hasNext();) {
0743: Engine.Constraint k = (Engine.Constraint) i.next();
0744: k.releaseInitialContext();
0745: }
0746: initialContext = true;
0747: }
0748:
0749: private static boolean initialContext = true;
0750:
0751: public static boolean isInRigidContext() {
0752: return !initialContext;
0753: }
0754:
0755: /****************************************************************
0756: * Engine.Constraint
0757: ****************************************************************/
0758:
0759: final public static class Constraint implements Kind {
0760: Constraint(String name) {
0761: this .name = name;
0762: }
0763:
0764: private String name;
0765:
0766: Constraint(String name, boolean variables) {
0767: this (name);
0768: this .variables = variables;
0769: }
0770:
0771: private boolean variables = false;
0772:
0773: // this is not too logical to have this...
0774: public mlsub.typing.Monotype freshMonotype(boolean existential) {
0775: return null;
0776: }
0777:
0778: /**
0779: * Returns true iff there is a concrete #class in this constraint.
0780: */
0781: public boolean hasConstants() {
0782: return !variables;
0783: }
0784:
0785: final K0 k0 = new K0(K0.BACKTRACK_UNLIMITED, new Callbacks());
0786:
0787: private Vector elements = new Vector(10); // ArrayList would be better, but has no setSize method
0788: private BitVector concreteElements = new BitVector();
0789:
0790: public final void register(Element e) {
0791: int id = k0.extend();
0792: e.setId(id);
0793: if (id >= elements.size())
0794: elements.setSize(id + 1);
0795: elements.set(id, e);
0796:
0797: if (e.isConcrete())
0798: concreteElements.set(id);
0799:
0800: if (dbg)
0801: Debug.println(e + " has id " + e.getId());
0802: }
0803:
0804: // public for Typing.enumerate...
0805: public Element getElement(int index) {
0806: return (Element) elements.get(index);
0807: }
0808:
0809: void tag(Element e, int variance) {
0810: k0.tag(e.getId(), variance);
0811: }
0812:
0813: class Callbacks extends K0.Callbacks {
0814: protected void indexMerged(int src, int dest) {
0815: if (dbg)
0816: Debug.println("Merged " + indexToString(src)
0817: + " into " + indexToString(dest));
0818: getElement(src).setId(dest);
0819: }
0820:
0821: protected void indexMoved(int src, int dest) {
0822: if (dbg)
0823: Debug.println("Changed index of "
0824: + indexToString(src));
0825:
0826: // indexToString(dest) is meaningless
0827:
0828: Element movedElement = getElement(src);
0829: movedElement.setId(dest);
0830: elements.set(dest, movedElement);
0831: }
0832:
0833: protected void indexDiscarded(int index) {
0834: if (dbg)
0835: Debug.println("Discarded " + indexToString(index));
0836:
0837: getElement(index).setId(-2);
0838: elements.set(index, null); // enable garbage collection
0839: }
0840:
0841: /*
0842: * Pretty printing
0843: */
0844: protected String getName() {
0845: return name;
0846: }
0847:
0848: protected String indexToString(int x) {
0849: if (x == BitVector.UNDEFINED_INDEX)
0850: return "[NONE]";
0851: else if (x == -1)
0852: return "[BOTTOM]";
0853: else
0854: return String.valueOf(getElement(x)) + "[" + x
0855: + "]";
0856: }
0857:
0858: protected String interfaceToString(int iid) {
0859: return ""
0860: + ((mlsub.typing.Variance) associatedKind)
0861: .getInterface(iid);
0862: }
0863: }
0864:
0865: public Kind associatedKind;
0866:
0867: /* the kind of the elements of this constraint
0868: * This is used in TypeConstructor.setKind
0869: */
0870:
0871: public String toString() {
0872: return "Constraint " + name + " for " + associatedKind
0873: + ":\n" + k0.toString();
0874: }
0875:
0876: public final boolean isValid(Element e) {
0877: int id = e.getId();
0878: return id >= 0 && id < k0.size();
0879: }
0880:
0881: public final void leq(Element e1, Element e2)
0882: throws Unsatisfiable {
0883: leq(e1, e2, false);
0884: }
0885:
0886: public final void leq(Element e1, Element e2, boolean initial)
0887: throws Unsatisfiable {
0888: if (dbg) {
0889: Debug.println(e1 + " <: " + e2 + " (" + e1.getId()
0890: + " <: " + e2.getId() + ")");
0891: if (e1.getId() < 0 || e1.getId() >= k0.size()) {
0892: Debug.println(e1 + " has invalid index");
0893: bossa.util.Internal.printStackTrace();
0894: }
0895:
0896: if (e2.getId() < 0 || e2.getId() >= k0.size()) {
0897: Debug.println(e2 + " has invalid index");
0898: bossa.util.Internal.printStackTrace();
0899: }
0900: }
0901:
0902: if (initial)
0903: k0.initialLeq(e1.getId(), e2.getId());
0904: else
0905: k0.leq(e1.getId(), e2.getId());
0906: }
0907:
0908: public final void assertMinimal(Element e) {
0909: if (dbg)
0910: Debug.println("Minimal: " + e);
0911:
0912: k0.minimal(e.getId());
0913: }
0914:
0915: public final boolean isMinimal(Element e) {
0916: return k0.isMinimal(e.getId());
0917: }
0918:
0919: public final void discard(Element e) {
0920: concreteElements.clear(e.getId());
0921: k0.discard(e.getId());
0922: }
0923:
0924: public Element lowestInstance(Element e) {
0925: //FIXME: Suboptimal: doesn't always return an instance when there is one.
0926: // Maybe this should be done by enumeration of the solutions
0927: // of the constraint.
0928:
0929: final int id = e.getId();
0930: int res = -1;
0931:
0932: for (int elem = 0; elem < k0.initialContextSize(); elem++)
0933: // We use wasEntered, since id is assumed not to be rigid
0934: // i and res are rigid, so we use isLeq.
0935: // an alternative would be to (require) rigidify
0936: // (at least a closure of leq relation + other axioms)
0937: // and use isLeq.
0938: // Could be more precise in presence of interfaces.
0939: if (k0.wasEntered(id, elem)
0940: && (res == -1 || k0.isLeq(elem, res)))
0941: res = elem;
0942:
0943: if (res == -1)
0944: for (int elem = 0; elem < k0.initialContextSize(); elem++)
0945: if (k0.wasEntered(elem, id)
0946: && (res == -1 || k0.isLeq(res, elem)))
0947: res = elem;
0948:
0949: if (res != -1)
0950: // Check we really found an instance.
0951: {
0952: final boolean[] ok = { true };
0953: final int candidate = res;
0954:
0955: try {
0956: k0.ineqIter(new K0.IneqIterator() {
0957: protected void iter(int x1, int x2) {
0958: if (x1 == id)
0959: ok[0] &= k0.isLeq(candidate, x2);
0960: else if (x2 == id)
0961: ok[0] &= k0.isLeq(x1, candidate);
0962: }
0963: });
0964: } catch (Unsatisfiable ex) {
0965: throw new Error("assert false");
0966: }
0967:
0968: if (!ok[0])
0969: res = -1;
0970: }
0971:
0972: if (res == -1)
0973: return null;
0974: else
0975: return getElement(res);
0976: }
0977:
0978: boolean isFreeUpwards(Element e) {
0979: final int id = e.getId();
0980:
0981: // If there is any i with a id <: i constraint, return false
0982: // TODO: handle cases when id <: i where i is non rigid, but not free
0983: // upwards
0984: for (int i = 0; i < k0.firstNonRigid(); i++)
0985: if (i != id && k0.wasEntered(id, i))
0986: return false;
0987:
0988: return true;
0989: }
0990:
0991: void mark() {
0992: k0.mark();
0993: }
0994:
0995: void backtrack(boolean ignore) {
0996: k0.backtrack(ignore);
0997: }
0998:
0999: void startSimplify() {
1000: k0.startSimplify();
1001: }
1002:
1003: void simplify() {
1004: k0.simplify();
1005: }
1006:
1007: void stopSimplify() {
1008: k0.stopSimplify();
1009: }
1010:
1011: void satisfy() throws Unsatisfiable {
1012: k0.satisfy();
1013: }
1014:
1015: void rigidify() {
1016: k0.rigidify();
1017: }
1018:
1019: boolean isRigid(Element e) {
1020: return k0.isRigid(e.getId());
1021: }
1022:
1023: void createInitialContext() throws Unsatisfiable {
1024: k0.createInitialContext();
1025: }
1026:
1027: void releaseInitialContext() {
1028: k0.releaseInitialContext();
1029: }
1030:
1031: public int newInterface() {
1032: return k0.newInterface();
1033: }
1034:
1035: public void subInterface(int i1, int i2) {
1036: k0.subInterface(i1, i2);
1037: }
1038:
1039: public void initialImplements(int x, int iid) {
1040: k0.initialImplements(x, iid);
1041: }
1042:
1043: public void initialAbstracts(int x, int iid) {
1044: k0.initialAbstracts(x, iid);
1045: }
1046:
1047: public void indexImplements(int x, int iid)
1048: throws Unsatisfiable {
1049: k0.indexImplements(x, iid);
1050: }
1051:
1052: public void enumerate(BitVector observers,
1053: LowlevelSolutionHandler handler) {
1054: k0.enumerate(observers, handler);
1055: }
1056:
1057: public void reduceDomainToConcrete(Element e)
1058: throws Unsatisfiable {
1059: k0.reduceDomain(e.getId(), false, concreteElements);
1060: }
1061:
1062: /**
1063: * Assume e1 and e2 are rigid
1064: **/
1065: public boolean isLeq(Element e1, Element e2) {
1066: return k0.isLeq(e1.getId(), e2.getId());
1067: }
1068: }
1069:
1070: public static boolean dbg = bossa.util.Debug.engine;
1071: }
|