001 /* Copyright 2000, 2001, Compaq Computer Corporation */
002
003 package escjava.prover;
004
005 import java.io.*;
006
007 /**
008 * <code>SList</code>s represent possibly-empty lists of
009 * <code>SExp</code>s.
010 *
011 * <h3> Creation </h3>
012 *
013 * <p> As a convenience, lists of fewer than 9 elements may be created
014 * directly by calling <code>SList.make</code> on the desired
015 * elements. E.g., <code>SList.make(x, y)</code> creates the list
016 * <code>(</code><i>x</i><code> </code><i>y</i><code>)</code> where
017 * <i>x</i> and <i>y</i> are the contents of the <code>SExp</code>
018 * variables <code>x</code> and <code>y</code>. Longer lists may be
019 * created either from arrays (see <code>fromArray</code>) or by
020 * combining shorter lists via <code>append</code>. </p>
021 *
022 * <p> As a further convenience, <code>SList.make</code> calls
023 * {@link SExp#fancyMake(Object)} on its arguments before placing them in
024 * the resulting list. This means that <code>Atom</code>s may be
025 * specified by a <code>String</code> holding their name and that
026 * S-expression integers may be specified by <code>Integer</code>s.
027 * E.g., <code>SList.make("NEG", new Integer(1))</code> represents the
028 * S-expression <code>(NEG, 1)</code>. </p>
029 *
030 * <p> <code>SList</code>s may not contain <code>null</code>
031 * elements. </p>
032 *
033 *
034 * <h3> Inspection </h3>
035 *
036 * <p> <code>SList</code>s can be tested to see if they are empty, can
037 * have their length determined, and can have their <i>i</i>-index
038 * element extracted. (If an attempt is made to extract a
039 * non-existent element, <code>SExpTypeError</code> will be
040 * thrown.) </p>
041 *
042 *
043 * <h3> Manipulation </h3>
044 *
045 * <p> S-expressions are currently immutable; accordingly all
046 * manipulation methods act functionally. S-expressions may be made
047 * mutable later via the addition of mutation methods. </p>
048 *
049 * <p> <code>SList</code>s can be appended to each other. Elements
050 * can also be added to the front or end of a list. </p>
051 *
052 *
053 * <h3> Implementation </h3>
054 *
055 * <p> <code>SList</code>s are currently implemented via pairs and a
056 * nil object a la Lisp. These are provided by the non-public classes
057 * <code>SPair</code> and <code>SNil</code>. This implementation is
058 * subject to change at any time; clients should rely only on the
059 * publically-provided interface of this class. </p>
060 *
061 * @see escjava.prover.SNil
062 * @see escjava.prover.SPair
063 *
064 * @todo kiniry 14 March 2003 - Add a list model.
065 */
066
067 public abstract class SList extends SExp
068 {
069 /**
070 * <code>SList</code> may not be extended outside this package.
071 */
072 /* package */ SList() {};
073
074 /**
075 * @return a S-expression representing the empty list.
076 */
077 //@ public normal_behavior
078 //@ ensures \result.isEmpty();
079 //@ ensures \result.length() == 0;
080 public static /*@ pure non_null @*/ SList make() {
081 return SNil.getNil();
082 }
083
084 /**
085 * @return a S-expression representing a 1-element list whose
086 * contents are the result of applying {@link SExp#fancyMake(Object)}
087 * to our arguments.
088 */
089 //-@ pure
090 public static /*@ non_null @*/ SList make(/*@ non_null @*/ Object a1) {
091 return new SPair(SExp.fancyMake(a1), SNil.make());
092 }
093
094 /**
095 * @return a S-expression representing a 2-element list whose
096 * contents are the result of applying {@link SExp#fancyMake(Object)}
097 * to our arguments.
098 */
099 //-@ pure
100 public static /*@ non_null @*/ SList make(/*@ non_null @*/ Object a1,
101 /*@ non_null @*/ Object a2) {
102 return new SPair(SExp.fancyMake(a1), make(a2));
103 }
104
105 /**
106 * @return a S-expression representing a 3-element list whose
107 * contents are the result of applying {@link SExp#fancyMake(Object)}
108 * to our arguments. <p>
109 */
110 public static /*@ pure non_null @*/ SList make(/*@ non_null @*/ Object a1,
111 /*@ non_null @*/ Object a2,
112 /*@ non_null @*/ Object a3) {
113 return new SPair(SExp.fancyMake(a1), make(a2,a3));
114 }
115
116 /**
117 * @return a S-expression representing a 4-element list whose
118 * contents are the result of applying {@link SExp#fancyMake(Object)}
119 * to our arguments. <p>
120 */
121 public static /*@ pure non_null @*/ SList make(/*@ non_null @*/ Object a1,
122 /*@ non_null @*/ Object a2,
123 /*@ non_null @*/ Object a3,
124 /*@ non_null @*/ Object a4) {
125 return new SPair(SExp.fancyMake(a1), make(a2,a3,a4));
126 }
127
128 /**
129 * @return a S-expression representing a 5-element list whose
130 * contents are the result of applying {@link SExp#fancyMake(Object)}
131 * to our arguments. <p>
132 */
133 public static /*@ pure non_null @*/ SList make(/*@ non_null @*/ Object a1,
134 /*@ non_null @*/ Object a2,
135 /*@ non_null @*/ Object a3,
136 /*@ non_null @*/ Object a4,
137 /*@ non_null @*/ Object a5) {
138 return new SPair(SExp.fancyMake(a1), make(a2,a3,a4,a5));
139 }
140
141 /**
142 * @return a S-expression representing a 6-element list whose
143 * contents are the result of applying {@link SExp#fancyMake(Object)}
144 * to our arguments. <p>
145 */
146 public static /*@ pure non_null @*/ SList make(/*@ non_null @*/ Object a1,
147 /*@ non_null @*/ Object a2,
148 /*@ non_null @*/ Object a3,
149 /*@ non_null @*/ Object a4,
150 /*@ non_null @*/ Object a5,
151 /*@ non_null @*/ Object a6) {
152 return new SPair(SExp.fancyMake(a1), make(a2,a3,a4,a5,a6));
153 }
154
155 /**
156 * @return a S-expression representing a 7-element list whose
157 * contents are the result of applying {@link SExp#fancyMake(Object)}
158 * to our arguments. <p>
159 */
160 public static /*@ pure non_null @*/ SList make(/*@ non_null @*/ Object a1,
161 /*@ non_null @*/ Object a2,
162 /*@ non_null @*/ Object a3,
163 /*@ non_null @*/ Object a4,
164 /*@ non_null @*/ Object a5,
165 /*@ non_null @*/ Object a6,
166 /*@ non_null @*/ Object a7) {
167 return new SPair(SExp.fancyMake(a1), make(a2,a3,a4,a5,a6,a7));
168 }
169
170 /**
171 * @return a S-expression representing a 8-element list whose
172 * contents are the result of applying {@link SExp#fancyMake(Object)}
173 * to our arguments.
174 */
175 public static /*@ pure non_null @*/ SList make(/*@ non_null @*/ Object a1,
176 /*@ non_null @*/ Object a2,
177 /*@ non_null @*/ Object a3,
178 /*@ non_null @*/ Object a4,
179 /*@ non_null @*/ Object a5,
180 /*@ non_null @*/ Object a6,
181 /*@ non_null @*/ Object a7,
182 /*@ non_null @*/ Object a8) {
183 return new SPair(SExp.fancyMake(a1), make(a2,a3,a4,a5,a6,a7,a8));
184 }
185
186
187 /**
188 * @return a S-expression representing a list whose
189 * contents are the contents of a given array.
190 */
191 //@ public normal_behavior
192 //@ requires \nonnullelements(a);
193 //@ ensures \result != null;
194 public static /*@ pure non_null @*/ SList fromArray(/*@ non_null @*/ SExp[] a) {
195 SList l = make();
196
197 for (int i = a.length-1; i >= 0; i--)
198 l = new SPair(a[i], l);
199
200 return l;
201 }
202
203 //@ also
204 //@ public normal_behavior
205 //@ ensures \result;
206 public /*@ pure @*/ boolean isList() {
207 return true;
208 }
209
210 //@ also
211 //@ public normal_behavior
212 //@ ensures \result == this;
213 public /*@ pure non_null @*/ SList getList() {
214 return this;
215 }
216
217 /**
218 * @return a flag indicating if we are we an empty list.
219 */
220 public abstract /*@ pure @*/ boolean isEmpty();
221
222 /**
223 * @return our length.
224 */
225 //@ public normal_behavior
226 //@ ensures \result >= 0;
227 public abstract /*@ pure @*/ int length();
228
229
230 /**
231 * If we represent a non-empty list, return it as a
232 * <code>SPair</code>; otherwise, throw <code>SExpTypeError</code>.
233 */
234 //@ exceptional_behavior
235 //@ signals (SExpTypeError) true;
236 /*package*/ /*@ non_null pure @*/ SPair getPair() throws SExpTypeError {
237 throw new SExpTypeError();
238 }
239
240 /**
241 * @return our element at index <code>i</code> (indices start at
242 * 0). If we are not long enough to have an element at that
243 * index, then <code>SExpTypeError</code> is thrown.
244 */
245 //@ public normal_behavior
246 //@ requires i >= 0;
247 //@ ensures \result != null;
248 //@ also
249 //@ public exceptional_behavior
250 //@ signals (SExpTypeError) true;
251 public /*@ pure @*/ SExp at(int i) throws SExpTypeError {
252 SPair ptr = getPair();
253
254 for (; i > 0; i--)
255 ptr = ptr.tail.getPair();
256
257 return ptr.head;
258 }
259
260 /**
261 * Modify the list in place by set the <code>i</code>th element to
262 * <code>s</code>.
263 */
264 //@ public normal_behavior
265 //@ requires 0 <= i;
266 //@ requires i < this.length();
267 //@ modifies \everything;
268 //@ ensures at(i) == s;
269 public void setAt(int i, /*@ non_null @*/ SExp s) throws SExpTypeError {
270 SPair ptr = getPair();
271
272 for (; i > 0; i--)
273 ptr = ptr.tail.getPair();
274
275 ptr.head = s;
276 }
277
278 /**
279 * @return the functional result of appending another list to
280 * us.
281 */
282 //@ public normal_behavior
283 //@ requires x != null;
284 //@ modifies \everything;
285 //@ ensures \result != null;
286 //@ also
287 //@ public normal_behavior
288 //@ requires (this instanceof SNil);
289 //@ modifies \everything;
290 //@ ensures \result == x;
291 public /*@ non_null @*/ SList append(/*@ non_null @*/ SList x) {
292 if (this instanceof SNil)
293 return x;
294 else {
295 SPair us = (SPair)this; //@ nowarn Cast;
296
297 return new SPair(us.head, us.tail.append(x));
298 }
299 }
300
301 /**
302 * Destructive list reversal
303 */
304 //@ public normal_behavior
305 //@ requires l != null;
306 //@ modifies \everything;
307 //@ ensures \result != null;
308 public static SList reverseD(SList l){
309 SList res = SNil.getNil();
310 while (! (l instanceof SNil)){
311 SList temp = res;
312 res = l; l = ((SPair)l).tail; ((SPair)res).tail = temp;
313 }
314 return res;
315 }
316
317 /**
318 * @return the functional result of adding a given element at the
319 * front of us.
320 *
321 * Precondition: <code>x</code> is non-null.<p>
322 */
323 //@ public normal_behavior
324 //@ requires x != null;
325 //@ modifies \everything;
326 //@ ensures \result != null;
327 //@ ensures \result.at(0) == x;
328 public SList addFront(SExp x) {
329 return new SPair(x, this);
330 }
331
332 /**
333 * @return the functional result of adding a given element at the
334 * end of us.
335 *
336 * <p> This function is likely to be slower than <code>addFront</code>.
337 */
338 //@ public normal_behavior
339 //@ requires x != null;
340 //@ modifies \everything;
341 //@ ensures \result != null;
342 //@ ensures \result.at(\result.length()) == x;
343 public SList addEnd(SExp x) {
344 return append(make(x));
345 }
346
347 /**
348 * Print a textual representation of us on a given
349 * <code>PrintStream</code>.
350 *
351 * <p> Note: This routine will take a <code>PrintWriter</code>
352 * instead when we switch to a more recent version of JDK. </p>
353 */
354 public /*@ pure @*/ void print(/*@ non_null @*/ PrintStream out) {
355 // Is this the first item to be printed?
356 boolean first = true;
357
358 // The remaining list to be printed:
359 SList remaining = this;
360
361 out.print("(");
362 while (remaining instanceof SPair) {
363 if (!first)
364 out.print(" ");
365
366 SPair p = (SPair)remaining;
367 p.head.print(out);
368 first = false;
369 remaining = p.tail;
370 }
371 out.print(")");
372 }
373
374 /**
375 * Pretty-print a textual representation of us on a given
376 * <code>PrintStream</code>.
377 *
378 * <p> Note: This routine will take a <code>PrintWriter</code>
379 * instead when we switch to a more recent version of JDK. </p>
380 */
381 public /*@ pure @*/ void prettyPrint(/*@ non_null @*/ PrintStream out) {
382 try {
383 if (!specialPrint(out)) {
384 if (this instanceof SNil)
385 out.print("()");
386 else {
387 // by default, print (op arg1 ... argn) as
388 // op(arg1 ... argn)
389 SPair p = (SPair) this;
390 SList remaining = p.tail;
391 boolean first = true;
392 p.head.prettyPrint(out);
393 out.print("(");
394 while (remaining instanceof SPair) {
395 if (!first)
396 out.print(" ");
397 p = (SPair) remaining;
398 p.head.prettyPrint(out);
399 first = false;
400 remaining = p.tail;
401 }
402 out.print(")");
403 }
404 }
405 }
406 catch (SExpTypeError e) {
407 javafe.util.Assert.fail("Error: Out of bounds access to SList");
408 }
409 }
410
411 /**
412 * Specially print a textual representation of us on a given
413 * <code>PrintStream</code>. This is a subroutine used in
414 * pretty-printing.
415 *
416 * <p> Note: This routine will take a <code>PrintWriter</code>
417 * instead when we switch to a more recent version of JDK. </p>
418 */
419 private boolean specialPrint(/*@ non_null @*/ PrintStream out) throws SExpTypeError {
420 int len = length();
421 if (len < 2 || len > 3)
422 return false;
423 String first = at(0).toString();
424 String op;
425 if (len == 2) {
426 if (first.equals("NOT") || first.equals("boolNot")
427 || first.equals("integralNot"))
428 op = "!";
429 else if (first.equals("floatingNeg") ||
430 first.equals("integralNeg"))
431 op = "-";
432 else if (first.equals("_array")) {
433 at(1).prettyPrint(out);
434 out.print("[]");
435 return true;
436 }
437 else
438 return false;
439 out.print(op);
440 at(1).prettyPrint(out);
441 return true;
442 }
443 else {
444 if (first.equals("EQ")) {
445 at(1).prettyPrint(out);
446 out.print(" == ");
447 at(2).prettyPrint(out);
448 return true;
449 }
450 else if (first.equals("NEQ")) {
451 at(1).prettyPrint(out);
452 out.print(" != ");
453 at(2).prettyPrint(out);
454 return true;
455 }
456 else if (first.equals("<:") || first.equals("typeLE")) {
457 at(1).prettyPrint(out);
458 out.print(" <: ");
459 at(2).prettyPrint(out);
460 return true;
461 }
462 else if (first.equals("is")) {
463 out.print("typeof(");
464 at(1).prettyPrint(out);
465 out.print(") <: ");
466 at(2).prettyPrint(out);
467 return true;
468 }
469 else if (first.equals("select")) {
470 SExp arg1 = at(1);
471 SExp arg2 = at(2);
472
473 // if this select is an array access, print it appropriately
474 // NOTE: This may screw up the printing of variables that
475 // contain the string "elems" in their name
476 if (arg1.isList()) {
477 SList arg1L = (SList) arg1;
478 if (arg1L.length() == 3 &&
479 arg1L.at(0).toString().equals("select") &&
480 arg1L.at(1).toString().startsWith("elems")) {
481 arg1L.at(2).prettyPrint(out);
482 out.print("[");
483 arg2.prettyPrint(out);
484 out.print("]");
485 return true;
486 }
487 }
488 //parenthesize identifiers containing special characters
489 if (arg2.isAtom() &&
490 Atom.printableVersion(arg2.toString()).startsWith("|"))
491 {
492 out.print("(");
493 arg2.prettyPrint(out);
494 out.print(")");
495 }
496 else
497 arg2.prettyPrint(out);
498 out.print(".");
499 if (arg1.isAtom() &&
500 Atom.printableVersion(arg1.toString()).startsWith("|"))
501 {
502 out.print("(");
503 arg1.prettyPrint(out);
504 out.print(")");
505 }
506 else
507 arg1.prettyPrint(out);
508 return true;
509 }
510 // print all of the infix operators correctly
511 else if (first.equals("anyEQ") || first.equals("boolEq") ||
512 first.equals("floatingEQ") ||
513 first.equals("integralEQ") || first.equals("refEQ")
514 || first.equals("typeEQ"))
515 op = " == ";
516 else if (first.equals("anyNE") || first.equals("boolNE") ||
517 first.equals("floatingNE") ||
518 first.equals("integralNE") || first.equals("refNE")
519 || first.equals("typeNE"))
520 op = " != ";
521 else if (first.equals("floatingAdd") ||
522 first.equals("integralAdd") ||
523 first.equals("stringCat") || first.equals("+"))
524 op = " + ";
525 else if (first.equals("floatingSub") ||
526 first.equals("integralSub") || first.equals("-"))
527 op = " - ";
528
529 else if (first.equals("floatingMul") ||
530 first.equals("integralMul") || first.equals("*"))
531 op = " * ";
532 else if (first.equals("floatingDiv") ||
533 first.equals("integralDiv") || first.equals("/"))
534 op = " / ";
535 else if (first.equals("floatingMod") ||
536 first.equals("integralMod"))
537 op = " % ";
538 else if (first.equals("allocLT") || first.equals("floatingLT")
539 || first.equals("integralLT") || first.equals("lockLT")
540 || first.equals("<"))
541 op = " < ";
542 else if (first.equals("allocLE") || first.equals("floatingLE")
543 || first.equals("integralLE") || first.equals("lockLE")
544 || first.equals("<="))
545 op = " <= ";
546 else if (first.equals("floatingGT") ||
547 first.equals("integralGT") || first.equals(">"))
548 op = " > ";
549 else if (first.equals("floatingGE") ||
550 first.equals("integralGE") || first.equals(">="))
551 op = " >= ";
552 else if (first.equals("boolAnd") || first.equals("integralAnd"))
553 op = " && ";
554 else if (first.equals("boolOr") || first.equals("integralOr"))
555 op = " || ";
556 else if (first.equals("boolImplies"))
557 op = " ==> ";
558 else
559 return false;
560
561 out.print("(");
562 at(1).prettyPrint(out);
563 out.print(op);
564 at(2).prettyPrint(out);
565 out.print(")");
566 return true;
567 }
568 }
569
570 /**
571 * A simple test routine
572 */
573 public static void main(/*@ non_null @*/ String[] args) throws SExpTypeError {
574 make().print(System.out);
575 System.out.println();
576 make("a").print(System.out);
577 System.out.println();
578 make("a","b").print(System.out);
579 System.out.println();
580 make("a","b","c").print(System.out);
581 System.out.println();
582 make("a","b","c","d").print(System.out);
583 System.out.println();
584 make("a","b","c","d","e").print(System.out);
585 System.out.println();
586 make("a","b","c","d","e","f").print(System.out);
587 System.out.println();
588 make("a","b","c","d","e","f","g").print(System.out);
589 System.out.println();
590 make("a","b","c","d","e","f","g","h").print(System.out);
591 System.out.println();
592 System.out.println();
593
594 make("a", make("b", "c"), make("d", "e", make(), "f"))
595 .print(System.out);
596 System.out.println();
597
598 SExp[] elements = new SExp[10];
599 for (int i=0; i<10; i++)
600 elements[i] = SExp.make(i);
601 fromArray(elements).print(System.out);
602 System.out.println();
603 System.out.println();
604
605 make("a", "b").append(make()).append(make("c", "d", "e"))
606 .print(System.out);
607 System.out.println();
608
609 make("a", "b").addFront(SExp.fancyMake("front")).addEnd(SExp.make(42))
610 .print(System.out);
611 System.out.println();
612 }
613 }