001: /**************************************************************************/
002: /* N I C E */
003: /* A high-level object-oriented research language */
004: /* (c) Daniel Bonniot 2002 */
005: /* */
006: /* This program is free software; you can redistribute it and/or modify */
007: /* it under the terms of the GNU General Public License as published by */
008: /* the Free Software Foundation; either version 2 of the License, or */
009: /* (at your option) any later version. */
010: /* */
011: /**************************************************************************/package mlsub.typing;
012:
013: import java.util.*;
014:
015: import mlsub.typing.lowlevel.Engine;
016: import mlsub.typing.lowlevel.Element;
017: import mlsub.typing.lowlevel.Unsatisfiable;
018:
019: /**
020: Static class for comparing types
021:
022: @version $Date: 2004/06/29 18:38:18 $
023: @author Daniel Bonniot
024: */
025: public final class Typing {
026: /****************************************************************
027: * Typing contexts
028: ****************************************************************/
029:
030: /**
031: Enters a new typing context.
032:
033: If an enter() completed successfully,
034: a matching leave() MUST be issued some time later by the caller.
035: */
036: public static int enter() {
037: return enter(false);
038: }
039:
040: /**
041: @param tentative when true, we will decide upon leaving if we want to
042: commit the changes made to existential type variables or not.
043: */
044: public static int enter(boolean tentative) {
045: if (dbg)
046: Debug.println("ENTER " + level);
047:
048: Engine.enter(tentative);
049: return level++;
050: }
051:
052: // used to verify that enter and leaves match
053: static int level = 0;
054:
055: /**
056: Enters a new typing context
057:
058: @param message A debug message to know where we are
059: */
060: public static int enter(String message) {
061: if (message != null && dbg)
062: Debug.println("## Typechecking " + message);
063: return enter();
064: }
065:
066: static public void introduce(Element e) {
067: if (dbg)
068: Debug.println("Typing introduced " + e);
069:
070: // a monotype var introduced earlier must be given a new null kind
071: // the cleaner way would be to reset it to null when we leave this level
072: // but it would be a pain, and the result is the same
073: if (e instanceof MonotypeVar)
074: ((MonotypeVar) e).reset();
075:
076: Engine.register(e);
077: }
078:
079: static public void introduce(Element[] elements) {
080: if (elements == null)
081: return;
082:
083: for (int i = 0; i < elements.length; i++)
084: if (elements[i] != null)
085: introduce(elements[i]);
086: }
087:
088: // TODO: fix this?
089: // pb with Interface being a type symbol
090: static public void introduceTypeSymbols(TypeSymbol[] elements) {
091: for (int i = 0; i < elements.length; i++)
092: introduce((Element) elements[i]);
093:
094: }
095:
096: /**
097: Leaves the last typing context.
098: */
099: public static int leave() throws TypingEx {
100: return leave(false, false);
101: }
102:
103: /**
104: @param tentative must match the parameter used when entering
105: @param commit if tentative is true, then commit selects whether we
106: want to commit the changes made to existential type variables or not.
107: */
108: public static int leave(boolean tentative, boolean commit)
109: throws TypingEx {
110: if (dbg)
111: Debug.println("LEAVE " + (level - 1));
112:
113: try {
114: level--;
115: Engine.leave(tentative, commit);
116: } catch (Unsatisfiable e) {
117: if (dbg)
118: e.printStackTrace();
119: throw new TypingEx("Unsatisfiable 1:" + e.getMessage());
120: }
121: return level;
122: }
123:
124: public static void implies() throws TypingEx {
125: if (dbg)
126: Debug.println("IMPLIES");
127: try {
128: Engine.implies();
129: } catch (Unsatisfiable e) {
130: throw new TypingEx("Not satisfiable " + e.getMessage());
131: }
132: }
133:
134: /** Called before each independant compilation.
135: This must clear any side-effect of previous compilations.
136: */
137: public static void startNewCompilation() {
138: Engine.reset();
139: FunTypeKind.reset();
140: }
141:
142: public static void createInitialContext() {
143: try {
144: Engine.createInitialContext();
145: } catch (Unsatisfiable e) {
146: throw new InternalError(
147: "Initial context is not satisfiable: " + e);
148: }
149: }
150:
151: public static void releaseInitialContext() {
152: Engine.releaseInitialContext();
153: }
154:
155: public static boolean isInRigidContext() {
156: return Engine.isInRigidContext();
157: }
158:
159: /****************************************************************
160: * Assertions
161: ****************************************************************/
162:
163: public static void leq(Collection c1, Collection c2)
164: throws TypingEx {
165: if (c1.size() != c2.size())
166: throw new InternalError("Unequal sizes in leq");
167:
168: Iterator i1 = c1.iterator();
169: Iterator i2 = c2.iterator();
170:
171: while (i1.hasNext()) {
172: leq((Polytype) i1.next(), (Polytype) i2.next());
173: }
174: }
175:
176: public static void initialLeq(TypeConstructor t,
177: TypeConstructor[] ts) throws TypingEx {
178: for (int i = 0; i < ts.length; i++)
179: initialLeq(t, ts[i]);
180: }
181:
182: public static void leq(TypeConstructor t, Collection c)
183: throws TypingEx {
184: Iterator i = c.iterator();
185:
186: while (i.hasNext())
187: leq(t, (TypeConstructor) i.next());
188: }
189:
190: /** Test that t is leq that m's head */
191: public static void leq(TypeConstructor t, Monotype m)
192: throws TypingEx {
193: if (t == null)
194: return;
195:
196: if (isTop(m))
197: // Trivially true.
198: return;
199:
200: AtomicKind v = t.variance;
201: if (v == null)
202: throw new InternalError("Don't know how to handle this");
203:
204: try {
205: Engine.setKind(m, v);
206: } catch (Unsatisfiable e) {
207: if (dbg)
208: throw new TypingEx(t + " < " + m + "'s head :" + e);
209: else
210: throw new TypingEx("Debugging off");
211: }
212: leq(t, ((MonotypeConstructor) m.equivalent()).getTC());
213: }
214:
215: public static void leq(TypeConstructor[] ts, Monotype[] ms)
216: throws TypingEx {
217: for (int i = 0; i < ts.length; i++)
218: leq(ts[i], ms[i]);
219: }
220:
221: /** Test that t is geq that m's head */
222: public static void leq(Monotype m, TypeConstructor t)
223: throws TypingEx {
224: AtomicKind v = t.variance;
225: if (v == null)
226: throw new InternalError("Don't know how to handle this");
227:
228: try {
229: Engine.setKind(m, v);
230: } catch (Unsatisfiable e) {
231: throw new TypingEx(t + " > " + m + "'s head");
232: }
233: leq(((MonotypeConstructor) m.equivalent()).getTC(), t);
234: }
235:
236: /** Assert that the vars are matching the base head constructors. */
237: public static void leqHead(Monotype[] vars, Monotype[] base)
238: throws TypingEx {
239: for (int i = 0; i < vars.length; i++) {
240: Monotype var = vars[i];
241: nice.tools.typing.Types.setMarkedKind(var);
242: nice.tools.typing.Types.setMarkedKind(base[i]);
243:
244: TypeConstructor baseMarker = base[i].head();
245: if (baseMarker != null)
246: leq(var.head(), baseMarker);
247:
248: TypeConstructor tag = nice.tools.typing.Types
249: .constructor(base[i]);
250: if (tag != null)
251: leq(nice.tools.typing.Types.equivalent(vars[i]), tag);
252: }
253: }
254:
255: /****************************************************************
256: * Testing Polytype <= Polytype
257: ****************************************************************/
258:
259: public static void leq(Polytype t1, Polytype t2) throws TypingEx {
260:
261: if (!(Constraint.hasBinders(t1.getConstraint()) || Constraint
262: .hasBinders(t2.getConstraint()))) {
263: leq(t1.getMonotype(), t2.getMonotype());
264: return;
265: }
266:
267: if (dbg)
268: Debug.println("Polytype leq: " + t1 + " <: " + t2);
269:
270: // The additions we are going to make should be discarded at the end,
271: // so as not to influence existential type variables in the context.
272: int l = enter(true);
273:
274: try {
275: if (!t2.isMonomorphic()) {
276: Constraint.enter(t2.getConstraint());
277:
278: implies();
279: }
280:
281: Constraint.enter(t1.getConstraint());
282: leq(t1.getMonotype(), t2.getMonotype());
283: } finally {
284: if (leave(true, false) != l)
285: throw new InternalError("Unmatched enters and leaves");
286: }
287: }
288:
289: /** Particular case. */
290: public static void leq(Polytype t1, Monotype m2) throws TypingEx {
291: if (!(Constraint.hasBinders(t1.getConstraint()))) {
292: leq(t1.getMonotype(), m2);
293: return;
294: }
295:
296: if (dbg)
297: Debug.println("Polytype leq: " + t1 + " <: " + m2);
298:
299: int l = enter();
300:
301: try {
302: Constraint.enter(t1.getConstraint());
303: leq(t1.getMonotype(), m2);
304: } finally {
305: if (leave() != l)
306: throw new InternalError("Unmatched enters and leaves");
307: }
308: }
309:
310: /****************************************************************
311: * Monotypes
312: ****************************************************************/
313:
314: public static void leq(Monotype m1, Monotype m2) throws TypingEx {
315: if (dbg)
316: Debug.println("Monotype leq: " + m1 + " <: " + m2);
317:
318: try {
319: Engine.leq(m1, m2);
320: } catch (Unsatisfiable e) {
321: if (dbg)
322: e.printStackTrace();
323: throw new MonotypeLeqEx(m1, m2, e);
324: }
325: }
326:
327: public static void eq(Monotype m1, Monotype m2) throws TypingEx {
328: leq(m1, m2);
329: leq(m2, m1);
330: }
331:
332: public static void leq(Monotype[] ms1, Monotype[] ms2)
333: throws TypingEx {
334: for (int i = 0; i < ms1.length; i++)
335: leq(ms1[i], ms2[i]);
336: }
337:
338: /** @param dispatchable when true, we require that non dispatchable types be
339: equal, not mere subtypes.
340: */
341: public static void leq(Monotype[] ms1, Monotype[] ms2,
342: boolean dispatchable) throws TypingEx {
343: if (!dispatchable)
344: for (int i = 0; i < ms1.length; i++)
345: leq(ms1[i], ms2[i]);
346: else
347: for (int i = 0; i < ms1.length; i++) {
348: Monotype m1 = ms1[i];
349: Monotype m2 = ms2[i];
350: leq(m1, m2);
351: if (!nice.tools.typing.Types.isDispatchable(m2))
352: leq(m2, m1);
353: }
354: }
355:
356: /****************************************************************
357: * Type constructors
358: ****************************************************************/
359:
360: public static void initialLeq(TypeConstructor t1, TypeConstructor t2)
361: throws TypingEx {
362: if (dbg)
363: Debug.println("Initial leq: " + t1 + " < " + t2);
364:
365: try {
366: Engine.leq(t1, t2, true);
367: } catch (Unsatisfiable e) {
368: throw new KindingEx(t1, t2);
369: }
370: }
371:
372: public static void leq(TypeConstructor t1, TypeConstructor t2)
373: throws TypingEx {
374: if (dbg)
375: Debug.println("TC leq: " + t1 + " < " + t2);
376:
377: try {
378: Engine.leq(t1, t2, false);
379: } catch (Unsatisfiable e) {
380: throw new TypingEx("Not satisfiable 4:" + e.getMessage());
381: }
382: }
383:
384: public static boolean testLeq(TypeConstructor t1, TypeConstructor t2) {
385: if (t1.getKind() == null || t2.getKind() == null)
386: throw new InternalError("Null kind for " + t1 + " or " + t2);
387:
388: try {
389: Engine.leq(t1, t2, false);
390: return true;
391: } catch (Unsatisfiable e) {
392: return false;
393: }
394: }
395:
396: /****************************************************************
397: * Domains
398: ****************************************************************/
399:
400: /** Test if d1 is a subdomain of d2. */
401: public static void leq(Domain d1, Domain d2) throws TypingEx {
402: leq(d1, d2, false);
403: }
404:
405: /** Test if d1 is a subdomain of d2.
406: @param dispatchable when true, we require that non dispatchable types be
407: equal, not mere subtypes.
408: */
409: public static void leq(Domain d1, Domain d2, boolean dispatchable)
410: throws TypingEx {
411: if (dbg)
412: Debug.println(d1 + " leq " + d2);
413:
414: if (d1 == Domain.bot)
415: return;
416:
417: if (!(Constraint.hasBinders(d1.getConstraint()) || Constraint
418: .hasBinders(d2.getConstraint()))) {
419: leq(d1.getMonotypes(), d2.getMonotypes(), dispatchable);
420: return;
421: }
422:
423: // The additions we are going to make should be discarded at the end,
424: // so as not to influence existential type variables in the context.
425: enter(true);
426: try {
427: Constraint.enter(d1.getConstraint());
428:
429: Typing.implies();
430:
431: Constraint.enter(d2.getConstraint());
432: leq(d1.getMonotypes(), d2.getMonotypes(), dispatchable);
433: } finally {
434: leave(true, false);
435: }
436: }
437:
438: public static boolean smaller(Domain d1, Domain d2) {
439: try {
440: leq(d1, d2);
441: return true;
442: } catch (TypingEx ex) {
443: return false;
444: }
445: }
446:
447: /** @param dispatchable when true, we require that non dispatchable types be
448: equal, not mere subtypes.
449: */
450: public static boolean smaller(Domain d1, Domain d2,
451: boolean dispatchable) {
452: try {
453: leq(d1, d2, dispatchable);
454: return true;
455: } catch (TypingEx ex) {
456: return false;
457: }
458: }
459:
460: /** Test if a polytype is in a domain. */
461: public static void in(Polytype type, Monotype domain)
462: throws TypingEx {
463: if (dbg)
464: Debug.println(type + " in " + domain);
465:
466: Constraint.enter(type.getConstraint());
467: leq(type.getMonotype(), domain);
468: }
469:
470: /**
471: * Checks wether types belong to domains
472: *
473: * @param types a collection of Polytypes
474: * @param domains a collection of domains
475: * @exception TypingEx
476: */
477: public static void in(Polytype[] types, Monotype[] domains)
478: throws TypingEx {
479: int expected = domains.length;
480: int actual = types.length;
481: if (expected != actual)
482: throw new BadSizeEx(expected, actual);
483:
484: for (int i = 0; i < actual; i++)
485: in(types[i], domains[i]);
486: }
487:
488: /****************************************************************
489: * Interfaces assertions
490: ****************************************************************/
491:
492: public static void assertLeq(Interface i, Interface j)
493: throws KindingEx {
494: if (dbg)
495: Debug.println(i + " < " + j);
496: if (!(i.variance.equals(j.variance)))
497: throw new KindingEx(i, j);
498: i.variance.subInterface(i.itf, j.itf);
499: }
500:
501: public static void assertLeq(Interface itf, Interface[] is)
502: throws KindingEx {
503: for (int i = is.length; --i >= 0;)
504: assertLeq(itf, is[i]);
505: }
506:
507: public static void assertImp(TypeConstructor t, Interface i,
508: boolean initial) throws TypingEx {
509: if (dbg)
510: Debug.println(t + " imp " + i);
511:
512: try {
513: Engine.setKind(t, i.variance.getConstraint());
514: } catch (Unsatisfiable e) {
515: throw new KindingEx(t, i);
516: }
517:
518: try {
519: if (initial)
520: ((Variance) t.variance).initialImplements(t.getId(),
521: i.itf);
522: else
523: ((Variance) t.variance).indexImplements(t.getId(),
524: i.itf);
525:
526: TypeConstructor tc = i.associatedTC();
527: if (tc != null)
528: Engine.leq(t, tc, initial);
529: } catch (Unsatisfiable e) {
530: throw new TypingEx(e.getMessage());
531: }
532: }
533:
534: public static void assertAbs(TypeConstructor t, Interface i)
535: throws TypingEx {
536: if (dbg)
537: Debug.println(t + " abs " + i);
538:
539: if (Engine.isRigid(t))
540: throw new InternalError(
541: "Abstraction required on a rigid type constructor : \n"
542: + t + " required to abstract " + i);
543:
544: i.variance.initialAbstracts(t.getId(), i.itf);
545: }
546:
547: public static void assertImp(TypeConstructor t, Interface[] is,
548: boolean initial) throws TypingEx {
549: for (int i = 0; i < is.length; i++)
550: assertImp(t, is[i], initial);
551: }
552:
553: public static void assertAbs(TypeConstructor t, Interface[] is)
554: throws TypingEx {
555: for (int i = 0; i < is.length; i++)
556: assertAbs(t, is[i]);
557: }
558:
559: /****************************************************************
560: * Rigid tests
561: ****************************************************************/
562:
563: public static boolean testRigidLeq(TypeConstructor t1,
564: TypeConstructor t2) {
565: if (t1.getKind() == null || t2.getKind() == null)
566: throw new InternalError("Null kind for " + t1 + " or " + t2);
567:
568: if (t1.getKind() != t2.getKind())
569: return false;
570:
571: return ((Engine.Constraint) t1.getKind()).isLeq(t1, t2);
572: }
573:
574: /**
575: Find an instance of the parameter
576: that can exist at runtime (isConcrete() is true).
577: It's better to return a lower (more precise) one.
578: */
579: public static TypeConstructor lowestInstance(TypeConstructor tc) {
580: Engine.Constraint cst = (Engine.Constraint) tc.getKind();
581:
582: if (!cst.isValid(tc))
583: // we are not in the context for TC anymore
584: // be careful to call lowestRigidSuperTC when the context is appropriate.
585: {
586: System.out
587: .println("Warning: lowestInstance called inapropriately for "
588: + tc);
589: return null;
590: }
591:
592: return (TypeConstructor) cst.lowestInstance(tc);
593: }
594:
595: /****************************************************************
596: * Tools
597: ****************************************************************/
598:
599: static boolean isTop(Monotype m) {
600: return m.getKind() == TopMonotype.TopKind.instance;
601: }
602:
603: public static boolean dbg = bossa.util.Debug.typing;
604: }
|