diff --git a/src/main/java/Main.java b/src/main/java/Main.java index dd29488..79908d4 100644 --- a/src/main/java/Main.java +++ b/src/main/java/Main.java @@ -1,15 +1,21 @@ import com.google.common.collect.TreeMultimap; import java.util.HashMap; +import java.util.List; import java.util.Map; import constants.Types; +import inference.axioms.RightSubstitution; import models.algebra.Constant; import models.algebra.Expression; import models.algebra.Type; import models.algebra.Variable; -import models.terms.meta.MetaDynaimcDependencyTerm; +import models.formulas.DependencyFormula; +import models.formulas.EquationFormula; +import models.terms.DependencyTerm; +import models.terms.Resource; import models.terms.meta.MetaDynamicDependency; +import models.terms.meta.MetaDynamicDependencyTerm; import models.terms.meta.MetaRDLTerm; import models.terms.meta.MetaResource; import models.terms.meta.MetaTermGenerator; @@ -24,6 +30,7 @@ sandbox2(); sandbox3(); sandbox4(); + sandbox5(); } @@ -64,12 +71,12 @@ } static void sandbox4() { - MetaDynaimcDependencyTerm t1 = new MetaDynaimcDependencyTerm((ci, cd, mi, md, contex) -> new MetaResource(new Variable("x" + ci))); - MetaDynaimcDependencyTerm t2 = new MetaDynaimcDependencyTerm(new MetaTermGenerator() { + MetaDynamicDependencyTerm t1 = new MetaDynamicDependencyTerm((ci, cd, mi, md, contex) -> new MetaResource(new Variable("x" + ci))); + MetaDynamicDependencyTerm t2 = new MetaDynamicDependencyTerm(new MetaTermGenerator() { @Override public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { if (curDepth == 0 && curIndex != 0 && curIndex % 2 == 0) { - return new MetaDynaimcDependencyTerm(this); + return new MetaDynamicDependencyTerm(this); } return new MetaResource(new Variable("x" + curDepth + "_" + curIndex)); } @@ -78,4 +85,29 @@ System.out.println(t2.generate(0, 3, 2, null)); } + static void sandbox5() { + RightSubstitution rs = new RightSubstitution(); + Resource a = new Resource("a", 1); + Resource b = new Resource("b", 1); + Resource c = new Resource("c", 1); + Resource d = new Resource("d", 1); + Resource e = new Resource("e", 1); + Resource f = new Resource("f", 1); + Resource g = new Resource("f", 1); + Resource h = new Resource("h", 1); + Resource i = new Resource("i", 1); + Resource j = new Resource("j", 1); + Resource k = new Resource("k", 1); + Resource l = new Resource("l", 1); + EquationFormula eq = new EquationFormula(a, b); + DependencyFormula dep = new DependencyFormula(c, d); + EquationFormula eq2 = new EquationFormula(new DependencyTerm(d, e, f), a); + System.out.println(rs.apply(List.of(eq, dep, eq2))); + DependencyTerm t1 = new DependencyTerm(c, d, a); + System.out.println(rs.generateRightSideHand(List.of(eq, dep, eq2), t1)); + DependencyFormula dep2 = new DependencyFormula(c, g); + EquationFormula eq3 = new EquationFormula(new DependencyTerm(g, h, i), j); + System.out.println(rs.apply(List.of(eq, eq2, eq3, dep, dep2))); + } + } diff --git a/src/main/java/inference/AssumptionSizeCalculator.java b/src/main/java/inference/AssumptionSizeCalculator.java new file mode 100644 index 0000000..aa9e971 --- /dev/null +++ b/src/main/java/inference/AssumptionSizeCalculator.java @@ -0,0 +1,10 @@ +package inference; + +import models.terms.RDLTerm; + +@FunctionalInterface +public interface AssumptionSizeCalculator { + + public int calculate(RDLTerm rightSideHand); + +} diff --git a/src/main/java/inference/ConclusionSizeCalculator.java b/src/main/java/inference/ConclusionSizeCalculator.java new file mode 100644 index 0000000..d2cdb23 --- /dev/null +++ b/src/main/java/inference/ConclusionSizeCalculator.java @@ -0,0 +1,12 @@ +package inference; + +import java.util.List; + +import models.formulas.Formula; + +@FunctionalInterface +public interface ConclusionSizeCalculator { + + public int calculate(List assumptions); + +} diff --git a/src/main/java/inference/InferenceRule.java b/src/main/java/inference/InferenceRule.java index 6abbded..eb955e1 100644 --- a/src/main/java/inference/InferenceRule.java +++ b/src/main/java/inference/InferenceRule.java @@ -16,40 +16,55 @@ import models.formulas.meta.MetaFormula; import models.terms.RDLTerm; import models.terms.meta.MatchConstraint; +import models.terms.meta.MetaRDLTerm; import models.terms.meta.MetaVariable; import utils.Permutation; public class InferenceRule { @Getter - private final String name; + protected String name; @Getter - private final List assumptions; + protected List assumptions; @Getter - private final MetaFormula conclusion; - protected final InferenceOrderConstraint defaultOrderConstraint; + protected MetaFormula conclusion; + protected InferenceOrderConstraint defaultOrderConstraint; - private final boolean hasDynamicAssumption; - private final AssumptionGenerator generator; + protected List repetitionAssumptions; + protected ConclusionSizeCalculator conclusionMaxIndexCalculator; + protected ConclusionSizeCalculator conclusionMaxDepthCalculator; + protected AssumptionSizeCalculator assumptionRepetitionSizeCalculator; + protected InferenceRule(String name) { + this.name = name; + } public InferenceRule(String name, List assumptions, MetaFormula conclusion, InferenceOrderConstraint constraint) { this.name = name; this.assumptions = assumptions; this.conclusion = conclusion; this.defaultOrderConstraint = constraint; - this.hasDynamicAssumption = false; - this.generator = null; } - public InferenceRule(String name, List assumptions, AssumptionGenerator generator, MetaFormula conclusion, InferenceOrderConstraint constraint) { + public InferenceRule( + String name, + List assumptions, + List repetitionAssumptions, + MetaFormula conclusion, + InferenceOrderConstraint constraint, + ConclusionSizeCalculator conclusionMaxIndexCalculator, + ConclusionSizeCalculator conclusionMaxDepthCalculator, + AssumptionSizeCalculator assumptionSizeCalculator + ) { this.name = name; this.assumptions = assumptions; + this.repetitionAssumptions = repetitionAssumptions; this.conclusion = conclusion; this.defaultOrderConstraint = constraint; - this.hasDynamicAssumption = true; - this.generator = generator; + this.conclusionMaxIndexCalculator = conclusionMaxIndexCalculator; + this.conclusionMaxDepthCalculator = conclusionMaxDepthCalculator; + this.assumptionRepetitionSizeCalculator = assumptionSizeCalculator; } public InferenceRule( List assumptions, MetaFormula conclusion, InferenceOrderConstraint constraint) { @@ -60,10 +75,6 @@ this(name, assumptions, conclusion, null); } - public InferenceRule(String name, List assumptions, AssumptionGenerator generator, MetaFormula conclusion) { - this(name, assumptions, generator, conclusion, null); - } - public InferenceRule(List assumptions, MetaFormula conclusion) { this("undefined", assumptions, conclusion, null); } @@ -182,19 +193,19 @@ return null; } } - if (hasDynamicAssumption) { - for (int i = 0; i < assumptions.size() - getAssumptionSize(); i++) { - int j = getAssumptionSize() + i; - result = this.generator.generate(i).isMatchedBy(assumptions.get(j), result); - if (result.isEmpty()) { - return null; - } - } - } +// if (hasDynamicAssumption) { +// for (int i = 0; i < assumptions.size() - getAssumptionSize(); i++) { +// int j = getAssumptionSize() + i; +// result = this.generator.generate(i).isMatchedBy(assumptions.get(j), result); +// if (result.isEmpty()) { +// return null; +// } +// } +// } Formula subRes = null; for (MatchConstraint con: result) { try { - subRes = conclusion.substitution(con.getBinding()); + subRes = conclusion.substitution(con.getBinding(), new HashMap<>()); } catch (SubstituteFailedException e) { continue; } @@ -212,12 +223,12 @@ for (int i = 0; i < getAssumptionSize(); i++) { constraints = this.assumptions.get(i).isMatchedBy(assumptionList.get(i), constraints); } - if (hasDynamicAssumption) { - for (int i = 0; i < assumptions.size() - getAssumptionSize(); i++) { - int j = getAssumptionSize() + i; - constraints = this.generator.generate(i).isMatchedBy(assumptions.get(j), constraints); - } - } +// if (hasDynamicAssumption) { +// for (int i = 0; i < assumptions.size() - getAssumptionSize(); i++) { +// int j = getAssumptionSize() + i; +// constraints = this.generator.generate(i).isMatchedBy(assumptions.get(j), constraints); +// } +// } for (MatchConstraint constraint: constraints) { try { return metaFormula.getRightSideHand().substitute(constraint.getBinding()); @@ -258,6 +269,21 @@ return sb.toString(); } + protected List repetitionAssumptionGenerate(int i) { + if (i == 0) { + return new ArrayList<>(this.repetitionAssumptions); + } + List result = new ArrayList<>(); + for (MetaFormula metaFormula : this.repetitionAssumptions) { + Map mapping = new HashMap<>(); + for (MetaVariable variable : metaFormula.getAllVariables()) { + mapping.put(variable, variable.cloneWithName(variable.getVariableName().getName() + i)); + } + result.add(metaFormula.replace(mapping)); + } + return result; + } + @Override public boolean equals(Object another) { if (! (another instanceof InferenceRule)) { diff --git a/src/main/java/inference/axioms/RightSubstitution.java b/src/main/java/inference/axioms/RightSubstitution.java new file mode 100644 index 0000000..b8f3929 --- /dev/null +++ b/src/main/java/inference/axioms/RightSubstitution.java @@ -0,0 +1,159 @@ +package inference.axioms; +import java.util.ArrayList; +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; + +import exceptions.SubstituteFailedException; +import inference.InferenceRule; +import models.algebra.Variable; +import models.formulas.Formula; +import models.formulas.meta.MetaDependencyFormula; +import models.formulas.meta.MetaEquationFormula; +import models.formulas.meta.MetaFormula; +import models.terms.RDLTerm; +import models.terms.meta.MatchConstraint; +import models.terms.meta.MetaDependencyTerm; +import models.terms.meta.MetaDynamicDependencyTerm; +import models.terms.meta.MetaEvaluatableTermVariable; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaTermGenerator; + +public class RightSubstitution extends InferenceRule { + + public RightSubstitution() { + super("Right Substitution"); + this.assumptions = new ArrayList<>(); + this.repetitionAssumptions = new ArrayList<>(); + assumptions.add(new MetaEquationFormula( + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaEvaluatableTermVariable(new Variable("ue")) + )); + repetitionAssumptions.add(new MetaDependencyFormula( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("re")) + )); + repetitionAssumptions.add(new MetaEquationFormula( + new MetaDependencyTerm( + new MetaEvaluatableTermVariable(new Variable("re")), + new MetaEvaluatableTermVariable(new Variable("x")), + new MetaEvaluatableTermVariable(new Variable("y")) + ), + new MetaEvaluatableTermVariable(new Variable("te")) + )); + conclusion = new MetaEquationFormula( + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + if (curIndex == 0) { + return new MetaEvaluatableTermVariable(new Variable("re")); + } + if (curIndex == 1) { + return new MetaEvaluatableTermVariable(new Variable("te")); + } + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("re" + curIndex / 2)); + } + return new MetaEvaluatableTermVariable(new Variable("te" + curIndex / 2)); + } + }, + new MetaEvaluatableTermVariable(new Variable("se")) + ), + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + if (curIndex == 0) { + return new MetaEvaluatableTermVariable(new Variable("re")); + } + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("re" + curIndex / 2)); + } + if (curIndex == 1) { + return new MetaEvaluatableTermVariable(new Variable("ue")); + } + return new MetaEvaluatableTermVariable(new Variable("te" + curIndex / 2)); + } + }, + new MetaEvaluatableTermVariable(new Variable("se")) + ) + ); + conclusionMaxIndexCalculator = (assumptions) -> (assumptions.size() - 1) / 2 * 2 + 1; + conclusionMaxDepthCalculator = (assumptions) -> 1; + assumptionRepetitionSizeCalculator = (conclusion) -> (conclusion.getMaxIndex() - 1) / 2; + } + + @Override + protected Formula apply(List assumptions, MatchConstraint constraint) { + Set result = new HashSet<>(); + result.add(constraint); + for (int i = 0; i < this.assumptions.size(); i++) { + MetaFormula metaAssumption = this.assumptions.get(i); + Formula assumption = assumptions.get(i); + result = metaAssumption.isMatchedBy(assumption, result); + if (result.isEmpty()) { + return null; + } + } + if (this.repetitionAssumptions.size() != 0 && (assumptions.size() - this.assumptions.size()) % this.repetitionAssumptions.size() != 0) { + return null; + } + for (int i = 0; i < (assumptions.size() - this.assumptions.size()) / this.repetitionAssumptions.size(); i++) { + List metaAssumptions = repetitionAssumptionGenerate(i); + for (int j = 0; j < this.repetitionAssumptions.size(); j++) { + Formula assumption = assumptions.get(this.assumptions.size() + i * this.repetitionAssumptions.size() + j); + MetaFormula metaAssumption = metaAssumptions.get(j); + result = metaAssumption.isMatchedBy(assumption, result); + if (result.isEmpty()) { + return null; + } + } + } + Formula subRes = null; + for (MatchConstraint con: result) { + try { + int maxIndex = conclusionMaxIndexCalculator != null ? conclusionMaxIndexCalculator.calculate(assumptions) : 0; + int maxDepth = conclusionMaxDepthCalculator != null ? conclusionMaxDepthCalculator.calculate(assumptions) : 0; + subRes = conclusion.substitution(con.getBinding(), Map.of("maxIndex", maxIndex, "maxDepth", maxDepth)); + } catch (SubstituteFailedException e) { + continue; + } + } + return subRes; + } + + @Override + public RDLTerm generateRightSideHand(List assumptions, RDLTerm leftSideHand) { + MetaRDLTerm metaLeftSideHand = ((MetaEquationFormula) conclusion).getLeftSideHand(); + Set result = metaLeftSideHand.isMatchedBy(leftSideHand); + int assumptionsSize = assumptionRepetitionSizeCalculator.calculate(leftSideHand); + for (int i = 0; i < this.assumptions.size(); i++) { + Formula assumption = assumptions.get(i); + MetaFormula metaAssumption = this.assumptions.get(i); + result = metaAssumption.isMatchedBy(assumption, result); + if (result.isEmpty()) { + return null; + } + } + if (this.repetitionAssumptions.size() != 0 && (assumptions.size() - this.assumptions.size()) % this.repetitionAssumptions.size() != 0) { + return null; + } + for (int i = 0; i < assumptionsSize; i++) { + List metaAssumptions = repetitionAssumptionGenerate(i); + for (int j = 0; j < metaAssumptions.size(); j++) { + Formula assumption = assumptions.get(this.assumptions.size() + i * this.repetitionAssumptions.size() + j); + MetaFormula metaAssumption = metaAssumptions.get(j); + result = metaAssumption.isMatchedBy(assumption, result); + if (result.isEmpty()) { + return null; + } + } + } + return ((MetaEquationFormula) conclusion).getRightSideHand().substitute(result.iterator().next().getBinding(), Map.of("maxIndex", leftSideHand.getMaxIndex(), "maxDepth", leftSideHand.getMaxDepth())); + } + +} diff --git a/src/main/java/models/formulas/meta/MetaDependencyFormula.java b/src/main/java/models/formulas/meta/MetaDependencyFormula.java index 04407e2..300d0ef 100644 --- a/src/main/java/models/formulas/meta/MetaDependencyFormula.java +++ b/src/main/java/models/formulas/meta/MetaDependencyFormula.java @@ -19,6 +19,7 @@ import models.terms.meta.MetaDynamicDependency; import models.terms.meta.MetaRDLTerm; import models.terms.meta.MetaTermGenerator; +import models.terms.meta.MetaVariable; @Getter public class MetaDependencyFormula extends MetaFormula { @@ -59,10 +60,19 @@ @Override - public DependencyFormula substitution(Map binding) { - return new DependencyFormula((Dependency) dependency.substitute(binding)); + public DependencyFormula substitution(Map binding, Map context) { + return new DependencyFormula((Dependency) dependency.substitute(binding, context)); } + @Override + public MetaDependencyFormula replace(Map mapping) { + return new MetaDependencyFormula(this.dependency.replace(mapping)); + } + + @Override + public Set getAllVariables() { + return this.dependency.getAllVariables(); + } public String toString() { diff --git a/src/main/java/models/formulas/meta/MetaEquationFormula.java b/src/main/java/models/formulas/meta/MetaEquationFormula.java index e061866..5edee3d 100644 --- a/src/main/java/models/formulas/meta/MetaEquationFormula.java +++ b/src/main/java/models/formulas/meta/MetaEquationFormula.java @@ -13,6 +13,7 @@ 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 { @@ -44,8 +45,21 @@ } @Override - public EquationFormula substitution(Map binding) { - return new EquationFormula((EvaluatableTerm) leftSideHand.substitute(binding), (EvaluatableTerm) rightSideHand.substitute(binding)); + public EquationFormula substitution(Map binding, Map context) { + return new EquationFormula((EvaluatableTerm) leftSideHand.substitute(binding, context), (EvaluatableTerm) rightSideHand.substitute(binding, context)); + } + + @Override + public MetaEquationFormula replace(Map mapping) { + return new MetaEquationFormula(this.leftSideHand.replace(mapping), this.rightSideHand.replace(mapping)); + } + + @Override + public Set getAllVariables() { + Set result = new HashSet<>(); + result.addAll(this.leftSideHand.getAllVariables()); + result.addAll(this.rightSideHand.getAllVariables()); + return result; } public String toString() { diff --git a/src/main/java/models/formulas/meta/MetaFormula.java b/src/main/java/models/formulas/meta/MetaFormula.java index bb54cc0..f6befda 100644 --- a/src/main/java/models/formulas/meta/MetaFormula.java +++ b/src/main/java/models/formulas/meta/MetaFormula.java @@ -9,6 +9,8 @@ import models.formulas.Formula; import models.terms.RDLTerm; import models.terms.meta.MatchConstraint; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaVariable; public abstract class MetaFormula { @@ -26,9 +28,12 @@ return result; } - public abstract Formula substitution(Map binding); + public abstract Formula substitution(Map binding, Map context); public abstract Set getSubTerms(Class clazz); + + public abstract MetaFormula replace(Map mapping); + public abstract Set getAllVariables(); public abstract String toString(); public abstract boolean equals(Object another); diff --git a/src/main/java/models/terms/meta/MetaDependency.java b/src/main/java/models/terms/meta/MetaDependency.java index c031e72..8342e29 100644 --- a/src/main/java/models/terms/meta/MetaDependency.java +++ b/src/main/java/models/terms/meta/MetaDependency.java @@ -127,6 +127,27 @@ } } + @Override + public MetaRDLTerm replace(Map mapping) { + RDLTerm dependingTerm = this.dependingTerm; + List dependedTerms = new ArrayList<>(); + if (dependingTerm instanceof MetaRDLTerm metaTerm) { + if (mapping.containsKey(metaTerm)) { + metaTerm = mapping.get(metaTerm); + } + dependingTerm = metaTerm.replace(mapping); + } + for (RDLTerm term : this.dependedTerms) { + if (term instanceof MetaRDLTerm metaTerm) { + if (mapping.containsKey(metaTerm)) { + metaTerm = mapping.get(metaTerm); + } + term = metaTerm.replace(mapping); + } + dependedTerms.add(term); + } + return new MetaDependency(dependingTerm, dependedTerms); + } @Override public String toString() { diff --git a/src/main/java/models/terms/meta/MetaDependencyTerm.java b/src/main/java/models/terms/meta/MetaDependencyTerm.java index 8d6fd7b..ec17a2f 100644 --- a/src/main/java/models/terms/meta/MetaDependencyTerm.java +++ b/src/main/java/models/terms/meta/MetaDependencyTerm.java @@ -152,6 +152,40 @@ } } + @Override + public MetaRDLTerm replace(Map mapping) { + RDLTerm dependingTerm = this.dependingTerm; + List termPairs = new ArrayList<>(); + if (dependingTerm instanceof MetaRDLTerm metaTerm) { + if (mapping.containsKey(metaTerm)) { + metaTerm = mapping.get(metaTerm); + } + dependingTerm = metaTerm.replace(mapping); + } + for (RDLTerm dependedTerm : this.termPairs.keySet()) { + RDLTerm nextDependedTerm; + if (dependedTerm instanceof MetaRDLTerm metaTerm) { + if (mapping.containsKey(metaTerm)) { + metaTerm = mapping.get(metaTerm); + } + nextDependedTerm = metaTerm.replace(mapping); + } else { + nextDependedTerm = dependedTerm; + } + for (RDLTerm argTerm : this.termPairs.get(dependedTerm)) { + if (argTerm instanceof MetaRDLTerm metaTerm) { + if (mapping.containsKey(metaTerm)) { + metaTerm = mapping.get(metaTerm); + } + argTerm = metaTerm.replace(mapping); + } + termPairs.add(nextDependedTerm); + termPairs.add(argTerm); + } + } + return new MetaDependencyTerm(dependingTerm, termPairs); + } + @Override public String toString() { diff --git a/src/main/java/models/terms/meta/MetaDependencyTermVariable.java b/src/main/java/models/terms/meta/MetaDependencyTermVariable.java index ab5291b..6a6a0a7 100644 --- a/src/main/java/models/terms/meta/MetaDependencyTermVariable.java +++ b/src/main/java/models/terms/meta/MetaDependencyTermVariable.java @@ -3,7 +3,6 @@ import lombok.Getter; import models.algebra.Constant; import models.algebra.Expression; -import models.algebra.Symbol; import models.algebra.Variable; @Getter @@ -21,4 +20,9 @@ super(MetaRDLTerm.TermType.META_DEPENDENCY_TERM_VARIABLE, variableName, OrderConstraint.EQ, order); } + @Override + public MetaDependencyTermVariable cloneWithName(String name) { + return new MetaDependencyTermVariable(new Variable(name), constraint, orderExpression); + } + } diff --git a/src/main/java/models/terms/meta/MetaDependencyVariable.java b/src/main/java/models/terms/meta/MetaDependencyVariable.java index b59886a..07765e6 100644 --- a/src/main/java/models/terms/meta/MetaDependencyVariable.java +++ b/src/main/java/models/terms/meta/MetaDependencyVariable.java @@ -3,7 +3,6 @@ import lombok.Getter; import models.algebra.Constant; import models.algebra.Expression; -import models.algebra.Symbol; import models.algebra.Variable; @Getter @@ -21,4 +20,9 @@ super(MetaRDLTerm.TermType.META_DEPENDENCY_VARIABLE, variableName, OrderConstraint.EQ, order); } + @Override + public MetaDependencyVariable cloneWithName(String name) { + return new MetaDependencyVariable(new Variable(name), constraint, orderExpression); + } + } diff --git a/src/main/java/models/terms/meta/MetaDynaimcDependencyTerm.java b/src/main/java/models/terms/meta/MetaDynaimcDependencyTerm.java deleted file mode 100644 index 8f2dbd6..0000000 --- a/src/main/java/models/terms/meta/MetaDynaimcDependencyTerm.java +++ /dev/null @@ -1,120 +0,0 @@ -package models.terms.meta; - -import com.google.common.collect.TreeMultiset; - -import java.util.ArrayList; -import java.util.HashMap; -import java.util.List; -import java.util.Map; -import java.util.Set; -import java.util.stream.Collectors; -import java.util.stream.IntStream; - -import exceptions.SubstituteFailedException; -import exceptions.SyntaxException; -import models.algebra.Variable; -import models.terms.RDLTerm; - -public class MetaDynaimcDependencyTerm extends MetaDependencyTerm implements MetaDynamicTerm{ - - private final MetaTermGenerator generator; - - public MetaDynaimcDependencyTerm (MetaTermGenerator generator) { - this.generator = generator; - } - - public MetaDynaimcDependencyTerm(MetaTermGenerator generator, List terms) { - this.generator = generator; - if (terms.size() != 0 && terms.size() % 2 != 1) { - throw new SyntaxException(""); - } - this.dependingTerm = terms.size() > 0 ? terms.get(0) : null; - for (int i = 0; i < (terms.size() - 1) / 2; i++) { - RDLTerm dependedTerm = terms.get(i * 2 + 1); - RDLTerm argTerm = terms.get(i * 2 + 2); - this.termPairs.computeIfAbsent(dependedTerm, k -> TreeMultiset.create()).add(argTerm); - addChild(dependedTerm); - addChild(argTerm); - } - } - - @Override - public MetaRDLTerm generate(int depth, Map context) { - // TODO 自動生成されたメソッド・スタブ - return null; - } - - public MetaRDLTerm generate(int maxIndex, int maxDepth, Map context) { - return generate(1, maxIndex, maxDepth, context); - } - - @Override - public MetaRDLTerm generate(int depth, int maxIndex, int maxDepth, Map context) { - if (maxIndex % 2 == 0 && maxIndex <= 2) return null; - RDLTerm dependingTerm; - List termPairs = new ArrayList<>(); - if (this.dependingTerm != null) { - dependingTerm = this.dependingTerm; - } else { - dependingTerm = generator.generate(0, depth, maxIndex, maxDepth, context); - } - while (dependingTerm instanceof MetaDynamicTerm dynamicTerm) { - dependingTerm = dynamicTerm.generate(depth + 1, maxIndex, maxDepth, context); - } - int index = 1; - for (RDLTerm dependedTerm : this.termPairs.keySet()) { - for (RDLTerm argTerm : this.termPairs.get(dependedTerm)) { - while (dependedTerm instanceof MetaDynamicTerm dynamicTerm) { - dependedTerm = dynamicTerm.generate(depth + 1, maxIndex, maxDepth, context); - } - while (argTerm instanceof MetaDynamicTerm dynamicTerm) { - argTerm = dynamicTerm.generate(depth + 1, maxIndex, maxDepth, context); - } - termPairs.add(dependedTerm); - termPairs.add(argTerm); - index+=2; - } - } - for (int i = 0; i < (maxIndex - index) / 2; i++) { - RDLTerm dependedTerm = generator.generate(i * 2 + 1, depth, maxIndex, maxDepth, context); - RDLTerm argTerm = generator.generate(i * 2 + 2, depth, maxIndex, maxDepth, context); - while (dependedTerm instanceof MetaDynamicTerm dynamicTerm) { - dependedTerm = dynamicTerm.generate(depth + 1, maxIndex, maxDepth, context); - } - while (argTerm instanceof MetaDynamicTerm dynamicTerm) { - argTerm = dynamicTerm.generate(depth + 1, maxIndex, maxDepth, context); - } - termPairs.add(dependedTerm); - termPairs.add(argTerm); - } - return new MetaDependencyTerm(dependingTerm, termPairs); - } - - @Override - public Set isMatchedBy(RDLTerm another, Set constraint) { - int maxIndex = another.getMaxIndex(); - int maxDepth = another.getMaxDepth(); - MetaRDLTerm metaTerm = generate(maxIndex, maxDepth, new HashMap<>()); - return metaTerm.isMatchedBy(another, constraint); - } - - @Override - public RDLTerm substitute(Map binding, Map context) { - if (! context.containsKey("maxIndex")) throw new SubstituteFailedException(); - if (! context.containsKey("maxDepth")) throw new SubstituteFailedException(); - int maxIndex = (int) context.get("maxIndex"); - int maxDepth = (int) context.get("maxDepth"); - return generate(0, maxIndex, maxDepth, context).substitute(binding, context); - } - - - @Override - public String toString() { - if (dependingTerm != null) { - 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(", ")) + " ...? ]"; - } - return "[ ...? ]"; - } - -} diff --git a/src/main/java/models/terms/meta/MetaDynamicDependencyTerm.java b/src/main/java/models/terms/meta/MetaDynamicDependencyTerm.java new file mode 100644 index 0000000..aeb528e --- /dev/null +++ b/src/main/java/models/terms/meta/MetaDynamicDependencyTerm.java @@ -0,0 +1,125 @@ +package models.terms.meta; + +import com.google.common.collect.TreeMultiset; + +import java.util.ArrayList; +import java.util.Arrays; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import java.util.Set; +import java.util.stream.Collectors; +import java.util.stream.IntStream; + +import exceptions.SubstituteFailedException; +import exceptions.SyntaxException; +import models.algebra.Variable; +import models.terms.RDLTerm; + +public class MetaDynamicDependencyTerm extends MetaDependencyTerm implements MetaDynamicTerm{ + + private final MetaTermGenerator generator; + + public MetaDynamicDependencyTerm (MetaTermGenerator generator) { + this.generator = generator; + } + + public MetaDynamicDependencyTerm(MetaTermGenerator generator, List terms) { + this.generator = generator; + if (terms.size() != 0 && terms.size() % 2 != 1) { + throw new SyntaxException(""); + } + this.dependingTerm = terms.size() > 0 ? terms.get(0) : null; + for (int i = 0; i < (terms.size() - 1) / 2; i++) { + RDLTerm dependedTerm = terms.get(i * 2 + 1); + RDLTerm argTerm = terms.get(i * 2 + 2); + this.termPairs.computeIfAbsent(dependedTerm, k -> TreeMultiset.create()).add(argTerm); + addChild(dependedTerm); + addChild(argTerm); + } + } + + public MetaDynamicDependencyTerm(MetaTermGenerator generator, RDLTerm ...terms) { + this(generator, Arrays.asList(terms)); + } + + @Override + public MetaRDLTerm generate(int depth, Map context) { + // TODO 自動生成されたメソッド・スタブ + return null; + } + + public MetaRDLTerm generate(int maxIndex, int maxDepth, Map context) { + return generate(1, maxIndex, maxDepth, context); + } + + @Override + public MetaRDLTerm generate(int depth, int maxIndex, int maxDepth, Map context) { + if (maxIndex % 2 == 0 && maxIndex <= 2) return null; + RDLTerm dependingTerm; + List termPairs = new ArrayList<>(); + if (this.dependingTerm != null) { + dependingTerm = this.dependingTerm; + } else { + dependingTerm = generator.generate(0, depth, maxIndex, maxDepth, context); + } + while (dependingTerm instanceof MetaDynamicTerm dynamicTerm) { + dependingTerm = dynamicTerm.generate(depth + 1, maxIndex, maxDepth, context); + } + int index = 1; + for (RDLTerm dependedTerm : this.termPairs.keySet()) { + for (RDLTerm argTerm : this.termPairs.get(dependedTerm)) { + while (dependedTerm instanceof MetaDynamicTerm dynamicTerm) { + dependedTerm = dynamicTerm.generate(depth + 1, maxIndex, maxDepth, context); + } + while (argTerm instanceof MetaDynamicTerm dynamicTerm) { + argTerm = dynamicTerm.generate(depth + 1, maxIndex, maxDepth, context); + } + termPairs.add(dependedTerm); + termPairs.add(argTerm); + index+=2; + } + } + for (int i = 0; i < (maxIndex - index) / 2; i++) { + RDLTerm dependedTerm = generator.generate(i * 2 + 1, depth, maxIndex, maxDepth, context); + RDLTerm argTerm = generator.generate(i * 2 + 2, depth, maxIndex, maxDepth, context); + while (dependedTerm instanceof MetaDynamicTerm dynamicTerm) { + dependedTerm = dynamicTerm.generate(depth + 1, maxIndex, maxDepth, context); + } + while (argTerm instanceof MetaDynamicTerm dynamicTerm) { + argTerm = dynamicTerm.generate(depth + 1, maxIndex, maxDepth, context); + } + termPairs.add(dependedTerm); + termPairs.add(argTerm); + } + return new MetaDependencyTerm(dependingTerm, termPairs); + } + + @Override + public Set isMatchedBy(RDLTerm another, MatchConstraint constraint) { + int maxIndex = another.getMaxIndex(); + int maxDepth = another.getMaxDepth(); + MetaRDLTerm metaTerm = generate(maxIndex, maxDepth, new HashMap<>()); + return metaTerm.isMatchedBy(another, constraint); + } + + @Override + public RDLTerm substitute(Map binding, Map context) { + if (! context.containsKey("maxIndex")) throw new SubstituteFailedException(); + if (! context.containsKey("maxDepth")) throw new SubstituteFailedException(); + int maxIndex = (int) context.get("maxIndex"); + int maxDepth = (int) context.get("maxDepth"); + return generate(maxIndex, maxDepth, context).substitute(binding, context); + } + + + @Override + public String toString() { + if (dependingTerm != null) { + 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(", ")) + " ...? ]"; + } + return "[ ...? ]"; + } + +} diff --git a/src/main/java/models/terms/meta/MetaEvaluatableTermVariable.java b/src/main/java/models/terms/meta/MetaEvaluatableTermVariable.java index 8c19328..9dbaaad 100644 --- a/src/main/java/models/terms/meta/MetaEvaluatableTermVariable.java +++ b/src/main/java/models/terms/meta/MetaEvaluatableTermVariable.java @@ -2,7 +2,6 @@ import models.algebra.Constant; import models.algebra.Expression; -import models.algebra.Symbol; import models.algebra.Variable; import models.terms.LinearRightNormalizedType; @@ -32,4 +31,9 @@ super(MetaRDLTerm.TermType.META_EVALUATABLE_TERM_VARIABLE, variableName, OrderConstraint.EQ, order, linearRIghtNormalizedType); } + @Override + public MetaEvaluatableTermVariable cloneWithName(String name) { + return new MetaEvaluatableTermVariable(new Variable(name), constraint, orderExpression); + } + } diff --git a/src/main/java/models/terms/meta/MetaRDLTerm.java b/src/main/java/models/terms/meta/MetaRDLTerm.java index 764fdb8..02d7a3d 100644 --- a/src/main/java/models/terms/meta/MetaRDLTerm.java +++ b/src/main/java/models/terms/meta/MetaRDLTerm.java @@ -1,6 +1,5 @@ package models.terms.meta; -import java.util.Collection; import java.util.HashMap; import java.util.HashSet; import java.util.Map; @@ -82,8 +81,8 @@ this.linearRightNormalizedType = next; } - public Collection getAllVariables() { - return getSubTerms(MetaVariable.class).values(); + public Set getAllVariables() { + return new HashSet<>(getSubTerms(MetaVariable.class).values()); } protected boolean islinearRightNormalizedMatchedBy(RDLTerm another) { @@ -113,6 +112,8 @@ return -1; } + public abstract MetaRDLTerm replace(Map mapping); + @Override public String toStringWithOrder() { switch(termType) { @@ -139,7 +140,7 @@ @Override public int hashCode() { - return (termType.toString() + toStringWithOrder()).hashCode(); + return (termType.toString() + toString()).hashCode(); } @Override diff --git a/src/main/java/models/terms/meta/MetaRDLTermVariable.java b/src/main/java/models/terms/meta/MetaRDLTermVariable.java index 75bdeea..0148aef 100644 --- a/src/main/java/models/terms/meta/MetaRDLTermVariable.java +++ b/src/main/java/models/terms/meta/MetaRDLTermVariable.java @@ -2,7 +2,6 @@ import models.algebra.Constant; import models.algebra.Expression; -import models.algebra.Symbol; import models.algebra.Variable; public class MetaRDLTermVariable extends MetaVariable { @@ -19,4 +18,9 @@ super(MetaRDLTerm.TermType.META_RDL_TERM, variableName, OrderConstraint.EQ, order); } + @Override + public MetaRDLTermVariable cloneWithName(String name) { + return new MetaRDLTermVariable(new Variable(name), constraint, orderExpression); + } + } diff --git a/src/main/java/models/terms/meta/MetaResource.java b/src/main/java/models/terms/meta/MetaResource.java index fbdc3c3..8b59887 100644 --- a/src/main/java/models/terms/meta/MetaResource.java +++ b/src/main/java/models/terms/meta/MetaResource.java @@ -7,7 +7,6 @@ import lombok.Getter; import models.algebra.Constant; import models.algebra.Expression; -import models.algebra.Symbol; import models.algebra.Variable; import models.terms.RDLTerm; import models.terms.Resource; @@ -54,4 +53,10 @@ } return result; } + + @Override + public MetaResource cloneWithName(String name) { + return new MetaResource(new Variable(name), constraint, orderExpression); + } + } diff --git a/src/main/java/models/terms/meta/MetaTermPairGenerator.java b/src/main/java/models/terms/meta/MetaTermPairGenerator.java deleted file mode 100644 index d8837eb..0000000 --- a/src/main/java/models/terms/meta/MetaTermPairGenerator.java +++ /dev/null @@ -1,10 +0,0 @@ -package models.terms.meta; - -@FunctionalInterface -public interface MetaTermPairGenerator { - - record TermPair(MetaRDLTerm dependedTerm, MetaRDLTerm argTerm) {}; - - TermPair generate(int index, int depth, boolean isLast); - -} diff --git a/src/main/java/models/terms/meta/MetaVariable.java b/src/main/java/models/terms/meta/MetaVariable.java index bef0d8c..8c8f717 100644 --- a/src/main/java/models/terms/meta/MetaVariable.java +++ b/src/main/java/models/terms/meta/MetaVariable.java @@ -135,7 +135,15 @@ return false; } + public abstract MetaVariable cloneWithName(String name); + @Override + public MetaRDLTerm replace(Map mapping) { + if (mapping.containsKey(this)) { + return mapping.get(this).replace(mapping); + } + return this; + } @Override diff --git a/src/test/java/terms/meta/MetaDependencyTermTest.java b/src/test/java/terms/meta/MetaDependencyTermTest.java index 273f1f8..16e9a7e 100644 --- a/src/test/java/terms/meta/MetaDependencyTermTest.java +++ b/src/test/java/terms/meta/MetaDependencyTermTest.java @@ -16,7 +16,6 @@ import models.terms.meta.MetaRDLTerm; import models.terms.meta.MetaResource; import models.terms.meta.OrderVariableConstraint; -import utils.Utils; public class MetaDependencyTermTest { @@ -103,4 +102,25 @@ assertTrue(! tmp.isEmpty()); } + @Test + void MetaDependencyTermReplaceTest() { + MetaResource x = new MetaResource(new Variable("x")); + MetaResource y = new MetaResource(new Variable("y")); + MetaResource z = new MetaResource(new Variable("z")); + MetaResource w = new MetaResource(new Variable("w")); + MetaResource p = new MetaResource(new Variable("p")); + MetaResource q = new MetaResource(new Variable("q")); + MetaResource r = new MetaResource(new Variable("r")); + MetaResource s = new MetaResource(new Variable("s")); + + MetaDependencyTerm t1 = new MetaDependencyTerm(x, y, z); + MetaDependencyTerm t2 = new MetaDependencyTerm(p, q, r); + assertEquals(t1.replace(Map.of(x, p, y, q, z, r)), t2); + + MetaDependencyTerm t3 = new MetaDependencyTerm(t1, w, z); + MetaDependencyTerm t4 = new MetaDependencyTerm(t2, s, r); + assertEquals(t3.replace(Map.of(x, p, y, q, z, r, w, s)), t4); + } + + } diff --git a/src/test/java/terms/meta/MetaDependencyTest.java b/src/test/java/terms/meta/MetaDependencyTest.java index 28c1523..5ddf185 100644 --- a/src/test/java/terms/meta/MetaDependencyTest.java +++ b/src/test/java/terms/meta/MetaDependencyTest.java @@ -22,7 +22,6 @@ import models.terms.meta.MetaRDLTerm; import models.terms.meta.MetaResource; import models.terms.meta.OrderVariableConstraint; -import utils.Utils; public class MetaDependencyTest { @@ -152,4 +151,24 @@ assertTrue(! vd3.isMatchedBy(d4).isEmpty()); } + @Test + void MetaDependencyReplaceTest() { + MetaResource x = new MetaResource(new Variable("x")); + MetaResource y = new MetaResource(new Variable("y")); + MetaResource z = new MetaResource(new Variable("z")); + MetaResource w = new MetaResource(new Variable("w")); + + MetaDependency md1 = new MetaDependency(x, y); + MetaDependency md2 = new MetaDependency(z, y); + assertEquals(md1.replace(Map.of(x, z)), md2); + + MetaDependency md3 = new MetaDependency(md1, y); + MetaDependency md4 = new MetaDependency(new MetaDependency(w, z), z); + assertEquals(md3.replace(Map.of(x, w, y, z)), md4); + + MetaDependency md5 = new MetaDependency(x, y, z); + MetaDependency md6 = new MetaDependency(x, y, w); + assertEquals(md5.replace(Map.of(z, w)), md6); + } + } diff --git a/src/test/java/terms/meta/MetaResourceVariableTest.java b/src/test/java/terms/meta/MetaResourceVariableTest.java index eed180b..30c3bf7 100644 --- a/src/test/java/terms/meta/MetaResourceVariableTest.java +++ b/src/test/java/terms/meta/MetaResourceVariableTest.java @@ -5,6 +5,8 @@ import org.junit.jupiter.api.Test; +import java.util.Map; + import models.algebra.Variable; import models.terms.Dependency; import models.terms.DependencyTerm; @@ -159,4 +161,11 @@ assertTrue(! x.isMatchedBy(a).isEmpty()); } + @Test + void MetaResourceReplaceTest() { + MetaResource x = new MetaResource(new Variable("x")); + MetaResource y = new MetaResource(new Variable("y")); + assertEquals(x.replace(Map.of(x, y)), y); + } + }