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

import org.junit.jupiter.api.Test;

import java.util.List;
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;
import utils.Utils;

public class DependencyAxiomTest {
	
	Resource a = new Resource("a", Utils.INT, 1);
	Resource b = new Resource("b", Utils.INT, 1);
	Resource c = new Resource("c", Utils.INT, 1);
	Resource d = new Resource("d", Utils.INT, 1);
	Resource e = new Resource("e", Utils.INT, 1);
	Resource f = new Resource("f", Utils.INT, 2);
	Resource g = new Resource("g", Utils.INT, 2);
	Resource h = new Resource("h", Utils.INT, 2);
	
	@Test
	void IdentityMappingTest() {
		EquationFormula ef1 = new EquationFormula(a, b);
		DependencyFormula df1 = new DependencyFormula(a, b);
		boolean tmp = ProofSystem.identityMapping.check(List.of(ef1), df1);
		assertTrue(tmp);
		Formula conclusion = ProofSystem.identityMapping.apply(List.of(ef1));
		assertEquals(df1, conclusion);
		
		DependencyTerm t1 = new DependencyTerm(a, b, c);
		EquationFormula ef2 = new EquationFormula(t1, d);
		DependencyFormula df2 = new DependencyFormula(t1, d);
		assertTrue(ProofSystem.identityMapping.check(List.of(ef2), df2));
		assertEquals(df2, ProofSystem.identityMapping.apply(ef2));
	}
	
	@Test
	void CompositeMappingTest() {
		DependencyFormula df1 = new DependencyFormula(a, b, c);
		DependencyFormula df2 = new DependencyFormula(c, d);
		DependencyFormula df3 = new DependencyFormula(a, d, b);
		assertTrue(ProofSystem.compositeMapping.check(List.of(df1, df2), df3));
		assertEquals(df3, ProofSystem.compositeMapping.apply(List.of(df1, df2)));
		
		DependencyFormula df4 = new DependencyFormula(a, b);
		DependencyFormula df5 = new DependencyFormula(b, c);
		DependencyFormula df6 = new DependencyFormula(a, c);
		assertTrue(ProofSystem.compositeMapping.check(List.of(df4, df5), df6));
		assertEquals(df6, ProofSystem.compositeMapping.apply(List.of(df4, df5)));
	}

	@Test
	void ConstantMapping() {
		Resource aa = new Resource("aa", Utils.INT, 1);
		Resource bb = new Resource("bb", Utils.INT, 2);
		Resource cc = new Resource("cc", Utils.INT, 1);
		DependencyFormula d1 = new DependencyFormula(aa, bb);
		DependencyFormula d3 = new DependencyFormula(aa, cc);
		Set<Formula> result = ProofSystem.constantMapping.apply(List.of(), Set.of(aa, bb, cc));
		assertTrue(result.contains(d1));
		assertFalse(result.contains(d3));
	}
	
	@Test
	void UncurriedMappingTest() {
		Dependency d1 = new Dependency(f, g);
		Dependency d2 = new Dependency(d1, a);
		DependencyTerm t1 = new DependencyTerm(f, g, b);
		Dependency d3 = new Dependency(t1, a, b);
		DependencyFormula df1 = new DependencyFormula(d2);
		DependencyFormula df2 = new DependencyFormula(d3);
		Set<Formula> results = ProofSystem.uncurriedMapping.apply(List.of(df1), Set.of(b));
		assertTrue(results.contains(df2));
	}
	
}