DPJRuntime
Class DPJArrayChar<region R>

java.lang.Object
  extended by DPJRuntime.DPJArrayChar<region R>
Type Parameters:
R - The region of a cell of this DPJArrayChar

public class DPJArrayChar<region R>
extends java.lang.Object

The DPJArray class, specialized to char.

The DPJArrayChar class wraps and provides a "view" of an ordinary Java array of char. In addition to array-element access, the DPJArrayChar class supports the creation of a subarray, which is a contiguous slice of the original array. The subarray itself is a new DPJArrayChar object. Both the original DPJArrayChar and the subarray wrap the same underlying Java array.

A DPJArrayChar stores a start position (indexed into the underlying array) and a length. Accesses to the DPJArrayChar are translated into accesses into the underlying array, offset by the start position. They are bounds-checked against the length of the DPJArrayChar. For example:

 // Create a Java array a of 10 char
 char[] a = new char[10];
 // Wrap a in a DPJArrayChar
 DPJArrayChar A = new DPJArrayChar(a);
 // Create a subarray of A
 DPJArrayChar B = A.subarray(5,2);
 // Store value 1 into position 5 of a
 B.put(0,1);
 // Error:  Out of bounds
 B.put(3,5);
 


Field Summary
 int length
          The number of elements in the DPJArrayChar
 int start
          The start index for indexing into the underlying array
 
Constructor Summary
DPJArrayChar(char[]<R> elts)
          Creates a DPJArrayChar that wraps the given Java array.
DPJArrayChar(int length)
          Creates a DPJArrayChar of the specified length, wrapping a freshly created Java array with the same length.
 
Method Summary
 char get(int idx)
          Returns the value stored at index idx of this DPJArrayChar.
 void put(int idx, char val)
          Replaces the value at index idx of this DPJArrayChar with value val.
 DPJArrayChar<R> subarray(int start, int length)
          Creates and returns a new DPJArrayChar starting at index start with length length that wraps the same underlying array as this DPJArrayChar.
 void swap(int i, int j)
          Swaps the values at indices i and j of this DPJArrayChar.
 char[]<R> toArray()
          Returns the underlying Java array for this DPJArrayChar.
 java.lang.String toString()
          Returns a string representation of this DPJArrayChar.
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
 

Field Detail

start

public final int start
The start index for indexing into the underlying array


length

public final int length
The number of elements in the DPJArrayChar

Constructor Detail

DPJArrayChar

public DPJArrayChar(int length)
             pure
Creates a DPJArrayChar of the specified length, wrapping a freshly created Java array with the same length.

Parameters:
length - The length of the DPJArrayChar

DPJArrayChar

public DPJArrayChar(char[]<R> elts)
             pure
Creates a DPJArrayChar that wraps the given Java array.

Parameters:
elts - The Java array to wrap
Method Detail

get

public char get(int idx)
         reads  R
Returns the value stored at index idx of this DPJArrayChar.

Throws ArrayIndexOutOfBoundsException if idx is outside the bounds of this DPJArrayChar (even if it is in bounds for the underlying array).

Parameters:
idx - Index of value to return
return - Value stored at idx

put

public void put(int idx,
                char val)
         writes R
Replaces the value at index idx of this DPJArrayChar with value val.

Throws ArrayIndexOutOfBoundsException if idx is outside the bounds of this DPJArrayChar (even if it is in bounds for the underlying array).

Parameters:
idx - Index of value to replace
val - New value

subarray

public DPJArrayChar<R> subarray(int start,
                                int length)
                         pure
Creates and returns a new DPJArrayChar starting at index start with length length that wraps the same underlying array as this DPJArrayChar. Index i of the new DPJArrayChar refers to the same cell of the underlying array as index start+i of this.

Throws ArrayIndexOutOfBoundsException if the interval start,start+length-1] is not in bounds for this DPJArrayChar.

Parameters:
start - Start index for the subarray
length - Length of the subarray
Returns:
Subarray of this DPJArrayChar defined by start and length

toArray

public char[]<R> toArray()
                        pure
Returns the underlying Java array for this DPJArrayChar.

Returns:
The underlying Java array

toString

public java.lang.String toString()
                          reads  R
Returns a string representation of this DPJArrayChar.

Overrides:
toString in class java.lang.Object
Returns:
A string representation

swap

public void swap(int i,
                 int j)
          writes R
Swaps the values at indices i and j of this DPJArrayChar.

Parameters:
i - First index to swap
j - Second index to swap