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 }