package tests.formulas.meta;

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

import org.junit.jupiter.api.Test;

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.EvaluatableTerm;
import models.terms.Resource;
import models.terms.meta.MetaEvaluatableTermVariable;
import models.terms.meta.MetaRDLTerm;
import models.terms.meta.MetaResource;

public class MetaEquationFormulaTest {

	@Test
	void MetaEquationFormulaMatchingTest() {
		
		Resource a = new Resource("a", INT, 0);
		Resource b = new Resource("b", INT, 0);
		Resource c = new Resource("c", INT, 0);
		Resource d = new Resource("d", INT, 0);
		EvaluatableTerm te1 = new DependencyTerm(a, b, c);
		EvaluatableTerm te2 = new DependencyTerm(a, b, d);
		EquationFormula formula = new EquationFormula(te1, te2);
		
		
		MetaEvaluatableTermVariable se = new MetaEvaluatableTermVariable(new Variable("se"));
		MetaResource v = new MetaResource(new Variable("v"));
		MetaEvaluatableTermVariable te = new MetaEvaluatableTermVariable(new Variable("te"));
		MetaEvaluatableTermVariable ue = new MetaEvaluatableTermVariable(new Variable("ue"));
		MetaRDLTerm left = new MetaRDLTerm(se, v, te);
		MetaRDLTerm right = new MetaRDLTerm(se, v, ue);
		MetaEquationFormula metaFormula = new MetaEquationFormula(left, right);
		
		// [a : b -> c] = [a : b -> d] matches [se : v -> te] = [se : v -> ue]
		assertTrue(metaFormula.isMatchedBy(formula));
		
	}
	
	@Test
	void MetaDependencyFormulaMatchingTest() {
		Resource a = new Resource("a", INT, 0);
		Resource b = new Resource("b", INT, 0);
		Resource c = new Resource("c", INT, 0);
		EvaluatableTerm te1 = new DependencyTerm(a, b, c);
		Resource d = new Resource("d", INT, 0);
		Dependency d1 = new Dependency(te1, d);
		DependencyFormula depF = new DependencyFormula(d1);
		
		MetaEvaluatableTermVariable te = new MetaEvaluatableTermVariable(new Variable("te"));
		MetaResource w = new MetaResource(new Variable("w"));
		MetaRDLTerm dep = new MetaRDLTerm(te, w);
		MetaDependencyFormula metaDepF = new MetaDependencyFormula(dep);
		
		//[a : b -> c] : d matches te : w
		assertTrue(metaDepF.isMatchedBy(depF));
	}
	
}