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 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);
	Resource h = new Resource("h", Utils.INT, 2);
	Resource i = new Resource("i", Utils.INT, 2);
	Resource j = new Resource("j", Utils.INT, 2);
	Resource k = new Resource("k", Utils.INT, 2);
	Resource l = new Resource("l", 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);
		
		Resource te0 = new Resource("te0", Utils.INT, 1);
		Resource te1 = new Resource("te1", Utils.INT, 1);
		Resource te2 = new Resource("te2", Utils.INT, 1);
		Resource ue = new Resource("ue", Utils.INT, 1);
		Resource se = new Resource("se", Utils.INT, 1);
		Resource re0 = new Resource("re0", Utils.INT, 1);
		Resource re1 = new Resource("r1", Utils.INT, 1);
		Resource re2 = new Resource("r2", Utils.INT, 1);
		EquationFormula eq1 = new EquationFormula(te0, ue);
		DependencyFormula df1 = new DependencyFormula(se, re0, re1, re2);
		EquationFormula eq2 = new EquationFormula(new DependencyTerm(re0, a, b), te0);
		DependencyTerm dt1 = new DependencyTerm(se, re0, te0, re1, te1, re2, te2);
		DependencyTerm dt2 = new DependencyTerm(se, re0, ue, re1, te1, re2, te2);
		EquationFormula eq3 = new EquationFormula(dt1, dt2);
		Set<Formula> result2 = ProofSystem.rightSubstitution.apply(List.of(eq1, df1, eq2), Set.of(te1, te2));
		assertTrue(result2.contains(eq3));
		
	}
	
	@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);
	}
	
	@Test
	void ConstantnessTest() {
		Resource a = new Resource("a", Utils.INT, 3);
		Resource b = new Resource("b", Utils.INT, 3);
		Resource c = new Resource("c", Utils.INT, 2);
		Resource d = new Resource("d", Utils.INT, 2);
		Resource e = new Resource("e", Utils.INT, 2);
		Resource f = new Resource("f", Utils.INT, 2);
		Resource g = new Resource("g", Utils.INT, 1);
		Resource h = new Resource("h", Utils.INT, 1);
		
		DependencyTerm t1 = new DependencyTerm(a, b, c);
		DependencyTerm t2 = new DependencyTerm(e, f, g);
		EquationFormula eq1 = new EquationFormula(t1, d);
		EquationFormula eq2 = new EquationFormula(t2, h);
		
		Resource x = new Resource("x", Utils.INT, 2);
		DependencyTerm t3 = new DependencyTerm(x, a, d);
		DependencyTerm t4 = new DependencyTerm(t3, e, h);
		EquationFormula eq3 = new EquationFormula(t4, x);
		
		
		Set<Formula> f1 = ProofSystem.constantness.apply(List.of(eq1, eq2), Set.of(x));
		assertTrue(f1.contains(eq3));
		
		Resource aa = new Resource("a", Utils.INT, 1);
		Resource bb = new Resource("b", Utils.INT, 1);
		Resource cc = new Resource("c", Utils.INT, 0);
		Resource dd = new Resource("d", Utils.INT, 0);
		Resource yy = new Resource("x", Utils.INT, 0);
		DependencyTerm t5 = new DependencyTerm(aa, bb, cc);
		EquationFormula eq4 = new EquationFormula(t5, dd);
		DependencyTerm t6 = new DependencyTerm(yy, aa, dd);
		EquationFormula eq5 = new EquationFormula(t6, yy);
		Set<Formula> f2 = ProofSystem.constantness.apply(List.of(eq4), Set.of(yy));
		assertTrue(f2.contains(eq5));
	}
	
	@Test
	void RightNormalizationTest() {
		Dependency d1 = new Dependency(a, b);
		Dependency d2 = new Dependency(c, d);
		DependencyTerm t1 = new DependencyTerm(a, b, c);
		DependencyTerm t2 = new DependencyTerm(t1, d, e);
		DependencyTerm t3 = new DependencyTerm(c, d, e);
		DependencyTerm t4 = new DependencyTerm(a, b, t3);
		
		DependencyFormula df1 = new DependencyFormula(d1);
		DependencyFormula df2 = new DependencyFormula(d2);
		EquationFormula eq1 = new EquationFormula(t2, t4);
		Set<Formula> result = ProofSystem.rightNormalization.apply(List.of(df1, df2), Set.of(e));
		assertTrue(result.contains(eq1));
		
	}
	
	@Test
	void PseudoConstantnessTest() {
		Dependency d1 = new Dependency(a, b);
		DependencyTerm t1 = new DependencyTerm(a, b, b);
		DependencyFormula df1 =  new DependencyFormula(d1);
		EquationFormula eq1 = new EquationFormula(t1, a);
		Formula result = ProofSystem.pseudoConstantness.apply(List.of(df1));
		assertEquals(eq1, result);
	}

	@Test
	void UncurryingTest() {
		Dependency d1 = new Dependency(h, i);
		Dependency d2 = new Dependency(d1, a);
		DependencyTerm t1 = new DependencyTerm(a, b, c);
		DependencyTerm t2 = new DependencyTerm(d, e, f);
		DependencyFormula df1 = new DependencyFormula(d2);
		EquationFormula eq1 = new EquationFormula(t1, f);
		EquationFormula eq2 = new EquationFormula(t2, l);
		
		DependencyTerm t3 = new DependencyTerm(h, i, l);
		DependencyTerm t4 = new DependencyTerm(t3, a, f);
		DependencyTerm t5 = new DependencyTerm(h, i, d);
		DependencyTerm t6 = new DependencyTerm(t5, a, f, d, l);
		EquationFormula eq3 = new EquationFormula(t4, t6);
		
		
		Formula result = ProofSystem.uncurrying.apply(List.of(df1, eq1, eq2));
		assertEquals(result, eq3);
		
	}
	
}