    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    }