import java.util.List;

import inference.InferenceRule;
import lombok.SneakyThrows;
import models.algebra.Expression;
import models.algebra.Type;
import models.algebra.Variable;
import models.dataConstraintModel.DataConstraintModel;
import models.dataFlowModel.DataTransferModel;
import models.formulas.EquationFormula;
import models.formulas.meta.MetaEquationFormula;
import models.terms.DependencyTerm;
import models.terms.ResourceVariable;
import models.terms.meta.MetaEvaluatableTermVariable;
import models.terms.meta.MetaRDLTerm;
import models.terms.meta.MetaResourceVariable;
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();
	
	public static void main(String[] args) {

		Type INT = DataConstraintModel.typeInt;
		
		MetaEvaluatableTermVariable te = new MetaEvaluatableTermVariable(new Variable("te"));
		MetaEvaluatableTermVariable ue = new MetaEvaluatableTermVariable(new Variable("ue"));
		MetaEvaluatableTermVariable se = new MetaEvaluatableTermVariable(new Variable("se"));
		MetaResourceVariable v = new MetaResourceVariable(new Variable("v"));
		MetaEquationFormula assump1 = new MetaEquationFormula(te, ue);
		MetaEquationFormula concl1 = new MetaEquationFormula(new MetaRDLTerm(se, v, te), new MetaRDLTerm(se, v, ue));
		/*
		 *                 te = ue
		 *  ----------------------------------------
		 *   [se : v -> te] = [se : v -> ue]
		 */
		InferenceRule rightReplacement = new InferenceRule(List.of(assump1), concl1);

		ResourceVariable a = new ResourceVariable("a", INT, 0);
		ResourceVariable b = new ResourceVariable("b", INT, 0);
		ResourceVariable c = new ResourceVariable("c", INT, 0);
		ResourceVariable d = new ResourceVariable("d", INT, 0);
		ResourceVariable x = new ResourceVariable("x", INT, 0);
		ResourceVariable y = new ResourceVariable("y", INT, 0);
		ResourceVariable z = new ResourceVariable("z", INT, 0);
		DependencyTerm xyz = new DependencyTerm(x, y, z);
		EquationFormula assump2 = new EquationFormula(a, xyz); // a = [x : y -> z]
		EquationFormula concl2 = new EquationFormula(new DependencyTerm(c, d, a), new DependencyTerm(c, d, xyz)); // [c : d -> a] = [c : d -> [x : y -> z]]
		
		System.out.println(rightReplacement.check(List.of(assump2), concl2));
		System.out.println(rightReplacement.toString());
		
	}

	@SneakyThrows
	static Expression parse(String expr) {
		stream.addLine(expr);
		return parser.parseTerm(stream, model);
	}
	
	
}