package inference;

import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;

import models.algebra.Variable;
import models.formulas.DependencyFormula;
import models.formulas.EquationFormula;
import models.formulas.Formula;
import models.formulas.meta.MetaDependencyFormula;
import models.formulas.meta.MetaEquationFormula;
import models.terms.RDLTerm;
import models.terms.meta.MetaDynamicDependency;
import models.terms.meta.MetaDynamicDependencyTerm;
import models.terms.meta.MetaEvaluatableTermVariable;
import models.terms.meta.MetaRDLTerm;
import models.terms.meta.MetaTermGenerator;

public class ProofSystem {

	//======================Equality Axioms=============================
	
	public static final EquationAxiom reflexivity = new EquationAxiom(
			"Reflexivity",
			List.of(),
			new MetaEquationFormula(
					new MetaEvaluatableTermVariable(new Variable("te")), 
					new MetaEvaluatableTermVariable(new Variable("te"))
			)
	);
	
	public static final EquationAxiom symmetry = new EquationAxiom(
			"Symmetry",
			List.of(
					new MetaEquationFormula(
							new MetaEvaluatableTermVariable(new Variable("te")), 
							new MetaEvaluatableTermVariable(new Variable("se"))
					)
			),
			new MetaEquationFormula(
					new MetaEvaluatableTermVariable(new Variable("se")), 
					new MetaEvaluatableTermVariable(new Variable("te"))
			)
	);
	
	public static final EquationAxiom transitivity = new EquationAxiom(
			"Transitivity",
			List.of(
					new MetaEquationFormula(
							new MetaEvaluatableTermVariable(new Variable("se")), 
							new MetaEvaluatableTermVariable(new Variable("te"))
					),
					new MetaEquationFormula(
							new MetaEvaluatableTermVariable(new Variable("te")), 
							new MetaEvaluatableTermVariable(new Variable("ue"))
					)
			),
			new MetaEquationFormula(
					new MetaEvaluatableTermVariable(new Variable("se")), 
					new MetaEvaluatableTermVariable(new Variable("ue"))
			)
			
	);
	
	public static final EquationAxiom rightSubstitution = new EquationAxiom(
			"Right Substitution",
			List.of(
					new MetaEquationFormula(
							new MetaEvaluatableTermVariable(new Variable("ue")),
							new MetaEvaluatableTermVariable(new Variable("ve"))
					),
					new MetaDependencyFormula(
							new MetaDynamicDependency(
									new MetaTermGenerator() {
										@Override
										public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
											curIndex -= 2;
											return new MetaEvaluatableTermVariable(new Variable("te" + curIndex));
										}
									},
									new MetaEvaluatableTermVariable(new Variable("se")),
									new MetaEvaluatableTermVariable(new Variable("te"))
							)
					)
			),
			new MetaEquationFormula(
					new MetaDynamicDependencyTerm(
							new MetaTermGenerator() {
								@Override
								public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
									curIndex -= 3;
									if (curIndex % 2 == 0) {
										return new MetaEvaluatableTermVariable(new Variable("te" + curIndex / 2));
									}
									return new MetaEvaluatableTermVariable(new Variable("x" + curIndex / 2));
								}
							},
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaEvaluatableTermVariable(new Variable("te")),
							new MetaEvaluatableTermVariable(new Variable("ue"))
					),
					new MetaDynamicDependencyTerm(
							new MetaTermGenerator() {
								@Override
								public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
									curIndex -= 3;
									if (curIndex % 2 == 0) {
										return new MetaEvaluatableTermVariable(new Variable("te" + curIndex / 2));
									}
									return new MetaEvaluatableTermVariable(new Variable("x" + curIndex / 2));
								}
							},
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaEvaluatableTermVariable(new Variable("te")),
							new MetaEvaluatableTermVariable(new Variable("ve"))
					)
			)
	);
	
	
	
	public static final InferenceRule leftSubstitution = new EquationAxiom(
			"Left Substitution",
			List.of(
					new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("se")), new MetaEvaluatableTermVariable(new Variable("te")))
			),
			new MetaEquationFormula(
					new MetaDynamicDependencyTerm(
							new MetaTermGenerator() {
								@Override
								public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
									curIndex -= 1;
									if (curIndex % 2 == 0) {
										return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2));
									}
									return new MetaEvaluatableTermVariable(new Variable("ve" + curIndex / 2));
								}
							},
							new MetaEvaluatableTermVariable(new Variable("se"))
					),
					new MetaDynamicDependencyTerm(
							new MetaTermGenerator() {
								@Override
								public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
									curIndex -= 1;
									if (curIndex % 2 == 0) {
										return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2));
									}
									return new MetaEvaluatableTermVariable(new Variable("ve" + curIndex / 2));
								}
							},
							new MetaEvaluatableTermVariable(new Variable("te"))
					)
			)
	);

	
	public static final EquationAxiom identity = new EquationAxiom(
			"Identity",
			List.of(),
			new MetaEquationFormula(
					new MetaDynamicDependencyTerm(
							new MetaTermGenerator() {
								@Override
								public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
									curIndex -= 1;
									if (curIndex % 2 == 0) {
										return new MetaEvaluatableTermVariable(new Variable("ue"));
									}
									return new MetaEvaluatableTermVariable(new Variable("ve"));
								}
							},
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaEvaluatableTermVariable(new Variable("te"))
					),
					new MetaEvaluatableTermVariable(new Variable("te"))
			)
	);
	
	public static final EquationAxiom mapComposition = new EquationAxiom(
			"Map Composition",
			List.of(
					new MetaDependencyFormula(
							new MetaDynamicDependency(
									new MetaTermGenerator() {
										@Override
										public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
											curIndex -= 2;
											return new MetaEvaluatableTermVariable(new Variable("te" + curIndex));
										}
									},
									new MetaEvaluatableTermVariable(new Variable("se")),
									new MetaEvaluatableTermVariable(new Variable("te"))
							)
					),
					new MetaDependencyFormula(
							new MetaDynamicDependency(
									new MetaTermGenerator() {
										@Override
										public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
											curIndex -= 1;
											context.put("uIndex", curIndex);
											return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex));
										}
									},
									new MetaEvaluatableTermVariable(new Variable("te"))
							)
					)
			),
			new MetaEquationFormula(
					new MetaDynamicDependencyTerm(
							new MetaTermGenerator() {
								@Override
								public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
									curIndex -= 3;
									if (curIndex % 2 == 0) {
										return new MetaEvaluatableTermVariable(new Variable("te" + curIndex / 2));
									} else {
										return new MetaEvaluatableTermVariable(new Variable("tex" + curIndex / 2));
									}
								}
							},
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaEvaluatableTermVariable(new Variable("te")),
							new MetaDynamicDependencyTerm(
									new MetaTermGenerator() {
										@Override
										public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
											curIndex -= 1;
											if (curIndex % 2 == 0) {
												return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2));
											} else {
												return new MetaEvaluatableTermVariable(new Variable("ve" + curIndex / 2));
											}
										}
									},
									new MetaEvaluatableTermVariable(new Variable("te"))
							)
					),
					new MetaDynamicDependencyTerm(
							new MetaTermGenerator() {
								@Override
								public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
									curIndex -= 1;
									int uIndex = (Integer) context.get("uIndex");
									if (curIndex % 2 == 0 && curIndex < uIndex) {
										return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2));
									} else if (curIndex < uIndex ){
										return new MetaEvaluatableTermVariable(new Variable("ve" + curIndex / 2));
									} else if (curIndex % 2 == 0) {
										return new MetaEvaluatableTermVariable(new Variable("te" + curIndex / 2));
									} else {
										return new MetaEvaluatableTermVariable(new Variable("tex" + curIndex / 2));
									}
								}
							},
							new MetaEvaluatableTermVariable(new Variable("se"))
					)
			)
	);
//	
//	public static final InferenceRule constantness = new Constantness();
//	
//	public static final InferenceRule rightNormalization = new RightNormalization();
//	
//	public static final InferenceRule pseudoConstantness = new InferenceRule(
//			"Pseudo-Constantness",
//			List.of(
//					new MetaDependencyFormula(
//							new MetaDynamicDependency(
//									(ci, cd, mi, md, context) -> new MetaEvaluatableTermVariable(new Variable("re" + (ci - 1)), new Variable("n")),
//									new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n"))
//							)
//					)
//			),
//			List.of(),
//			new MetaEquationFormula(
//					new MetaDynamicDependencyTerm(
//							(ci, cd, mi, md, context) -> new MetaEvaluatableTermVariable(new Variable("re" + (ci - 1) / 2), new Variable("n")),
//							new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n"))
//					),
//					new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n"))
//			),
//			new InferenceOrderConstraint(new Constant("0"), OrderConstraint.GT, new Variable("n")),
//			(assumptions) -> (((DependencyFormula)assumptions.get(0)).getDependency().getMaxIndex() - 1) * 2 + 1,
//			(assumptions) -> 1,
//			(term) -> (term.getMaxIndex() - 1) / 2 + 1
//	);
	
//	public static final InferenceRule uncurrying = new Uncurrying();
//	
//	public static final InferenceRule argumentDependencyExtraction = new ArgumentDependencyExtraction();
	
	
//	
//	//======================Dependency Axioms=============================
//	

//	public static final InferenceRule identityMapping = new InferenceRule(
//			"Identity Mapping",
//			List.of(
//					new MetaEquationFormula(
//							new MetaEvaluatableTermVariable(new Variable("te")),
//							new MetaEvaluatableTermVariable(new Variable("se"))
//					)
//			),
//			List.of(),
//			new MetaDependencyFormula(
//					new MetaEvaluatableTermVariable(new Variable("te")),
//					new MetaEvaluatableTermVariable(new Variable("se"))
//			),
//			null,
//			null,
//			null,
//			null
//	);
	
//	public static final InferenceRule compositeMapping = new CompositeMapping();
	
//	public static final InferenceRule constantMapping = new InferenceRule(
//			"Constant Mapping",
//			List.of(),
//			List.of(),
//			new MetaDependencyFormula(
//					new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")),
//					new MetaEvaluatableTermVariable(new Variable("re"), new Variable("m"))
//			),
//			new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m")),
//			null,
//			null,
//			null
//	);
	
//	public static final InferenceRule uncurriedMapping = new UncurriedMapping();
	
//	public static final InferenceRule redundantDependency  = new InferenceRule(
//			"Redundant Dependency",
//			List.of(
//					new MetaDependencyFormula(new MetaDependencyVariable(new Variable("d"), new Variable("n")))
//			),
//			List.of(),
//			new MetaDependencyFormula(new MetaDependencyVariable(new Variable("d"), new Variable("n")), new MetaEvaluatableTermVariable(new Variable("p"), ExpressionUtils.parse("n - 1"))),
//			null,
//			null,
//			null,
//			null
//	);
	
//	public static final InferenceRule redundancyElimination = new RedundancyElimination();
	
	/*
	 * new InferenceRule(
			"",
			List.of(),
			List.of(),
			null,
			null,
			null,
			null,
			null
	);
	 */
	
	
	private static final List<InferenceRule> axioms = List.of(
//			reflexivity, 
//			symmetry, 
//			transitivity,
//			rightSubstitution, 
//			leftSubstitution, 
//			identity, 
//			mapComposition, 
//			constantness,
//			rightNormalization,
//			pseudoConstantness,
//			identityMapping,
//			compositeMapping,
//			constantMapping,
//			slicedMapping,
//			memberSubstitution, 
//			membershipChain, 
//			collectionSubstitution,
//			setEquivelence,
//			setHomomorphism,
//			leftProjection,
//			rightProjection,
//			domainMembership,
//			codomainMembership,
//			codomainMembership2
	);
	

	private Set<DependencyFormula> dependencyFormulas = new HashSet<>();
	private Set<EquationFormula> equationFormulas = new HashSet<>();
	private Set<RDLTerm> terms = new HashSet<>();
	
	public void addDependencyFormula(DependencyFormula dep) {
		dependencyFormulas.add(dep);
		addExistTerms(dep);
	}
	
	public void addEquationFormula(EquationFormula eq) {
		equationFormulas.add(eq);
		addExistTerms(eq);
	}
	
	private void addExistTerms(Formula formula) {
		if (formula instanceof EquationFormula) {
			RDLTerm leftSideHand = ((EquationFormula) formula).getLeftSideHand();
			RDLTerm rightSideHand = ((EquationFormula) formula).getRightSideHand();
			terms.addAll(leftSideHand.getSubTerms(RDLTerm.class).values());
			terms.addAll(rightSideHand.getSubTerms(RDLTerm.class).values());
		} else if (formula instanceof DependencyFormula) {
			RDLTerm dependency = ((DependencyFormula) formula).getDependency();
			terms.addAll(dependency.getSubTerms(RDLTerm.class).values());
		} 
	}
	
}