001: /**************************************************************************/
002: /* B O S S A */
003: /* A simple imperative object-oriented research language */
004: /* (c) Daniel Bonniot 1999 */
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 mlsub.typing.lowlevel.Engine;
014: import java.util.ArrayList;
015: import java.util.Map;
016:
017: /**
018: A constrained monotype.
019:
020: @author Daniel Bonniot
021: */
022:
023: public final class Polytype {
024: public Polytype(Constraint constraint, Monotype monotype) {
025: this .constraint = constraint;
026: this .monotype = monotype;
027: }
028:
029: public Polytype(Monotype monotype) {
030: this .constraint = null;
031: this .monotype = monotype;
032: }
033:
034: public final boolean isMonomorphic() {
035: return !Constraint.hasBinders(constraint);
036: }
037:
038: public Polytype cloneType() {
039: //Optimization
040: if (isMonomorphic())
041: return this ;
042:
043: Map map = new java.util.HashMap();
044:
045: TypeSymbol[] binders = constraint.binders();
046: TypeSymbol[] newBinders = new TypeSymbol[binders.length];
047:
048: for (int i = 0; i < binders.length; i++) {
049: newBinders[i] = binders[i].cloneTypeSymbol();
050: map.put(binders[i], newBinders[i]);
051: // Clone the persistent equivalents of marked type variables.
052: if (binders[i] instanceof MonotypeVar
053: && ((MonotypeVar) binders[i]).persistentKind != null) {
054: MonotypeConstructor mc = (MonotypeConstructor) ((MonotypeVar) binders[i])
055: .equivalent();
056: MonotypeConstructor nmc = (MonotypeConstructor) ((MonotypeVar) newBinders[i])
057: .equivalent();
058: map.put(mc.getTC(), nmc.getTC());
059: map.put(mc.getTP()[0], nmc.getTP()[0]);
060: }
061: }
062:
063: return new Polytype(new Constraint(newBinders, AtomicConstraint
064: .substitute(map, constraint.atoms())), monotype
065: .substitute(map));
066: }
067:
068: public Constraint getConstraint() {
069: return constraint;
070: }
071:
072: public static Constraint[] getConstraint(Polytype[] p) {
073: Constraint[] res = new Constraint[p.length];
074:
075: for (int i = 0; i < p.length; i++)
076: res[i] = p[i].getConstraint();
077:
078: return res;
079: }
080:
081: public Monotype getMonotype() {
082: return monotype;
083: }
084:
085: public static Monotype[] getMonotype(Polytype[] p) {
086: Monotype[] res = new Monotype[p.length];
087:
088: for (int i = 0; i < p.length; i++)
089: res[i] = p[i].getMonotype();
090:
091: return res;
092: }
093:
094: public static final Polytype bottom() {
095: MonotypeVar alpha = new MonotypeVar();
096: return new Polytype(new Constraint(new TypeSymbol[] { alpha },
097: null), alpha);
098: }
099:
100: /****************************************************************
101: * Typechecking
102: ****************************************************************/
103:
104: public void checkWellFormedness() throws TypingEx {
105: // Optimization
106: if (!Constraint.hasBinders(constraint))
107: return;
108:
109: Typing.enter();
110:
111: try {
112: constraint.enter();
113: } finally {
114: Typing.leave();
115: }
116: }
117:
118: /****************************************************************
119: * Computations on types
120: ****************************************************************/
121:
122: public static Polytype apply(Polytype funt, Polytype[] parameters) {
123: return apply(funt.constraint, (FunType) funt.monotype,
124: parameters);
125: }
126:
127: public static Polytype apply(Constraint cst, FunType type,
128: Polytype[] parameters) {
129: Monotype codom = type.codomain();
130: /*
131: Optimization:
132: If we know codom is a constant,
133: the constraint parameters<dom is useless.
134: */
135: if (codom.isRigid())
136: return new Polytype(Constraint.True, codom);
137:
138: Monotype[] dom = type.domain();
139:
140: cst = Constraint.and(Polytype.getConstraint(parameters), cst,
141: MonotypeLeqCst.constraint(Polytype
142: .getMonotype(parameters), dom));
143:
144: Polytype res = new Polytype(cst, codom);
145: res.simplified = false;
146: return res;
147: }
148:
149: public static Polytype union(Polytype t1, Polytype t2) {
150: if (t1 == t2)
151: return t1;
152:
153: MonotypeVar t = new MonotypeVar();
154:
155: Constraint c = Constraint.and(t, t1.constraint, t2.constraint,
156: new MonotypeLeqCst(t1.monotype, t), new MonotypeLeqCst(
157: t2.monotype, t));
158:
159: Polytype res = new Polytype(c, t);
160: res.simplified = false;
161: return res;
162: }
163:
164: public static Polytype union(Polytype[] types) {
165: if (types.length == 0)
166: return bottom();
167:
168: /* Even if there is only one type, we quantify over all super-types.
169: This is needed when a non-variant type constructor like []
170: is added around the returned type. Probably this means a wrong
171: spec for this union function.
172: */
173:
174: MonotypeVar t = new MonotypeVar();
175:
176: Constraint c = new Constraint(new TypeSymbol[] { t }, null);
177: for (int i = 0; i < types.length; i++)
178: c = Constraint.and(c, types[i].constraint,
179: new MonotypeLeqCst(types[i].monotype, t));
180:
181: Polytype res = new Polytype(c, t);
182: res.simplified = false;
183: return res;
184: }
185:
186: /****************************************************************
187: * Functional types
188: ****************************************************************/
189:
190: public Monotype[] domain() {
191: Monotype m = monotype.equivalent();
192: if (!(m instanceof FunType))
193: return null;
194:
195: return ((FunType) m).domain();
196: }
197:
198: public Monotype codomain() {
199: Monotype m = monotype.equivalent();
200: if (!(m instanceof FunType))
201: return null;
202:
203: return ((FunType) m).codomain();
204: }
205:
206: /****************************************************************
207: * Accessors
208: ****************************************************************/
209:
210: /**
211: * Returns the domain of a functional polytype.
212: *
213: * @return a 'tuple' Domain
214: */
215: public Domain getDomain() {
216: Monotype[] domains = domain();
217:
218: if (domains == null)
219: throw new InternalError(
220: "getDomain on non functional polytype " + this );
221:
222: return new Domain(constraint, domains);
223: }
224:
225: /****************************************************************
226: * Simplification
227: ****************************************************************/
228:
229: /*
230: Whether this polytype is in simplified form.
231: The default value is true, so it shoud be set to false
232: for any polytype constructed in a way that does not guaranty it to
233: be simplified.
234: */
235: private boolean simplified = true;
236:
237: public void setNotSimplified() {
238: simplified = false;
239: }
240:
241: public void simplify() {
242: if (!Constraint.hasBinders(constraint) || simplified
243: || Polytype.noSimplify)
244: return;
245:
246: ArrayList binders = new ArrayList(), atoms = new ArrayList();
247:
248: Engine.startSimplify();
249: try {
250: Constraint.enter(constraint);
251: Engine.satisfy();
252: monotype.tag(Variance.COVARIANT);
253: Engine.simplify(binders, atoms);
254: } catch (mlsub.typing.lowlevel.Unsatisfiable e) {
255: // Avoid looping.
256: simplified = true;
257: throw new InternalError("Simplifying ill-formed polytype: "
258: + this );
259: } catch (TypingEx e) {
260: // Avoid looping.
261: simplified = true;
262: throw new InternalError("Simplifying ill-formed polytype: "
263: + this );
264: } finally {
265: Engine.stopSimplify();
266: }
267:
268: int nbinders = binders.size(), natoms = atoms.size();
269:
270: if (nbinders >= constraint.binders().length) {
271: // The "simplified" version is longer than the original, so we
272: // keep the original.
273: simplified = true;
274: return;
275: }
276:
277: monotype = monotype.canonify();
278:
279: constraint = Constraint.create(nbinders == 0 ? null
280: : (TypeSymbol[]) binders
281: .toArray(new TypeSymbol[nbinders]),
282: natoms == 0 ? null : (AtomicConstraint[]) atoms
283: .toArray(new AtomicConstraint[natoms]));
284:
285: simplified = true;
286: }
287:
288: /** Try to simplify this type.
289: @return false if the type is ill-formed.
290: */
291: public boolean trySimplify() {
292: try {
293: simplify();
294: return true;
295: } catch (InternalError e) {
296: return false;
297: }
298: }
299:
300: /****************************************************************
301: * Misc
302: ****************************************************************/
303:
304: public String toString() {
305: // We want a simple form for printing
306: try {
307: simplify();
308: } catch (InternalError e) {
309: return Constraint.toString(constraint)
310: + monotype.toString() + " (Ill-formed type)";
311: }
312:
313: return Constraint.toString(constraint)
314: + String.valueOf(monotype);
315: }
316:
317: public String toStringNoSimplify() {
318: return Constraint.toString(constraint)
319: + String.valueOf(monotype);
320: }
321:
322: private Constraint constraint;
323: private Monotype monotype;
324:
325: public static boolean noSimplify = bossa.util.Debug.noSimplify;
326: }
|