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.Unsatisfiable;
017: import mlsub.typing.lowlevel.BitVector;
018: import mlsub.typing.lowlevel.Element;
019: import mlsub.typing.lowlevel.Kind;
020:
021: /**
022: Enumeration of the type constructors in a domain.
023:
024: @version $Date: 2005/05/26 15:25:53 $
025: @author Daniel Bonniot
026: */
027:
028: public class Enumeration {
029: /**
030: * Enumerate all the tuples of tags in a Domain
031: *
032: * @return a List of TypeConstructor[]
033: * an element of an array is set to null
034: * if it cannot be matched (e.g. a function type)
035: */
036: /*
037: public static List enumerate(Domain domain)
038: {
039: // XXX try LinkedList
040: List res = new ArrayList();
041:
042: Monotype[] tags = null;
043:
044: if (domain.getMonotype().equivalent() instanceof TupleType)
045: tags = ((TupleType) domain.getMonotype().equivalent()).types;
046:
047: if (tags == null)
048: throw new InternalError("enumerate should be done on a tuple domain");
049:
050: try
051: {
052: int l = Typing.enter();
053:
054: try{
055: Constraint.enter(domain.getConstraint());
056: setFloatingKinds(tags,0,res);
057: }
058: finally{
059: if (Typing.leave() != l)
060: throw new InternalError("Unmatched enter and leaves");
061: }
062: }
063: catch(TypingEx e){
064: // There is no solution
065: return new LinkedList();
066: }
067: catch(Unsatisfiable e){
068: throw new InternalError("This shouldn't happen");
069: }
070:
071: return res;
072: }
073: */
074:
075: /**
076: * Enumerate all the tuples of tags in a Domain
077: *
078: * If all[i] is false, we are not interested in getting all solutions
079: * for position i, only one witness is enough.
080: *
081: * @return a List of TypeConstructor[]
082: * an element of an array is set to null
083: * if it cannot be matched (e.g. a function type)
084: */
085: public static List enumerate(Constraint cst, Element[] tags,
086: boolean[] all) {
087: // XXX try LinkedList
088: List res = new ArrayList();
089:
090: try {
091: int l = Typing.enter();
092:
093: try {
094: Constraint.enter(cst);
095: setFloatingKinds(tags, all, 0, res, true);
096: } finally {
097: if (Typing.leave() != l)
098: throw new InternalError(
099: "Unmatched enter and leaves");
100: }
101: } catch (TypingEx e) {
102: // There is no solution
103: return new LinkedList();
104: } catch (Unsatisfiable e) {
105: throw new InternalError("This shouldn't happen");
106: }
107:
108: return res;
109: }
110:
111: /** Try all combinations of Kinds for free type variables.
112: There are two stages:
113: If doAll is true, set the tags for which all solutions must be listed.
114: Otherwise, set the other tags, and stop as soon as one solution is found.
115: */
116: private static final void setFloatingKinds(Element[] tags,
117: boolean[] all, int minFloating, List res, boolean doAll)
118: throws Unsatisfiable {
119: while (minFloating < tags.length
120: && (all[minFloating] != doAll || isFixedKind(tags[minFloating]
121: .getKind())))
122: minFloating++;
123:
124: if (minFloating < tags.length) {
125: Element tag = tags[minFloating];
126:
127: if (tag.getKind() == TopMonotype.TopKind.instance) {
128: if (all[minFloating])
129: // Tag is "Object". All TCs are solutions.
130: tag = tags[minFloating] = new MonotypeVar(
131: "enumeration");
132: else {
133: // We only want one solution anyway, which surely exists ;-)
134: // No need to set kinds
135: // recursive call
136: setFloatingKinds(tags, all, minFloating + 1, res,
137: doAll);
138: return;
139: }
140: } else {
141: // There might be a garbagy Engine.variablesConstraint
142: // in the monotype variable variable
143: tag.setKind(null);
144: }
145:
146: for (Iterator cs = Engine.listConstraints(); cs.hasNext();) {
147: Engine.Constraint c = (Engine.Constraint) cs.next();
148:
149: if (c.hasConstants()
150: && c != nice.tools.typing.PrimitiveType.nullTC
151: .getKind()) {
152: if (linkDbg && Typing.dbg)
153: Debug.println("Choosing kind " + c + " for "
154: + minFloating + ":" + tag);
155:
156: if (tag instanceof MonotypeVar)
157: Engine.forceKind(tag, c.associatedKind);
158: else
159: Engine.forceKind(tag, c);
160:
161: // recursive call
162: setFloatingKinds(tags, all, minFloating + 1, res,
163: doAll);
164:
165: tag.setKind(null);
166: }
167: }
168: } else if (doAll) {
169: try {
170: setFloatingKinds(tags, all, 0, res, false);
171: } catch (SolutionFound ex) {
172: // Continue with modifying kinds of all-marked tags.
173: }
174: } else {
175: List solutions = enumerateTags(tags, all);
176: res.addAll(solutions);
177: if (solutions.size() > 0)
178: /*
179: We found solutions for the current choice of kinds for tags.
180: We might find more by changing the kinds of non all-marked tags,
181: but we are not interested in this. So we skip to the next choice
182: of kinds for all-marked tags.
183: */
184: throw SolutionFound.instance;
185: }
186: }
187:
188: private static boolean isFixedKind(Kind k) {
189: return k != null && k != Engine.variablesConstraint
190: && k != TopMonotype.TopKind.instance;
191: }
192:
193: private static class SolutionFound extends RuntimeException {
194: static SolutionFound instance = new SolutionFound();
195: }
196:
197: private static List enumerateTags(Element[] tags, boolean[] all) {
198: TagsList tuples = new TagsList(tags.length);
199: List kinds = new ArrayList(tags.length); /* euristic:
200: at most one kind per tag */
201: List observers = new ArrayList(tags.length); // idem
202:
203: // The variable TCs that will hold the solutions.
204: TypeConstructor[] vars = new TypeConstructor[tags.length];
205:
206: Engine.enter(false);
207: try {
208:
209: for (int i = 0; i < tags.length; i++) {
210: Kind kind = tags[i].getKind();
211:
212: if (kind == TopMonotype.TopKind.instance)
213: continue;
214:
215: Engine.Constraint k = Engine.getConstraint(kind);
216:
217: BitVector obs;
218:
219: int idx = kinds.indexOf(k);
220: if (idx < 0) {
221: kinds.add(k);
222: observers.add(obs = new BitVector());
223: } else
224: obs = (BitVector) observers.get(idx);
225:
226: // ignore non matchable kinds
227: // XXX move up ?
228: if (tags[i].getKind() instanceof FunTypeKind
229: || tags[i].getKind() instanceof TupleKind)
230: continue;
231:
232: TypeConstructor constTC;
233: if (tags[i] instanceof TypeConstructor)
234: constTC = (TypeConstructor) tags[i];
235: else
236: constTC = ((Monotype) tags[i]).head();
237:
238: if (constTC == null)
239: throw new InternalError(tags[i].getKind()
240: + " is not a valid kind in enumerate");
241:
242: TypeConstructor varTC = new TypeConstructor(
243: constTC.variance);
244: vars[i] = varTC;
245:
246: Typing.introduce(varTC);
247:
248: // We only observe those positions where all solutions are needed.
249: if (all[i])
250: obs.set(varTC.getId());
251:
252: try {
253: k.leq(varTC, constTC);
254: k.reduceDomainToConcrete(varTC);
255: } catch (Unsatisfiable e) {
256: return emptyList;
257: }
258: }
259:
260: Engine.Constraint[] pKinds = (Engine.Constraint[]) kinds
261: .toArray(new Engine.Constraint[kinds.size()]);
262:
263: BitVector[] pObs = (BitVector[]) observers
264: .toArray(new BitVector[observers.size()]);
265:
266: if (enumerateInConstraints(pKinds, pObs, tuples, tags,
267: vars, all))
268: return emptyList;
269: } finally {
270: Engine.backtrack(false, false);
271: }
272:
273: return tuples.tags;
274: }
275:
276: private static List emptyList = new LinkedList();
277:
278: /** return true if there is no solution. */
279: private static boolean enumerateInConstraints(
280: Engine.Constraint[] kinds, BitVector[] observers,
281: final TagsList tuples, final Element[] tags,
282: final TypeConstructor[] vars, final boolean[] all) {
283: for (int act = 0; act < kinds.length; act++) {
284: tuples.startAddition();
285:
286: final BitVector obs = observers[act];
287: final mlsub.typing.lowlevel.Engine.Constraint kind = kinds[act];
288:
289: kind
290: .enumerate(
291: obs,
292: new mlsub.typing.lowlevel.LowlevelSolutionHandler() {
293: public void handle() {
294: // Check if this is really a solution, because of
295: // class constraints.
296: for (int index = 0; index < vars.length; index++) {
297: /* If this index does not need all solutions
298: (i.e. all[index] is false), and the solution
299: sol does not pass checkClassConstraint,
300: it might have been that some other solution, which
301: we don't generate, would pass. So in this case
302: we should restart to try other solutions for this
303: index to see if at least one passes or not.
304: */
305:
306: TypeConstructor var, solution;
307: var = vars[index];
308:
309: // We only deal with matchable tags,
310: // and those that belong to this kind.
311: if (var == null
312: || var.getKind() != kind)
313: continue;
314:
315: solution = (TypeConstructor) kind
316: .getElement(getSolutionOf(var
317: .getId()));
318: if (!checkClassConstraint(
319: tags[index], solution))
320: return;
321: }
322:
323: // It is a solution, let's add it to the list.
324: tuples.startEntry();
325: for (int index = 0; index < vars.length; index++) {
326: TypeConstructor var, solution;
327: var = vars[index];
328:
329: // We only deal with matchable tags,
330: // and those that belong to this kind.
331: if (var == null
332: || var.getKind() != kind)
333: continue;
334:
335: solution = (TypeConstructor) kind
336: .getElement(getSolutionOf(var
337: .getId()));
338: tuples.set(index, solution);
339: }
340: }
341: });
342:
343: // If there is no solution for a variable in the current kind,
344: // then handle() will never be called and endAddition() returns true.
345: // There is therefore no global solution, and we return true.
346: if (tuples.endAddition())
347: return true;
348: }
349: return false;
350: }
351:
352: /**
353: Return true if and only if sol can be the runtime tag of a
354: subtype of var. This especially involves checking the eventual
355: constraints on the type parameters of the class sol.
356: */
357: private static boolean checkClassConstraint(Element var,
358: TypeConstructor sol) {
359: Constraint constraint = bossa.syntax.dispatch
360: .getTypeDefResolvedConstraint(sol);
361:
362: if (mlsub.typing.Constraint.trivial(constraint))
363: return true;
364:
365: if (!(var instanceof Monotype))
366: return true;
367:
368: Monotype m = (Monotype) var;
369:
370: /* We don't want to modify var by reducing its domain, since that would
371: prevent other valid solutions to be discovered later.
372: Therefore we introduce a new tc, since what we want is to test
373: the type parameters.
374:
375: Another approach would be to mark/backtrack here. That would at least
376: require to slightly change the marking system, so that the exisisting
377: domain is backed-up and the cloned one is used immediately, since
378: the existing one is held by Satisfier.
379: */
380: TypeConstructor tc = new TypeConstructor(sol.variance);
381: Typing.introduce(tc);
382: MonotypeConstructor type = new MonotypeConstructor(tc,
383: bossa.syntax.dispatch.getTypeDefTypeParameters(sol));
384:
385: try {
386: constraint.enter();
387: Engine.leq(type, var);
388:
389: return true;
390: } catch (TypingEx ex) {
391: return false;
392: } catch (Unsatisfiable ex) {
393: return false;
394: }
395: }
396:
397: /**
398: A list of possible values for tags.
399:
400: Typical usage:
401: <code>
402:
403: TagsList tags = new TagsList(width);
404: for (...)
405: {
406: ...
407: tags.startAddition();
408: for (each possibility for the tags in the group)
409: {
410: tags.startEntry();
411: tags.set(tag1, value1);
412: tags.set(tag1, value2);
413: }
414: }
415:
416: </code>
417: */
418: private static class TagsList {
419: TagsList(int width) {
420: this .width = width;
421: }
422:
423: private int size, width;
424: private boolean first;
425: final List tags = new ArrayList();
426:
427: /** Call before enumeration of the possibilities for some tags */
428: void startAddition() {
429: size = tags.size();
430: first = true;
431: }
432:
433: // return true if there is no solution
434: boolean endAddition() {
435: return first;
436: }
437:
438: /** Call before each possibility for these tags */
439: void startEntry() {
440: if (first) {
441: first = false;
442: if (tags.size() == 0) {
443: tags.add(new TypeConstructor[width]);
444: size = 1;
445: }
446: } else
447: // copy the first elements at the end,
448: // so that they can be overwritten with the new values
449: for (int i = 0; i < size; i++)
450: tags.add(((Object[]) tags.get(i)).clone());
451: }
452:
453: /** Set the value of one tag */
454: void set(int index, TypeConstructor tag) {
455: for (int i = 0; i < size; i++)
456: ((TypeConstructor[]) tags.get(i))[index] = tag;
457: }
458: }
459:
460: public static boolean linkDbg = bossa.util.Debug.linkTests;
461: }
|