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.DependencyTerm;
import models.terms.Resource;
import utils.Utils;

public class EqualityAxiomTest {
	
	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, 1);
	Resource g = new Resource("g", Utils.INT, 1);
	
	@Test
	void ReflexivityTest() {
		EquationFormula f = new EquationFormula(a, a);
		Set<Formula> results = ProofSystem.reflexivity.apply(List.of(), Set.of(a));
		assertTrue(results.contains(f));
	}
	
	@Test
	void SymmetryTest() {
		EquationFormula f1 = new EquationFormula(a, b);
		EquationFormula f2 = new EquationFormula(b, a);
		assertFalse(f1.equals(f2));
		
		Formula result = ProofSystem.symmetry.apply(List.of(f1));
		assertTrue(f2.equals(result));
	}

	@Test
	void TransitivitiyTest() {
		EquationFormula ab = new EquationFormula(a, b);
		EquationFormula bc = new EquationFormula(b, c);
		EquationFormula ac = new EquationFormula(a, c);
		
		Formula result = ProofSystem.transitivity.apply(List.of(ab, bc));
		assertEquals(ac, result);
	}
	
	@Test
	void RightSubstitutionTest() {
		EquationFormula f1 = new EquationFormula(a, b);
		DependencyFormula d1 = new DependencyFormula(c, d);
		DependencyTerm t1 = new DependencyTerm(d, f, g);
		EquationFormula f2 = new EquationFormula(t1, a);
		DependencyTerm t2 = new DependencyTerm(c, d, a);
		DependencyTerm t3 = new DependencyTerm(c, d, b);
		EquationFormula f3 = new EquationFormula(t2, t3);
		Formula result = ProofSystem.rightSubstitution.apply(List.of(f1, d1, f2));
		assertEquals(result, f3);
	}
	
	@Test
	void LeftSubstituitionTest() {
		EquationFormula f1 = new EquationFormula(a, b);
		DependencyFormula d1 = new DependencyFormula(a, c);
		DependencyTerm t1 = new DependencyTerm(c, f, g);
		EquationFormula f2 = new EquationFormula(t1, d);
		DependencyTerm t2 = new DependencyTerm(a, c, d);
		DependencyTerm t3 = new DependencyTerm(b, c, d);
		EquationFormula f3 = new EquationFormula(t2, t3);
		Formula result = ProofSystem.leftSubstitution.apply(List.of(f1, d1, f2));
		assertEquals(result, f3);
	}
	
	@Test
	void IdentityTest() {
		DependencyTerm t1 = new DependencyTerm(a, f, g);
		DependencyTerm t2 = new DependencyTerm(a, a, b);
		EquationFormula f1 = new EquationFormula(t1, b);
		EquationFormula f2 = new EquationFormula(t2, b);
		
		Formula result = ProofSystem.identity.apply(List.of(f1));
		assertEquals(f2, result);
	}
	
	@Test
	void MapCompositionTest() {
		DependencyFormula d1 = new DependencyFormula(a, b);
		DependencyFormula d2 = new DependencyFormula(b, c);
		DependencyTerm t1 = new DependencyTerm(c, f, g);
		EquationFormula f1 = new EquationFormula(t1, d);
		
		DependencyTerm t2 = new DependencyTerm(b, c, d);
		DependencyTerm t3 = new DependencyTerm(a, b, t2);
		DependencyTerm t4 = new DependencyTerm(a, c, d);
		EquationFormula f2 = new EquationFormula(t3, t4);
		
		Formula result = ProofSystem.mapComposition.apply(List.of(d1, d2, f1));
		assertEquals(f2, result);
	}
	
}