package inference;

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

import inference.axioms.Constantness;
import inference.axioms.Identity;
import inference.axioms.LeftSubstitution;
import inference.axioms.MapComposition;
import inference.axioms.PseudoConstantness;
import inference.axioms.RightSubstitution;
import inference.axioms.Uncurrying;
import models.algebra.Variable;
import models.formulas.DependencyFormula;
import models.formulas.EquationFormula;
import models.formulas.Formula;
import models.formulas.meta.MetaEquationFormula;
import models.terms.RDLTerm;
import models.terms.meta.MetaEvaluatableTermVariable;

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 RightSubstitution();
	
	
	
	public static final EquationAxiom leftSubstitution = new LeftSubstitution();

	
	public static final EquationAxiom identity = new Identity();
	
	public static final EquationAxiom mapComposition = new MapComposition();
//	
	public static final EquationAxiom constantness = new Constantness();
//	
//	public static final InferenceRule rightNormalization = new RightNormalization();
//	

	public static final EquationAxiom pseudoConstantness = new PseudoConstantness();
	
	public static final EquationAxiom uncurrying = new Uncurrying();
	
	
//	
//	//======================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());
		} 
	}
	
}