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

import java.util.HashSet;
import java.util.List;
import java.util.Set;

import org.junit.jupiter.api.Test;

import inference.ProofSystem;
import models.formulas.DependencyFormula;
import models.formulas.EquationFormula;
import models.terms.DependencyTerm;
import models.terms.EvaluatableTerm;
import models.terms.RDLTerm;
import models.terms.Resource;

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);
	Resource o = new Resource("o", 3);
	
	@Test
	void ReflexivityTest() {
		Set<RDLTerm> terms = new HashSet<>();
		terms.add(a);
		terms.add(b);
		Set<EvaluatableTerm> formulas = ProofSystem.reflexivity.apply(List.of(), a);
		assertTrue(formulas.contains(a));
	}
	
	@Test
	void SymmetryTest() {
		Set<EvaluatableTerm> formulas = ProofSystem.symmetry.apply(List.of(new EquationFormula(a, b)), a);
		assertTrue(formulas.contains(b));
		formulas = ProofSystem.symmetry.apply(List.of(new EquationFormula(a, b)), b);
		assertTrue(formulas.contains(a));
	}
	
	@Test
	void TransitivityTest() {
		Set<EvaluatableTerm> formulas = ProofSystem.transitivity.apply(List.of(new EquationFormula(a, b), new EquationFormula(b, c)), c);
		assertTrue(formulas.contains(a));
	}
	
	@Test
	void RightSubTest() {
		EquationFormula eq1 = new EquationFormula(a, b);
		DependencyFormula d1 = new DependencyFormula(c, d);
		Set<EvaluatableTerm> formulas = ProofSystem.rightSubstitution.apply(List.of(eq1, d1), new DependencyTerm(c, d, a));
		assertTrue(formulas.contains(new DependencyTerm(c, d, b)));
	}
	
	@Test
	void LeftSubTest() {
		EquationFormula eq1 = new EquationFormula(a, b);
		Set<EvaluatableTerm> formulas = ProofSystem.leftSubstitution.apply(List.of(eq1), new DependencyTerm(a, c, d));
		assertTrue(formulas.contains(new DependencyTerm(b, c, d)));
		formulas = ProofSystem.leftSubstitution.apply(List.of(eq1), new DependencyTerm(b, c, d));
		assertTrue(formulas.contains(new DependencyTerm(a, c, d)));
		
	}
	
	@Test
	void IdentityTest() {
		Set<EvaluatableTerm> terms = ProofSystem.identity.apply(List.of(), new DependencyTerm(a, a, b));
		assertTrue(terms.contains(b));
	}
	
	@Test
	void MapCompositionTest() {
		DependencyFormula d1 = new DependencyFormula(a, b, c);
		DependencyFormula d2 = new DependencyFormula(b, d, e);
		DependencyTerm dt1 = new DependencyTerm(a, d, f, e, g, c, h);
		DependencyTerm dt2 = new DependencyTerm(a, b, new DependencyTerm(b, d, f, e, g), c, h);
		Set<EvaluatableTerm> terms = ProofSystem.mapComposition.apply(List.of(d1, d2), dt1);
		assertTrue(terms.contains(dt2));
		terms = ProofSystem.mapComposition.apply(List.of(d1, d2), dt2);
		assertTrue(terms.contains(dt1));
	}
	
	@Test
	void ConstantnessTest() {
		DependencyTerm dt1 = new DependencyTerm(new DependencyTerm(a, o, b), m, c);
		DependencyTerm dt2 = new DependencyTerm(a, m, b);
		Set<EvaluatableTerm> terms = ProofSystem.constantness.apply(List.of(), dt1);
		assertTrue(terms.contains(a));
		terms = ProofSystem.constantness.apply(List.of(), dt2);
		assertTrue(terms.contains(a));
	}
	
	@Test
	void RightNormalizationTest() {
	}
	
	@Test
	void PseudoConstantnessTest() {
	}
	
	@Test
	void UncurryingTest() {
	}
	
	@Test
	void ArgumentDependencyExtractionTest() {
	}
	
}