package tests.equivalence;

import java.util.List;

import org.junit.jupiter.api.Test;

import inference.equivalence.MetaSemanticEquivalenceRelation;
import models.algebra.Variable;
import models.terms.DependencyTerm;
import models.terms.LinearRightNormalizedType;
import models.terms.ResourceVariable;
import models.terms.meta.MetaEvaluatableTermVariable;
import models.terms.meta.MetaRDLTerm;
import models.terms.meta.MetaResourceVariable;
import tests.Utils;

public class SubstituteTest {

	ResourceVariable A = new ResourceVariable("A", Utils.INT, 2);
	ResourceVariable Ap = new ResourceVariable("A'", Utils.INT, 2);
	ResourceVariable B = new ResourceVariable("B", Utils.INT, 2);
	ResourceVariable Bp = new ResourceVariable("B'", Utils.INT, 2);
	ResourceVariable C = new ResourceVariable("C", Utils.INT, 2);
	ResourceVariable Cp = new ResourceVariable("C'", Utils.INT, 2);
	ResourceVariable D = new ResourceVariable("D", Utils.INT, 2);
	ResourceVariable E = new ResourceVariable("E", Utils.INT, 1);
	ResourceVariable F = new ResourceVariable("F", Utils.INT, 1);
	ResourceVariable G = new ResourceVariable("G", Utils.INT, 0);
	
	@Test
	void SubstituteTest1() {
		MetaResourceVariable v = new MetaResourceVariable(new Variable("v"), Utils.parse("n + 1"));
		MetaEvaluatableTermVariable t = new MetaEvaluatableTermVariable(new Variable("t"), Utils.parse("n"));
		t.setLinearRightNormalizedType(LinearRightNormalizedType.LINEAR_RIGHT_NORMALIZED);
		MetaSemanticEquivalenceRelation r1 = new MetaSemanticEquivalenceRelation(new MetaRDLTerm(v, v, t), t, new Variable("n"));
		DependencyTerm t1 = new DependencyTerm(A, A, E);
		var tmp = r1.substitute(t1, List.of(Ap, Bp, C, Cp, D, E, F, G));
		for(var a : tmp) {
			System.out.println(a);
		}
	}
	
}