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.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)));
		Formula 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);
	}
	
	@SneakyThrows
	static Expression parse(String expr) {
		stream.addLine(expr);
		return parser.parseTerm(stream, model);
	}
	
	
}