package inference.axioms;
import java.util.Map;

import inference.EquationAxiom;
import models.algebra.Variable;
import models.formulas.EquationFormula;
import models.formulas.meta.MetaDependencyFormula;
import models.formulas.meta.MetaEquationFormula;
import models.terms.meta.MetaDynamicDependency;
import models.terms.meta.MetaDynamicDependencyTerm;
import models.terms.meta.MetaEvaluatableTermVariable;
import models.terms.meta.MetaRDLTerm;
import models.terms.meta.MetaTermGenerator;

public class ArgumentDependencyExtraction extends EquationAxiom {

	public ArgumentDependencyExtraction() {
		super("Argument Dependency Extraction");
		assumptions.add(
				new MetaDependencyFormula(
						new MetaDynamicDependency(
								new MetaTermGenerator() {
									@Override
									public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
										curIndex -= 1;
										context.put("firstAssumptionIndex", curIndex + 2);
										return new MetaEvaluatableTermVariable(new Variable("t" + curIndex));
									}
								},
								new MetaEvaluatableTermVariable(new Variable("t"))
						)
				)
		);
		assumptions.add(
				new MetaDependencyFormula(
						new MetaDynamicDependency(
								new MetaTermGenerator() {
									@Override
									public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
										curIndex -= 2;
										return new MetaEvaluatableTermVariable(new Variable("t" + curIndex));
									}
								},
								new MetaEvaluatableTermVariable(new Variable("s")),
								new MetaEvaluatableTermVariable(new Variable("t"))
						)
				)
		);
		assumptions.add(
				new MetaEquationFormula(
						new MetaDynamicDependencyTerm(
								new MetaTermGenerator() {
									@Override
									public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
										curIndex -= 3;
										if (curIndex % 2 == 0) {
											return new MetaEvaluatableTermVariable(new Variable("t" + curIndex / 2));
										}
										return new MetaEvaluatableTermVariable(new Variable("x" + curIndex / 2));
									}
								},
								new MetaEvaluatableTermVariable(new Variable("s")),
								new MetaEvaluatableTermVariable(new Variable("t")),
								new MetaEvaluatableTermVariable(new Variable("x"))
						),
						new MetaEvaluatableTermVariable(new Variable("c"))
				)
		);
		
		conclusion = new MetaEquationFormula(
				new MetaDynamicDependencyTerm(
						new MetaTermGenerator() {
							@Override
							public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
								int firstAssumptionIndex = (Integer) context.get("firstAssumptionIndex");
								curIndex -= 1;
								if (curIndex >= firstAssumptionIndex) {
									return null;
								}
								if (curIndex % 2 == 0) {
									return new MetaEvaluatableTermVariable(new Variable("t" + curIndex / 2));
								}
								return new MetaEvaluatableTermVariable(new Variable("x" + curIndex / 2));
							}
						},
						new MetaEvaluatableTermVariable(new Variable("t"))
				),
				new MetaEvaluatableTermVariable(new Variable("x"))
		);
		conclusionMaxIndexCalculator = (assumptions) -> ((EquationFormula) assumptions.get(2)).getLeftSideHand().getMaxIndex() - 3 + 1;
	}

}