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

import org.junit.jupiter.api.Test;

import java.util.Set;

import inference.ProofSystem;
import models.formulas.DependencyFormula;
import models.formulas.EquationFormula;
import models.formulas.Formula;
import models.terms.Dependency;
import models.terms.DependencyTerm;
import models.terms.Resource;

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", 2);
	Resource j = new Resource("j", 2);
	Resource k = new Resource("k", 2);
	
	@Test
	void IdentityMappingTest() {
		Set<Formula> res = ProofSystem.identityMapping.apply(new EquationFormula(a, b));
		assertTrue(res.contains(new DependencyFormula(a, b)));
	}
	
	@Test
	void CompositeMappingTest() {
		Set<Formula> res = ProofSystem.compositeMapping.apply(new DependencyFormula(a, b), new DependencyFormula(b, c));
		assertTrue(res.contains(new DependencyFormula(a, c)));
		
		res = ProofSystem.compositeMapping.apply(new DependencyFormula(a, b, c), new DependencyFormula(c, d, e, f));
		assertTrue(res.contains(new DependencyFormula(a, b, d, e, f)));
	}
	
	@Test
	void ConstantMappingTest() {
		//todo
	}
	
	@Test
	void UncurriedMappingTest() {
		Set<Formula> res = ProofSystem.uncurriedMapping.apply(
				new DependencyFormula(new Dependency(i, j), a),
				new EquationFormula(new DependencyTerm(j, h, c), b)
		);
		assertTrue(res.contains(new DependencyFormula(new DependencyTerm(i, j, b), a, b)));
		
		Resource a4 = new Resource("a4", 4);
		Resource b4 = new Resource("b4", 4);
		Resource x= new Resource("y", 4);
		Resource y = new Resource("x", 4);
		Resource a3 = new Resource("a3", 3);
		Resource a2 = new Resource("a2", 2);
		Resource a1 = new Resource("a1", 1);
		Resource c2 = new Resource("c2", 2);
		
		Dependency d4 = new Dependency(b4, a4);
		Dependency d3 = new Dependency(d4, a3);
		Dependency d2 = new Dependency(d3, a2);
		Dependency d1 = new Dependency(d2, a1);
		
		res = ProofSystem.uncurriedMapping.apply(
				new DependencyFormula(d1),
				new EquationFormula(new DependencyTerm(a4, x, y), c2)
		);
		DependencyTerm t1 = new DependencyTerm(b4, a4, c2);
		Dependency d33 = new Dependency(t1, a3);
		Dependency d22 = new Dependency(d33, a2, c2);
		Dependency d11 = new Dependency(d22, a1);
		assertTrue(res.contains(new DependencyFormula(d11)));
	}
	
	@Test
	void RedundantDependencyTest() {
		//todo
	}
	
	@Test
	void RedundancyEliminationTest() {
		Set<Formula> result = ProofSystem.redundancyElimination.apply(new DependencyFormula(a, b), new DependencyFormula(c, a, b, d));
		assertTrue(result.contains(new DependencyFormula(c, a, d)));
		
		result = ProofSystem.redundancyElimination.apply(new DependencyFormula(a, b, c, d), new DependencyFormula(c, a, b, c, d, e, f, g));
		assertTrue(result.contains(new DependencyFormula(c, a, e, f, g)));
	}
	
}