/* 
 * Kodkod -- Copyright (c) 2005-2011, Emina Torlak
 *
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * in the Software without restriction, including without limitation the rights
 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
 * copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 *
 * The above copyright notice and this permission notice shall be included in
 * all copies or substantial portions of the Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
 * THE SOFTWARE.
 */
package kodkod.util.ints;

import java.util.Collection;
import java.util.Iterator;

/**
 * <p>Represents a sparse sequence -- a sequence whose indices are not
 * necessarily contiguous.  For example, a sparse sequence can have
 * elements at indices 10, 2121, and 3000, without having any elements
 * in between.  This specification of sparse sequences also supports
 * negative indeces.  Formally, the following methods specify a partial
 * function from integers to values of type V.</p>
 * 
 * <p>Sequence implementations are not required to support mutation.
 * All mutating operations are optional and may 
 * throw an UnsupportedOperationException.</p>  
 * 
 * @specfield entries: int -> lone V
 * 
 * @author Emina Torlak
 */
public interface SparseSequence<V> extends Iterable<IndexedEntry<V>> {

	/**
	 * Returns the number of entries in this sequence.
	 * @return #this.entries
	 */
	public abstract int size();
	
	/**
	 * Returns true if this sequence is empty; otherwise returns false.
	 * @return no this.entries
	 */
	public abstract boolean isEmpty();
	
	/**
	 * Removes all entries from this sequences.
	 * @ensures no this.entries'
	 */
	public abstract void clear();
	
	/**
	 * Puts the given value at the specified index.  If the 
	 * sequence already mapped the index to a value, the 
	 * previous value is replaced with the new one and returned.
	 *
	 * @ensures this.entries' = this.entries + index->value
	 * @return this.entries[index]
	 * @throws IndexOutOfBoundsException  the given index
	 * is not valid for this sequence.
	 * @throws IllegalArgumentException  the given value cannot 
	 * be stored in this sequence.
	 */
	public abstract V put(int index, V value);
	
	/**
	 * Copies all of the entries from the specified sparse sequence to 
	 * this sequence. The effect of this call is equivalent to that of 
	 * calling put(e.index, e.value) on this sequence once for each entry 
     * e in the specified sequence. 
     * @ensures this.entries' = this.entries ++ s.entries
     * @throws IndexOutOfBoundsException  s contains indeces that are
     * not valid for this sequence.
     * @throws IllegalArgumentException  s contains a value that cannot
     * be stored in this sequence.
	 */
	public abstract void putAll(SparseSequence<? extends V> s);
	
	
	/**
	 * Returns the value to which this sequence maps the given
	 * index.  If the index is not mapped, null is returned.
	 * @return this.entries[index]
	 */
	public abstract V get(int index);
	
	/**
	 * Removes the entry with the given index, if it exists, and
	 * returns the value previously stored at the index.  If the
	 * sequence had no previous mapping for the index, null is returned.
	 * @ensures this.entries' = this.entries - index->E
	 * @return this.entries[index]
	 */
	public abstract V remove(int index);
	
	/**
	 * Returns true if this sparse sequence has an entry for the
	 * given index; otherwise returns false.
	 * @return some this.entries[index]
	 */
	public abstract boolean containsIndex(int index);
	
	/**
	 * Returns the set of all indices mapped by this sparse sequence.
	 * The returned set supports removal iff this is not an unmodifiable
	 * sparse sequence.  The returned set may be uncloneable.
	 * @return {s: IntSet | s.ints = this.entries.V}
	 */
	public abstract IntSet indices();
	
	/**
	 * Returns true if this sequence has an entry with the given value;
	 * otherwise returns false.
	 * @return some this.entries.value
	 */
	public abstract boolean contains(Object value);
	
	/**
	 * Returns a Collection view of the values stored in this sequence.
	 * The returned collection supports removal iff this is not an
	 * unmodifiable sparse sequence.
	 * @return {c: Collection | c.size()=this.size() && 
	 *          all v: V | c.contains(v) <=> this.contains(v) }
	 */
	public abstract Collection<V> values();
	
	/**
	 * Returns an iterator over the entries in this sequence
	 * in the ascending order of indeces, starting at this.first().
	 * @return an iterator over this.entries starting at the entry
	 * with the smallest index
	 */
	public abstract Iterator<IndexedEntry<V>> iterator();
	
	/**
	 * Returns an iterator over the entries in this sequence,
	 * whose indeces are between from and to.  If from < to, 
	 * the entries are returned in the ascending order of 
	 * indeces.  Otherwise, they are returned in the descending
	 * order of indeces.
	 * @return an iterator over the entries in this sequence
	 * whose indeces are between from and to.  Formally, if 
	 * from < to, then the first and last entries returned
	 * by the iterator are this.ceil(from) and this.floor(to).
	 * Otherwise, they are this.floor(from) and this.ceil(to).
	 */
	public abstract Iterator<IndexedEntry<V>> iterator(int from, int to);
	
	/**
	 * Returns the entry with the smallest index.  If the sequence
	 * is empty, returns null.
	 * @return {e: IndexedEntry | e.index = min(this.entries.E) && 
	 *                            e.value = this.entries[e.index] }
	 */
	public abstract IndexedEntry<V> first();
	
	/**
	 * Returns the entry with the largest index.  If the sequence
	 * is empty, returns null.
	 * @return {e: IndexedEntry | e.index = max(this.entries.E) && 
	 *                            e.value = this.entries[e.index] }
	 */
	public abstract IndexedEntry<V> last();
	
	/**
	 * If an entry for the given index exists, it is returned.  Otherwise, 
	 * successor(index) is returned.
	 * @return this.containsIndex(index) => 
	 *          {e: IndexedEntry | e.index = index && e.value = this.entries[index] }, 
	 *          successor(index)
	 */
	public abstract IndexedEntry<V> ceil(int index);
	
	/**
	 * If an entry for the given index exists, it is returned.  Otherwise, 
	 * predecessor(index) is returned.
	 * @return this.containsIndex(index) => 
	 *          {e: IndexedEntry | e.index = index && e.value = this.entries[index] }, 
	 *          predecessor(index)
	 */
	public abstract IndexedEntry<V> floor(int index);
	
	/**
	 * Compares the specified object with this sequence for equality. 
	 * Returns true if the given object is also a sparse sequence and the two 
	 * sequences have the same entries. More formally, two sequences t1 and t2 have the 
	 * the same entries if they represent the same function from integers to values: i.e.
	 * t1.entries = t2.entries. This ensures that the equals method works properly across 
	 * different implementations of the SparseSequence interface.
	 * @return o in SparseSequence && o.entries = this.entries
	 */
	public abstract boolean equals(Object o);
	
	/**
	 * Returns the hash code value for this sparse sequence. 
	 * A hash function for a sparse sequence must ensure that t1.equals(t2) 
	 * implies that t1.hashCode()==t2.hashCode() for any two sequences t1 and t2, 
	 * as required by the general contract of Object.hashCode.
	 * @return hash code for this sparse sequence
	 */
	public abstract int hashCode();
	
	/**
	 * Returns a copy of this sparse sequence.  The copy is independent of this 
	 * sequence unless this is a singleton or immutable, in which case
	 * clone() may return this.  An implementing class that does not support
	 * cloning may throw a CloneNotSupportedException.
	 * @return a copy of this sparse sequence.
	 * @throws CloneNotSupportedException  this is not cloneable
	 */
	public abstract SparseSequence<V> clone() throws CloneNotSupportedException;
	
}
