/* 
 * 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.instance;

import java.util.Arrays;
import java.util.Collection;
import java.util.HashMap;
import java.util.Iterator;
import java.util.Map;

import kodkod.util.collections.Containers;

/** 
 * <p>Represents an ordered set of unique atoms.  Objects used as atoms <b>must</b> properly  
 * implement {@link java.lang.Object#equals equals} and {@link java.lang.Object#hashCode hashCode}
 * methods.  The behavior of a universe is not specified if the value of an object is changed in a 
 * manner that affects equals comparisons while the object is an atom in the universe.</p>
 * 
 * <p>Each universe provides a {@link kodkod.instance.TupleFactory tuple factory}
 * to facilitate creation of {@link kodkod.instance.Tuple tuples} and 
 * {@link kodkod.instance.TupleSet sets of tuples} based on the atoms in the universe.</p>
 * 
 * <p><b>Implementation Note:</b> although the atoms in a universe are not interpreted in any
 * way by the Kodkod engine, it is strongly recommended that the atoms
 * of the same 'type' be grouped together.  For instance, suppose that a client model is specified in
 * terms of disjoint types Person = {Person0, Person1, Person2} and Dog = {Dog0, Dog1}.  Then, 
 * the client may observe an improvement in performance if he constructs the universe over the
 * sequences {Person0, Person1, Person2, Dog0, Dog1} or {Dog0, Dog1, Person0, Person1, Person2} rather
 * than any other permutation of these five atoms.
 * 
 * @specfield size: int
 * @specfield atoms: [0..size)->one Object
 * @specfield factory: TupleFactory
 * @invariant factory = (TupleFactory<:universe).this
 * @invariant size > 0
 * @author Emina Torlak 
 */
public final class Universe implements Iterable<Object> {
	private final Object[] atoms;
	private final Map<Object,Integer> indices;
	private final TupleFactory factory;
	
	/**  
	 * Constructs a new Universe consisting of the given atoms, in the order that they are returned 
	 * by the specified Collection's Iterator.
	 * 
	 * @ensures this.size' = atoms.size && this.atoms' = atoms.iterator
	 * @throws NullPointerException  atoms = null 
	 * @throws IllegalArgumentException  atoms contains duplicates
	 * @throws IllegalArgumentException  atoms is empty
	 */
	public Universe(Collection<?> atoms) {
		if (atoms.isEmpty()) throw new IllegalArgumentException("Cannot create an empty universe.");
		this.atoms = new Object[atoms.size()];
		this.indices = new HashMap<Object, Integer>();
		int i = 0;
		for (Object atom : atoms) {
			if (indices.containsKey(atom))
				throw new IllegalArgumentException(atom + " appears multiple times."); 
			indices.put(atom, i); 
			this.atoms[i] = atom;
			i++;
		}
		this.factory = new TupleFactory(this);
	}
	
	/**  
	 * Constructs a new Universe consisting of the given atoms, in the order that they appear 
	 * in the specified array
	 * 
	 * @ensures this.size' = atoms.length && this.atoms' = atoms
	 * @throws NullPointerException  atoms = null 
	 * @throws IllegalArgumentException  atoms contains duplicates
	 * @throws IllegalArgumentException  atoms is empty
	 */
	public Universe(Object...atoms) { 
		if (atoms.length==0) throw new IllegalArgumentException("Cannot create an empty universe.");
		this.atoms = Containers.copy(atoms, new Object[atoms.length]);
		this.indices = new HashMap<Object, Integer>();
		for (int i = 0; i < atoms.length; i++) {
			if (indices.containsKey(atoms[i]))
				throw new IllegalArgumentException(atoms[i] + " appears multiple times."); 
			indices.put(atoms[i], i);	              	
		}
		this.factory = new TupleFactory(this);
	}
	
	/**
//	 * Returns a universe that stores the given atoms explicitly, in the specified order.
//	 * The returned universe provides constant time index and atom lookup.
//	 * @ensures { u: Universe | u.size = atoms.length && u.atoms = atoms }
//	 * @throws IllegalArgumentException  atoms contains duplicates
//	 * @throws IllegalArgumentException  atoms is empty  
//	 */
//	public static Universe universe(Object...atoms) { return new ExplicitUniverse(atoms); }
//	
//	/**
//	 * Returns a universe that stores the given atoms explicitly, in the order in which they 
//	 * are returned by the collection's iterator.  The returned universe provides constant 
//	 * time index and atom lookup.
//	 * @ensures { u: Universe | u.size = atoms.size() && u.atoms[int] = atoms }
//	 * @throws IllegalArgumentException  atoms contains duplicates
//	 * @throws IllegalArgumentException  atoms is empty  
//	 */
//	public static Universe universe(Collection<?> atoms) { return new ExplicitUniverse(atoms); }
	
	/**
	 * Returns a TupleFactory that can be used to construct tuples and sets
	 * of tuples based on this universe.
	 * @return this.factory
	 */
	public TupleFactory factory() { return this.factory; }
	
	/**
	 * Returns the size of this universe
	 *
	 * @return #this.atoms
	 */
	public int size() { return atoms.length; }
	
	/**
	 * Returns true if atom is in this universe, otherwise returns false.
	 *
	 * @return atom in this.atoms[int]
	 */
	public boolean contains(Object atom) { return indices.containsKey(atom); }
	
	/**
	 * Returns the i_th atom in this universe
	 * 
	 * @return this.atoms[i]
	 * @throws IndexOutOfBoundsException  i < 0 || i >= this.size
	 */
	public Object atom(int index) { 
		if (index<0||index>=atoms.length) throw new IndexOutOfBoundsException();
		return atoms[index];
	}
	
	/**
	 * Returns the index of the specified atom in this universe; if the
	 * atom is not in this universe, an IllegalArgumentException is thrown.
	 * 
	 * @return this.atoms.atom
	 * @throws IllegalArgumentException  no this.atoms.atom
	 */
	public int index(Object atom) { 
		if (indices.containsKey(atom)) return indices.get(atom);
		else throw new IllegalArgumentException("no this.atoms." + atom);
	}
	
	/**
	 * Returns an iterator over atoms in this universe, according to their
	 * order in the universe.
	 * @return an iterator over atoms in this universe, according to their
	 * order in the universe
	 */
	public Iterator<Object> iterator() {
		return Containers.iterate(atoms);
	}
	
	/**
	 * Returns a string representation of this universe.
	 * @return string representation of this universe.
	 */
	public String toString() { 
		return Arrays.toString(atoms);
	}
	
}
