package rapanui.core;

import java.util.ArrayList;
import java.util.List;
import java.util.stream.Collectors;

import rapanui.dsl.Term;

import static rapanui.core.Patterns.*;

/**
 * Represents the core proof process, in which a term is transformed using rules and premises.
 */
public class ConclusionProcess {
	private final ProofEnvironment environment;
	private final Term startTerm;
	private final List<Transformation> transformations;
	private final List<ConclusionProcessObserver> observers;

	/**
	 * Creates a new conclusion process
	 *
	 * @param environment The environment containing the process. Must not be null.
	 * @param startTerm The initial term of the process. Must not be null.
	 */
	ConclusionProcess(ProofEnvironment environment, Term startTerm) {
		assert environment != null;
		assert startTerm != null;

		this.environment = environment;
		this.startTerm = startTerm;
		this.transformations = new ArrayList<Transformation>();
		this.observers = new ArrayList<ConclusionProcessObserver>();
	}

	/**
	 * @return The environment containing the conclusion. Guaranteed to be non-null.
	 */
	public ProofEnvironment getEnvironment() {
		return environment;
	}

	/**
	 * @return The conclusion's start term. Guaranteed to be non-null.
	 */
	public Term getStartTerm() {
		return startTerm;
	}

	/**
	 * Retrieves the (current) last term in the transformation chain.
	 * @return The output term of the last transformation, or if there are none, the initial term. Guaranteed to be non-null.
	 */
	public Term getLastTerm() {
		if (transformations.size() == 0)
			return startTerm;
		return transformations.get(transformations.size() - 1).getOutput();
	}

	/**
	 * Computes the type of the conclusion, i.e. equality or inclusion.
	 *
	 * @return @see FormulaType.INCLUSION if any transformation is an inclusion, @see FormulaType.EQUATION otherwise. Guaranteed to be non-null.
	 */
	public FormulaType getFormulaType() {
		return getFormulaType(0, transformations.size());
	}

	/**
	 * Computes the type of a range of transformations in the conclusion.
	 *
	 * @param startRange The index of the first term (not transformation!) to include in the range
	 * @param endRange The index of the last term (not transformation!) to include in the range
	 *
	 * @return @see FormulaType.INCLUSION if any transformation in the range is an inclusion, @see FormulaType.EQUATION otherwise.
	 * 	If startIndex == endIndex, there is no transformation in the range and @see FormulaType.EQUATION is returned.
	 * 	Guaranteed to be non-null.
	 *
	 * @throws IllegalArgumentException if the arguments do not specify a valid range
	 */
	public FormulaType getFormulaType(int startRange, int endRange) {
		if (startRange < 0 || startRange > transformations.size())
			throw new IllegalArgumentException("startRange");
		else if (endRange < startRange || endRange > transformations.size())
			throw new IllegalArgumentException("endRange");

		if (startRange == endRange)
			return FormulaType.EQUATION;

		List<FormulaType> transformationTypes = transformations
				.subList(Math.max(startRange - 1, 0), endRange)
				.stream()
				.map(Transformation::getType)
				.collect(Collectors.toList());

		if (transformationTypes.contains(FormulaType.INCLUSION))
			return FormulaType.INCLUSION;
		return FormulaType.EQUATION;
	}

	public Transformation[] getTransformations() {
		return listToArray(transformations, Transformation[]::new);
	}

	/**
	 * Appends a new transformation to the chain.
	 *
	 * @param transformation The transformation to append. Must not be null.
	 *
	 * The new transformation's input term must equal the current last term on the conclusion process.
	 */
	public void appendTransformation(Transformation transformation) {
		assert transformation != null;
		assert transformation.getContainer() == this;

		if (!getLastTerm().structurallyEquals(transformation.getInput()))
			throw new IllegalArgumentException();
		transformations.add(transformation);
		notifyObservers(observers, ConclusionProcessObserver::transformationAdded, transformation);
	}

	/**
	 * Adds an observer to the process. Observers are notified upon changes.
	 *
	 * @param observer The new observer. Must not be null.
	 */
	public void addObserver(ConclusionProcessObserver observer) {
		assert observer != null;
		observers.add(observer);
	}

	/**
	 * Unregisters an observer from the process, so it is no longer notified of changes.
	 *
	 * @param observer The observer to remove
	 */
	public void deleteObserver(ConclusionProcessObserver observer) {
		observers.remove(observer);
	}
}

@@ -1658,32 +1658,484 @@
 etOutput();%0A%09%7D%0A%0A
+%09/**%0A%09 * Computes the list of all terms occurring in the transformation chain.%0A%09 * @return The terms in the conclusion, in order. Guaranteed to be non-null.%0A%09 */%0A%09public Term%5B%5D getTerms() %7B%0A%09%09Transformation%5B%5D transformations = getTransformations();%0A%09%09Term%5B%5D terms = new Term%5B1+transformations.length%5D;%0A%0A%09%09terms%5B0%5D = getStartTerm();%0A%09%09for (int i = 0; i %3C transformations.length; ++i)%0A%09%09%09terms%5Bi+1%5D = transformations%5Bi%5D.getOutput();%0A%0A%09%09return terms;%0A%09%7D%0A%0A
 %09/**%0A%09 * Compute

add ConclusionProcess.getTerms()