import java.util.Set;

import constants.Types;
import inference.ProofSystem;
import models.Position;
import models.algebra.Type;
import models.formulas.DependencyFormula;
import models.formulas.EquationFormula;
import models.terms.DependencyTerm;
import models.terms.EvaluatableTerm;
import models.terms.Resource;
import models.terms.ResourceConstant;

public class Main {

	static Type INT = Types.typeInt;

	public static void main(String[] args) {
		//
		sandbox3();
	}
	
	static void sandbox() {
		Resource x = new Resource("x", 1);
		Resource y = new Resource("y", 1);
		Resource z = new Resource("z", 1);
		DependencyTerm t1 = new DependencyTerm(x, y, z);
		DependencyTerm t2 = new DependencyTerm(t1, y, z);
		var tmp = t2.getSubTerms(EvaluatableTerm.class);
		System.out.println(tmp);
		for (var pos: tmp.keySet()) {
			System.out.println(Position.convertPosition(pos) + ", " + tmp.get(pos));
		}
	}

	static void sandbox2() {
		Resource x = new Resource("x", 1);
		Resource y = new Resource("y", 1);
		Resource z = new Resource("z", 1);
		DependencyFormula d1 = new DependencyFormula(x, y);
		DependencyFormula d2 = new DependencyFormula(y, z);
		DependencyFormula d3 = new DependencyFormula(x, z);
		DependencyTerm t1 = new DependencyTerm(x, y, new ResourceConstant("2"));
		DependencyTerm t2 = new DependencyTerm(y, z, new ResourceConstant("4"));
		DependencyTerm t3 = new DependencyTerm(x, z, new ResourceConstant("4"));
		EquationFormula eq1 = new EquationFormula(t1, new ResourceConstant("3"));
		EquationFormula eq2 = new EquationFormula(t2, new ResourceConstant("2"));
		EquationFormula eq3 = new EquationFormula(t3, new ResourceConstant("2"));
		ProofSystem ps = new ProofSystem(Set.of(d1, d2, eq1, eq2), eq3);
		ps.inference();
		System.out.println(ps.getInferenceHistoryString());
		
	}
	
	static void sandbox3() {
		Resource x = new Resource("x", 1);
		Resource y = new Resource("y", 1);
		Resource z = new Resource("z", 1);
		Resource w = new Resource("w", 1);
		DependencyFormula d1 = new DependencyFormula(x, y);
		DependencyFormula d2 = new DependencyFormula(y, z);
		DependencyFormula d3 = new DependencyFormula(z, w);
		DependencyTerm t1 = new DependencyTerm(x, y, new ResourceConstant("1"));
		DependencyTerm t2 = new DependencyTerm(y, z, new ResourceConstant("3"));
		DependencyTerm t3 = new DependencyTerm(z, w, new ResourceConstant("4"));
		DependencyTerm t4 = new DependencyTerm(x, w, new ResourceConstant("4"));
		EquationFormula eq1 = new EquationFormula(t1, new ResourceConstant("2"));
		EquationFormula eq2 = new EquationFormula(t2, new ResourceConstant("1"));
		EquationFormula eq3 = new EquationFormula(t3, new ResourceConstant("3"));
		EquationFormula eq4 = new EquationFormula(t4, new ResourceConstant("2"));
		ProofSystem ps = new ProofSystem(Set.of(d1, d2, d3, eq1, eq2, eq3), eq4);
		ps.inference();
		System.out.println(ps.getInferenceHistoryString());
	}
	
}