package inference.equivalence;

import java.util.ArrayList;
import java.util.Collection;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;

import models.algebra.Constant;
import models.algebra.Term;
import models.algebra.Variable;
import models.dataConstraintModel.DataConstraintModel;
import models.terms.LinearRightNormalizedType;
import models.terms.RDLTerm;
import models.terms.meta.MetaEvaluatableTermVariable;
import models.terms.meta.MetaRDLTerm;
import models.terms.meta.MetaResourceVariable;
import models.terms.meta.OrderConstraint;
import models.terms.meta.OrderVariableConstraint;

public class SemanticEquivalenceProofSystem {

	private Map<Integer, List<SemanticEquivalenceRelation>> assumptions;
	private SemanticEquivalenceRelation conclusion;
	int maxOrder = -1;
	
	private static MetaSemanticEquivalenceRelation rule1 = new MetaSemanticEquivalenceRelation(
			new MetaRDLTerm(
					new MetaResourceVariable(new Variable("v"), new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1")))),
					new MetaResourceVariable(new Variable("v"), new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1")))),
					new MetaEvaluatableTermVariable(new Variable("t"), new Variable("n"), LinearRightNormalizedType.LINEAR_RIGHT_NORMALIZED)
			),
			new MetaEvaluatableTermVariable(new Variable("t"), new Variable("n"), LinearRightNormalizedType.LINEAR_RIGHT_NORMALIZED),
			new Variable("n")
	);
	
	private static MetaSemanticEquivalenceRelation rule4_1 = new MetaSemanticEquivalenceRelation(
			new MetaEvaluatableTermVariable(new Variable("t"), new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1"))), LinearRightNormalizedType.LINEAR_RIGHT_NORMALIZED),
			new MetaEvaluatableTermVariable(new Variable("t'"), new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1"))), LinearRightNormalizedType.LINEAR_RIGHT_NORMALIZED),
			new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1")))
	);
	
	private static MetaSemanticEquivalenceRelation rule4_2 = new MetaSemanticEquivalenceRelation(
			new MetaRDLTerm(
					new MetaEvaluatableTermVariable(new Variable("t"), new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1")))),
					new MetaResourceVariable(new Variable("v"), new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1")))),
					new MetaEvaluatableTermVariable(new Variable("s"), OrderConstraint.LT, new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1"))))
			),
			new MetaRDLTerm(
					new MetaEvaluatableTermVariable(new Variable("t'"), new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1")))),
					new MetaResourceVariable(new Variable("v"), new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1")))),
					new MetaEvaluatableTermVariable(new Variable("s"), OrderConstraint.LT, new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1"))))
			),
			new Variable("n")
	);
	
	public SemanticEquivalenceProofSystem(Collection<SemanticEquivalenceRelation> assumptions, SemanticEquivalenceRelation conclusion) {
		for(SemanticEquivalenceRelation assumption : assumptions) {
			maxOrder = Math.max(maxOrder, assumption.getOrder());
			if (! this.assumptions.containsKey(assumption.getOrder())) {
				this.assumptions.put(assumption.getOrder(), new ArrayList<>());
			}
		}
		this.conclusion = conclusion;
	}
	
	public boolean proof() {
		Set<RDLTerm> existTerms = new HashSet<>();
		for(int key : assumptions.keySet()) {
			for(SemanticEquivalenceRelation relation : assumptions.get(key)) {
				existTerms.addAll(relation.getLeftSideHand().getSubTerms(RDLTerm.class).values());
				existTerms.add(relation.getLeftSideHand());
				existTerms.addAll(relation.getRightSideHand().getSubTerms(RDLTerm.class).values());
				existTerms.add(relation.getRightSideHand());
			}
		}
		for (int i = maxOrder; i > 0; i--) {
			for (SemanticEquivalenceRelation relation : assumptions.get(i)) {
				applyRule4(relation, existTerms);
			}
		}
		System.out.println(assumptions);
		return false;
	}
	
	private void applyRule1() {
		
	}
	
	private void applyRule4(SemanticEquivalenceRelation relation, Set<RDLTerm> existTerms) {
		Map<Variable, RDLTerm> binding = new HashMap<>();
		Map<Variable, OrderVariableConstraint> orderConstraint = new HashMap<>();
		if (rule4_1.isMatchedBy(relation, binding, orderConstraint)) {
			Set<SemanticEquivalenceRelation> results = rule4_2.substitute(binding, orderConstraint, existTerms);
			for (SemanticEquivalenceRelation result : results) {
				if (! assumptions.containsKey(result.getOrder())) {
					assumptions.put(result.getOrder(), new ArrayList<>());
				}
				assumptions.get(result.getOrder()).add(result);
				existTerms.addAll(result.getLeftSideHand().getSubTerms(RDLTerm.class).values());
				existTerms.add(result.getLeftSideHand());
				existTerms.addAll(result.getRightSideHand().getSubTerms(RDLTerm.class).values());
				existTerms.add(result.getRightSideHand());
			}
		}
		
	}
	
}