    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    }