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 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(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(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 }