import java.util.List;

import inference.equivalence.SemanticEquivalenceProofSystem;
import inference.equivalence.SemanticEquivalenceRelation;
import lombok.SneakyThrows;
import models.algebra.Expression;
import models.algebra.Type;
import models.dataConstraintModel.DataConstraintModel;
import models.dataFlowModel.DataTransferModel;
import models.formulas.EquationFormula;
import models.terms.DependencyTerm;
import models.terms.ResourceVariable;
import parser.Parser;
import parser.Parser.TokenStream;
import tests.Utils;

public class Main {

	static TokenStream stream = new Parser.TokenStream();
	static Parser parser = new Parser(stream);
	static DataTransferModel model = new DataTransferModel();
	
	static Type INT = DataConstraintModel.typeInt;

	public static void main(String[] args) {
		
		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);
		DependencyTerm t1 = new DependencyTerm(A, B, C);
		DependencyTerm t2 = new DependencyTerm(Ap, Bp, Cp);
		EquationFormula assumptionFormula = new EquationFormula(t1, t2);
		EquationFormula conclusionFormula = new EquationFormula(
				new DependencyTerm(new DependencyTerm(new DependencyTerm(A, B, C), D, E), F, G),
				new DependencyTerm(new DependencyTerm(new DependencyTerm(Ap, Bp, Cp), D, E), F, G)
		);
		
		SemanticEquivalenceProofSystem proofSystem = new SemanticEquivalenceProofSystem(
				List.of(new SemanticEquivalenceRelation(assumptionFormula, 2)),
				conclusionFormula
		);
		
//		System.out.println(conclusionFormula.linearRightNormalized());
		System.out.println(proofSystem.proof());
//		sandbox2();
	}
	
	static void sandbox2() {
		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);
		DependencyTerm t1 = new DependencyTerm(A, B, C);
		DependencyTerm t2 = new DependencyTerm(t1, B, E);
		System.out.println(t2);
		System.out.println(t2.isLinearRightNormalized());
		t2.selfLinearRightNormalize();
		System.out.println(t2);
	}
	
	
	
	@SneakyThrows
	static Expression parse(String expr) {
		stream.addLine(expr);
		return parser.parseTerm(stream, model);
	}
	
	
}