import java.util.ArrayList;
import java.util.List;

import inference.ProofSystem;
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.Formula;
import models.terms.Dependency;
import models.terms.DependencyTerm;
import models.terms.EvaluatableTerm;
import models.terms.ResourceVariable;
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) {
		
		List<Formula> initialConditions = new ArrayList<>();
		ResourceVariable A = new ResourceVariable("A", INT, 2);
		ResourceVariable B = new ResourceVariable("B", INT, 2);
		ResourceVariable C = new ResourceVariable("C", INT, 2);
		ResourceVariable D = new ResourceVariable("D", INT, 2);
		ResourceVariable E = new ResourceVariable("E", INT, 1);
		ResourceVariable F = new ResourceVariable("F", INT, 1);
		ResourceVariable G = new ResourceVariable("G", INT, 0);
		
		ResourceVariable Ap = new ResourceVariable("A'", INT, 2);
		ResourceVariable Bp = new ResourceVariable("B'", INT, 2);
		ResourceVariable Cp = new ResourceVariable("C'", INT, 2);
		ResourceVariable Dp = new ResourceVariable("D'", INT, 2);
		ResourceVariable Fp = new ResourceVariable("F'", INT, 1);
		
		initialConditions.add(new DependencyFormula(new Dependency(new Dependency(A, B), D), F));
		initialConditions.add(new DependencyFormula(new Dependency(new Dependency(Ap, Bp), Dp), Fp));
		initialConditions.add(new EquationFormula(new DependencyTerm(A, B, C), new DependencyTerm(Ap, Bp, Cp)));
		EquationFormula conclusion = 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)
		);
		for(var cond : initialConditions) {
			System.out.println(cond.toString());
		}
		System.out.println(conclusion.toString());
		ProofSystem.check(initialConditions, conclusion);
		System.out.println("=======================");
		EvaluatableTerm lrn = conclusion.getLeftSideHand().linearRightNormalize();
		var subTerms = lrn.getSubTerms(EvaluatableTerm.class);
		System.out.println(conclusion.getLeftSideHand().linearRightNormalize().toString());
		for(var sub: subTerms.keySet()) {
			System.out.println(sub.getOrders().toString());
			System.out.println(subTerms.get(sub).toString());
		}
		System.out.println("==================");
		System.out.println(conclusion.getRightSideHand().linearRightNormalize().toString()); 
		
		
		sandbox1();
	}
	
	static void sandbox1() {
		System.out.println("------------------------------------------------------------sandbox1");
		ResourceVariable a = new ResourceVariable("A", INT, 2);
		ResourceVariable b = new ResourceVariable("B", INT, 2);
		ResourceVariable c = new ResourceVariable("C", INT, 2);
		ResourceVariable ap = new ResourceVariable("A'", INT, 2);
		ResourceVariable bp = new ResourceVariable("B'", INT, 2);
		ResourceVariable cp = new ResourceVariable("C'", INT, 2);
		
		DependencyTerm d1 = new DependencyTerm(a, b, c);
		DependencyTerm d11 = new DependencyTerm(a, b, c);
		DependencyTerm d2 = new DependencyTerm(ap, bp, cp);
		EquationFormula conclu1 = new EquationFormula(d1, d11);
		boolean tmp1 = ProofSystem.REFLEXIVE_LAW.check(List.of(), conclu1);
		d11.setDependingTerm(ap);
		boolean tmp2 = ProofSystem.LEFT_REPLACEMENT.check(List.of(new EquationFormula(a, ap)), conclu1);
		d11.setDependingTerm(a);
		d11.setDependedVariable(bp);
		boolean tmp3 = ProofSystem.CENTER_REPLACEMENT.check(List.of(new EquationFormula(b, bp)), conclu1);
		d11.setDependedVariable(b);
		d11.setArgumentTerm(cp);
		boolean tmp4 = ProofSystem.RIGHT_REPLACEMENT.check(List.of(new EquationFormula(c, cp)), conclu1);
		d11.setArgumentTerm(c);
		System.out.println(tmp2);
		System.out.println(tmp3);
		System.out.println(tmp4);
	}
	
	@SneakyThrows
	static Expression parse(String expr) {
		stream.addLine(expr);
		return parser.parseTerm(stream, model);
	}
	
	
}