001 /* Copyright 2000, 2001, Compaq Computer Corporation */
002
003 package escjava.prover;
004
005
006 import java.util.Hashtable;
007 import java.io.*;
008
009
010 /**
011 ** <code>Atom</code>s are S-expressions representing symbols. <p>
012 **
013 ** Interned <code>String</code>s are used to represent symbols.
014 ** Accordingly, two <code>Atom</code>s are equal (via <code>==</code>)
015 ** iff they represent the same symbol.<p>
016 **/
017
018 final public class Atom extends SExp {
019
020 /***************************************************
021 * *
022 * Class fields: *
023 * *
024 ***************************************************/
025
026 /**
027 ** Our map from interned <code>String</code>s to already created
028 ** non-null <code>Atom</code>s.
029 **/
030 //@ invariant map != null;
031 //+@ invariant map.keyType == \type(String);
032 //+@ invariant map.elementType == \type(Atom);
033 //@ spec_public
034 static private Hashtable map = new Hashtable(200);
035
036
037 /***************************************************
038 * *
039 * Instance fields: *
040 * *
041 ***************************************************/
042
043 /**
044 ** The symbol we represent; always already interned.
045 **/
046 //@ invariant value != null;
047 //@ spec_public
048 private String value;
049
050
051 /***************************************************
052 * *
053 * Creation: *
054 * *
055 ***************************************************/
056
057 /**
058 ** Create an <code>Atom</code> representing a given
059 ** symbol. Clients are allowed to create
060 ** <code>Atom</code>s only by calling <code>fromString</code> so we can
061 ** intern.<p>
062 **
063 ** Precondition: <code>symbol</code> must already have been
064 ** interned.<p>
065 **/
066 //@ requires symbol != null;
067 private Atom(String symbol) {
068 value = symbol;
069
070 //+@ set map.keyType = \type(String);
071 //+@ set map.elementType = \type(Atom);
072
073 map.put(value, this); // Save us in the interning table
074 }
075
076 /**
077 ** Create a <code>Atom</code> representing a given symbol. <p>
078 **
079 ** This function always returns the same <code>Atom</code> when
080 ** called on equal <code>String</code>s.<p>
081 **/
082 //@ requires symbol != null;
083 //@ ensures \result != null;
084 public static Atom fromString(String symbol) {
085 String key = symbol.intern();
086 Atom existing = (Atom)map.get(key);
087 if (existing != null)
088 return existing;
089 return new Atom(key);
090 }
091
092
093 /***************************************************
094 * *
095 * Simple Accessors: *
096 * *
097 ***************************************************/
098
099 /**
100 ** Do we represent an atom?
101 **/
102 public boolean isAtom() {
103 return true;
104 }
105
106
107 /**
108 ** If we represent an atom, return it as an <code>Atom</code>; otherwise,
109 ** throw <code>SExpTypeError</code>.
110 **/
111 public Atom getAtom() {
112 return this;
113 }
114
115
116 /**
117 ** Return the interned <code>String</code> for the symbol we
118 ** represent.
119 **/
120 public /*@non_null*/String toString() {
121 return value;
122 }
123
124
125 /**
126 ** Return true if this atom and object o are the same atom.
127 **/
128 public boolean equals(Object o) {
129 return this == o;
130 }
131
132 /***************************************************
133 * *
134 * Printing: *
135 * *
136 ***************************************************/
137
138 /**
139 ** The list of special symbols that don't need to be quoted when by
140 ** themselves.
141 **/
142 //@ invariant special != null;
143 public final static String special = "!#$%&*+-./:<=>?@[]^_{}";
144
145
146 /**
147 ** Returns the printable version (e.g., with escape codes added as
148 ** needed) of an S-expression symbol's name.
149 **/
150 //@ requires symbol != null;
151 public static String printableVersion(String symbol) {
152 if (symbol.equals(""))
153 return "||";
154
155 // Determine if symbol fits <alpha><alphanumeric>*:
156 boolean identifier = true;
157 for (int i=0; i<symbol.length(); i++) {
158 char c = symbol.charAt(i);
159 if ((c>='a' && c<='z') || (c>='A' && c<='Z') || (c=='_'))
160 continue;
161 if (c>='0' && c<='9' && i>0)
162 continue;
163 identifier = false; break;
164 }
165
166 if (identifier)
167 return symbol;
168
169
170 // Determine if symbol fits <special>+:
171 boolean operator = true;
172 for (int i=0; i<symbol.length(); i++) {
173 char c = symbol.charAt(i);
174 if (special.indexOf(c)==-1) {
175 operator = false;
176 break;
177 }
178 }
179
180 if (operator)
181 return symbol;
182
183 // don't escape a symbol that is already escaped
184 if (symbol.startsWith("|") && symbol.endsWith("|")) {
185 return symbol;
186 }
187
188 // Deal with escape codes later... HACK!!!!
189 return "|" + symbol + "|";
190 }
191
192
193 /**
194 ** Print a textual representation of us on a given
195 ** <code>PrintStream</code>. <p>
196 **
197 ** Note: This routine will take a <code>PrintWriter</code> instead
198 ** when we switch to a more recent version of JDK.<p>
199 **/
200 public void print(/*@non_null*/PrintStream out) {
201 out.print(printableVersion(value));
202 }
203
204
205 /**
206 ** Pretty print a textual representation of us on a given
207 ** <code>PrintStream</code>. <p>
208 **
209 ** Note: This routine will take a <code>PrintWriter</code> instead
210 ** when we switch to a more recent version of JDK.<p>
211 **/
212 public void prettyPrint(/*@non_null*/PrintStream out) {
213 out.print(value);
214 }
215
216
217 /***************************************************
218 * *
219 * Test methods: *
220 * *
221 ***************************************************/
222
223 /**
224 ** A simple test routine
225 **/
226 public static void main(String[] args) {
227 Atom a1 = fromString("a");
228 Atom b = fromString("b");
229 Atom a2 = fromString("a"+"");
230
231 System.out.println("same: " + (a1==a2));
232 System.out.println("different: " + (a1==b));
233 System.out.println();
234
235 fromString("").print(System.out); System.out.println();
236 System.out.println();
237
238 // identifiers:
239 fromString("abcde").print(System.out); System.out.println();
240 fromString("a253").print(System.out); System.out.println();
241 fromString("a2b3c4de").print(System.out); System.out.println();
242 fromString("a124b234").print(System.out); System.out.println();
243 System.out.println();
244
245 // non-identifiers:
246 fromString("1abcd").print(System.out); System.out.println();
247 fromString("ab+d").print(System.out); System.out.println();
248 fromString("-a2b3c4de").print(System.out); System.out.println();
249 System.out.println();
250 System.out.println();
251
252
253 // operators:
254 fromString(special).print(System.out); System.out.println();
255 fromString("=>").print(System.out); System.out.println();
256 fromString("<==>").print(System.out); System.out.println();
257 fromString("+").print(System.out); System.out.println();
258 System.out.println();
259
260 // non-operators:
261 fromString("~").print(System.out); System.out.println();
262 fromString("=~>").print(System.out); System.out.println();
263 fromString("a+").print(System.out); System.out.println();
264 fromString("~==+").print(System.out); System.out.println();
265 System.out.println();
266
267 // Test escape codes later...
268 }
269 }