import java.util.List;

import inference.ProofSystem;
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.DependencyFormula;
import models.formulas.EquationFormula;
import models.formulas.InFormula;
import models.terms.Dependency;
import models.terms.DependencyTerm;
import models.terms.ResourceConstant;
import models.terms.ResourceVariable;
import models.terms.SetEvaluatableTerm;
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) {
		
//		sandbox2();
		sandbox3();
	}
	
	static void sandbox1() {
		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());
	}
	
	static void sandbox2() {
		ProofSystem.debug();
	}
	
	static void sandbox3() {
		ResourceVariable followee = new ResourceVariable("followee", INT, 2);
		ResourceVariable fno = new ResourceVariable("fno", INT, 2);
		ResourceConstant one = new ResourceConstant("1");
		ResourceConstant A = new ResourceConstant("A");
		ResourceConstant C = new ResourceConstant("C");
		ResourceVariable aid = new ResourceVariable("aid", INT, 1);
		DependencyTerm t1 = new DependencyTerm(followee, fno, one);
		Dependency d1 = new Dependency(t1, aid);
		DependencyTerm t2 = new DependencyTerm(one, aid, A);
		DependencyTerm t3 = new DependencyTerm(new SetEvaluatableTerm(fno), aid, A);
		DependencyTerm t4 = new DependencyTerm(t1, aid, A);
		
		DependencyFormula f1 = new DependencyFormula(d1);
		InFormula f2 = new InFormula(t2, t3);
		EquationFormula f3 = new EquationFormula(t4, C);
		InFormula conclusion = new InFormula(C, new SetEvaluatableTerm(new SetEvaluatableTerm(followee)));
		
		System.out.println(f1);
		System.out.println(f2);
		System.out.println(f3);
		System.out.println(conclusion);
		boolean result = ProofSystem.check(List.of(f1, f2, f3), conclusion);
		System.out.println(result);
	}
	
	
	
	@SneakyThrows
	static Expression parse(String expr) {
		stream.addLine(expr);
		return parser.parseTerm(stream, model);
	}
	
	
}