Newer
Older
RDLProofSystem / src / main / java / models / terms / meta / MetaDependencyTerm.java
@Sakoda2269 Sakoda2269 1 day ago 5 KB dynami 修正 途中まで
package models.terms.meta;

import com.google.common.collect.TreeMultiset;

import java.util.ArrayList;
import java.util.Arrays;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.TreeMap;
import java.util.stream.Collectors;
import java.util.stream.IntStream;

import exceptions.SubstituteFailedException;
import exceptions.SyntaxException;
import models.algebra.Symbol;
import models.algebra.Variable;
import models.terms.DependencyTerm;
import models.terms.EvaluatableTerm;
import models.terms.RDLTerm;
import utils.Permutation;

public class MetaDependencyTerm extends MetaRDLTerm{

	protected RDLTerm dependingTerm;
	protected Map<RDLTerm, TreeMultiset<RDLTerm>> termPairs = new TreeMap<>();
	
	protected MetaDependencyTerm() {
		super(new Symbol(":", -1), TermType.META_DEPENDENCY_TERM, -1);
	}
	
	public MetaDependencyTerm(RDLTerm dependingTerm, List<? extends RDLTerm> terms) {
		super(new Symbol(":", -1), TermType.META_DEPENDENCY_TERM, -1);
		TreeMap<RDLTerm, TreeMultiset<RDLTerm>> sortedMap = new TreeMap<>();
		this.dependingTerm = dependingTerm;
		addChild(dependingTerm);
		int size = dependingTerm.getSize();
		for (int i = 0; i < terms.size() / 2; i++) {
			RDLTerm dependedTerm = terms.get(i * 2);
			RDLTerm argTerm = terms.get(i * 2 + 1);
			sortedMap.computeIfAbsent(dependedTerm, k -> TreeMultiset.create()).add(argTerm);
		}
		for (RDLTerm dependedTerm: sortedMap.keySet()) {
			for (RDLTerm argTerm: sortedMap.get(dependedTerm)) {
				termPairs.computeIfAbsent(dependedTerm, k -> TreeMultiset.create()).add(argTerm);
				addChild(dependedTerm);
				addChild(argTerm);
				size += dependedTerm.getSize();
				size += argTerm.getSize();
			}
		}
		this.size = size;
	}
	
	public MetaDependencyTerm(RDLTerm dependingTerm, RDLTerm ...terms) {
		this(dependingTerm, Arrays.asList(terms));
	}
	
	@Override
	protected Set<MatchConstraint> isMatchedBy(RDLTerm another, MatchConstraint constraint, int depth) {
		Set<MatchConstraint> result = new HashSet<>();
		if (! another.getClass().isAssignableFrom(this.termType.getBaseTermClass())) {
			return result;
		}
		if (isDependencyTerm() && (! islinearRightNormalizedMatchedBy(another))) {
			return result;
		}
		result = dependingTermMatch(another, constraint, depth);
		return termPairsMatch(another, result, depth);
	}
	
	private Set<MatchConstraint> dependingTermMatch(RDLTerm another, MatchConstraint constraint, int depth) {
		RDLTerm dependingChild = (RDLTerm) this.getChild(0);
		RDLTerm anotherDependingChild = (RDLTerm) another.getChild(0);
		if (dependingChild instanceof MetaRDLTerm) {
			MetaRDLTerm metaChild = (MetaRDLTerm) dependingChild;
			return metaChild.isMatchedBy(anotherDependingChild, constraint, depth + 1);
		} else {
			if (!(dependingChild.equals(anotherDependingChild))) {
				return new HashSet<>();
			}
		}
		return new HashSet<>();
	}
	
	private Set<MatchConstraint> termPairsMatch(RDLTerm another, Set<MatchConstraint> constraint, int depth) {
		Set<MatchConstraint> result = new HashSet<>();
		for (List<Integer> perm : Permutation.permutation((another.getChildren().size() - 1) / 2)) {
			Set<MatchConstraint> localResult = new HashSet<>(constraint);
			boolean flg = true;
			for (int metaTermIndex = 0; metaTermIndex < perm.size(); metaTermIndex++) {
				int anotherTermIndex = perm.get(metaTermIndex);
				RDLTerm metaDependedTerm = (RDLTerm) getChild(2 * metaTermIndex + 1);
				RDLTerm anotherDependedTerm = (RDLTerm) another.getChild(2 * anotherTermIndex + 1);
				RDLTerm metaArgTerm = (RDLTerm) getChild(2 * metaTermIndex + 2);
				RDLTerm anotherArgTerm = (RDLTerm) another.getChild(2 * anotherTermIndex + 2);
				if (metaDependedTerm instanceof MetaRDLTerm metaTerm) {
					localResult = metaTerm.isMatchedBy(anotherDependedTerm, localResult, depth + 1);
					if (localResult.isEmpty()) {
						flg = false;
						break;
					}
				} else {
					if (!(metaDependedTerm.equals(anotherDependedTerm))) {
						flg = false;
						break;
					}
				}
				if (metaArgTerm instanceof MetaRDLTerm metaTerm) {
					localResult = metaTerm.isMatchedBy(anotherArgTerm, localResult, depth + 1);
					if (localResult.isEmpty()) {
						flg = false;
						break;
					}
				} else {
					if (!(metaArgTerm.equals(anotherArgTerm))) {
						flg = false;
						break;
					}
				}
			}
			if (flg) {
				result.addAll(localResult);
			}
		}
		return result;
	}

	@Override
	protected RDLTerm substitute(Map<Variable, RDLTerm> binding, int depth) {
		RDLTerm dependingTerm = (RDLTerm) getChild(0);
		if (dependingTerm instanceof MetaRDLTerm) {
			dependingTerm = ((MetaRDLTerm) dependingTerm).substitute(binding, depth + 1);
		}
		List<EvaluatableTerm> termPairs = new ArrayList<>();
		for (int i = 0; i < (getChildren().size() - 1) / 2; i++) {
			RDLTerm dependedTerm = (RDLTerm) getChild(i * 2 + 1);
			RDLTerm argTerm = (RDLTerm) getChild(i * 2 + 2);
			if (dependedTerm instanceof MetaRDLTerm metaTerm) {
				dependedTerm = metaTerm.substitute(binding, depth + 1);
			}
			if (argTerm instanceof MetaRDLTerm metaTerm) {
				argTerm = metaTerm.substitute(binding, depth + 1);
			}
			termPairs.add((EvaluatableTerm) dependedTerm);
			termPairs.add((EvaluatableTerm) argTerm);
		}
		try {
			return new DependencyTerm((EvaluatableTerm) dependingTerm, termPairs);
		} catch (SyntaxException e) {
			throw new SubstituteFailedException(e.getMessage());
		}
	}

	
	@Override
	public String toString() {
		return "[" + getChild(0).toString() + " : " + IntStream.range(0, (getChildren().size() - 1) / 2)
		.mapToObj(i -> getChild(i * 2 + 1).toString() + " -> " + getChild(i * 2 + 2)).collect(Collectors.joining(", ")) + "]";
	}
	
}