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.*;
014:
015: import java.util.Map;
016:
017: /**
018: * Atomic constraint.
019: *
020: * @author Daniel Bonniot
021: */
022:
023: public final class Constraint {
024: public Constraint(TypeSymbol[] binders, AtomicConstraint[] atoms) {
025: this .binders = binders;
026: if (binders != null)
027: nbinders = binders.length;
028:
029: this .atoms = atoms;
030: if (atoms != null)
031: natoms = atoms.length;
032: }
033:
034: /** Ensures that null is returned if there are no binders and atoms */
035: public final static Constraint create(TypeSymbol[] binders,
036: AtomicConstraint[] atoms) {
037: if (binders == null && atoms == null)
038: return True;
039: if (binders != null && binders.length == 0)
040: throw new Error("Please optimize");
041: if (atoms != null && atoms.length == 0)
042: throw new Error("Please optimize");
043:
044: return new Constraint(binders, atoms);
045: }
046:
047: /**
048: Empty constraint. private use only.
049: */
050: private Constraint() {
051: }
052:
053: public static final Constraint True = null;
054:
055: public static final boolean hasBinders(Constraint c) {
056: return c != null && c.binders != null;
057: }
058:
059: public static final boolean trivial(Constraint c) {
060: return c == null || c.natoms == 0;
061: }
062:
063: public TypeSymbol[] binders() {
064: return binders;
065: }
066:
067: public AtomicConstraint[] atoms() {
068: return atoms;
069: }
070:
071: /****************************************************************
072: * Manipulation
073: ****************************************************************/
074:
075: public static Constraint and(Constraint c1, Constraint c2) {
076: final int nbinders1 = (c1 == null ? 0 : c1.nbinders), nbinders2 = (c2 == null ? 0
077: : c2.nbinders), natoms1 = (c1 == null ? 0 : c1.natoms), natoms2 = (c2 == null ? 0
078: : c2.natoms);
079:
080: if (nbinders1 == 0 && nbinders2 == 0 && natoms1 == 0
081: && natoms2 == 0)
082: return True;
083:
084: Constraint res = new Constraint();
085: res.nbinders = nbinders1 + nbinders2;
086: res.natoms = natoms1 + natoms2;
087:
088: if (res.nbinders > 0) {
089: res.binders = new TypeSymbol[res.nbinders];
090: for (int i = 0; i < nbinders1; i++)
091: res.binders[i] = c1.binders[i];
092: for (int i = 0; i < nbinders2; i++)
093: res.binders[nbinders1 + i] = c2.binders[i];
094: }
095:
096: if (res.natoms > 0) {
097: res.atoms = new AtomicConstraint[res.natoms];
098: for (int i = 0; i < natoms1; i++)
099: res.atoms[i] = c1.atoms[i];
100: for (int i = 0; i < natoms2; i++)
101: res.atoms[natoms1 + i] = c2.atoms[i];
102: }
103:
104: return res;
105: }
106:
107: public static Constraint and(Constraint c1, TypeSymbol t0,
108: TypeSymbol t1, AtomicConstraint a1, AtomicConstraint a2) {
109: final int nbinders = (c1 == null ? 0 : c1.nbinders) + 2, natoms = (c1 == null ? 0
110: : c1.natoms) + 2;
111:
112: Constraint res = new Constraint();
113: res.nbinders = nbinders;
114: res.natoms = natoms;
115:
116: res.binders = new TypeSymbol[nbinders];
117: for (int i = 0; i < nbinders - 2; i++)
118: res.binders[i] = c1.binders[i];
119: res.binders[nbinders - 2] = t0;
120: res.binders[nbinders - 1] = t1;
121:
122: res.atoms = new AtomicConstraint[res.natoms];
123: for (int i = 0; i < natoms - 2; i++)
124: res.atoms[i] = c1.atoms[i];
125: res.atoms[natoms - 2] = a2;
126: res.atoms[natoms - 1] = a1;
127:
128: return res;
129: }
130:
131: static Constraint and(TypeSymbol m, Constraint c1, Constraint c2,
132: AtomicConstraint a1, AtomicConstraint a2) {
133: Constraint res = new Constraint();
134:
135: final int nbinders1 = (c1 == null ? 0 : c1.nbinders), nbinders2 = (c2 == null ? 0
136: : c2.nbinders), natoms1 = (c1 == null ? 0 : c1.natoms), natoms2 = (c2 == null ? 0
137: : c2.natoms);
138:
139: res.nbinders = nbinders1 + nbinders2 + 1;
140: res.binders = new TypeSymbol[res.nbinders];
141: for (int i = 0; i < nbinders1; i++)
142: res.binders[i] = c1.binders[i];
143: for (int i = 0; i < nbinders2; i++)
144: res.binders[nbinders1 + i] = c2.binders[i];
145: res.binders[res.nbinders - 1] = m;
146:
147: res.natoms = natoms1 + natoms2 + 2;
148: res.atoms = new AtomicConstraint[res.natoms];
149: for (int i = 0; i < natoms1; i++)
150: res.atoms[i] = c1.atoms[i];
151: for (int i = 0; i < natoms2; i++)
152: res.atoms[natoms1 + i] = c2.atoms[i];
153: res.atoms[res.natoms - 2] = a2;
154: res.atoms[res.natoms - 1] = a1;
155:
156: return res;
157: }
158:
159: static Constraint and(Constraint c1, Constraint c2,
160: AtomicConstraint a1) {
161: Constraint res = new Constraint();
162:
163: final int nbinders1 = (c1 == null ? 0 : c1.nbinders), nbinders2 = (c2 == null ? 0
164: : c2.nbinders), natoms1 = (c1 == null ? 0 : c1.natoms), natoms2 = (c2 == null ? 0
165: : c2.natoms);
166:
167: res.nbinders = nbinders1 + nbinders2;
168: res.binders = new TypeSymbol[res.nbinders];
169: for (int i = 0; i < nbinders1; i++)
170: res.binders[i] = c1.binders[i];
171: for (int i = 0; i < nbinders2; i++)
172: res.binders[nbinders1 + i] = c2.binders[i];
173:
174: res.natoms = natoms1 + natoms2 + 1;
175: res.atoms = new AtomicConstraint[res.natoms];
176: for (int i = 0; i < natoms1; i++)
177: res.atoms[i] = c1.atoms[i];
178: for (int i = 0; i < natoms2; i++)
179: res.atoms[natoms1 + i] = c2.atoms[i];
180: res.atoms[res.natoms - 1] = a1;
181:
182: return res;
183: }
184:
185: /**
186: Conjunction of the given constraints.
187:
188: Leaves the parameters unmodified.
189: */
190: public static Constraint and(Constraint[] cs, Constraint c1,
191: Constraint c2) {
192: final int nbinders1 = (c1 == null ? 0 : c1.nbinders), nbinders2 = (c2 == null ? 0
193: : c2.nbinders), natoms1 = (c1 == null ? 0 : c1.natoms), natoms2 = (c2 == null ? 0
194: : c2.natoms);
195:
196: int lenBinders = nbinders1 + nbinders2;
197: int lenAtoms = natoms1 + natoms2;
198:
199: for (int i = 0; i < cs.length; i++) {
200: Constraint c = cs[i];
201: if (c == True)
202: continue;
203:
204: lenBinders += cs[i].nbinders;
205: lenAtoms += cs[i].natoms;
206: }
207:
208: if (lenAtoms == 0 && lenBinders == 0)
209: return True;
210:
211: Constraint res = new Constraint();
212: if (lenBinders > 0) {
213: res.nbinders = lenBinders;
214: res.binders = new TypeSymbol[lenBinders];
215: for (int i = 0; i < nbinders2; i++)
216: res.binders[--lenBinders] = c2.binders[i];
217: for (int i = 0; i < nbinders1; i++)
218: res.binders[--lenBinders] = c1.binders[i];
219: }
220:
221: if (lenAtoms > 0) {
222: res.natoms = lenAtoms;
223: res.atoms = new AtomicConstraint[lenAtoms];
224: for (int i = 0; i < natoms2; i++)
225: res.atoms[--lenAtoms] = c2.atoms[i];
226: for (int i = 0; i < natoms1; i++)
227: res.atoms[--lenAtoms] = c1.atoms[i];
228: }
229:
230: for (int j = 0; j < cs.length; j++) {
231: Constraint c = cs[j];
232: if (c == True)
233: continue;
234:
235: for (int i = 0; i < c.nbinders; i++)
236: res.binders[--lenBinders] = c.binders[i];
237:
238: for (int i = 0; i < c.natoms; i++)
239: res.atoms[--lenAtoms] = c.atoms[i];
240: }
241:
242: return res;
243: }
244:
245: /****************************************************************
246: * Typechecking
247: ****************************************************************/
248:
249: public static void enter(Constraint c) throws TypingEx {
250: if (c != null)
251: c.enter();
252: }
253:
254: public void enter() throws TypingEx {
255: if (binders != null)
256: Typing.introduceTypeSymbols(binders);
257:
258: if (atoms != null)
259: for (int i = 0; i < natoms; i++)
260: atoms[i].enter();
261: }
262:
263: public void enter(boolean existential) throws TypingEx {
264: if (existential && binders != null)
265: for (int i = 0; i < nbinders; i++)
266: if (binders[i] instanceof MonotypeVar)
267: ((MonotypeVar) binders[i]).setExistential();
268:
269: enter();
270: }
271:
272: /****************************************************************
273: * Printing
274: ****************************************************************/
275:
276: public String toString() {
277: StringBuffer res = new StringBuffer("<");
278: for (int i = 0; i < nbinders; i++) {
279: res.append(binders[i].toString());
280: if (i < nbinders - 1)
281: res.append(", ");
282: }
283: if (nbinders > 0 && natoms > 0)
284: res.append(" | ");
285: for (int i = 0; i < natoms; i++) {
286: res.append(String.valueOf(atoms[i]));
287: if (i < natoms - 1)
288: res.append(", ");
289: }
290: res.append("> ");
291: return res.toString();
292: }
293:
294: public static String toString(Constraint c) {
295: if (c == True)
296: return "";
297: else
298: return c.toString();
299: }
300:
301: private TypeSymbol[] binders;
302: /** length of the binders array */
303: private int nbinders;
304:
305: private AtomicConstraint[] atoms;
306: /** length of the atoms array */
307: private int natoms;
308: }
|