package inference;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
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.DependencyTerm;
import models.terms.EvaluatableTerm;
import models.terms.RDLTerm;
import models.terms.Resource;
import models.terms.ResourceConstant;
import models.terms.meta.MetaEvaluatableTermVariable;
import models.terms.meta.OrderConstraint;
import utils.Permutation;
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<? extends Formula> assumptions;
	private Formula conclusion;
	@Getter
	private ProofState state;
	
	
	public ProofSystem(Set<? extends Formula> assumptions, Formula conclusion) {
		this(assumptions, conclusion, Set.of());
	}
	
	public ProofSystem(Set<? extends Formula> assumptions, Formula conclusion, Set<Resource> existResources) {
		state = new ProofState(assumptions);
		this.assumptions = assumptions;
		this.conclusion = conclusion;
		state.getEvaluatableTerms().addAll(existResources);
		checkDefinitionFormulaFormat();
	}
	
	private void checkDefinitionFormulaFormat() {
		Set<EvaluatableTerm> leftSideHands = new HashSet<>(assumptions.stream()
					.filter(f -> f instanceof EquationFormula)
					.map(v -> ((EquationFormula) v).getLeftHandSide())
					.toList());
		for (EvaluatableTerm te: leftSideHands) {
			if (te instanceof Resource | te instanceof ResourceConstant) {
				throw new IllegalArgumentException("Resource or ResourceConstant can't be placed left-hand side.");
			}
			Set<Dependency> dependencies = state.getDependencies();
			DependencyTerm dt = (DependencyTerm) te;
			Set<Dependency> requiredDependencies = dt.requiredDependenciesForAdmissible();
			requiredDependencies.retainAll(dependencies);
			if (requiredDependencies.isEmpty()) {
				for (Dependency d: dt.requiredDependenciesForAdmissible()) {
					if (! dependencyInference(new DependencyFormula(d))) {
						throw new IllegalArgumentException(dt.toString() + "is not definition formula format.");
					}
				}
			}
		}
	}
	
	public void inference() {
		if (conclusion instanceof DependencyFormula) {
			dependencyInference();
			return;
		}
		EquationFormula conclusion = (EquationFormula) this.conclusion;
		DependencyTerm dt = (DependencyTerm) conclusion.getLeftHandSide();
		DependencyFormula df = new DependencyFormula(dt.getNoArgumentDependency());
		dependencyInference(df);
		List<InferenceHistoryNode> inferenceHisotries = this.state.getHistory().getHistoryByBFS(df);
//		Collections.reverse(inferenceHisotry);
		Set<EvaluatableTerm> curTerms = new HashSet<>();
		curTerms.add(conclusion.getLeftHandSide());
		for (InferenceHistoryNode history: inferenceHisotries) {
			Set<EvaluatableTerm> nextTerms = new HashSet<>();
			for (EvaluatableTerm curTerm: curTerms) {
				Set<EvaluatableTerm> inferenceRes = new HashSet<>();
				if (history.getUsedRule() == compositeMapping) {
					inferenceRes = applyAxiom(new HashSet<>(history.getAssumptions()), curTerm, mapComposition);
				}
				for (EvaluatableTerm te: inferenceRes) {
					for (EquationFormula eq: state.getDefinitionFormulas()) {
						nextTerms.addAll(applyAxiom(Set.of(eq, new DependencyFormula(te.getDependency())), te, rightSubstitution));
						nextTerms.addAll(applyAxiom(Set.of(eq), te, leftSubstitution));
					}
				}
			}
			curTerms = nextTerms;
		}
		applyTransitivity();
	}
	
	private Set<EvaluatableTerm> applyAxiom (Set<Formula> assumptions, EvaluatableTerm term, EquationAxiom axiom) {
		Set<EvaluatableTerm> res = new HashSet<>();
		for (List<Formula> perm: Permutation.permutation(assumptions, assumptions.size())) {
			for (EvaluatableTerm rsh: axiom.apply(perm, term)) {
				res.add(rsh);
				state.addHistory(perm, axiom, new EquationFormula(term, rsh));
				state.addFormuals(Set.of(new EquationFormula(term, rsh)));
			}
		}
		return res;
	}
	
	private void applyTransitivity() {
		Set<EquationFormula> eq = new HashSet<>(state.getEquationFormulas());
		Map<EquationFormula, Set<EquationFormula>> used = new HashMap<>();
		while (true) {
			Set<EquationFormula> derived = new HashSet<>();
			for (EquationFormula eq1: eq) {
				for (EquationFormula eq2: eq) {
					if (used.computeIfAbsent(eq1, k -> new HashSet<>()).contains(eq2)) {
						continue;
					}
					used.computeIfAbsent(eq1, k -> new HashSet<>()).add(eq2);
					Set<Formula> formulas = transitivity.derive(List.of(eq1, eq2));
					for (Formula f: formulas) {
						derived.add((EquationFormula) f);
						state.addHistory(List.of(eq1, eq2), transitivity, f);
					}
				}
			}
			if (derived.isEmpty()) {
				break;
			}
			eq.addAll(derived);
		}
		
	}
	
	public String getInferenceHistoryString() {
		return state.getHistory().getHistoryString(conclusion);
	}
	
	public boolean dependencyInference() {
		return dependencyInference(this.conclusion);
	}
	
	public boolean dependencyInference(Formula conclusion) {
		if (conclusion instanceof EquationFormula eq) {
			RDLTerm lhs = eq.getLeftHandSide();
			RDLTerm rhs = eq.getRightHandSide();
			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;
	}
	
	private void checkAdmissibility(DependencyTerm dt) {
		checkRequiredDependency(dt);
		checkMembership(dt);
	}
	
	private void checkRequiredDependency(DependencyTerm dt) {
	}
	
	private void checkMembership(DependencyTerm dt) {
	}
	
}