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

escjava.prover
Class SList

java.lang.Object
  extended byescjava.prover.SExp
      extended byescjava.prover.SList
Direct Known Subclasses:
SNil, SPair

public abstract class SList
extends SExp

SLists represent possibly-empty lists of SExps.

Creation

As a convenience, lists of fewer than 9 elements may be created directly by calling SList.make on the desired elements. E.g., SList.make(x, y) creates the list (x y) where x and y are the contents of the SExp variables x and y. Longer lists may be created either from arrays (see fromArray) or by combining shorter lists via append.

As a further convenience, SList.make calls SExp.fancyMake(Object) on its arguments before placing them in the resulting list. This means that Atoms may be specified by a String holding their name and that S-expression integers may be specified by Integers. E.g., SList.make("NEG", new Integer(1)) represents the S-expression (NEG, 1).

SLists may not contain null elements.

Inspection

SLists can be tested to see if they are empty, can have their length determined, and can have their i-index element extracted. (If an attempt is made to extract a non-existent element, SExpTypeError will be thrown.)

Manipulation

S-expressions are currently immutable; accordingly all manipulation methods act functionally. S-expressions may be made mutable later via the addition of mutation methods.

SLists can be appended to each other. Elements can also be added to the front or end of a list.

Implementation

SLists are currently implemented via pairs and a nil object a la Lisp. These are provided by the non-public classes SPair and SNil. This implementation is subject to change at any time; clients should rely only on the publically-provided interface of this class.

See Also:
SNil, SPair
Todo:
kiniry 14 March 2003 - Add a list model.

Constructor Summary
(package private) SList()
          SList may not be extended outside this package.
 
Method Summary
 SList addEnd(SExp x)
           
 SList addFront(SExp x)
           
 SList append(SList x)
           
 SExp at(int i)
           
static SList fromArray(SExp[] a)
           
 SList getList()
          If we represent a list, return it as an SList; otherwise, throw SExpTypeError.
(package private)  SPair getPair()
          If we represent a non-empty list, return it as a SPair; otherwise, throw SExpTypeError.
abstract  boolean isEmpty()
           
 boolean isList()
          Do we represent a list?
abstract  int length()
           
static void main(java.lang.String[] args)
          A simple test routine
static SList make()
           
static SList make(java.lang.Object a1)
           
static SList make(java.lang.Object a1, java.lang.Object a2)
           
static SList make(java.lang.Object a1, java.lang.Object a2, java.lang.Object a3)
           
static SList make(java.lang.Object a1, java.lang.Object a2, java.lang.Object a3, java.lang.Object a4)
           
static SList make(java.lang.Object a1, java.lang.Object a2, java.lang.Object a3, java.lang.Object a4, java.lang.Object a5)
           
static SList make(java.lang.Object a1, java.lang.Object a2, java.lang.Object a3, java.lang.Object a4, java.lang.Object a5, java.lang.Object a6)
           
static SList make(java.lang.Object a1, java.lang.Object a2, java.lang.Object a3, java.lang.Object a4, java.lang.Object a5, java.lang.Object a6, java.lang.Object a7)
           
static SList make(java.lang.Object a1, java.lang.Object a2, java.lang.Object a3, java.lang.Object a4, java.lang.Object a5, java.lang.Object a6, java.lang.Object a7, java.lang.Object a8)
           
 void prettyPrint(java.io.PrintStream out)
          Pretty-print a textual representation of us on a given PrintStream.
 void print(java.io.PrintStream out)
          Print a textual representation of us on a given PrintStream.
static SList reverseD(SList l)
          Destructive list reversal
 void setAt(int i, SExp s)
          Modify the list in place by set the ith element to s.
private  boolean specialPrint(java.io.PrintStream out)
          Specially print a textual representation of us on a given PrintStream.
 
Methods inherited from class escjava.prover.SExp
display, fancyMake, getAtom, getInteger, isAtom, isInteger, make, print, toString
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
 

Constructor Detail

SList

SList()
SList may not be extended outside this package.

Method Detail

make

public static SList make()
Returns:
a S-expression representing the empty list.

make

public static SList make(java.lang.Object a1)
Returns:
a S-expression representing a 1-element list whose contents are the result of applying SExp.fancyMake(Object) to our arguments.

make

public static SList make(java.lang.Object a1,
                         java.lang.Object a2)
Returns:
a S-expression representing a 2-element list whose contents are the result of applying SExp.fancyMake(Object) to our arguments.

make

public static SList make(java.lang.Object a1,
                         java.lang.Object a2,
                         java.lang.Object a3)
Returns:
a S-expression representing a 3-element list whose contents are the result of applying SExp.fancyMake(Object) to our arguments.


make

public static SList make(java.lang.Object a1,
                         java.lang.Object a2,
                         java.lang.Object a3,
                         java.lang.Object a4)
Returns:
a S-expression representing a 4-element list whose contents are the result of applying SExp.fancyMake(Object) to our arguments.


make

public static SList make(java.lang.Object a1,
                         java.lang.Object a2,
                         java.lang.Object a3,
                         java.lang.Object a4,
                         java.lang.Object a5)
Returns:
a S-expression representing a 5-element list whose contents are the result of applying SExp.fancyMake(Object) to our arguments.


make

public static SList make(java.lang.Object a1,
                         java.lang.Object a2,
                         java.lang.Object a3,
                         java.lang.Object a4,
                         java.lang.Object a5,
                         java.lang.Object a6)
Returns:
a S-expression representing a 6-element list whose contents are the result of applying SExp.fancyMake(Object) to our arguments.


make

public static SList make(java.lang.Object a1,
                         java.lang.Object a2,
                         java.lang.Object a3,
                         java.lang.Object a4,
                         java.lang.Object a5,
                         java.lang.Object a6,
                         java.lang.Object a7)
Returns:
a S-expression representing a 7-element list whose contents are the result of applying SExp.fancyMake(Object) to our arguments.


make

public static SList make(java.lang.Object a1,
                         java.lang.Object a2,
                         java.lang.Object a3,
                         java.lang.Object a4,
                         java.lang.Object a5,
                         java.lang.Object a6,
                         java.lang.Object a7,
                         java.lang.Object a8)
Returns:
a S-expression representing a 8-element list whose contents are the result of applying SExp.fancyMake(Object) to our arguments.

fromArray

public static SList fromArray(SExp[] a)
Returns:
a S-expression representing a list whose contents are the contents of a given array.

isList

public boolean isList()
Description copied from class: SExp
Do we represent a list?

Overrides:
isList in class SExp

getList

public SList getList()
Description copied from class: SExp
If we represent a list, return it as an SList; otherwise, throw SExpTypeError.

Overrides:
getList in class SExp

isEmpty

public abstract boolean isEmpty()
Returns:
a flag indicating if we are we an empty list.

length

public abstract int length()
Returns:
our length.

getPair

SPair getPair()
        throws SExpTypeError
If we represent a non-empty list, return it as a SPair; otherwise, throw SExpTypeError.

Throws:
SExpTypeError

at

public SExp at(int i)
        throws SExpTypeError
Returns:
our element at index i (indices start at 0). If we are not long enough to have an element at that index, then SExpTypeError is thrown.
Throws:
SExpTypeError

setAt

public void setAt(int i,
                  SExp s)
           throws SExpTypeError
Modify the list in place by set the ith element to s.

Throws:
SExpTypeError

append

public SList append(SList x)
Returns:
the functional result of appending another list to us.

reverseD

public static SList reverseD(SList l)
Destructive list reversal


addFront

public SList addFront(SExp x)
Returns:
the functional result of adding a given element at the front of us. Precondition: x is non-null.


addEnd

public SList addEnd(SExp x)
Returns:
the functional result of adding a given element at the end of us.

This function is likely to be slower than addFront.


print

public void print(java.io.PrintStream out)
Print a textual representation of us on a given PrintStream.

Note: This routine will take a PrintWriter instead when we switch to a more recent version of JDK.

Specified by:
print in class SExp

prettyPrint

public void prettyPrint(java.io.PrintStream out)
Pretty-print a textual representation of us on a given PrintStream.

Note: This routine will take a PrintWriter instead when we switch to a more recent version of JDK.

Specified by:
prettyPrint in class SExp

specialPrint

private boolean specialPrint(java.io.PrintStream out)
                      throws SExpTypeError
Specially print a textual representation of us on a given PrintStream. This is a subroutine used in pretty-printing.

Note: This routine will take a PrintWriter instead when we switch to a more recent version of JDK.

Throws:
SExpTypeError

main

public static void main(java.lang.String[] args)
                 throws SExpTypeError
A simple test routine

Throws:
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

The ESC/Java2 Project Homepage