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 inference.axioms.RightSubstitution;
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 utils.Utils;

public class EqualityAxiomTest {
	
	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", 1);
	Resource m = new Resource("m", 2);
	Resource n = new Resource("n", 2);
	
	@Test
	void ReflexivityTest() {
	}
	
	@Test
	void SymmetryTest() {
		EquationFormula eq1 = new EquationFormula(a, b);
		Set<Formula> result = ProofSystem.symmetry.apply(eq1);
		assertTrue(result.contains(new EquationFormula(b, a)));
	}
	
	@Test
	void TransitivityTest() {
		EquationFormula eq1 = new EquationFormula(a, b);
		EquationFormula eq2 = new EquationFormula(b, c);
		EquationFormula eq3 = new EquationFormula(a, c);
		Set<Formula> result = ProofSystem.transitivity.apply(eq1, eq2);
		assertTrue(result.contains(eq3));
		
	}
	
	@Test
	void RightSubTest() {
		RightSubstitution rs = new RightSubstitution();
		EquationFormula eq = new EquationFormula(a, b);
		DependencyFormula dep = new DependencyFormula(c, d);
		DependencyTerm t1 = new DependencyTerm(c, d, a);
		DependencyTerm t2 = new DependencyTerm(c, d, b);
		EquationFormula eq2 = new EquationFormula(new DependencyTerm(d, e, f), a);
		Set<Formula> result = rs.apply(Set.of(eq, dep, eq2)); 
		assertTrue(result.contains(new EquationFormula(t1, t2)));
		
		assertEquals(rs.generateRightSideHand(List.of(eq, dep, eq2), t1), t2);
		DependencyFormula dep2 = new DependencyFormula(c, g);
		EquationFormula eq3 = new EquationFormula(new DependencyTerm(g, h, i), j);
		DependencyTerm t3 = new DependencyTerm(c, d, a, g, j);
		DependencyTerm t4 = new DependencyTerm(c, d, b, g, j);
		result = rs.apply(Set.of(eq, eq2, eq3, dep, dep2));
		assertTrue(result.contains(new EquationFormula(t3, t4)));
	}
	
	@Test
	void LeftSubTest() {
		EquationFormula eq1 = new EquationFormula(a, b);
		DependencyFormula d1 = new DependencyFormula(a, c);
		EquationFormula eq2 = new EquationFormula(new DependencyTerm(c, d, e), f);
		Set<Formula> result = ProofSystem.leftSubstitution.apply(eq1, d1, eq2);
		assertTrue(result.contains(new EquationFormula(new DependencyTerm(a, c, f), new DependencyTerm(b, c, f))));
	}
	
	@Test
	void IdentityTest() {
		EquationFormula eq1 = new EquationFormula(new DependencyTerm(a, b, c), d);
		Set<Formula> result = ProofSystem.identity.apply(eq1);
		assertTrue(result.contains(new EquationFormula(new DependencyTerm(a, a, d), d)));
		
		EquationFormula eq2 = new EquationFormula(new DependencyTerm(a, b, c), d);
		EquationFormula eq3 = new EquationFormula(new DependencyTerm(e, f, g), h);
		result = ProofSystem.identity.apply(eq2, eq3);
		assertTrue(result.contains(new EquationFormula(new DependencyTerm(a, a, d, e, h), d)));
	}
	
	@Test
	void MapCompositionTest() {
		DependencyFormula df1 = new DependencyFormula(a, b, c);
		DependencyFormula df2 = new DependencyFormula(b, d, e);
		EquationFormula eq1 = Utils.in(f, c);
		EquationFormula eq2 = Utils.in(g, d);
		EquationFormula eq3 = Utils.in(h, e);
		Set<Formula> result = ProofSystem.mapComposition.apply(df2, df1, eq2, eq3, eq1);
		EquationFormula conc1 = new EquationFormula(
				new DependencyTerm(
						a, b, new DependencyTerm(b, d, g, e, h), c, f
				),
				new DependencyTerm(a, d, g, e, h, c, f)
		);
		assertTrue(result.contains(conc1));
	}
	
	@Test
	void ConstantnessTest() {
		
	}
	
	@Test
	void RightNormalizationTest() {
		DependencyFormula d1 = new DependencyFormula(new Dependency(m, n), a, b);
		DependencyFormula d2 = new DependencyFormula(c, d, e);
		EquationFormula eq1 = Utils.in(c, n);
		EquationFormula eq2 = Utils.in(f, a);
		EquationFormula eq3 = Utils.in(g, b);
		EquationFormula eq4 = Utils.in(h, d);
		EquationFormula eq5 = Utils.in(j, e);
		Set<Formula> result = ProofSystem.rightNormalization.apply(d1, d2, eq1, eq2, eq3, eq4, eq5);
		EquationFormula conc1 = new EquationFormula(
				new DependencyTerm(
						new DependencyTerm(
								m, n, c
						),
						a, f, b, g, d, h, e, j
				),
				new DependencyTerm(
						new DependencyTerm(
								m ,n, new DependencyTerm(
										c, d, h, e, j
								)
						),
						a, f, b, g
				)
		);
		assertTrue(result.contains(conc1));
	}
	
	@Test
	void PseudoConstantnessTest() {
		Set<Formula> result = ProofSystem.pseudoConstantness.apply(new DependencyFormula(a, b));
		assertTrue(result.contains(new EquationFormula(new DependencyTerm(a, b, b), a)));
		
		result =  ProofSystem.pseudoConstantness.apply(new DependencyFormula(a, b, c, d));
		assertTrue(result.contains(new EquationFormula(new DependencyTerm(a, b, b, c, c, d, d), a)));
	}
	
	@Test
	void ArgumentDependencyExtractionTest() {
		Set<Formula> result = ProofSystem.argumentDependencyExtraction.apply(
				new DependencyFormula(a, b, c), 
				new DependencyFormula(b, c), 
				new EquationFormula(new DependencyTerm(a, b, d, c, e), new ResourceConstant("ccc")));
		assertTrue(result.contains(new EquationFormula(new DependencyTerm(b, c, e), d)));
	}
	
}