package inferencerule;
import static org.junit.jupiter.api.Assertions.*;

import java.util.List;
import java.util.Set;

import org.junit.jupiter.api.Test;

import inference.ProofSystem;
import models.Position;
import models.algebra.Variable;
import models.formulas.DependencyFormula;
import models.formulas.EquationFormula;
import models.formulas.Formula;
import models.terms.Dependency;
import models.terms.DependencyTerm;
import models.terms.Resource;
import models.terms.ResourceConstant;
import models.terms.meta.MatchConstraint;

public class DependencyAxiomTest {
	
	Resource a = new Resource("a", 1);
	Resource b = new Resource("b", 1);
	Resource c = new Resource("c", 1);
	Resource d = new Resource("d", 1);
	Resource e = new Resource("e", 1);
	Resource f = new Resource("f", 1);
	Resource g = new Resource("g", 1);
	Resource h = new Resource("h", 1);
	Resource i = new Resource("i", 1);
	Resource j = new Resource("j", 1);
	Resource k = new Resource("k", 1);
	Resource l = new Resource("l", 2);
	Resource m = new Resource("m", 2);
	
	@Test
	void IdentityMappingTest() {
		Set<Formula> res = ProofSystem.identityMapping.derive(List.of(new EquationFormula(a, b)));
		assertTrue(res.contains(new DependencyFormula(a, b)));
	}
	
	@Test
	void ArgumentExtensionTest() {
		MatchConstraint constraint = MatchConstraint.createDefault();
		constraint.setBinding(new Variable("ue"), d);
		Set<Formula> res = ProofSystem.argumentExtension.derive(List.of(new DependencyFormula(a, b, c)), constraint);
		assertTrue(res.contains(new DependencyFormula(a, b, c, d)));
	}
	
	@Test
	void ArgumentReductionTest() {
		DependencyFormula d1 = new DependencyFormula(a, b, c);
		DependencyFormula d2 = new DependencyFormula(d, a, b, c, e, f);
		Set<Formula> res = ProofSystem.argumentReduction.derive(List.of(d1, d2));
		assertTrue(res.contains(new DependencyFormula(d, b, c, e, f)));
	}
	
	@Test
	void ArgumentConstraintTest() {
		DependencyTerm t1 = new DependencyTerm(a, b, c, d, e, f, g, h, i);
		EquationFormula eq1 = new EquationFormula(t1, new ResourceConstant("0"));
		DependencyFormula d1 = new DependencyFormula(b, d, f);
		Set<Formula> res = ProofSystem.argumentConstraint.derive(List.of(eq1, d1));
		DependencyTerm t2 = new DependencyTerm(b, d, e, f, g);
		assertTrue(res.contains(new EquationFormula(t2, c)));
	}
	
	@Test
	void CompositeMappingTest() {
		DependencyFormula d1 = new DependencyFormula(a, b, c, d);
		DependencyFormula d2 = new DependencyFormula(e, a, f, g, h);
		Set<Formula> res = ProofSystem.compositeMapping.derive(List.of(d1, d2));
		assertTrue(res.contains(new DependencyFormula(e, b, c, d, f, g, h)));
	}
	
	@Test
	void ConstantMappingTest() {
		MatchConstraint constraint = MatchConstraint.createDefault();
		constraint.getContext().put(new Position(), 3);
		constraint.setBinding(new Variable("se"), a);
		constraint.setBinding(new Variable("te0"), l);
		constraint.setBinding(new Variable("te1"), m);
		constraint.getContext().put("maxDepth", 1);
		Set<Formula> res = ProofSystem.constatnMapping.derive(List.of(), constraint);
		assertTrue(res.contains(new DependencyFormula(a, l, m)));
	}
	
	@Test
	void UncurriedMappingTest() {
		Resource a = new Resource("a", 4);
		Resource b = new Resource("b", 4);
		Resource d = new Resource("d", 3);
		Resource e = new Resource("e", 3);
		Resource f = new Resource("f", 3);
		Resource g = new Resource("g", 3);
		Resource h = new Resource("h", 2);
		Resource i = new Resource("i", 2);
		Resource x = new Resource("x", 2);
		DependencyFormula d1 = new DependencyFormula(new Dependency(new Dependency(new Dependency(a, b), d, e, f, g), h, i));
		MatchConstraint constraint = MatchConstraint.createDefault();
		constraint.setBinding(new Variable("ve"), x);
		Set<Formula> res = ProofSystem.uncurriedMapping.derive(List.of(d1), constraint);
		DependencyFormula d2 = new DependencyFormula(new Dependency(new Dependency(new DependencyTerm(a, b, x), d, e, f, g), h, i, x));
		assertTrue(res.contains(d2));
	}
	
	@Test
	void DependencyExtensionTest() {
		Resource a = new Resource("a", 4);
		Resource b = new Resource("b", 4);
		Resource d = new Resource("d", 4);
		Resource e = new Resource("e", 3);
		Resource f = new Resource("f", 3);
		DependencyFormula d1 = new DependencyFormula(a, b, d);
		DependencyFormula d2 = new DependencyFormula(d1.getDependency(), e, f);
		MatchConstraint constraint = MatchConstraint.createDefault();
		constraint.getContext().put("j", 2);
		constraint.setBinding(new Variable("ue0"), e);
		constraint.setBinding(new Variable("ue1"), f);
		Set<Formula> res = ProofSystem.dependencyExtension.derive(List.of(d1), constraint);
		assertTrue(res.contains(d2));
	}
	
	
}