package tests.equivalence;

import java.util.HashMap;
import java.util.List;
import java.util.Map;

import org.junit.jupiter.api.Test;

import inference.equivalence.MetaSemanticEquivalenceRelation;
import inference.equivalence.SemanticEquivalenceRelation;
import models.algebra.Variable;
import models.terms.DependencyTerm;
import models.terms.LinearRightNormalizedType;
import models.terms.RDLTerm;
import models.terms.ResourceVariable;
import models.terms.meta.MetaEvaluatableTermVariable;
import models.terms.meta.MetaRDLTerm;
import models.terms.meta.MetaResourceVariable;
import models.terms.meta.OrderConstraint;
import models.terms.meta.OrderVariableConstraint;
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);
		}
	}
	
	@Test
	void SubstituteTest2() {
		MetaEvaluatableTermVariable t = new MetaEvaluatableTermVariable(new Variable("t"), Utils.parse("n + 1"));
		t.setLinearRightNormalizedType(LinearRightNormalizedType.LINEAR_RIGHT_NORMALIZED);
		MetaEvaluatableTermVariable tp = new MetaEvaluatableTermVariable(new Variable("t'"), Utils.parse("n + 1"));
		tp.setLinearRightNormalizedType(LinearRightNormalizedType.LINEAR_RIGHT_NORMALIZED);
		MetaSemanticEquivalenceRelation r1 = new MetaSemanticEquivalenceRelation(t, tp, Utils.parse("n + 1"));
		DependencyTerm t1 = new DependencyTerm(A, B, C);
		DependencyTerm t2 = new DependencyTerm(Ap, Bp, Cp);
		SemanticEquivalenceRelation r2 = new SemanticEquivalenceRelation(t1, t2, 2);
		MetaResourceVariable v = new MetaResourceVariable(new Variable("v"), Utils.parse("n + 1"));
		MetaEvaluatableTermVariable s = new MetaEvaluatableTermVariable(new Variable("s"), OrderConstraint.LT, Utils.parse("n + 1"));
		MetaSemanticEquivalenceRelation r3 = new MetaSemanticEquivalenceRelation(
				new MetaRDLTerm(t, v, s),
				new MetaRDLTerm(tp, v, s),
				Utils.parse("n")
		);
		
		Map<Variable, RDLTerm> binding = new HashMap<>();
		Map<Variable, OrderVariableConstraint> orderConstraint = new HashMap<>();
		r1.isMatchedBy(r2, binding, orderConstraint);
		var tmp = r3.substitute(binding, orderConstraint, List.of(D, E, F, G));
		System.out.println();
		System.out.println(binding);
		for(var a : tmp) {
			System.out.println(a);
		}
	}
	
}