package tests.inferencerule;

import static org.junit.jupiter.api.Assertions.*;
import static tests.Utils.*;

import java.util.List;

import org.junit.jupiter.api.Test;

import inference.InferenceRule;
import models.algebra.Variable;
import models.formulas.DependencyFormula;
import models.formulas.EquationFormula;
import models.formulas.meta.MetaDependencyFormula;
import models.formulas.meta.MetaEquationFormula;
import models.terms.Dependency;
import models.terms.DependencyTerm;
import models.terms.Resource;
import models.terms.meta.MetaEvaluatableTermVariable;
import models.terms.meta.MetaRDLTerm;
import models.terms.meta.MetaResource;

public class InferenceRuleTest {

	@Test
	void InferenceRuleTerst1() {
		MetaEvaluatableTermVariable te = new MetaEvaluatableTermVariable(new  Variable("te"));
		MetaResource v = new MetaResource(new Variable("v"));
		MetaResource w = new MetaResource(new Variable("w"));
		MetaRDLTerm metaD1 = new MetaRDLTerm(te, v);
		MetaRDLTerm metaD2 = new MetaRDLTerm(v, w);
		MetaRDLTerm metaD3 = new MetaRDLTerm(te, w);
		MetaDependencyFormula metaDf1 = new MetaDependencyFormula(metaD1);
		MetaDependencyFormula metaDf2 = new MetaDependencyFormula(metaD2);
		MetaDependencyFormula metaDf3 = new MetaDependencyFormula(metaD3);
		InferenceRule goseShazo = new InferenceRule(List.of(metaDf1, metaDf2), metaDf3);
		
		Resource a = new Resource("a", INT, 0);
		Resource b = new Resource("b", INT, 0);
		Resource c = new Resource("c", INT, 0);
		Dependency d1 = new Dependency(a, b);
		Dependency d2 = new Dependency(b, c);
		Dependency d3 = new Dependency(a, c);
		DependencyFormula df1 = new DependencyFormula(d1); // a : b
		DependencyFormula df2 = new DependencyFormula(d2); // b : c
		DependencyFormula df3 = new DependencyFormula(d3); // a : c
		assertTrue(goseShazo.check(List.of(df1, df2), df3));
		
	}
	
	@Test
	void InferencuRuleTest2() {
		MetaEvaluatableTermVariable te = new MetaEvaluatableTermVariable(new Variable("te"));
		MetaEvaluatableTermVariable ue = new MetaEvaluatableTermVariable(new Variable("ue"));
		MetaEvaluatableTermVariable se = new MetaEvaluatableTermVariable(new Variable("se"));
		MetaResource v = new MetaResource(new Variable("v"));
		MetaEquationFormula assump1 = new MetaEquationFormula(te, ue);
		MetaEquationFormula concl1 = new MetaEquationFormula(new MetaRDLTerm(se, v, te), new MetaRDLTerm(se, v, ue));
		/*
		 *                 te = ue
		 *  ----------------------------------------
		 *   [se : v -> te] = [se : v -> ue]
		 */
		InferenceRule rightReplacement = new InferenceRule(List.of(assump1), concl1);

		Resource a = new Resource("a", INT, 0);
		Resource c = new Resource("c", INT, 0);
		Resource d = new Resource("d", INT, 0);
		Resource x = new Resource("x", INT, 0);
		Resource y = new Resource("y", INT, 0);
		Resource z = new Resource("z", INT, 0);
		DependencyTerm xyz = new DependencyTerm(x, y, z);
		EquationFormula assump2 = new EquationFormula(a, xyz); // a = [x : y -> z]
		EquationFormula concl2 = new EquationFormula(new DependencyTerm(c, d, a), new DependencyTerm(c, d, xyz)); // [c : d -> a] = [c : d -> [x : y -> z]]
		
		assertTrue(rightReplacement.check(List.of(assump2), concl2));
	}
	
}