package inference;

import java.util.Collection;
import java.util.List;

import models.algebra.Constant;
import models.algebra.Variable;
import models.formulas.Formula;
import models.formulas.meta.MetaDependencyFormula;
import models.formulas.meta.MetaEquationFormula;
import models.formulas.meta.MetaInFormula;
import models.terms.meta.MetaDependencyVariable;
import models.terms.meta.MetaEvaluatableTermVariable;
import models.terms.meta.MetaRDLTerm;
import models.terms.meta.MetaResourceVariable;
import models.terms.meta.OrderConstraint;

public class ProofSystem {

	public final static InferenceRule REFLEXIVE_LAW = new InferenceRule("relfexive law", List.of(), 
			new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("te")), new MetaEvaluatableTermVariable(new Variable("te"))));
	
	public final static InferenceRule SYMMETRIC_LAW = new InferenceRule("symmetric law", 
		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 final static InferenceRule TRANSITIVE_LAW = new InferenceRule("transitive law", 
			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 final static InferenceRule IDENTITY_MAPPING = new InferenceRule("identity mapping", 
			List.of(new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("te")), new MetaResourceVariable(new Variable("v")))),
			new MetaDependencyFormula(new MetaEvaluatableTermVariable(new Variable("te")), new MetaResourceVariable(new Variable("v")))
	);
	
	public final static InferenceRule COMPOSITE_MAPPING = new InferenceRule("composite mapping", 
			List.of(
					new MetaDependencyFormula(new MetaEvaluatableTermVariable(new Variable("te")), new MetaResourceVariable(new Variable("v"))),
					new MetaDependencyFormula(new MetaResourceVariable(new Variable("v")), new MetaResourceVariable(new Variable("w")))
			),
			new MetaDependencyFormula(new MetaEvaluatableTermVariable(new Variable("te")), new MetaResourceVariable(new Variable("w")))
	);
	
	public final static InferenceRule LEFT_PROJECTION = new InferenceRule("left projection", 
			List.of(new MetaDependencyFormula(
								new MetaRDLTerm(
										new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")),
										new MetaResourceVariable(new Variable("v"), new Variable("m"))
								),
								new MetaResourceVariable(new Variable("w"), new Variable("l"))
			)),
			new MetaDependencyFormula(
					new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n"))),
					new MetaResourceVariable(new Variable("w"), new Variable("l"))
			)
	);
	
	public final static InferenceRule RIGHT_PROJECTION = new InferenceRule("left projection", 
			List.of(new MetaDependencyFormula(
								new MetaRDLTerm(
										new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")),
										new MetaResourceVariable(new Variable("v"), new Variable("m"))
								),
								new MetaResourceVariable(new Variable("w"), new Variable("l"))
			)),
			new MetaDependencyFormula(
					new MetaRDLTerm(new MetaResourceVariable(new Variable("v"), new Variable("m"))),
					new MetaResourceVariable(new Variable("w"), new Variable("l"))
			)
	);
	
	public final static InferenceRule CONSTANT_MAPPING = new InferenceRule("constant mapping", 
			List.of(),
			new MetaDependencyFormula(
					new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")),
					new MetaResourceVariable(new Variable("v"), new Variable("m"))
			),
			new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m"))
	); // 定値写像??
	
	public final static InferenceRule ORDER_DESCENTING = new InferenceRule("order descenting", 
			List.of(new MetaDependencyFormula(new MetaDependencyVariable(new Variable("d"), new Variable("n")))),
			new MetaDependencyFormula(new MetaRDLTerm(new MetaDependencyVariable(new Variable("d"), new Variable("n")))),
			new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0"))
	); // 階数降下??
		
	public final static InferenceRule RIGHT_REPLACEMENT = new InferenceRule("right replacement",
			List.of(new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("te")), new MetaEvaluatableTermVariable(new Variable("ue")))),
			new MetaEquationFormula(
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaResourceVariable(new Variable("v")),
							new MetaEvaluatableTermVariable(new Variable("te"))
					),
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaResourceVariable(new Variable("v")),
							new MetaEvaluatableTermVariable(new Variable("ue"))
					)
			)
	);
	
	public final static InferenceRule LEFT_REPLACEMENT = new InferenceRule("left replacement",
			List.of(new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("se")), new MetaEvaluatableTermVariable(new Variable("ue")))),
			new MetaEquationFormula(
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaResourceVariable(new Variable("v")),
							new MetaEvaluatableTermVariable(new Variable("te"))
					),
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("ue")),
							new MetaResourceVariable(new Variable("v")),
							new MetaEvaluatableTermVariable(new Variable("te"))
					)
			)
	);
	
	public final static InferenceRule CENTER_REPLACEMENT = new InferenceRule("center replacement",
			List.of(new MetaEquationFormula(new MetaResourceVariable(new Variable("v")), new MetaResourceVariable(new Variable("w")))),
			new MetaEquationFormula(
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaResourceVariable(new Variable("v")),
							new MetaEvaluatableTermVariable(new Variable("te"))
					),
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaResourceVariable(new Variable("w")),
							new MetaEvaluatableTermVariable(new Variable("te"))
					)
			)
	);
	
	
	public final static InferenceRule IDENTITY_LAW = new InferenceRule("identity law", 
			List.of(new MetaInFormula(
					new MetaEvaluatableTermVariable(new Variable("te")), 
					new MetaRDLTerm(new MetaResourceVariable(new Variable("v"))))
			),
			new MetaEquationFormula(
					new MetaRDLTerm(
							new MetaResourceVariable(new Variable("v")),
							new MetaResourceVariable(new Variable("v")),
							new MetaEvaluatableTermVariable(new Variable("te"))
					),
					new MetaEvaluatableTermVariable(new Variable("te"))
			)
	);
	
	public final static InferenceRule JOIN = new InferenceRule("join",
			List.of(new MetaEquationFormula(new MetaResourceVariable(new Variable("v")), new MetaResourceVariable(new Variable("w")))),
			new MetaEquationFormula(
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaResourceVariable(new Variable("v")),
							new MetaRDLTerm(
									new MetaResourceVariable(new Variable("w")),
									new MetaResourceVariable(new Variable("x")),
									new MetaEvaluatableTermVariable(new Variable("te"))
							)
					),
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaResourceVariable(new Variable("x")),
							new MetaEvaluatableTermVariable(new Variable("te"))
					)
			)
	);
	
	public final static InferenceRule CONSTANT_VALUE_LAW = new InferenceRule("constant value law", 
			List.of(new MetaInFormula(
					new MetaEvaluatableTermVariable(new Variable("t")), 
					new MetaRDLTerm(new MetaResourceVariable(new Variable("v"), new Variable("m"))))
			),
			new MetaEquationFormula(
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")),
							new MetaResourceVariable(new Variable("v"), new Variable("m")),
							new MetaEvaluatableTermVariable(new Variable("t"))
					),
					new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n"))
			),
			new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m"))
	);//定値性??
	
	public final static InferenceRule RIGHT_NORMALIZE = new InferenceRule("right normalize", 
			List.of(
					new MetaDependencyFormula(
							new MetaEvaluatableTermVariable(new Variable("te")),
							new MetaResourceVariable(new Variable("v"), new Variable("n"))
					),
					new MetaDependencyFormula(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaResourceVariable(new Variable("w"), new Variable("n"))
					)
			),
			new MetaEquationFormula(
					new MetaRDLTerm(
							new MetaRDLTerm(
									new MetaEvaluatableTermVariable(new Variable("te")),
									new MetaResourceVariable(new Variable("v"), new Variable("n")),
									new MetaEvaluatableTermVariable(new Variable("se"))
							),
							new MetaResourceVariable(new Variable("w"), new Variable("n")),
							new MetaEvaluatableTermVariable(new Variable("ue"))
					),
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("te")),
							new MetaResourceVariable(new Variable("v"), new Variable("n")),
							new MetaRDLTerm(
									new MetaEvaluatableTermVariable(new Variable("se")),
									new MetaResourceVariable(new Variable("w"), new Variable("n")),
									new MetaEvaluatableTermVariable(new Variable("ue"))
							)
					)
			),
			new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0"))
	);
	
	public final static InferenceRule PSEUDO_IDENTITY_LAW = new InferenceRule("pseudo identity law",
			List.of(
					new MetaDependencyFormula(
							new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")),
							new MetaResourceVariable(new Variable("v"), new Variable("n"))
					)
			),
			new MetaEquationFormula(
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")),
							new MetaResourceVariable(new Variable("v"), new Variable("n")),
							new MetaResourceVariable(new Variable("v"), new Variable("n"))
					),
					new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n"))
			),
			new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0"))
	);//疑似恒等性??
	
	public final static InferenceRule SET_EQUIVALENCE = new InferenceRule("set equivalence",
			List.of(new MetaEquationFormula(
					new MetaEvaluatableTermVariable(new  Variable("se"), new Variable("n")),
					new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n"))
			)),
			new MetaEquationFormula(
					new MetaRDLTerm(new MetaEvaluatableTermVariable(new  Variable("se"), new Variable("n"))),
					new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")))
			),
			new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0"))
	);//集合同値性??
	
	public final static InferenceRule HOMOMORPHISM = new InferenceRule("homomorphism",
			List.of(new MetaDependencyFormula(
					new MetaEvaluatableTermVariable(new Variable("se")),
					new MetaResourceVariable(new Variable("v"))
			)),
			new MetaEquationFormula(
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaResourceVariable(new Variable("v")),
							new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("te")))
					),
					new MetaRDLTerm(
							new MetaRDLTerm(
									new MetaEvaluatableTermVariable(new Variable("se")),
									new MetaResourceVariable(new Variable("v")),
									new MetaEvaluatableTermVariable(new Variable("te"))
							)
					)
			)
	);//準同型性??
	
	public static boolean check(Collection<Formula> assumptions, Formula conclusion) {
		if (assumptionsContainConclusionCheck(assumptions, conclusion)) {
			return true;
		}
		return false;
	}
	
	private static boolean assumptionsContainConclusionCheck(Collection<Formula> assumptions, Formula conclusion) {
		for(var assumption : assumptions) {
			if (assumption.equals(conclusion)) {
				return true;
			}
		}
		return false;
	}
	
}