import java.util.HashMap;
import java.util.List;
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.formulas.EquationFormula;
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) {
		//
		sandbox5();
	}
	
	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);
		Resource d = new Resource("d", 1);
		DependencyFormula d1 = new DependencyFormula(a, b);
		DependencyFormula d2 = new DependencyFormula(b, c);
		DependencyFormula d3 = new DependencyFormula(c, d);
		DependencyFormula d4 = new DependencyFormula(a, d);
		ProofSystem ps = new ProofSystem(Set.of(d1, d2, d3), d4);
		ps.dependencyInference();
		System.out.println(ps.getState().getHistory().getHistoryString(d4));
	}
	
	static void sandbox3() {
		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);
		DependencyFormula d1 = new DependencyFormula(a, b);
		DependencyFormula d2 = new DependencyFormula(b, c);
		DependencyFormula d3 = new DependencyFormula(c, d);
		DependencyFormula d4 = new DependencyFormula(d, e);
		DependencyFormula d5 = new DependencyFormula(a, e);
		ProofSystem ps = new ProofSystem(Set.of(d1, d2, d3, d4), d5);
		ps.dependencyInference();
		System.out.println(ps.getState().getHistory().getHistoryString(d5));
	}
	
	static void sandbox4() {
		Resource a = new Resource("a", 2);
		Resource b = new Resource("b", 2);
		Resource c = new Resource("c", 1);
		Resource d = new Resource("d", 1);
		DependencyFormula d2 = new DependencyFormula(new Dependency(a, b), c);
		EquationFormula eq1 = new EquationFormula(d, d);
		DependencyFormula d3 = new DependencyFormula(new DependencyTerm(a, b, d), c, d);
		ProofSystem ps = new ProofSystem(Set.of(d2, eq1), d3);
		ps.dependencyInference();
		System.out.println(ps.getState().getHistory().getHistoryString(d3));
	}
	
	static void sandbox5() {
		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", 2);
		Resource g = new Resource("g", 2);
		Resource h = new Resource("h", 3);
		Resource i = new Resource("i", 3);
		Dependency d1 = new Dependency(new DependencyTerm(f, g, b), b);
		var tmp = ProofSystem.argumentExtension.getAssumptions().get(0).isMatchedBy(new DependencyFormula(d1));
		var tmp1 = ProofSystem.argumentExtension.derive(List.of(new DependencyFormula(d1)), Set.of(a));
		System.out.println(tmp1);
	}
	
	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()));
	}
	
}