package inference;

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

import inference.axioms.ArgumentConstraint;
import inference.axioms.ArgumentExtension;
import inference.axioms.ArgumentReduction;
import inference.axioms.CompositeMapping;
import inference.axioms.ConstantMapping;
import inference.axioms.Constantness;
import inference.axioms.DependencyExtension;
import inference.axioms.Identity;
import inference.axioms.LeftSubstitution;
import inference.axioms.MapComposition;
import inference.axioms.PseudoConstantness;
import inference.axioms.RightSubstitution;
import inference.axioms.UncurriedMapping;
import inference.axioms.Uncurrying;
import lombok.Getter;
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.Dependency;
import models.terms.EvaluatableTerm;
import models.terms.RDLTerm;
import models.terms.Resource;
import models.terms.meta.MetaEvaluatableTermVariable;
import models.terms.meta.OrderConstraint;
import utils.Product;

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"))
					)
			),
			new MetaDependencyFormula(
					new MetaEvaluatableTermVariable(new Variable("te")),
					new MetaEvaluatableTermVariable(new Variable("se"))
			)
	);
	
	public static final InferenceRule argumentExtension = new ArgumentExtension();
	
	public static final InferenceRule argumentReduction = new ArgumentReduction();
	
	public static final InferenceRule argumentConstraint = new ArgumentConstraint();
	
	public static final InferenceRule compositeMapping = new CompositeMapping();
	
	public static final InferenceRule constantMapping = new ConstantMapping();
	
	public static final InferenceRule constantMapping1 = new InferenceRule(
			"Constant Mapping",
			List.of(),
			new MetaDependencyFormula(
					new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")),
					new MetaEvaluatableTermVariable(new Variable("te"), new Variable("m"))
			),
			new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m"))
	); 
	
	public static final InferenceRule uncurriedMapping = new UncurriedMapping();
	
	public static final InferenceRule dependencyExtension = new DependencyExtension();
	
	public static final List<InferenceRule> axioms = List.of(
			reflexivity,
			symmetry,
			transitivity,
			rightSubstitution,
			leftSubstitution,
			identity,
			mapComposition,
			constantness,
			pseudoConstantness,
			uncurrying,
			identityMapping,
			argumentExtension,
			argumentReduction,
			compositeMapping,
			constantMapping1,
			uncurriedMapping,
			dependencyExtension
	);
	
	public static final List<EquationAxiom> equationAxioms = List.of(
			reflexivity,
			symmetry,
			transitivity,
			rightSubstitution,
			leftSubstitution,
			identity,
			mapComposition,
			constantness,
			pseudoConstantness,
			uncurrying
	);
	
	public static final List<InferenceRule> dependencyAxioms = List.of(
			identityMapping,
			argumentExtension,
			argumentReduction,
			compositeMapping,
			constantMapping1,
			uncurriedMapping,
			dependencyExtension
	);
	
	private Set<Formula> assumptions;
	private Formula conclusion;
	@Getter
	private ProofState state;
	
	
	public ProofSystem(Set<Formula> assumptions, Formula conclusion) {
		this(assumptions, conclusion, Set.of());
	}
	
	public ProofSystem(Set<Formula> assumptions, Formula conclusion, Set<Resource> existResources) {
		state = new ProofState(assumptions);
		this.assumptions = assumptions;
		this.conclusion = conclusion;
		state.getEvaluatableTerms().addAll(existResources);
	}
	
	public void inference() {
	}
	
	public String getInferenceHistoryString() {
		return state.getHistory().getHistoryString(conclusion);
	}
	
	public boolean dependencyInference() {
		if (conclusion instanceof EquationFormula eq) {
			RDLTerm lhs = eq.getLeftSideHand();
			RDLTerm rhs = eq.getRightSideHand();
			Dependency leftDependency = lhs.getDependency();
			Dependency rightDependency = rhs.getDependency();
			while((! state.getDependencies().contains(leftDependency)) && (! state.getDependencies().contains(rightDependency))) {
				state.addFormuals(dependencyInferenceStep());
			}
			return true;
		} else if (conclusion instanceof DependencyFormula dep) {
			while((! state.getDependencyFormulas().contains(dep))) {
				Set<DependencyFormula> result = dependencyInferenceStep();
				Set<DependencyFormula> sizeConstraintOk = new HashSet<>();
				for (DependencyFormula df: result) {
					if (dep.getDependency().getSize() >= df.getDependency().getSize()) {
						if (! state.getFormulas().contains(df)) {
							sizeConstraintOk.add(df);
						}
					}
				}
				if (sizeConstraintOk.size() == 0) {
					return false;
				}
				state.addFormuals(sizeConstraintOk);
			}
			return true;
		}
		return false;
	}
	
	public Set<DependencyFormula> dependencyInferenceStep() {
		Set<DependencyFormula> result = new HashSet<>();
		for (InferenceRule rule: dependencyAxioms) {
			List<List<Formula>> matchedFormulas = new ArrayList<>();
			for (Set<Formula> formulas: state.getMatchedFormulas().get(rule)) {
				matchedFormulas.add(new ArrayList<>(formulas));
			}
			if (rule.getAssumptions().size() == 0) {
				result.addAll(dependencyDerive(List.of(), rule));
			} else {
				for (List<Formula> formulas: Product.product(matchedFormulas)) {
					result.addAll(dependencyDerive(formulas, rule));
				}
			}
		}
		return result;
	}
	
	private Set<DependencyFormula> dependencyDerive(List<Formula> assumptions, InferenceRule rule) {
		Set<DependencyFormula> result = new HashSet<>();
		for (Formula res: rule.derive(assumptions, state.getExistTerms())) {
			if (state.formulaExist(res)) continue;
			state.addHistory(assumptions, rule, res);
			if (res instanceof DependencyFormula df) {
				result.add(df);
			}
		}
		return result;
	}
	
	public Set<Formula> equationInferenceStep() {
		Set<Formula> result = new HashSet<>();
		for (EquationAxiom rule: equationAxioms) {
			List<List<Formula>> matchedFormulas = new ArrayList<>();
			for (Set<Formula> formulas: state.getMatchedFormulas().get(rule)) {
				matchedFormulas.add(new ArrayList<>(formulas));
			}
			for (EvaluatableTerm left: state.getMatchedTerms().get(rule).leftSideHands()) {
				for (List<Formula> formulas: Product.product(matchedFormulas)) {
					for (EvaluatableTerm right: rule.apply(formulas, left)) {
						result.add(new EquationFormula(left, right));
						state.addHistory(formulas, rule, new EquationFormula(left, right));
					}
				}
			}
			for (EvaluatableTerm right: state.getMatchedTerms().get(rule).rightSideHands()) {
				for (List<Formula> formulas: Product.product(matchedFormulas)) {
					for (EvaluatableTerm left: rule.apply(formulas, right)) {
						result.add(new EquationFormula(left, right));
						state.addHistory(formulas, rule, new EquationFormula(left, right));
					}
				}
			}
		}
		return result;
	}
	
}