import java.util.List;

import inference.rewrite.Position;
import inference.rewrite.ResourceTree;
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.EquationFormula;
import models.formulas.Then;
import models.terms.DependencyTerm;
import models.terms.Resource;
import parser.Parser;
import parser.Parser.TokenStream;

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) {
		sandbox4();
		System.out.println("=====================================");
		System.out.println("=====================================");
		System.out.println("=====================================");
		sandbox5();
	}
	
	static void sandbox1() {
		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 G = new Resource("G",  INT, 1);
		DependencyTerm t1 = new DependencyTerm(A, B, C, D, E);
		DependencyTerm t2 = new DependencyTerm(t1, F, G);
		System.out.println(t2);
		ResourceTree rt = new ResourceTree(t2);
		System.out.println(rt);
		rt.debug(new Position(List.of(0)));
	}
	
	static void sandbox2() {
		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 G = new Resource("G",  INT, 1);
		Resource H = new Resource("H",  INT, 1);
		Resource I = new Resource("I",  INT, 1);
		Resource J = new Resource("J",  INT, 1);
		Resource K = new Resource("K",  INT, 1);
		Resource L = new Resource("L",  INT, 1);
		Resource M = new Resource("M",  INT, 1);
		Resource N = new Resource("N",  INT, 1);
		Resource O = new Resource("O",  INT, 1);
		Resource P = new Resource("P",  INT, 1);
		Resource Q = new Resource("Q",  INT, 1);
		
		DependencyTerm t1 = new DependencyTerm(A, B, C, D, E);
		DependencyTerm t2 = new DependencyTerm(G, H, I, J, K);
		DependencyTerm t3 = new DependencyTerm(M, N, O, P, Q);
		DependencyTerm t4 = new DependencyTerm(t1, F, t2, L, t3);
		System.out.println(t4);
		ResourceTree rt = new ResourceTree(t4);
		System.out.println(rt);
		rt.debug(new Position());
		rt.debugAllPath();
		
	}
	
	static void sandbox3() {
		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 x = new Resource("x",  INT, 0);
		Resource y = new Resource("y",  INT, 1);
		DependencyTerm t1 = new DependencyTerm(A, B, C);
		DependencyTerm t2 = new DependencyTerm(B, C, D);
		EquationFormula f1 = new EquationFormula(t1, x);
		EquationFormula f2 = new EquationFormula(y, t2);
		RewriteInferenceSystem ris = new RewriteInferenceSystem(List.of(f1, f2), null);
		ris.inference();
		
	}
	
	static void sandbox4() {
		Resource uadd = new Resource("uadd", INT, 1);
		Resource add = new Resource("add", INT, 1);
		Resource cid = new Resource("cid", INT, 1);
		Resource org = new Resource("org", INT, 1);
		Resource uid = new Resource("uid", INT, 1);
		Resource x = new Resource("x", INT, 0);
		Resource y = new Resource("y", INT, 0);
		DependencyTerm t1 = new DependencyTerm(add, cid, org);
		DependencyTerm t2 = new DependencyTerm(org, uid, x);
		DependencyTerm t3 = new DependencyTerm(uadd, uid, x);
		DependencyTerm t4 = new DependencyTerm(add, cid, y);
		EquationFormula f1 = new EquationFormula(uadd, t1);
		EquationFormula f2 = new EquationFormula(t2, y);
		EquationFormula f3 = new EquationFormula(t3, t4);
		RewriteInferenceSystem ris = new RewriteInferenceSystem(List.of(f1, f2), f3);
		ris.inference();
		
	}
	
	static void sandbox5() {
		Resource uadd = new Resource("uadd", INT, 1);
		Resource add = new Resource("add", INT, 1);
		Resource cid = new Resource("cid", INT, 1);
		Resource org = new Resource("org", INT, 1);
		Resource uid = new Resource("uid", 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(add, cid, x);
		DependencyTerm t3 = new DependencyTerm(org, uid, z);
		DependencyTerm t4 = new DependencyTerm(uadd, uid, z);
		
		EquationFormula f1 = new EquationFormula(uadd, t1);
		EquationFormula f2 = new EquationFormula(t2, y);
		EquationFormula f3 = new EquationFormula(t3, x);
		EquationFormula f4 = new EquationFormula(t4, y);
		Then f5 = new Then(f3, f4);
		
		RewriteInferenceSystem ris = new RewriteInferenceSystem(List.of(f1, f2), f5);
		ris.inference();
		
	}
	
	
	static void sandbox7() {
		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 G = new Resource("G",  INT, 1);
		Resource H = new Resource("H",  INT, 1);
		Resource I = new Resource("I",  INT, 1);
		Resource J = new Resource("J",  INT, 1);
		Resource K = new Resource("K",  INT, 1);
		Resource L = new Resource("L",  INT, 1);
		Resource M = new Resource("M",  INT, 1);
		Resource N = new Resource("N",  INT, 1);
		Resource O = new Resource("O",  INT, 1);
		
		DependencyTerm t1 = new DependencyTerm(A, B, C);
		DependencyTerm t2 = new DependencyTerm(I, J, K);
		DependencyTerm t3 = new DependencyTerm(M, N, O);
		DependencyTerm t4 = new DependencyTerm(E, F, G, H, t2);
		DependencyTerm t5 = new DependencyTerm(t1, D, t4, L, t3);
		
		ResourceTree rt = new ResourceTree(t5);
		System.out.println(rt);
		rt.debug(new Position(List.of(0)));
	}
	
	
	@SneakyThrows
	static Expression parse(String expr) {
		stream.addLine(expr);
		return parser.parseTerm(stream, model);
	}
	
	
}