/*
 * class String
 */
class String {
  private char[] chars;

  public String( char[] chars ) {
    this.chars = chars;
  }

  public int length() {
    return chars.length;
  }

  public char charAt( int i ) {
    if ( 0 <= i && i < chars.length )
      return chars[ i ];

    else {
      throwRuntimeError( "ParameterOutOfBounds", "i", "" + i );

      return (char) 0;
    }
  }

  public int indexOf( char c ) {
    for ( int i=0; i<chars.length; i++ )
      if ( chars[ i ] == c )
        return i;

    return -1;
  }

  public native int indexOf( String s );

  public boolean contains( String s ) {
    return indexOf( s ) >= 0;
  }

  public String replace( char oldChar, char newChar ) {
    char[] newChars = new char[ chars.length ];

    for ( int i=0; i<chars.length; i++ )
      if ( chars[ i ] == oldChar )
        newChars[ i ] = newChar;
      else
        newChars[ i ] = chars[ i ];

    return new String( newChars );
  }

  public String substring( int start, int end ) {
    if ( start < 0 || start >= chars.length || start >= end )
      throwRuntimeError( "ParameterOutOfBounds", "start", "" + start );
    
    if ( end < 0 || end > chars.length )
      throwRuntimeError( "ParameterOutOfBounds", "end", "" + end );

    // INV: start < end

    char[] sub = new char[ end - start ];

    for ( int i=0; i<sub.length; i++ )
      sub[ i ] = chars[ start + i ];

    return new String( sub );
  }

  public String substring( int start ) {
    return this.substring( start, length() );
  }

  public native String toLowerCase();

  public native String toUpperCase();

  public native String trim();

  public int compareTo( String other ) {
    if ( other == null )
      throwRuntimeError( "ParameterOutOfBounds", "other", "" + other );
  
    int commonLength = min( this.length(), other.length() );
  
    for ( int i=0; i < commonLength; i++ )
      if ( this.charAt( i ) != other.charAt( i ) )
        return (int) this.charAt( i ) - (int) other.charAt( i );
      
    if ( this.length() != other.length() )
      return this.length() - other.length();
    else
      return 0;
  }

  public boolean equals( Object obj ) {
    if ( obj instanceof String )
      return compareTo( (String) obj ) == 0;
    else
      return super.equals( obj );
  }

  public boolean equalsIgnoreCase( String other ) {
    String t1 = this.toLowerCase();
    String t2 = other.toLowerCase();

    return t1.compareTo( t2 ) == 0;
  }

  public native int hashCode();

  public String toString() {
    return this;
  }
}
