/**
 * Copyright (c) 2020, the Alpha Team.
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 * 1) Redistributions of source code must retain the above copyright notice, this
 *    list of conditions and the following disclaimer.
 *
 * 2) Redistributions in binary form must reproduce the above copyright notice,
 *    this list of conditions and the following disclaimer in the documentation
 *    and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
 * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
 * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 */
package at.ac.tuwien.kr.alpha.core.grounder.instantiation;

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

import org.apache.commons.lang3.tuple.ImmutablePair;

import at.ac.tuwien.kr.alpha.api.grounder.Substitution;
import at.ac.tuwien.kr.alpha.api.programs.literals.Literal;
import at.ac.tuwien.kr.alpha.commons.substitutions.BasicSubstitution;
import at.ac.tuwien.kr.alpha.core.grounder.Grounder;
import at.ac.tuwien.kr.alpha.core.programs.rules.InternalRule;

/**
 * Representation of the result of instantiating, i.e. finding ground instances for a literal, as performed by
 * {@link LiteralInstantiator#instantiateLiteral(Literal, BasicSubstitution)}.
 * 
 * A {@link LiteralInstantiationResult} bundles obtained ground substitutions - or the lack thereof, if none exist for a given literal -
 * together with status information that can be used by a {@link Grounder} to determine how to proceed when grounding an
 * {@link InternalRule}.
 * 
 * Copyright (c) 2020, the Alpha Team.
 */
public class LiteralInstantiationResult {

	/**
	 * Indicates how a {@link Grounder} should treat this result.
	 */
	private final Type type;

	/**
	 * Ground substitutions together with the {@link AssignmentStatus} of the last literal bound to obtain the substitution. Empty for result
	 * types STOP_BINDING, PUSH_BACK and MAYBE_PUSH_BACK.
	 */
	private final List<ImmutablePair<Substitution, AssignmentStatus>> substitutions;

	private LiteralInstantiationResult(Type type, List<ImmutablePair<Substitution, AssignmentStatus>> substitutions) {
		if (type == Type.CONTINUE && substitutions == null) {
			throw new UnsupportedOperationException("A LiteralInstantiationResult of type CONTINUE must have substitutions!");
		}
		this.type = type;
		this.substitutions = substitutions;
	}

	public static LiteralInstantiationResult continueBinding(List<ImmutablePair<Substitution, AssignmentStatus>> substitutions) {
		return new LiteralInstantiationResult(Type.CONTINUE, substitutions);
	}

	//@formatter:off
	public static LiteralInstantiationResult continueBindingWithTrueSubstitutions(List<Substitution> substitutions) {
		List<ImmutablePair<Substitution, AssignmentStatus>> substitutionsWithAssignment = substitutions.stream()
				.map((substitution) -> new ImmutablePair<>(substitution, AssignmentStatus.TRUE))
				.collect(Collectors.toList());
		return new LiteralInstantiationResult(Type.CONTINUE, substitutionsWithAssignment);
	}
	//@formatter:on

	public static LiteralInstantiationResult continueBinding(Substitution substitution, AssignmentStatus assignmentStatus) {
		return new LiteralInstantiationResult(Type.CONTINUE, Collections.singletonList(new ImmutablePair<>(substitution, assignmentStatus)));
	}

	public static LiteralInstantiationResult stopBinding() {
		return new LiteralInstantiationResult(Type.STOP_BINDING, null);
	}

	public static LiteralInstantiationResult pushBack() {
		return new LiteralInstantiationResult(Type.PUSH_BACK, null);
	}

	public static LiteralInstantiationResult maybePushBack() {
		return new LiteralInstantiationResult(Type.MAYBE_PUSH_BACK, null);
	}

	public Type getType() {
		return this.type;
	}

	public List<ImmutablePair<Substitution, AssignmentStatus>> getSubstitutions() {
		if (this.type != Type.CONTINUE) {
			throw new UnsupportedOperationException("A LiteralInstantiationResult of type " + this.type + " does not have substitutions!");
		}
		return this.substitutions;
	}

	/**
	 * Result type. Used by {@link Grounder}s to determine how to proceed grounding a rule after instantiating the literal that yielded the
	 * respective instantiation result.
	 * 
	 * Copyright (c) 2020, the Alpha Team.
	 */
	public static enum Type {

		/**
		 * Grounder should stop working on the rule, no valid substitutions exist.
		 */
		STOP_BINDING,

		/**
		 * Grounder should continue with the next literal.
		 */
		CONTINUE,

		/**
		 * Literal instantiation yielded no ground instances, but depending on the specific workflow of the grounder, proceeding with another
		 * literal might yet make sense. Grounder should decide whether to stop binding or push the literal back in the overall grounding order.
		 */
		MAYBE_PUSH_BACK,

		/**
		 * Currently no ground instances, but proceeding with another literal might make sense, push the literal back in the overall grounding
		 * order. This is used for {@link at.ac.tuwien.kr.alpha.common.atoms.FixedInterpretationLiteral}s that do not produce bindings, like a
		 * comparision "X < Y" when one variable is not yet bound.
		 */
		PUSH_BACK;
	}
}
