import java.util.List;

import inference.ProofSystem;
import inference.equivalence.SemanticEquivalenceProofSystem;
import inference.equivalence.SemanticEquivalenceRelation;
import inference.rewrite.RewriteInferenceSystem;
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.Resource;
import models.terms.ResourceConstant;
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) {
//		sandbox1();
//		sandbox2();
//		sandbox3();
//		sandbox4();
//		ProofSystem.debug();
		sandbox6();
	}
	
	static void sandbox1() {
		Resource A = new Resource("A", Utils.INT, 2);
		Resource Ap = new Resource("A'", Utils.INT, 2);
		Resource B = new Resource("B", Utils.INT, 2);
		Resource Bp = new Resource("B'", Utils.INT, 2);
		Resource C = new Resource("C", Utils.INT, 2);
		Resource Cp = new Resource("C'", Utils.INT, 2);
		Resource D = new Resource("D", Utils.INT, 2);
		Resource E = new Resource("E", Utils.INT, 1);
		Resource F = new Resource("F", Utils.INT, 1);
		Resource G = new Resource("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
		);
		SemanticEquivalenceProofSystem.debug();
		System.out.println();
		System.out.println(assumptionFormula);
		System.out.println(conclusionFormula);
//		System.out.println(conclusionFormula.linearRightNormalized());
		System.out.println(proofSystem.proof());
	}
	
	static void sandbox2() {
		ProofSystem.debug();
	}
	
	static void sandbox3() {
		Resource followee = new Resource("followee", INT, 2);
		Resource fno = new Resource("fno", INT, 2);
		ResourceConstant one = new ResourceConstant("1");
		ResourceConstant A = new ResourceConstant("A");
		ResourceConstant C = new ResourceConstant("C");
		Resource aid = new Resource("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);
		DependencyFormula f4 = new DependencyFormula(new Dependency(new SetEvaluatableTerm(followee), aid));
		InFormula f5 = new InFormula(A, new SetEvaluatableTerm(aid));
		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);
		System.out.println();
		boolean result = ProofSystem.check(List.of(f1, f2, f3, f4, f5), conclusion);
		System.out.println();
		System.out.println(result);
	}
	
	static void sandbox4() {
		Resource X = new Resource("X", INT, 1);
		Resource Y= new Resource("Y", INT, 1);
		Resource U = new Resource("U", INT, 1);
		Resource W = new Resource("W", INT, 1);
		
		EquationFormula f1 = new EquationFormula(X, Y);
		DependencyFormula f2 = new DependencyFormula(X, U);
		DependencyFormula f3 = new DependencyFormula(U, W);
		DependencyTerm t1 = new DependencyTerm(X, U, U);
		DependencyTerm t2 = new DependencyTerm(t1, W, W);
		DependencyTerm t3 = new DependencyTerm(Y, U, U);
		DependencyTerm t4 = new DependencyTerm(t3, W, W);
//		EquationFormula f4 = new EquationFormula(t1, X);
//		EquationFormula f4 = new EquationFormula(X, t1);
//		EquationFormula f4 = new EquationFormula(t2, X);
//		EquationFormula f4 = new EquationFormula(t3, Y);
//		EquationFormula f4 = new EquationFormula(t4, Y);
		EquationFormula f4 = new EquationFormula(t2, t4);
//		DependencyFormula f4 = new DependencyFormula(Y, U);
		System.out.println(f1 + ", " + f2 + ", " + f3);
		boolean result = ProofSystem.check(List.of(f1, f2, f3), f4);
		System.out.println(result);
	}
	
	static void sandbox5() {
		Resource a = new Resource("a", INT, 1);
		Resource b = new Resource("b", INT, 1);
		Resource c = new Resource("c", INT, 1);
		Resource d = new Resource("d", INT, 1);
		Resource e = new Resource("e", INT, 1);
		Resource f = new Resource("f", INT, 1);
		Resource x = new Resource("x", INT, 0);
		Resource y = new Resource("y", INT, 0);
		DependencyTerm t1 = new DependencyTerm(a, b, c, d, e);
		DependencyTerm t2 = new DependencyTerm(t1, f, x);
		EquationFormula fm = new EquationFormula(t2, y);
		System.out.println(t1);
		System.out.println(t2);
		System.out.println(fm);
		RewriteInferenceSystem tmp = new RewriteInferenceSystem(List.of(fm), null);
		tmp.debug();
		tmp.inference();
	}
	
	static void sandbox6() {
		Resource uid = new Resource("uid", INT, 1);
		Resource org = new Resource("org", INT, 1);
		Resource uadd = new Resource("uadd", INT, 1);
		Resource cid = new Resource("cid", INT, 1);
		Resource add = new Resource("add", INT, 1);
		Resource addP = new Resource("add'", INT, 1);
		Resource cidP = new Resource("cid'", INT, 1);
		Resource orgP = new Resource("org'", INT, 1);
		Resource uidP = new Resource("uid'", INT, 1);
		Resource uaddP = new Resource("uadd'", INT, 1);
		Resource x = new Resource("x", INT, 0);
		Resource y = new Resource("y", INT, 0);
		Resource z = new Resource("z", INT, 0);
		
		DependencyTerm t1 = new DependencyTerm(add, cid, org);
		DependencyTerm t2 = new DependencyTerm(addP, cidP, orgP);
		DependencyTerm t3 = new DependencyTerm(orgP, uidP, x);
		DependencyTerm t4 = new DependencyTerm(add, cid, y);
		DependencyTerm t5 = new DependencyTerm(uaddP, uidP, x);
		
		EquationFormula f1 = new EquationFormula(uadd, t1);
		EquationFormula f2 = new EquationFormula(uaddP, t2);
		EquationFormula f3 = new EquationFormula(t3, y);
		EquationFormula f4 = new EquationFormula(t4, t5);
		
		RewriteInferenceSystem tmp = new RewriteInferenceSystem(List.of(f1, f2, f3), f4);
		tmp.debug();
		tmp.inference();
		
	}
	
	
	@SneakyThrows
	static Expression parse(String expr) {
		stream.addLine(expr);
		return parser.parseTerm(stream, model);
	}
	
	
}