diff --git a/src/main/java/inference/AssumptionGenerator.java b/src/main/java/inference/AssumptionGenerator.java new file mode 100644 index 0000000..f6d313e --- /dev/null +++ b/src/main/java/inference/AssumptionGenerator.java @@ -0,0 +1,12 @@ +package inference; + +import java.util.Map; + +import models.formulas.meta.MetaFormula; + +@FunctionalInterface +public interface AssumptionGenerator { + + MetaFormula generate(int i, Map context); + +} diff --git a/src/main/java/inference/InferenceRule.java b/src/main/java/inference/InferenceRule.java index 4673023..4ad3266 100644 --- a/src/main/java/inference/InferenceRule.java +++ b/src/main/java/inference/InferenceRule.java @@ -29,32 +29,38 @@ private final MetaFormula conclusion; private final InferenceOrderConstraint defaultOrderConstraint; + private final boolean hasDynamicAssumption; + private final AssumptionGenerator generator; + + 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( List assumptions, MetaFormula conclusion, InferenceOrderConstraint constraint) { - this.name = "undefined"; + public InferenceRule(String name, List assumptions, AssumptionGenerator generator, MetaFormula conclusion, InferenceOrderConstraint constraint) { + this.name = name; this.assumptions = assumptions; this.conclusion = conclusion; this.defaultOrderConstraint = constraint; + this.hasDynamicAssumption = true; + this.generator = generator; + } + + public InferenceRule( List assumptions, MetaFormula conclusion, InferenceOrderConstraint constraint) { + this("undefined", assumptions, conclusion, constraint); } public InferenceRule(String name, List assumptions, MetaFormula conclusion) { - this.assumptions = assumptions; - this.conclusion = conclusion; - this.name = name; - this.defaultOrderConstraint = null; + this(name, assumptions, conclusion, null); } public InferenceRule(List assumptions, MetaFormula conclusion) { - this.assumptions = assumptions; - this.conclusion = conclusion; - this.name = "undefined"; - this.defaultOrderConstraint = null; + this("undefined", assumptions, conclusion, null); } public boolean check(Collection assumptions, Formula conclusion) { @@ -155,21 +161,31 @@ } private Formula apply(List assumptions) { - if (assumptions.size() != getAssumptionSize()) { - return null; - } - Set result = this.assumptions.get(0).isMatchedBy(assumptions.get(0)); - for (int i = 1; i < getAssumptionSize(); i++) { - result = this.assumptions.get(i).isMatchedBy(assumptions.get(i), result); - if (result.isEmpty()) { - return null; - } - } - return conclusion.substitution(result.iterator().next().getBinding()); +// if (assumptions.size() < getAssumptionSize()) { +// return null; +// } +// Set result = this.assumptions.get(0).isMatchedBy(assumptions.get(0)); +// for (int i = 1; i < getAssumptionSize(); i++) { +// result = this.assumptions.get(i).isMatchedBy(assumptions.get(i), result); +// if (result.isEmpty()) { +// return null; +// } +// } +// if (hasDynamicAssumption) { +// for (int i = 0; i < assumptions.size(); i++) { +// int j = 1 + getAssumptionSize() + i; +// result = this.generator.generate(i, null).isMatchedBy(assumptions.get(j), result); +// if (result.isEmpty()) { +// return null; +// } +// } +// } +// return conclusion.substitution(result.iterator().next().getBinding()); + return apply(assumptions, MatchConstraint.createDefault()); } private Formula apply(List assumptions, MatchConstraint constraint) { - if (assumptions.size() != getAssumptionSize()) { + if (assumptions.size() < getAssumptionSize()) { return null; } @@ -181,6 +197,15 @@ return null; } } + if (hasDynamicAssumption) { + for (int i = 0; i < assumptions.size(); i++) { + int j = getAssumptionSize() + i; + result = this.generator.generate(i, new HashMap<>()).isMatchedBy(assumptions.get(j), result); + if (result.isEmpty()) { + return null; + } + } + } Formula subRes = conclusion.substitution(result.iterator().next().getBinding()); return subRes; } diff --git a/src/main/java/inference/ProofSystem.java b/src/main/java/inference/ProofSystem.java index 1d83544..67c2d30 100644 --- a/src/main/java/inference/ProofSystem.java +++ b/src/main/java/inference/ProofSystem.java @@ -20,10 +20,10 @@ import models.formulas.meta.MetaEquationFormula; import models.terms.EvaluatableTerm; import models.terms.RDLTerm; -import models.terms.meta.MetaDependencyGenerator; import models.terms.meta.MetaEvaluatableTermVariable; import models.terms.meta.MetaRDLTerm; import models.terms.meta.MetaResource; +import models.terms.meta.MetaTermGenerator; import models.terms.meta.OrderConstraint; import utils.Product; @@ -200,24 +200,27 @@ ) ); -// public static final InferenceRule constantness = new InferenceRule( -// "Constantness", -// List.of( -// new MetaInFormula( -// new MetaEvaluatableTermVariable(new Variable("t1")), -// new MetaRDLTerm(new MetaResource(new Variable("r1"), new Variable("m"))) -// ) -// ), -// new MetaEquationFormula( -// new MetaRDLTerm( -// new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")), -// new MetaResource(new Variable("r1"), new Variable("m")), -// new MetaEvaluatableTermVariable(new Variable("t1")) -// ), -// new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")) -// ), -// new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m")) -// ); + public static final InferenceRule constantness = new InferenceRule( + "Constantness", + List.of(), + (i, context) -> new MetaEquationFormula( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("r" + i), new Variable("m+" + i)), + new MetaEvaluatableTermVariable(new Variable("x" + i)), + new MetaEvaluatableTermVariable(new Variable("y" + i)) + ), + new MetaEvaluatableTermVariable(new Variable("t" + i)) + ), + new MetaEquationFormula( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")), + new MetaResource(new Variable("r1"), new Variable("m")), + new MetaEvaluatableTermVariable(new Variable("t1")) + ), + new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")) + ), + new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m")) + ); // // private static final InferenceRule rightNormalization = new InferenceRule( // "Right Normalization", @@ -300,9 +303,9 @@ List.of( new MetaDependencyFormula( new MetaEvaluatableTermVariable(new Variable("te")), - new MetaDependencyGenerator() { + new MetaTermGenerator() { @Override - public RDLTerm generate(int i) { + public MetaRDLTerm generate(int i, int depth, boolean isLast) { if (i == 0) { return new MetaResource(new Variable("r")); } else { @@ -317,9 +320,9 @@ ), new MetaDependencyFormula( new MetaEvaluatableTermVariable(new Variable("te")), - new MetaDependencyGenerator() { + new MetaTermGenerator() { @Override - public RDLTerm generate(int i) { + public MetaRDLTerm generate(int i, int depth, boolean isLast) { if (i == 0) { return new MetaResource(new Variable("q")); } else { diff --git a/src/main/java/models/formulas/meta/MetaDependencyFormula.java b/src/main/java/models/formulas/meta/MetaDependencyFormula.java index 871deee..10df361 100644 --- a/src/main/java/models/formulas/meta/MetaDependencyFormula.java +++ b/src/main/java/models/formulas/meta/MetaDependencyFormula.java @@ -13,7 +13,7 @@ import models.terms.Dependency; import models.terms.RDLTerm; import models.terms.meta.MatchConstraint; -import models.terms.meta.MetaDependencyGenerator; +import models.terms.meta.MetaTermGenerator; import models.terms.meta.MetaDependencyVariable; import models.terms.meta.MetaRDLTerm; @@ -41,7 +41,7 @@ this(dependingTerm, new HashSet<>(Arrays.asList(dependedTerms))); } - public MetaDependencyFormula(MetaRDLTerm dependingTerm, MetaDependencyGenerator generator) { + public MetaDependencyFormula(MetaRDLTerm dependingTerm, MetaTermGenerator generator) { this.dependency = new MetaRDLTerm(dependingTerm, generator); } diff --git a/src/main/java/models/terms/meta/MatchConstraint.java b/src/main/java/models/terms/meta/MatchConstraint.java index 05adc4b..68aa933 100644 --- a/src/main/java/models/terms/meta/MatchConstraint.java +++ b/src/main/java/models/terms/meta/MatchConstraint.java @@ -33,4 +33,8 @@ return res; } + public static MatchConstraint createDefault() { + return new MatchConstraint(new HashMap<>(), new HashMap<>()); + } + } diff --git a/src/main/java/models/terms/meta/MetaDependencyGenerator.java b/src/main/java/models/terms/meta/MetaDependencyGenerator.java deleted file mode 100644 index d90f8e0..0000000 --- a/src/main/java/models/terms/meta/MetaDependencyGenerator.java +++ /dev/null @@ -1,10 +0,0 @@ -package models.terms.meta; - -import models.terms.RDLTerm; - -@FunctionalInterface -public interface MetaDependencyGenerator { - - RDLTerm generate(int i); - -} diff --git a/src/main/java/models/terms/meta/MetaDependencyTermGenerator.java b/src/main/java/models/terms/meta/MetaDependencyTermGenerator.java deleted file mode 100644 index 07c1ef8..0000000 --- a/src/main/java/models/terms/meta/MetaDependencyTermGenerator.java +++ /dev/null @@ -1,12 +0,0 @@ -package models.terms.meta; - -import models.terms.RDLTerm; - -@FunctionalInterface -public interface MetaDependencyTermGenerator { - - record TermPair(RDLTerm dependedTerm, RDLTerm argTerm) {}; - - TermPair generate(int i); - -} diff --git a/src/main/java/models/terms/meta/MetaDynamicTerm.java b/src/main/java/models/terms/meta/MetaDynamicTerm.java new file mode 100644 index 0000000..bee1554 --- /dev/null +++ b/src/main/java/models/terms/meta/MetaDynamicTerm.java @@ -0,0 +1,202 @@ +package models.terms.meta; + +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; + +public class MetaDynamicTerm extends MetaRDLTerm { + + private MetaTermGenerator dependingTermGenerator; + private MetaTermGenerator dependedTermGenerator; + private MetaTermPairGenerator termPairGenerator; + + 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); + } + + 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)); + } + + @Override + public RDLTerm substitute(Map binding, int depth) { + switch (this.termType) { + case META_DEPENDENCY: + return dependencySubstitute(binding); + case META_DEPENDENCY_TERM: + break; + default: + break; + } + return null; + } + + private RDLTerm dependencySubstitute(Map binding) { + return dependencyGenerate(binding).substitute(binding); + } + + @Override + public Set isMatchedBy(RDLTerm another, MatchConstraint constraint, int depth) { + Set 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 dependencyMatch(Dependency another, MatchConstraint constraint, int depth) { + Set result = new HashSet<>(); + RDLTerm anotherDependingTerm = another.getDependingTerm(); + TreeSet anotherDependedTerms = another.getDependedTerms(); + boolean isLast = anotherDependingTerm instanceof Resource || anotherDependingTerm instanceof ResourceConstant; + MetaRDLTerm metaDependingTerm = dependingTermGenerator.generate(0, depth, isLast); + result = metaDependingTerm.isMatchedBy(anotherDependingTerm, constraint, depth + 1); + if (result.isEmpty()) { + return result; + } + int i = 0; + for (EvaluatableTerm anotherDependedTerm : anotherDependedTerms) { + isLast = anotherDependedTerm instanceof Resource || anotherDependedTerm instanceof ResourceConstant; + MetaRDLTerm metaDependedTerm = dependedTermGenerator.generate(i, depth, isLast); + result = metaDependedTerm.isMatchedBy(anotherDependedTerm, result, depth + 1); + if (result.isEmpty()) { + return result; + } + i++; + } + return result; + } + + private Set dependencyTermMatch(DependencyTerm another, MatchConstraint constraint, int depth) { + Set result = new HashSet<>(); + RDLTerm anotherDependingTerm = another.getDependingTerm(); + List anotherDependedTerms = another.getDependedTerms(); + List anotherArgumentTerms = another.getArgumentTerms(); + boolean isLast = anotherDependingTerm instanceof Resource || anotherDependingTerm instanceof ResourceConstant; + MetaRDLTerm metaDependingTerm = dependingTermGenerator.generate(0, depth, isLast); + result = metaDependingTerm.isMatchedBy(anotherDependingTerm, constraint, depth + 1); + if (result.isEmpty()) { + return result; + } + int i = 0; + for (EvaluatableTerm anotherDependedTerm : anotherDependedTerms) { + isLast = anotherDependedTerm instanceof Resource || anotherDependedTerm instanceof ResourceConstant; + TermPair termPair = termPairGenerator.generate(i, depth, isLast); + result = termPair.dependedTerm().isMatchedBy(anotherDependedTerm, result, depth + 1); + isLast = anotherDependedTerm instanceof Resource || anotherDependedTerm instanceof ResourceConstant; + result = termPair.argTerm().isMatchedBy(anotherDependedTerm, result, depth + 1); + if (result.isEmpty()) { + return result; + } + i++; + } + 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 binding, int maxRecursion, int depth) { + MetaRDLTerm dependingTerm = dependingTermGenerator.generate(0, depth, depth == maxRecursion - 1); + Set 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 int searchMaxTermIndex(Map binding, int depth, boolean isLast) { + 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 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; + } + + public MetaRDLTerm dependencyGenerate(Map binding) { + int ok = -1; + int ng = 100; + while (Math.abs(ok - ng) > 1) { + int mid = (ok + ng) / 2; + MetaRDLTerm generatedTerm = dependencyRecursionGenerate(mid, 0); + Set 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); + } +} diff --git a/src/main/java/models/terms/meta/MetaRDLTerm.java b/src/main/java/models/terms/meta/MetaRDLTerm.java index 1a244ae..4f72e6a 100644 --- a/src/main/java/models/terms/meta/MetaRDLTerm.java +++ b/src/main/java/models/terms/meta/MetaRDLTerm.java @@ -3,7 +3,6 @@ import java.util.ArrayList; import java.util.Arrays; import java.util.Collection; -import java.util.HashMap; import java.util.HashSet; import java.util.List; import java.util.Map; @@ -26,7 +25,7 @@ import models.terms.LinearRightNormalizedType; import models.terms.RDLTerm; import models.terms.Resource; -import models.terms.meta.MetaDependencyTermGenerator.TermPair; +import models.terms.meta.MetaTermPairGenerator.TermPair; import utils.Permutation; public class MetaRDLTerm extends RDLTerm { @@ -37,8 +36,8 @@ protected LinearRightNormalizedType linearRightNormalizedType = LinearRightNormalizedType.UNDEFINED; private boolean isDynamic = false; - private MetaDependencyTermGenerator metaDependencyTermGenerator; - private MetaDependencyGenerator metaDependencyGenerator; + private MetaTermPairGenerator metaDependencyTermGenerator; + private MetaTermGenerator metaDependencyGenerator; protected MetaRDLTerm(Symbol symbol, TermType termType, int size) { super(symbol, -1, size); @@ -59,14 +58,14 @@ } this.size = size; this.termType = TermType.META_DEPENDENCY; - this.metaDependencyGenerator = (i) -> (RDLTerm) this.getChild(i + 1); + this.metaDependencyGenerator = (index, depth, isLast) -> (MetaRDLTerm) this.getChild(index + 1); } public MetaRDLTerm(MetaRDLTerm dependingTerm, MetaRDLTerm dependedTerm) { this(dependingTerm, new TreeSet<>(Set.of(dependedTerm))); } - public MetaRDLTerm(MetaRDLTerm dependingTerm, MetaDependencyGenerator generator) { + public MetaRDLTerm(MetaRDLTerm dependingTerm, MetaTermGenerator generator) { super(new Symbol(":", 1), -1, -1); addChild(dependingTerm); this.metaDependencyGenerator = generator; @@ -106,14 +105,14 @@ addChild(argTerm); } this.termType = TermType.META_DEPENDENCY_TERM; - this.metaDependencyTermGenerator = (i) -> new TermPair((RDLTerm) this.getChild(i * 2 + 1), (RDLTerm) this.getChild(i * 2 + 2)); + this.metaDependencyTermGenerator = (index, depth, isLast) -> new TermPair((MetaRDLTerm) this.getChild(index * 2 + 1), (MetaRDLTerm) this.getChild(index * 2 + 2)); } public MetaRDLTerm(MetaRDLTerm dependingTerm, MetaRDLTerm ...terms) { this(dependingTerm, Arrays.asList(terms)); } - public MetaRDLTerm(MetaRDLTerm dependingTerm, MetaDependencyTermGenerator generator) { + public MetaRDLTerm(MetaRDLTerm dependingTerm, MetaTermPairGenerator generator) { super(new Symbol(":", 1), -1, -1); addChild(dependingTerm); this.metaDependencyTermGenerator = generator; @@ -122,18 +121,22 @@ } public RDLTerm substitute(Map binding) { + return substitute(binding, 0); + } + + protected RDLTerm substitute(Map binding, int depth) { RDLTerm dependingTerm = (RDLTerm) getChild(0); List dependedTerms = new ArrayList<>(); if (dependingTerm instanceof MetaRDLTerm) { - dependingTerm = ((MetaRDLTerm) dependingTerm).substitute(binding); + dependingTerm = ((MetaRDLTerm) dependingTerm).substitute(binding, depth + 1); } if (isDependency()) { for (int i = 0; i < binding.size(); i++) { if ((! isDynamic) && (i >= getChildren().size() - 1)) break; - RDLTerm term = metaDependencyGenerator.generate(i); + RDLTerm term = metaDependencyGenerator.generate(i, depth, i == getChildren().size() - 2); try { if (term instanceof MetaRDLTerm metaTerm) { - term = metaTerm.substitute(binding); + term = metaTerm.substitute(binding, depth + 1); } } catch(SubstituteFailedException e) { continue; @@ -152,15 +155,15 @@ List terms = new ArrayList<>(); for (int i = 0; i < binding.size(); i++) { if ((! isDynamic) && (i >= (getChildren().size() - 1) / 2)) break; - TermPair termPair = metaDependencyTermGenerator.generate(i); + TermPair termPair = metaDependencyTermGenerator.generate(i, depth, i == (getChildren().size() - 1) / 2 - 1); RDLTerm dependedTerm = termPair.dependedTerm(); RDLTerm argTerm = termPair.argTerm(); try { if (dependedTerm instanceof MetaRDLTerm metaTerm) { - dependedTerm = metaTerm.substitute(binding); + dependedTerm = metaTerm.substitute(binding, depth + 1); } if (argTerm instanceof MetaRDLTerm metaTerm) { - argTerm = metaTerm.substitute(binding); + argTerm = metaTerm.substitute(binding, depth + 1); } terms.add((EvaluatableTerm) dependedTerm); terms.add((EvaluatableTerm) argTerm); @@ -182,18 +185,30 @@ } public Set isMatchedBy(RDLTerm another) { - return isMatchedBy(another, new MatchConstraint(new HashMap<>(), new HashMap<>())); + return isMatchedBy(another, 0); + } + + protected Set isMatchedBy(RDLTerm another, int depth) { + return isMatchedBy(another, MatchConstraint.createDefault(), depth); } public Set isMatchedBy(RDLTerm another, Set constraints) { + return isMatchedBy(another, constraints, 0); + } + + protected Set isMatchedBy(RDLTerm another, Set constraints, int depth) { Set result = new HashSet<>(); for (MatchConstraint constraint : constraints) { - result.addAll(isMatchedBy(another, constraint)); + result.addAll(isMatchedBy(another, constraint, depth + 1)); } return result; } public Set isMatchedBy(RDLTerm another, MatchConstraint constraint) { + return isMatchedBy(another, constraint, 0); + } + + protected Set isMatchedBy(RDLTerm another, MatchConstraint constraint, int depth) { Set result = new HashSet<>(); if (! another.getClass().isAssignableFrom(this.termType.getBaseTermClass())) { return result; @@ -209,7 +224,7 @@ Set res = new HashSet<>(); if (dependingChild instanceof MetaRDLTerm) { MetaRDLTerm metaChild = (MetaRDLTerm) dependingChild; - res = metaChild.isMatchedBy(anotherDependingChild, constraint); + res = metaChild.isMatchedBy(anotherDependingChild, constraint, depth + 1); } else { if (!(dependingChild.equals(anotherDependingChild))) { return result; @@ -221,14 +236,14 @@ boolean flg = true; for (int i = 0; i < perm.size(); i++) { int j = perm.get(i); - TermPair termPair = this.metaDependencyTermGenerator.generate(j); + TermPair termPair = this.metaDependencyTermGenerator.generate(j, depth, false); RDLTerm dependedChild = termPair.dependedTerm(); RDLTerm argChild = termPair.argTerm(); RDLTerm anotherDependedChild = (RDLTerm) another.getChild(i * 2 + 1); RDLTerm anotherArgChild = (RDLTerm) another.getChild(i * 2 + 2); if (dependedChild instanceof MetaRDLTerm) { MetaRDLTerm metaChild = (MetaRDLTerm) dependedChild; - res2 = metaChild.isMatchedBy(anotherDependedChild, res2); + res2 = metaChild.isMatchedBy(anotherDependedChild, res2, depth + 1); if (res2.isEmpty()) { flg = false; break; @@ -241,7 +256,7 @@ } if (argChild instanceof MetaRDLTerm) { MetaRDLTerm metaChild = (MetaRDLTerm) argChild; - res2 = metaChild.isMatchedBy(anotherArgChild, res2); + res2 = metaChild.isMatchedBy(anotherArgChild, res2, depth + 1); if (res2.isEmpty()) { flg = false; break; @@ -264,11 +279,11 @@ boolean flg = true; for (int i = 0; i < perm.size(); i++) { int j = perm.get(i); - RDLTerm dependedChild = this.metaDependencyGenerator.generate(j); + RDLTerm dependedChild = this.metaDependencyGenerator.generate(j, depth, false); RDLTerm anotherDependedChild = (RDLTerm) another.getChild(i + 1); if (dependedChild instanceof MetaRDLTerm) { MetaRDLTerm metaChild = (MetaRDLTerm) dependedChild; - res2 = metaChild.isMatchedBy(anotherDependedChild, res2); + res2 = metaChild.isMatchedBy(anotherDependedChild, res2, depth + 1); if (res2.isEmpty()) { flg = false; break; diff --git a/src/main/java/models/terms/meta/MetaTermGenerator.java b/src/main/java/models/terms/meta/MetaTermGenerator.java new file mode 100644 index 0000000..36d7db5 --- /dev/null +++ b/src/main/java/models/terms/meta/MetaTermGenerator.java @@ -0,0 +1,8 @@ +package models.terms.meta; + +@FunctionalInterface +public interface MetaTermGenerator { + + MetaRDLTerm generate(int index, int depth, boolean isLast); + +} diff --git a/src/main/java/models/terms/meta/MetaTermPairGenerator.java b/src/main/java/models/terms/meta/MetaTermPairGenerator.java new file mode 100644 index 0000000..d8837eb --- /dev/null +++ b/src/main/java/models/terms/meta/MetaTermPairGenerator.java @@ -0,0 +1,10 @@ +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 7c8e0fc..4c3479c 100644 --- a/src/main/java/models/terms/meta/MetaVariable.java +++ b/src/main/java/models/terms/meta/MetaVariable.java @@ -76,7 +76,7 @@ } @Override - public Set isMatchedBy(RDLTerm another, MatchConstraint constraint) { + public Set isMatchedBy(RDLTerm another, MatchConstraint constraint, int depth) { Set result = new HashSet<>(); Map binding = constraint.getBinding(); Map orderConstraint = constraint.getOrderConstraint(); @@ -103,7 +103,7 @@ } @Override - public RDLTerm substitute(Map binding) { + public RDLTerm substitute(Map binding, int depth) { if (binding.containsKey(variableName)) { return binding.get(variableName); } diff --git a/src/test/java/terms/DependencyTermTest.java b/src/test/java/terms/DependencyTermTest.java index 8fedc28..f8ef97a 100644 --- a/src/test/java/terms/DependencyTermTest.java +++ b/src/test/java/terms/DependencyTermTest.java @@ -13,10 +13,10 @@ import models.terms.RDLTerm; import models.terms.Resource; import models.terms.meta.MatchConstraint; -import models.terms.meta.MetaDependencyTermGenerator; -import models.terms.meta.MetaDependencyTermGenerator.TermPair; import models.terms.meta.MetaRDLTerm; import models.terms.meta.MetaResource; +import models.terms.meta.MetaTermPairGenerator; +import models.terms.meta.MetaTermPairGenerator.TermPair; import models.terms.meta.OrderVariableConstraint; import utils.Utils; @@ -139,7 +139,7 @@ DependencyTerm t1 = new DependencyTerm(a1, a2, a3, a4, a5); MetaResource x = new MetaResource(new Variable("x"), new Variable("n")); MetaRDLTerm mt1 = new MetaRDLTerm(x, - (MetaDependencyTermGenerator) (i) -> + (MetaTermPairGenerator) (i, depth, isLast) -> new TermPair( new MetaResource(new Variable("x" + (2*i + 1)), Utils.parse("n-1-" + i)), new MetaResource(new Variable("x" + (2*i + 2)), Utils.parse("n+1")) @@ -154,7 +154,7 @@ @Test void DynamicMatchTest2() { MetaResource x = new MetaResource(new Variable("x")); - MetaRDLTerm mt1 = new MetaRDLTerm(x, (MetaDependencyTermGenerator) (i) -> new TermPair(new MetaResource(new Variable("x" + i)), new MetaResource(new Variable("y"+i)))); + MetaRDLTerm mt1 = new MetaRDLTerm(x, (MetaTermPairGenerator) (i, depth, isLast) -> new TermPair(new MetaResource(new Variable("x" + i)), new MetaResource(new Variable("y"+i)))); DependencyTerm d1 = new DependencyTerm(a, b, c); DependencyTerm d2 = new DependencyTerm(a, b, c, d, e); assertTrue(! mt1.isMatchedBy(d1).isEmpty()); diff --git a/src/test/java/terms/DependencyTest.java b/src/test/java/terms/DependencyTest.java index 13c885b..360ef2d 100644 --- a/src/test/java/terms/DependencyTest.java +++ b/src/test/java/terms/DependencyTest.java @@ -14,9 +14,9 @@ import models.terms.RDLTerm; import models.terms.Resource; import models.terms.meta.MatchConstraint; -import models.terms.meta.MetaDependencyGenerator; import models.terms.meta.MetaRDLTerm; import models.terms.meta.MetaResource; +import models.terms.meta.MetaTermGenerator; import models.terms.meta.OrderVariableConstraint; import utils.Utils; @@ -122,11 +122,11 @@ @Test void DynamicMatchTest() { MetaResource x = new MetaResource(new Variable("x")); - MetaRDLTerm md1 = new MetaRDLTerm(x, new MetaDependencyGenerator() { + MetaRDLTerm md1 = new MetaRDLTerm(x, new MetaTermGenerator() { @Override - public RDLTerm generate(int i) { - if (i != 0) { - return new MetaResource(new Variable("r" + i)); + public MetaRDLTerm generate(int index, int depth, boolean isLast) { + if (index != 0) { + return new MetaResource(new Variable("r" + index)); } else { return new MetaResource(new Variable("y")); } diff --git a/src/test/java/terms/meta/MetaDynamicTermTest.java b/src/test/java/terms/meta/MetaDynamicTermTest.java new file mode 100644 index 0000000..fc1a8c0 --- /dev/null +++ b/src/test/java/terms/meta/MetaDynamicTermTest.java @@ -0,0 +1,93 @@ +package terms.meta; +import static org.junit.jupiter.api.Assertions.*; + +import org.junit.jupiter.api.Test; + +import models.algebra.Variable; +import models.terms.Dependency; +import models.terms.Resource; +import models.terms.meta.MatchConstraint; +import models.terms.meta.MetaDynamicTerm; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaResource; +import models.terms.meta.MetaTermGenerator; +import utils.Utils; + +public class MetaDynamicTermTest { + + Resource a = new Resource("a", Utils.INT, 1); + Resource b = new Resource("b", Utils.INT, 1); + Resource c = new Resource("c", Utils.INT, 1); + Resource d = new Resource("d", Utils.INT, 1); + + @Test + void GenerateTest1() { + MetaDynamicTerm mt1 = new MetaDynamicTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int index, int depth, boolean isLast) { + if (isLast) { + return new MetaResource(new Variable("x")); + } + return new MetaDynamicTerm(this, new MetaResource(new Variable("y" + depth))); + } + }, + new MetaResource(new Variable("y")) + ); + Dependency d1 = new Dependency(a, b); + Dependency d2 = new Dependency(d1, c); + Dependency d3 = new Dependency(d2, d); + assertTrue(! mt1.isMatchedBy(d1).isEmpty()); + assertTrue(! mt1.isMatchedBy(d2).isEmpty()); + assertTrue(! mt1.isMatchedBy(d3).isEmpty()); + + MatchConstraint result = mt1.isMatchedBy(d3).iterator().next(); + MetaRDLTerm mt2 = mt1.dependencyGenerate(result.getBinding()); + assertTrue(mt2.isMatchedBy(d3, result).contains(result)); + + assertEquals(mt1.substitute(result.getBinding()), d3); + } + + @Test + void GenerateTest2() { + MetaDynamicTerm mt1 = new MetaDynamicTerm( + new MetaResource(new Variable("x")), + (MetaTermGenerator) (i, d, l) -> new MetaResource(new Variable("y" + i)) + ); + Dependency d1 = new Dependency(a, b); + Dependency d2 = new Dependency(a, b, c); + Dependency d3 = new Dependency(a, b, c, d); + + assertTrue(! mt1.isMatchedBy(d1).isEmpty()); + assertTrue(! mt1.isMatchedBy(d2).isEmpty()); + assertTrue(! mt1.isMatchedBy(d3).isEmpty()); + } + + @Test + void GenerateTest3() { + MetaDynamicTerm mt1 = new MetaDynamicTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int index, int depth, boolean isLast) { + if (isLast) { + return new MetaResource(new Variable("x")); + } + return new MetaDynamicTerm(this, (MetaTermGenerator) (i, d, l) -> new MetaResource(new Variable("y" + (d+1) + "," + i))); + } + }, + (MetaTermGenerator) (i, d, l) -> new MetaResource(new Variable("y0," + i)) + ); + Dependency d1 = new Dependency(a, b, c, d); + Dependency d2 = new Dependency(d1, c, d); + assertTrue(! mt1.isMatchedBy(d1).isEmpty()); + assertTrue(! mt1.isMatchedBy(d2).isEmpty()); + + MatchConstraint result = mt1.isMatchedBy(d2).iterator().next(); + MetaRDLTerm mt2 = mt1.dependencyGenerate(result.getBinding()); + assertTrue(mt2.isMatchedBy(d2, result).contains(result)); + + assertEquals(mt1.substitute(result.getBinding()), d2); + } + + +}