content: package aima.core.logic.fol.kb.data;
  
  import java.util.ArrayList;
  import java.util.Collections;
  import java.util.List;
  import java.util.Set;
  
  import aima.core.logic.fol.inference.proof.ProofStep;
  import aima.core.logic.fol.inference.proof.ProofStepChainContrapositive;
  import aima.core.logic.fol.inference.proof.ProofStepPremise;
  
  /**
   * 
   * A Chain is a sequence of literals (while a clause is a set) - order is
   * important for a chain.
   * 
   * @see <a
   *      href="http://logic.stanford.edu/classes/cs157/2008/lectures/lecture13.pdf"
   *      >Chain</a>
   * 
   * @author Ciaran O'Reilly
   * 
   */
  public class Chain {
  	private static List<Literal> _emptyLiteralsList = Collections
  			.unmodifiableList(new ArrayList<Literal>());
  	//
  	private List<Literal> literals = new ArrayList<Literal>();
  	private ProofStep proofStep = null;
  
  	public Chain() {
  		// i.e. the empty chain
  	}
  
  	public Chain(List<Literal> literals) {
  		this.literals.addAll(literals);
  	}
  
  	public Chain(Set<Literal> literals) {
  		this.literals.addAll(literals);
  	}
  
  	public ProofStep getProofStep() {
  		if (null == proofStep) {
  			// Assume was a premise
  			proofStep = new ProofStepPremise(this);
  		}
  		return proofStep;
  	}
  
  	public void setProofStep(ProofStep proofStep) {
  		this.proofStep = proofStep;
  	}
  
  	public boolean isEmpty() {
  		return literals.size() == 0;
  	}
  
  	public void addLiteral(Literal literal) {
  		literals.add(literal);
  	}
  
  	public Literal getHead() {
  		if (0 == literals.size()) {
  			return null;
  		}
  		return literals.get(0);
  	}
  
  	public List<Literal> getTail() {
  		if (0 == literals.size()) {
  			return _emptyLiteralsList;
  		}
  		return Collections
  				.unmodifiableList(literals.subList(1, literals.size()));
  	}
  
  	public int getNumberLiterals() {
  		return literals.size();
  	}
  
  	public List<Literal> getLiterals() {
  		return Collections.unmodifiableList(literals);
  	}
  
  	/**
  	 * A contrapositive of a chain is a permutation in which a different literal
  	 * is placed at the front. The contrapositives of a chain are logically
  	 * equivalent to the original chain.
  	 * 
  	 * @return a list of contrapositives for this chain.
  	 */
  	public List<Chain> getContrapositives() {
  		List<Chain> contrapositives = new ArrayList<Chain>();
  		List<Literal> lits = new ArrayList<Literal>();
  
  		for (int i = 1; i < literals.size(); i++) {
  			lits.clear();
  			lits.add(literals.get(i));
  			lits.addAll(literals.subList(0, i));
  			lits.addAll(literals.subList(i + 1, literals.size()));
  			Chain cont = new Chain(lits);
  			cont.setProofStep(new ProofStepChainContrapositive(cont, this));
  			contrapositives.add(cont);
  		}
  
  		return contrapositives;
  	}
  
  	@Override
  	public String toString() {
  		StringBuilder sb = new StringBuilder();
  		sb.append("<");
  
  		for (int i = 0; i < literals.size(); i++) {
  			if (i > 0) {
  				sb.append(",");
  			}
  			sb.append(literals.get(i).toString());
  		}
  
  		sb.append(">");
  
  		return sb.toString();
  	}
  }
  