package inference;

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

import java.util.Set;

import org.junit.jupiter.api.Test;

import models.formulas.DependencyFormula;
import models.formulas.EquationFormula;
import models.terms.Dependency;
import models.terms.DependencyTerm;
import models.terms.Resource;

public class DependencyInferenceTest {

	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", 2);
	Resource g = new Resource("g", 2);
	Resource h = new Resource("h", 3);
	Resource i = new Resource("i", 3);
	
	@Test
	void IdentityMappingInferenceTest() {
		EquationFormula eq1 = new EquationFormula(a, b);
		DependencyFormula d1 = new DependencyFormula(a, b);
		ProofSystem ps = new ProofSystem(Set.of(eq1), d1);
		assertTrue(ps.dependencyInference());
	}
	
	@Test
	void ArgumentExtensionInferenceTest() {
		DependencyFormula d1 = new DependencyFormula(a, b);
		DependencyFormula d2 = new DependencyFormula(a, b, c);
		DependencyFormula d3 = new DependencyFormula(a, b, c, d, e);
		ProofSystem ps = new ProofSystem(Set.of(d1), d2);
		assertFalse(ps.dependencyInference());
		ProofSystem ps2 = new ProofSystem(Set.of(d1), d2, Set.of(c));
		assertTrue(ps2.dependencyInference());
		ProofSystem ps3 = new ProofSystem(Set.of(d1), d3, Set.of(c, d, e));
		assertTrue(ps3.dependencyInference());
	}
	
	@Test
	void ArgumentReductionInferenceTest() {
		DependencyFormula d1 = new DependencyFormula(a, b, c);
		DependencyFormula d2 = new DependencyFormula(b, c);
		DependencyFormula d3 = new DependencyFormula(a, c);
		ProofSystem ps = new ProofSystem(Set.of(d1, d2), d3);
		assertTrue(ps.dependencyInference());
		
		DependencyFormula d4 = new DependencyFormula(a, b, b);
		EquationFormula eq1 = new EquationFormula(b, b);
		DependencyFormula d5 = new DependencyFormula(a, b);
		ProofSystem ps2 = new ProofSystem(Set.of(d4, eq1), d5);
		assertTrue(ps2.dependencyInference());
	}	
	
	@Test
	void CompositeMappingInferenceTest() {
		DependencyFormula d1 = new DependencyFormula(a, b);
		DependencyFormula d2 = new DependencyFormula(b, c, d);
		DependencyFormula d3 = new DependencyFormula(a, c, d);
		ProofSystem ps = new ProofSystem(Set.of(d1, d2), d3);
		assertTrue(ps.dependencyInference());
	}
	
	@Test
	void ConstantMappingInferenceTest() {
		DependencyFormula d1 = new DependencyFormula(a, f);
		ProofSystem ps = new ProofSystem(Set.of(), d1, Set.of(a, f));
		assertTrue(ps.dependencyInference());
		
		DependencyFormula d2 = new DependencyFormula(a, f, g);
		ProofSystem ps2 = new ProofSystem(Set.of(), d2, Set.of(a, b, f, g));
		assertTrue(ps2.dependencyInference());
	}
	
	@Test
	void UncurriedMappingInferenceTest() {
		DependencyFormula d1 = new DependencyFormula(new Dependency(f, g), a);
		DependencyFormula d2 = new DependencyFormula(new DependencyTerm(f, g, b), a, b);
		ProofSystem ps = new ProofSystem(Set.of(d1), d2, Set.of(b));
		assertTrue(ps.dependencyInference());
		
		DependencyFormula d3 = new DependencyFormula(new Dependency(new Dependency(h, i), f, g), a);
		DependencyFormula d4 = new DependencyFormula(new Dependency(new DependencyTerm(h, i, b), f, g), a, b);
		ProofSystem ps2 = new ProofSystem(Set.of(d3), d4, Set.of(b));
		assertTrue(ps2.dependencyInference());
		
		DependencyFormula d5 = new DependencyFormula(new Dependency(new Dependency(h, i), f), a);
		DependencyFormula d6 = new DependencyFormula(new Dependency(new DependencyTerm(h, i, g), f, g), a);
		ProofSystem ps3 = new ProofSystem(Set.of(d5), d6, Set.of(g));
		assertTrue(ps3.dependencyInference());
	}
	
}