/**
 *  Description of the Class
 *
 * @author     Marc Champesme
 * @version    7 décembre 2004
 */
public class PureListeElem {
	private CellElem _premiereCellule;
	private int _nbElements;


	/**
	 *  Constructeur pouvant se substituer à l'opération listevide.
	 *
	 * @return    Description of the Return Value
	 */
	/*@
	  @ ensures estVide();
	  @*/
	public PureListeElem() { }


	/**
	 *  Description of the Method
	 *
	 * @return    Description of the Return Value
	 */
	/*@
	  @ ensures \result != null;
	  @ ensures \result != this;
	  @
	  @ pure
	  @*/
	private PureListeElem copie() {
		PureListeElem result = new PureListeElem();

		if (!estVide()) {
			result._premiereCellule = new CellElem(premier());
			result._nbElements = 1;

			if (_premiereCellule.hasNext()) {
				CellElem celluleCouranteThis;
				CellElem celluleCouranteResult = result._premiereCellule;

				for (celluleCouranteThis = _premiereCellule.getNext();
					celluleCouranteThis.hasNext();
					celluleCouranteThis = celluleCouranteThis.getNext()) {
					CellElem newCell = new CellElem(celluleCouranteThis.getEntry());
					celluleCouranteResult.setNext(newCell);
					result._nbElements++;
					celluleCouranteResult = newCell;
				}
				//@ assume result._nbElements == (_nbElements - 1);
				//@ assume celluleCouranteThis != null;
				//@ assume !celluleCouranteThis.hasNext();

				// Ajout de la derniere cellule
				celluleCouranteResult.setNext(new CellElem(celluleCouranteThis.getEntry()));
				result._nbElements++;
			}
		}

		return result;
	}


	/**
	 *  Adds a feature to the PureListeElem object
	 *
	 * @param  elt  The feature to be added
	 * @return      Description of the Return Value
	 */
	/*@
	  @ ensures \result != null;
	  @ ensures !\result.estVide();
	  @ ensures \result.premier() == elt;
	  @ ensures \result.longueur() == (longueur() + 1);
	  @
	  @ pure
	  @*/
	public PureListeElem cons(Elem elt) {
		PureListeElem result = new PureListeElem();

		result._premiereCellule = new CellElem(elt);
		result._nbElements = _nbElements + 1;
		if (!estVide()) {
			PureListeElem copieThis = copie();
			result._premiereCellule.setNext(copieThis._premiereCellule);
		}

		return result;
	}



	/**
	 *  ...
	 *
	 * @return    Description of the Return Value
	 */
	/*@
	  @ requires !estVide();
	  @
	  @ pure
	  @*/
	public Elem premier() {
		return _premiereCellule.getEntry();
	}


	/**
	 *  Description of the Method
	 *
	 * @return    Description of the Return Value
	 */
	/*@
	  @ requires !estVide();
	  @ ensures \result != null;
	  @ ensures \result.longueur() == longueur() - 1;
	  @
	  @ pure
	  @*/
	public PureListeElem fin() {
		PureListeElem result = new PureListeElem();

		if (_premiereCellule.hasNext()) {
			PureListeElem copieThis = copie();
			result._premiereCellule = copieThis._premiereCellule.getNext();
			result._nbElements = _nbElements - 1;
		}

		return result;
	}



	/**
	 *  Description of the Method
	 *
	 * @return    Description of the Return Value
	 */
	/*@
	  @ ensures \result <==> (longueur() == 0);
	  @
	  @ pure
	  @*/
	public boolean estVide() {
		return _premiereCellule == null;
	}



	/**
	 *  Description of the Method
	 *
	 * @param  elt  Description of the Parameter
	 * @return      Description of the Return Value
	 */
	/*@
	  @ 	requires estVide();
	  @ 	ensures !\result;
	  @ also
	  @ 	requires !estVide();
	  @ 	ensures (premier() == elt) ==> \result;
	  @ 	ensures (premier() != elt) ==> (\result <==> fin().estPresent(elt));
	  @
	  @ pure
	  @*/
	public boolean estPresent(Elem elt) {
		if (estVide()) {
			return false;
		} else if (premier() == elt) {
			return true;
		} else if (_premiereCellule.hasNext()) {
			boolean trouve = false;
			CellElem cell = _premiereCellule.getNext();

			for (cell = _premiereCellule.getNext();
				cell.hasNext() && !trouve;
				cell = cell.getNext()) {
				trouve = (cell.getEntry() == elt);
			}
			return trouve || (cell.getEntry() == elt);
		} else {
			// la liste possède une seule cellule et ce n'est pas
			// celle cherchée
			//@ assume longueur() == 1;
			return false;
		}
	}



	/**
	 *  Description of the Method
	 *
	 * @return    Description of the Return Value
	 */
	/*@
	  @ ensures \result >= 0;
	  @
	  @ pure
	  @*/
	public int longueur() {
		return _nbElements;
	}



	/**
	 *  Description of the Method
	 *
	 * @param  liste  Description of the Parameter
	 * @return        Description of the Return Value
	 */
	/*@
	  @ requires liste != null;
	  @ ensures \result != null;
	  @ ensures !estVide() ==> (\result.premier() == premier());
	  @ ensures \result.longueur() == (this.longueur() + liste.longueur());
	  @
	  @ pure
	  @*/
	public PureListeElem concatener(PureListeElem liste) {
		if (estVide()) {
			return liste;
		} else if (liste.estVide()) {
			return this;
		} else {
			PureListeElem result = copie();
			PureListeElem copieListe = liste.copie();
			CellElem cell;

			for (cell = result._premiereCellule;
				cell.hasNext();
				cell = cell.getNext()) {
			}
			cell.setNext(copieListe._premiereCellule);
			result._nbElements = longueur() + liste.longueur();

			return result;
		}
	}


	/**
	 *  Description of the Method
	 *
	 * @param  elt  Description of the Parameter
	 * @return      Description of the Return Value
	 */
	/*@
	  @ requires !estVide();
	  @ requires estPresent(elt);
	  @ ensures \result >= 1;
	  @ ensures elt == premier() ==> \result == 1;
	  @ ensures elt != premier() ==> \result == fin().rechercher(elt) + 1;
	  @
	  @ pure
	  @*/
	public int rechercher(Elem elt) {
		int rangEltTrouve = 0;
		int rangEltCourant = 1;

		if (premier() == elt) {
			rangEltTrouve = 1;
		} else {
			CellElem cell = _premiereCellule.getNext();

			for (cell = _premiereCellule.getNext();
				cell.hasNext() && rangEltTrouve == 0;
				cell = cell.getNext()) {
				rangEltCourant++;
				if (cell.getEntry() == elt) {
					rangEltTrouve = rangEltCourant;
				}
			}
			//@ assume cell != null;
			//@ assume (rangEltTrouve == 0) ==> !cell.hasNext();
			if (rangEltTrouve == 0) {
				rangEltTrouve = rangEltCourant + 1;
			}
		}
		return rangEltTrouve;
	}

}