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    }