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    }