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 /*@ non_null 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 }