|
ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved |
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Objectescjava.prover.SExp
S-Expression datatype for use in interfacing to the ESC Theorem prover, Simplify.
Considered as a language, the grammer of s-expressions is as follows:
SExp ::= Atom | int | SList SList ::= ( SExp* )
That is, s-expressions consist of either an atom, an integer,
or a possibly-empty list of s-expressions. Atom
s are
interned String
s used to represent symbols.
Methods are available to test whether an SExp
is
an Atom
, an integer, or a list. If the "type" of an
SExp
is known, it can be converted into what it
represents. If an attempt is made to convert an SExp
to an incorrect "type", the checked exception
SExpTypeError
will be thrown.
SExp
s can be printed onto a
PrintStream
.
SExpTypeError
,
Atom
,
SList
Constructor Summary | |
(package private) |
SExp()
|
Method Summary | |
static void |
display(SExp x)
Display a SExp verbosely, using all its accessor
methods.
|
static SExp |
fancyMake(java.lang.Object o)
Return an S-expression representing an integer (passed wrapped in an Integer ), an atom (specified via a
String ), or an existing S-expression (this case
leaves the argument unchanged). |
Atom |
getAtom()
If we represent an atom, return it as an Atom ;
otherwise, throw SExpTypeError . |
int |
getInteger()
If we represent an integer, return it as an int ;
otherwise, throw an SExpTypeError . |
SList |
getList()
If we represent a list, return it as an SList ;
otherwise, throw SExpTypeError . |
boolean |
isAtom()
Do we represent an atom? |
boolean |
isInteger()
|
boolean |
isList()
Do we represent a list? |
static void |
main(java.lang.String[] args)
A simple test routine |
static SExp |
make(int i)
Return an S-expression representing a given integer. |
abstract void |
prettyPrint(java.io.PrintStream out)
Pretty-print a textual representation of us on a given PrintStream .
|
void |
print()
Print a textual representation of us on System.out .
|
abstract void |
print(java.io.PrintStream out)
Print a textual representation of us on a given PrintStream .
|
java.lang.String |
toString()
|
Methods inherited from class java.lang.Object |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait |
Constructor Detail |
SExp()
Method Detail |
public static SExp make(int i)
This is faster than using fancyMake(new
Integer(i))
.
public static SExp fancyMake(java.lang.Object o)
Integer
), an atom (specified via a
String
), or an existing S-expression (this case
leaves the argument unchanged).
public boolean isAtom()
public boolean isInteger()
public boolean isList()
public Atom getAtom() throws SExpTypeError
Atom
;
otherwise, throw SExpTypeError
.
SExpTypeError
public int getInteger() throws SExpTypeError
int
;
otherwise, throw an SExpTypeError
.
SExpTypeError
public SList getList() throws SExpTypeError
SList
;
otherwise, throw SExpTypeError
.
SExpTypeError
public abstract void print(java.io.PrintStream out)
PrintStream
.
Note: This routine will take a PrintWriter
instead when we switch to a more recent version of JDK.
public void print()
System.out
.
(This is a convenience function.)
public abstract void prettyPrint(java.io.PrintStream out)
PrintStream
.
Note: This routine will take a PrintWriter
instead when we switch to a more recent version of JDK.
public java.lang.String toString()
public static void main(java.lang.String[] args) throws SExpTypeError
SExpTypeError
public static void display(SExp x) throws SExpTypeError
SExp
verbosely, using all its accessor
methods.
This method is intended for test use.
SExpTypeError
|
ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved |
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |