    001    /* Copyright 2000, 2001, Compaq Computer Corporation */
    002
    003    package escjava.prover;
    004
    005    import java.io.*;
    006
    007    /**
    008     * S-Expression datatype for use in interfacing to the ESC Theorem
    009     * prover, Simplify.
    010     *
    011     * <p> Considered as a language, the grammer of s-expressions is as
    012     * follows:
    013     * <pre>
    014     *   SExp ::= Atom | int | SList
    015     *   SList ::= ( SExp* )
    016     * </pre>
    017     *
    018     * <p> That is, s-expressions consist of either an atom, an integer,
    019     * or a possibly-empty list of s-expressions.  <code>Atom</code>s are
    020     * interned <code>String</code>s used to represent symbols. </p>
    021     *
    022     * <p> Methods are available to test whether an <code>SExp</code> is
    023     * an <code>Atom</code>, an integer, or a list.  If the "type" of an
    024     * <code>SExp</code> is known, it can be converted into what it
    025     * represents.  If an attempt is made to convert an <code>SExp</code>
    026     * to an incorrect "type", the checked exception
    027     * <code>SExpTypeError<code> will be thrown. </p>
    028     *
    029     * <p> <code>SExp</code>s can be printed onto a
    030     * <code>PrintStream</code>. </p>
    031     *
    032     * @see SExpTypeError
    033     * @see Atom
    034     * @see SList
    035     */
    036
    037    public abstract class SExp
    038    {
    039        // <code>SExp</code> may not be extended outside this package:
    040        /* package */ SExp() {};
    041
    042        /**
    043         * Return an S-expression representing a given integer.
    044         *
    045         * <p> This is faster than using <code>fancyMake(new
    046         * Integer(i))</code>. </p>
    047         */
    048        public static /*@ pure non_null @*/ SExp make(int i) {
    049            return SInt.fromInt(i);
    050        }
    051
    052        /**
    053         * Return an S-expression representing an integer (passed wrapped
    054         * in an <code>Integer</code>), an atom (specified via a
    055         * <code>String</code>), or an existing S-expression (this case
    056         * leaves the argument unchanged).
    057         */
    058        //@ public normal_behavior
    059        //@   requires \typeof(o) <: \type(String) || \typeof(o) <: \type(Integer) || \typeof(o) <: \type(SExp);
    060        //@   requires o != null;
    061        //@   ensures \result != null;
    062        //@ pure
    063        public static SExp fancyMake(Object o) {
    064            javafe.util.Assert.precondition(o != null);
    065            if (o instanceof SExp)
    066                return (SExp)o;
    067            else if (o instanceof String)
    068                return Atom.fromString((String)o);
    069            else if (o instanceof Integer)
    070                return SInt.fromInt(((Integer)o).intValue());
    071            else {
    072                javafe.util.Assert.fail(
    073                    "Non-String/Integer/SExp passed to SExp.make");
    074                return null;                // make compiler happy...
    075            }
    076        }
    077
    078        /**
    079         * Do we represent an atom?
    080         */
    081        //@ public normal_behavior
    082        //@   ensures !\result;
    083        public /*@ pure @*/ boolean isAtom() {
    084            return false;
    085        }
    086
    087        /**
    088         * @return a flag indicating if we represent an integer.
    089         */
    090        //@ public normal_behavior
    091        //@   ensures !\result;
    092        public /*@ pure @*/ boolean isInteger() {
    093            return false;
    094        }
    095
    096        /**
    097         * Do we represent a list?
    098         */
    099        //@ public normal_behavior
    100        //@   ensures !\result;
    101        public /*@ pure @*/ boolean isList() {
    102            return false;
    103        }
    104
    105        /**
    106         * If we represent an atom, return it as an <code>Atom</code>;
    107         * otherwise, throw {@link SExpTypeError}.
    108         */
    109        //@ public exceptional_behavior
    110        //@   signals (SExpTypeError) true;
    111        public /*@ pure @*/ Atom getAtom() throws SExpTypeError {
    112            throw new SExpTypeError();
    113        }
    114
    115        /**
    116         * If we represent an integer, return it as an <code>int</code>;
    117         * otherwise, throw an {@link SExpTypeError}.
    118         */
    119        //@ public exceptional_behavior
    120        //@   signals (SExpTypeError) true;
    121        public /*@ pure @*/ int getInteger() throws SExpTypeError {
    122            throw new SExpTypeError();
    123        }
    124
    125        /**
    126         * If we represent a list, return it as an <code>SList</code>;
    127         * otherwise, throw {@link SExpTypeError}.
    128         */
    129        //@ public exceptional_behavior
    130        //@   signals (SExpTypeError) true;
    131        public /*@ pure @*/ SList getList() throws SExpTypeError {
    132            throw new SExpTypeError();
    133        }
    134
    135        /**
    136         * Print a textual representation of us on a given
    137         * <code>PrintStream</code>.
    138         *
    139         * <p> Note: This routine will take a <code>PrintWriter</code>
    140         * instead when we switch to a more recent version of JDK. </p>
    141         */
    142        public abstract /*@ pure @*/ void print(/*@ non_null @*/ PrintStream out);
    143
    144        /**
    145         * Print a textual representation of us on {@link System#out}.
    146         *
    147         * <p> (This is a convenience function.) </p>
    148         */
    149        public /*@ pure @*/ void print() {
    150            print(System.out);
    151        }
    152
    153        /**
    154         * Pretty-print a textual representation of us on a given
    155         * <code>PrintStream</code>.
    156         *
    157         * <p> Note: This routine will take a <code>PrintWriter</code>
    158         * instead when we switch to a more recent version of JDK. </p>
    159         */
    160        public abstract /*@ pure @*/ void prettyPrint(/*@ non_null @*/ PrintStream out);
    161
    162        /**
    163         * @return a textual representation of this s-expression.
    164         */
    165        //@ also
    166        //@ public normal_behavior
    167        //@   ensures \result != null;
    168        public /*@ pure @*/ String toString() {
    169            ByteArrayOutputStream baos = new ByteArrayOutputStream();
    170            PrintStream ps = new PrintStream(baos);
    171            print(ps);
    172            String result = baos.toString();
    173            ps.close();
    174            return result;
    175        }
    176
    177        /**
    178         * A simple test routine
    179         */
    180        public static void main(String[] args) throws SExpTypeError {
    181            display(make(14));
    182
    183            display(fancyMake("hello"));
    184            display(fancyMake(new Integer(42)));
    185
    186            display(fancyMake(SList.make()));
    187            display(fancyMake(SList.make("NOT", make(0))));
    188            display(fancyMake(SList.make("a", "b", "c", "d", "e")));
    189
    190
    191            System.out.println(
    192                SList.make().equals(
    193                SList.make()));
    194
    195            System.out.println(
    196                SList.make("a", "b", "c", "d", "e").equals(
    197                SList.make("a", "b", "c", "d", "3")));
    198
    199            System.out.println(
    200                SList.make("a", "b", "c", "d", "e").equals(
    201                SList.make("a", "b", "c", "d", "f")));
    202
    203            System.out.println(
    204                SList.make("NOT", SExp.make(3)).equals(
    205                SList.make("NOT", SExp.make(2))));
    206
    207
    208            System.out.println(
    209                SList.make("NOT", SExp.make(3)).equals(
    210                SList.make("NOT", SExp.make(3))));
    211
    212
    213            // Intentionally invoke a SExpTypeError...
    214            System.out.println();
    215            System.out.println("Type error case:");
    216            make(14).getAtom();
    217        }
    218
    219        /**
    220         * Display a <code>SExp</code> verbosely, using all its accessor
    221         * methods.
    222         *
    223         * <p> This method is intended for test use. </p>
    224         */
    225        //-@ pure
    226        public static void display(/*@ non_null @*/ SExp x) throws SExpTypeError {
    227            if (x.isAtom()) {
    228                System.out.print("[Atom]  "+x.getAtom().toString());
    229            }
    230            if (x.isInteger()) {
    231                System.out.print("[int]  "+x.getInteger());
    232            }
    233            if (x.isList()) {
    234                SList l = x.getList();
    235                int n = l.length();
    236                System.out.print("[" + (l.isEmpty() ? "empty " : "") +
    237                                    n + "-element SList]  ");
    238                for (int i=0; i<n; i++) {
    239                    if (i!=0)
    240                        System.out.print(" ");
    241                    System.out.print("@" + i + "=");
    242                    l.at(i).print(System.out);
    243                }
    244            }
    245
    246            System.out.print("  =>  ");
    247            x.print(System.out);
    248            System.out.println();
    249        }
    250    }