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    }