import java.util.HashMap;
import java.util.Map;
import java.util.Set;

import constants.Types;
import inference.ProofSystem;
import models.algebra.Type;
import models.algebra.Variable;
import models.formulas.DependencyFormula;
import models.terms.Dependency;
import models.terms.DependencyTerm;
import models.terms.EvaluatableTerm;
import models.terms.Resource;
import models.terms.meta.MatchConstraint;
import models.terms.meta.MetaDynamicDependency;
import models.terms.meta.MetaEvaluatableTermVariable;
import models.terms.meta.MetaRDLTerm;
import models.terms.meta.MetaTermGenerator;

public class Main {

	static Type INT = Types.typeInt;

	public static void main(String[] args) {
		//
		sandbox2();
	}
	
	static void sandbox() {
		EvaluatableTerm t = new DependencyTerm(new Resource("a", 1), new Resource("b", 1), new Resource("c", 1));
		System.out.println(t.getSubTerms(EvaluatableTerm.class).values());
	}
	
	static void sandbox2() {
		Resource a = new Resource("a", 1);
		Resource b = new Resource("b", 1);
		Resource c = new Resource("c", 1);
		DependencyFormula d1 = new DependencyFormula(a, b);
		DependencyFormula d2 = new DependencyFormula(b, c);
		DependencyFormula d3 = new DependencyFormula(a, c);
		ProofSystem ps = new ProofSystem(Set.of(d1, d2), d3);
		ps.dependencyInference();
		System.out.println(ps.getState().getHistory().getHistoryString(d3));
	}
	
	static void sandBox8() {
		MetaDynamicDependency md = new MetaDynamicDependency(
				new MetaTermGenerator() {
					@Override
					public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<Object, Object> context) {
						if (curDepth == maxDepth && curIndex == 0) {
							return new MetaEvaluatableTermVariable(new Variable("se"));
						} else if (curIndex == 0) {
							return new MetaDynamicDependency(this);
						}
						curIndex -= 1;
						return new MetaEvaluatableTermVariable(new Variable("te" + curDepth + "_" + curIndex));
					}
				}
		);
		MetaRDLTerm mt = md.generate(1, 2, 3, new HashMap<>());
		System.out.println(mt);
		MetaRDLTerm mt2 = md.allGenerate(2, 3, new HashMap<>());
		System.out.println(mt2);
		Resource a = new Resource("a", 1);
		Resource b = new Resource("b", 1);
		Resource c = new Resource("c", 1);
		Resource d = new Resource("d", 1);
		Resource e = new Resource("e", 1);
		Resource f = new Resource("f", 1);
		Resource g = new Resource("g", 1);
		Dependency d1 = new Dependency(a, b);
		Dependency d2 = new Dependency(d1, c, d);
		System.out.println(md.isMatchedBy(d1));
		System.out.println(md.isMatchedBy(d2));
		Dependency d3 = new Dependency(d2, e, f, g);
		MatchConstraint constraint = md.isMatchedBy(d3).iterator().next();
		System.out.println(md.isMatchedBy(d3));
		constraint.getContext().put("maxDepth", d3.getMaxDepth());
		System.out.println(md.substitute(constraint.getBinding(), constraint.getContext()));
	}
	
}