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.algebra.Variable;
import models.formulas.DependencyFormula;
import models.formulas.EquationFormula;
import models.formulas.Formula;
import models.terms.Resource;
import models.terms.meta.MatchConstraint;

public class DependencyAxiomTest {
	
	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", 2);
	Resource j = new Resource("j", 2);
	Resource k = new Resource("k", 2);
	
	@Test
	void IdentityMappingTest() {
		Set<Formula> res = ProofSystem.identityMapping.derive(List.of(new EquationFormula(a, b)));
		assertTrue(res.contains(new DependencyFormula(a, b)));
	}
	
	@Test
	void ArgumentExtensionTest() {
		MatchConstraint constraint = MatchConstraint.createDefault();
		constraint.setBinding(new Variable("ue"), d);
		Set<Formula> res = ProofSystem.argumentExtension.derive(List.of(new DependencyFormula(a, b, c)), constraint);
		assertTrue(res.contains(new DependencyFormula(a, b, c, d)));
	}
	
	@Test
	void CompositeMappingTest() {
	}
	
	@Test
	void ConstantMappingTest() {
		//todo
	}
	
	@Test
	void UncurriedMappingTest() {
	}
	
	@Test
	void RedundantDependencyTest() {
		//todo
	}
	
	@Test
	void RedundancyEliminationTest() {
	}
	
}