Newer
Older
RDLProofSystem / src / main / java / models / terms / meta / MetaDynamicTerm.java
@Sakoda2269 Sakoda2269 12 days ago 12 KB left subとright subをdynamicに
package models.terms.meta;

import java.util.ArrayList;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.TreeSet;

import models.algebra.Symbol;
import models.algebra.Variable;
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.MetaTermPairGenerator.TermPair;
import utils.Permutation;

public class MetaDynamicTerm extends MetaRDLTerm {
	
	private MetaTermGenerator dependingTermGenerator;
	private MetaTermGenerator dependedTermGenerator;
	private MetaTermPairGenerator termPairGenerator;
	private boolean isStaticSize = false;
	
	public MetaDynamicTerm(MetaTermGenerator dependingTermGenerator, MetaTermGenerator dependedTermGenerator) {
		super(new Symbol("", -1), TermType.META_DEPENDENCY, -1);
		this.dependingTermGenerator = dependingTermGenerator;
		this.dependedTermGenerator = dependedTermGenerator;
	}
	
	public MetaDynamicTerm(MetaRDLTerm dependingTerm, MetaTermGenerator dependedTermGenerator) {
		this((index, depth, isLast) -> dependingTerm, dependedTermGenerator);
	}
	
	public MetaDynamicTerm(MetaTermGenerator dependingTermGenerator,  MetaRDLTerm dependedTerm) {
		this(dependingTermGenerator, (MetaTermGenerator) (index, depht, isLast) -> dependedTerm);
		isStaticSize = true;
	}
	
	public MetaDynamicTerm(MetaTermGenerator dependingTermGenerator, MetaTermPairGenerator termPairGenerator) {
		super(new Symbol("", -1), TermType.META_DEPENDENCY_TERM, -1);
		this.dependingTermGenerator = dependingTermGenerator;
		this.termPairGenerator = termPairGenerator;
	}
	
	public MetaDynamicTerm(MetaRDLTerm dependingTerm, MetaTermPairGenerator termPairGenerator) {
		this((index, depth, isLast) -> dependingTerm, termPairGenerator);
	}
	
	public MetaDynamicTerm(MetaTermGenerator dependingTermGenerator, MetaRDLTerm dependedTerm, MetaRDLTerm argTerm) {
		this(dependingTermGenerator, (MetaTermPairGenerator)(index, depht, isLast) -> new TermPair(dependedTerm, argTerm));
		isStaticSize = true;
	}
	
	@Override
	public RDLTerm substitute(Map<Variable, RDLTerm> binding, int depth) {
		switch (this.termType) {
		case META_DEPENDENCY:
			return dependencyGenerate(binding).substitute(binding);
		case META_DEPENDENCY_TERM:
			return dependencyTermGenerate(binding).substitute(binding);
		default:
			break;
		}
		return null;
	}
	
	@Override
	public Set<MatchConstraint> isMatchedBy(RDLTerm another, MatchConstraint constraint, int depth) {
		Set<MatchConstraint> result = new HashSet<>();
		if (! another.getClass().isAssignableFrom(this.termType.getBaseTermClass())) {
			return result;
		}
		switch (this.termType) {
		case META_DEPENDENCY:
			return dependencyMatch((Dependency) another, constraint, depth);
		case META_DEPENDENCY_TERM:
			return dependencyTermMatch((DependencyTerm) another, constraint, depth);
		default:
			break;
		}
		return result;
	}
	
	private Set<MatchConstraint> dependencyMatch(Dependency another, MatchConstraint constraint, int depth) {
		Set<MatchConstraint> result = new HashSet<>();
		Set<MatchConstraint> tmpRes = new HashSet<>();
		RDLTerm anotherDependingTerm = another.getDependingTerm();
		TreeSet<EvaluatableTerm> anotherDependedTerms = another.getDependedTerms();
		boolean isLast = anotherDependingTerm instanceof Resource || anotherDependingTerm instanceof ResourceConstant;
		MetaRDLTerm metaDependingTerm = dependingTermGenerator.generate(0, depth, isLast);
		tmpRes = metaDependingTerm.isMatchedBy(anotherDependingTerm, constraint, depth + 1);
		if (tmpRes.isEmpty()) {
			return result;
		}
		for (List<Integer> perm: Permutation.permutation(anotherDependedTerms.size())) {
			Set<MatchConstraint> localResult = new HashSet<>(tmpRes);
			boolean flg = true;
			for (int metaTermIndex = 0; metaTermIndex < perm.size(); metaTermIndex++) {
				int anotherTermIndex = perm.get(metaTermIndex);
				EvaluatableTerm anotherDependedTerm = anotherDependedTerms.stream().skip(anotherTermIndex).findFirst().orElse(null);
				isLast = anotherDependedTerm instanceof Resource || anotherDependedTerm instanceof ResourceConstant;
				MetaRDLTerm metaDependedTerm = dependedTermGenerator.generate(metaTermIndex, depth, isLast);
				localResult = metaDependedTerm.isMatchedBy(anotherDependedTerm, localResult, depth + 1);
				if (localResult.isEmpty()) {
					flg = false;
					break;
				}
			}
			if (flg) {
				result.addAll(localResult);
			}
		}
		return result;
	}
	
	private Set<MatchConstraint> dependencyTermMatch(DependencyTerm another, MatchConstraint constraint, int depth) {
		Set<MatchConstraint> result = new HashSet<>();
		Set<MatchConstraint> tmpRes = new HashSet<>();
		RDLTerm anotherDependingTerm = another.getDependingTerm();
		List<EvaluatableTerm> anotherDependedTerms = another.getDependedTerms();
		List<EvaluatableTerm> anotherArgumentTerms = another.getArgumentTerms();
		boolean isLast = anotherDependingTerm instanceof Resource || anotherDependingTerm instanceof ResourceConstant;
		MetaRDLTerm metaDependingTerm = dependingTermGenerator.generate(0, depth, isLast);
		tmpRes = metaDependingTerm.isMatchedBy(anotherDependingTerm, constraint, depth + 1);
		if (tmpRes.isEmpty()) {
			return tmpRes;
		}
		for (List<Integer> perm: Permutation.permutation(anotherDependedTerms.size())) {
			Set<MatchConstraint> localResult = new HashSet<>(tmpRes);
			boolean flg = true;
			for (int metaTermIndex = 0; metaTermIndex < perm.size(); metaTermIndex++) {
				int anotherTermIndex = perm.get(metaTermIndex);
				EvaluatableTerm anotherDependedTerm = anotherDependedTerms.get(anotherTermIndex);
				EvaluatableTerm anotherArgTerm = anotherArgumentTerms.get(anotherTermIndex);
				TermPair metaTermPair = termPairGenerator.generate(metaTermIndex, depth, isLast);
				isLast = anotherDependedTerm instanceof Resource || anotherDependedTerm instanceof ResourceConstant;
				localResult = metaTermPair.dependedTerm().isMatchedBy(anotherDependedTerm, localResult, depth + 1);
				if (localResult.isEmpty()) {
					flg = false;
					break;
				}
				
				isLast = anotherArgTerm instanceof Resource || anotherArgTerm instanceof ResourceConstant;
				localResult = metaTermPair.argTerm().isMatchedBy(anotherArgTerm, localResult, depth + 1);
				if (localResult.isEmpty()) {
					flg = false;
					break;
				}
			}
			if (flg) {
				result.addAll(localResult);
			}
		}
		return result;
	}
	
	private MetaRDLTerm dependencyRecursionGenerate(int maxRecursion, int depth) {
		MetaRDLTerm dependingTerm = dependingTermGenerator.generate(0, depth, depth == maxRecursion - 1);
		MetaRDLTerm dependedTerm = dependedTermGenerator.generate(0, depth, depth == maxRecursion - 1);
		if (depth == maxRecursion - 1) {
			return new MetaRDLTerm(dependingTerm, dependedTerm);
		}
		if (dependingTerm instanceof MetaDynamicTerm generator) {
			return new MetaRDLTerm(generator.dependencyRecursionGenerate(maxRecursion, depth + 1), dependedTerm);
		} else if (dependedTerm instanceof MetaDynamicTerm generator) {
			return new MetaRDLTerm(dependedTerm, generator.dependencyRecursionGenerate(maxRecursion, depth + 1));
		}
		return null;
	}
	
	private MetaRDLTerm dependencyRecursionGenerate(Map<Variable, RDLTerm> binding, int maxRecursion, int depth) {
		MetaRDLTerm dependingTerm = dependingTermGenerator.generate(0, depth, depth == maxRecursion - 1);
		Set<MetaRDLTerm> dependedTerms = new HashSet<>();
		MetaRDLTerm dependedTerm = dependedTermGenerator.generate(0, depth, depth == maxRecursion - 1);
		dependedTerms.add(dependedTerm);
		for (int i = 0; i < searchMaxTermIndex(binding, depth, depth == maxRecursion - 1); i++) {
			dependedTerms.add(dependedTermGenerator.generate(i + 1, depth, depth == maxRecursion - 1));
		}
		if (depth == maxRecursion - 1) {
			return new MetaRDLTerm(dependingTerm, dependedTerms);
		}
		if (dependingTerm instanceof MetaDynamicTerm generator) {
			return new MetaRDLTerm(generator.dependencyRecursionGenerate(binding, maxRecursion, depth + 1), dependedTerms);
		} else if (dependedTerm instanceof MetaDynamicTerm generator) {
			return new MetaRDLTerm(dependedTerm, generator.dependencyRecursionGenerate(binding, maxRecursion, depth + 1));
		}
		return null;
	}
	
	private MetaRDLTerm dependencyTermRecursionGenerate(int maxRecursion, int depth) {
		MetaRDLTerm dependingTerm = dependingTermGenerator.generate(0, depth, depth == maxRecursion - 1);
		TermPair termPair = termPairGenerator.generate(0, depth, depth == maxRecursion - 1);
		MetaRDLTerm dependedTerm = termPair.dependedTerm();
		MetaRDLTerm argTerm = termPair.argTerm();
		if (depth == maxRecursion - 1) {
			return new MetaRDLTerm(dependingTerm, dependedTerm, argTerm);
		}
		if (dependingTerm instanceof MetaDynamicTerm generator) {
			return new MetaRDLTerm(generator.dependencyTermRecursionGenerate(maxRecursion, depth + 1), dependedTerm, argTerm);
		} else if (dependedTerm instanceof MetaDynamicTerm generator) {
			return new MetaRDLTerm(dependedTerm, generator.dependencyTermRecursionGenerate(maxRecursion, depth + 1), argTerm);
		} else if (argTerm instanceof MetaDynamicTerm generator) {
			return new MetaRDLTerm(dependedTerm, dependedTerm, generator.dependencyTermRecursionGenerate(maxRecursion, depth + 1));
		}
		return null;
	}
	
	private MetaRDLTerm dependencyTermRecursionGenerate(Map<Variable, RDLTerm> binding, int maxRecursion, int depth) {
		MetaRDLTerm dependingTerm = dependingTermGenerator.generate(0, depth, depth == maxRecursion - 1);
		List<MetaRDLTerm> termPairs = new ArrayList<>();
		TermPair termPair = termPairGenerator.generate(0, depth, depth == maxRecursion - 1);
		termPairs.add(termPair.dependedTerm());
		termPairs.add(termPair.argTerm());
		for (int i = 1; i <= searchMaxTermPairIndex(binding, depth, depth == maxRecursion - 1); i++) {
			TermPair pair = termPairGenerator.generate(i, depth, depth == maxRecursion - 1);
			termPairs.add(pair.dependedTerm());
			termPairs.add(pair.argTerm());
		}
		if (depth == maxRecursion - 1) {
			return new MetaRDLTerm(dependingTerm, termPairs);
		}
		List<MetaRDLTerm> resTerms = new ArrayList<>();
		for (MetaRDLTerm term : termPairs) {
			if (term instanceof MetaDynamicTerm generator) {
				resTerms.add(generator.dependencyTermRecursionGenerate(binding,  maxRecursion, depth+1));
			} else {
				resTerms.add(term);
			}
		}
		if (dependingTerm instanceof MetaDynamicTerm generator) {
			return new MetaRDLTerm(generator.dependencyTermRecursionGenerate(binding, maxRecursion, depth + 1), resTerms);
		}
		return new MetaRDLTerm(dependingTerm, resTerms);
	}
	
	private int searchMaxTermIndex(Map<Variable, RDLTerm> binding, int depth, boolean isLast) {
		if (isStaticSize) return 0;
		int ok = -1;
		int ng = 100;
		while (Math.abs(ok - ng) > 1) {
			int mid = (ok + ng) / 2;
			MetaRDLTerm generatedTerm = dependedTermGenerator.generate(mid, depth, isLast);
			Set<Variable> variables = new HashSet<>(generatedTerm.getAllVariables().stream().map(v -> v.getVariableName()).toList());
			variables.removeAll(binding.keySet());
			if (variables.isEmpty()) {
				ok = mid;
			} else {
				ng = mid;
			}
		}
		return ok;
	}
	
	private int searchMaxTermPairIndex(Map<Variable, RDLTerm> binding, int depth, boolean isLast) {
		if (isStaticSize) return 0;
		int ok = -1;
		int ng = 100;
		while (Math.abs(ok - ng) > 1) {
			int mid = (ok + ng) / 2;
			TermPair generatedTerm = termPairGenerator.generate(mid, depth, isLast);
			Set<Variable> variables = new HashSet<>(generatedTerm.dependedTerm().getAllVariables().stream().map(v -> v.getVariableName()).toList());
			variables.removeAll(binding.keySet());
			if (variables.isEmpty()) {
				ok = mid;
			} else {
				ng = mid;
			}
		}
		return ok;
	}
	
	public MetaRDLTerm dependencyGenerate(Map<Variable, RDLTerm> binding) {
		int ok = 0;
		int ng = 100;
		while (Math.abs(ok - ng) > 1) {
			int mid = (ok + ng) / 2;
			MetaRDLTerm generatedTerm = dependencyRecursionGenerate(mid, 0);
			if (generatedTerm == null) {
				ng = mid;
				continue;
			}
			Set<Variable> variables = new HashSet<>(generatedTerm.getAllVariables().stream().map(v -> v.getVariableName()).toList());
			variables.removeAll(binding.keySet());
			if (variables.isEmpty()) {
				ok = mid;
			} else {
				ng = mid;
			}
		}
		return dependencyRecursionGenerate(binding, ok, 0);
	}
	
	public MetaRDLTerm dependencyTermGenerate(Map<Variable, RDLTerm> binding) {
		int ok = 0;
		int ng = 100;
		while (Math.abs(ok - ng) > 1) {
			int mid = (ok + ng) / 2;
			MetaRDLTerm generatedTerm = dependencyTermRecursionGenerate(mid, 0);
			if (generatedTerm == null) {
				ng = mid;
				continue;
			}
			Set<Variable> variables = new HashSet<>(generatedTerm.getAllVariables().stream().map(v -> v.getVariableName()).toList());
			variables.removeAll(binding.keySet());
			if (variables.isEmpty()) {
				ok = mid;
			} else {
				ng = mid;
			}
		}
		return dependencyTermRecursionGenerate(binding, ok, 0);
	}
	
}