package inference;

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

import models.algebra.Variable;
import models.formulas.meta.MetaDependencyFormula;
import models.formulas.meta.MetaEquationFormula;
import models.terms.RDLTerm;
import models.terms.meta.MetaEvaluatableTermVariable;
import models.terms.meta.MetaRDLTerm;
import models.terms.meta.MetaResourceVariable;

public class ProofSystem {

	private final static InferenceRule REFLEXIVE_LAW = new InferenceRule("relfexive law", List.of(), 
			new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("te")), new MetaEvaluatableTermVariable(new Variable("te"))));
	
	private 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"))));
	
	private 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")))
	);
	
	private 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")))
	);
	
	private 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")))
	);
	
	private final static InferenceRule LEFT_PROJECTION = null;
	private final static InferenceRule RIGHT_PROJECTION = null;
	private final static InferenceRule CONSTANT_MAPPING = null; // 定値写像??
	private final static InferenceRule ORDER_DESCENTING = null; // 階数降下??
	
	private 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"))
					)
			)
	);
	
	private final static InferenceRule IDENTITY_LAW = null;
	
	private 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"))
					)
			)
	);
	
	private final static InferenceRule CONSTANT_VALUE_LAW = null;//定値性??
	private final static InferenceRule LINEAR_RIGHT_NORMALIZE = null;
	private final static InferenceRule PSEUDO_IDENTITY_LAW = null;//疑似恒等性??
	private final static InferenceRule SET_EQUIVALENCE = null;//集合同値性??
	private final static InferenceRule HOMOMORPHISM = null;//準同型性??
	
	public static boolean check(Collection<RDLTerm> assumptions, RDLTerm conclusion) {
		return false;
	}
	
}