Newer
Older
RDLProofSystem / src / main / java / models / formulas / meta / MetaEquationFormula.java
@Sakoda2269 Sakoda2269 14 days ago 3 KB requiredAssumptions実装まで
package models.formulas.meta;

import java.util.HashSet;
import java.util.Map;
import java.util.Set;

import exceptions.IllegalTypeException;
import lombok.Getter;
import models.algebra.Variable;
import models.formulas.EquationFormula;
import models.formulas.Formula;
import models.terms.EvaluatableTerm;
import models.terms.RDLTerm;
import models.terms.meta.MatchConstraint;
import models.terms.meta.MetaRDLTerm;
import models.terms.meta.MetaVariable;

@Getter
public class MetaEquationFormula extends MetaFormula {

	private RDLTerm leftSideHand;
	private RDLTerm rightSideHand;
	
	public MetaEquationFormula(RDLTerm left, RDLTerm right) {
		if (! left.isEvaluatableTerm()) {
			throw new IllegalTypeException();
		}
		if (! right.isEvaluatableTerm()) {
			throw new IllegalTypeException();
		}
		this.leftSideHand = left;
		this.rightSideHand = right;
	}
	
	@Override
	public Set<MatchConstraint> isMatchedBy(Formula formula, MatchConstraint constraint) {
		Set<MatchConstraint> result = new HashSet<>();
		if (! (formula instanceof EquationFormula)) {
			return result;
		}
		result.add(constraint);
		EquationFormula eq = (EquationFormula) formula;
		if (leftSideHand instanceof MetaRDLTerm metaLeft) {
			result = metaLeft.isMatchedBy(eq.getLeftSideHand(), result);
		} else {
			if (! leftSideHand.equals(eq.getLeftSideHand())) {
				return new HashSet<>();
			}
		}
		if (rightSideHand instanceof MetaRDLTerm metaRight) {
			result = metaRight.isMatchedBy(eq.getRightSideHand(), result);
		} else {
			if (! rightSideHand.equals(eq.getRightSideHand())) {
				return new HashSet<>();
			}
		}
		return result;
	}
	
	@Override
	public EquationFormula substitution(Map<Variable, RDLTerm> binding, Map<String, Object> context) {
		RDLTerm left = leftSideHand;
		RDLTerm right = rightSideHand;
		if (leftSideHand instanceof MetaRDLTerm metaLeft) {
			left = metaLeft.substitute(binding, context);
		}
		if (rightSideHand instanceof MetaRDLTerm metaRight) {
			right = metaRight.substitute(binding, context);
		}
		return new EquationFormula((EvaluatableTerm) left, (EvaluatableTerm) right);
	}
	
	@Override
	public MetaEquationFormula replace(Map<? extends MetaRDLTerm, ? extends RDLTerm> mapping) {
		RDLTerm left = leftSideHand;
		RDLTerm right = rightSideHand;
		if (leftSideHand instanceof MetaRDLTerm metaLeft) {
			left = metaLeft.replace(mapping);
		}
		if (rightSideHand instanceof MetaRDLTerm metaRight) {
			right = metaRight.replace(mapping);
		}
		return new MetaEquationFormula(left, right);
	}
	
	@Override
	public Set<MetaVariable> getAllVariables() {
		Set<MetaVariable> result = new HashSet<>();
		if (leftSideHand instanceof MetaRDLTerm metaLeft) {
			result.addAll(metaLeft.getAllVariables());
		}
		if (rightSideHand instanceof MetaRDLTerm metaRight) {
			result.addAll(metaRight.getAllVariables());
		}
		return result;
	}
	
	public String toString() {
		return leftSideHand.toString() + " = " + rightSideHand.toString();
	}
	
	public boolean equals(Object another) {
		if (! (another instanceof MetaEquationFormula)) {
			return false;
		}
		MetaEquationFormula anohterFormula = (MetaEquationFormula) another;
		return leftSideHand.equals(anohterFormula.getLeftSideHand()) && rightSideHand.equals(anohterFormula.getRightSideHand());
	}
	
	public int hashCode() {
		return ("MEF" + toString()).hashCode();
	}

	@Override
	public <T extends RDLTerm> Set<T> getSubTerms(Class<T> clazz) {
		Set<T> result = new HashSet<>();
		result.addAll(leftSideHand.getSubTerms(clazz).values());
		result.addAll(rightSideHand.getSubTerms(clazz).values());
		return result;
	}
	
}