diff --git a/src/main/java/inference/AssumptionGenerator.java b/src/main/java/inference/AssumptionGenerator.java index f6d313e..37148ff 100644 --- a/src/main/java/inference/AssumptionGenerator.java +++ b/src/main/java/inference/AssumptionGenerator.java @@ -1,12 +1,10 @@ package inference; -import java.util.Map; - import models.formulas.meta.MetaFormula; @FunctionalInterface public interface AssumptionGenerator { - MetaFormula generate(int i, Map context); + MetaFormula generate(int i); } diff --git a/src/main/java/inference/InferenceRule.java b/src/main/java/inference/InferenceRule.java index 4ad3266..5c86b88 100644 --- a/src/main/java/inference/InferenceRule.java +++ b/src/main/java/inference/InferenceRule.java @@ -200,7 +200,7 @@ 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); + result = this.generator.generate(i).isMatchedBy(assumptions.get(j), result); if (result.isEmpty()) { return null; } diff --git a/src/main/java/inference/ProofSystem.java b/src/main/java/inference/ProofSystem.java index 67c2d30..9283825 100644 --- a/src/main/java/inference/ProofSystem.java +++ b/src/main/java/inference/ProofSystem.java @@ -12,6 +12,7 @@ import java.util.Set; import java.util.stream.Collectors; +import models.algebra.Constant; import models.algebra.Variable; import models.formulas.DependencyFormula; import models.formulas.EquationFormula; @@ -25,6 +26,7 @@ import models.terms.meta.MetaResource; import models.terms.meta.MetaTermGenerator; import models.terms.meta.OrderConstraint; +import utils.ExpressionUitls; import utils.Product; public class ProofSystem { @@ -200,87 +202,147 @@ ) ); - 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)) + //todo +// public static final InferenceRule constantness = new InferenceRule( +// "Constantness", +// List.of(), +// (i) -> new MetaEquationFormula( +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("r" + (i + 1)), new Variable("m+" + i)), +// new MetaEvaluatableTermVariable(new Variable("x" + (i + 1))), +// new MetaEvaluatableTermVariable(new Variable("y" + (i + 1))) +// ), +// new MetaEvaluatableTermVariable(new Variable("t" + (i + 1))) +// ), +// new MetaEquationFormula( +// new MetaDynamicTerm( +// new MetaTermGenerator() { +// @Override +// public MetaRDLTerm generate(int index, int depth, boolean isLast) { +// if (isLast) { +// return new MetaResource(new Variable("se"), new Variable("n")); +// } +// return new MetaDynamicTerm(this, new MetaResource(new Variable("r" + (depth + 1)), new Variable("n+" + depth)), new MetaResource(new Variable("t" + (depth + 1)))); +// } +// +// }, +// new MetaResource(new Variable("r1")), +// new MetaResource(new Variable("t1")) +// ), +// new MetaResource(new Variable("se"), new Variable("n")) +// ), +// new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m")) +// ); +// + public static final InferenceRule rightNormalization = new InferenceRule( + "Right Normalization", + List.of( + new MetaDependencyFormula( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("re"), new Variable("n")) + ) ), - new MetaEvaluatableTermVariable(new Variable("t" + i)) + new MetaDependencyFormula( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaEvaluatableTermVariable(new Variable("qe"), new Variable("n")) + ) + ) + ), + new MetaEquationFormula( + new MetaRDLTerm( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("re"), new Variable("n")), + new MetaEvaluatableTermVariable(new Variable("te")) + ), + new MetaEvaluatableTermVariable(new Variable("qe"), new Variable("n")), + new MetaEvaluatableTermVariable(new Variable("ue")) + ), + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("re"), new Variable("n")), + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaEvaluatableTermVariable(new Variable("qe"), new Variable("n")), + new MetaEvaluatableTermVariable(new Variable("ue")) + ) + ) + ), + new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0")) + ); + + public static final InferenceRule pseudoConstantness = new InferenceRule( + "Pseudo-Constantness", + List.of( + new MetaDependencyFormula( + new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")), + new MetaEvaluatableTermVariable(new Variable("re"), new Variable("n")) + ) ), 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("re"), new Variable("n")), + new MetaEvaluatableTermVariable(new Variable("re"), new Variable("n")) ), new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")) ), - new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m")) + new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0")) ); -// -// private static final InferenceRule rightNormalization = new InferenceRule( -// "Right Normalization", -// List.of( -// new MetaDependencyFormula( -// new MetaRDLTerm( -// new MetaEvaluatableTermVariable(new Variable("te")), -// new MetaResource(new Variable("r"), new Variable("n")) -// ) -// ), -// new MetaDependencyFormula( -// new MetaRDLTerm( -// new MetaEvaluatableTermVariable(new Variable("se")), -// new MetaResource(new Variable("q"), new Variable("n")) -// ) -// ) -// ), -// new MetaEquationFormula( -// new MetaRDLTerm( -// new MetaRDLTerm( -// new MetaEvaluatableTermVariable(new Variable("te")), -// new MetaResource(new Variable("r"), new Variable("n")), -// new MetaEvaluatableTermVariable(new Variable("se")) -// ), -// new MetaResource(new Variable("q"), new Variable("n")), -// new MetaEvaluatableTermVariable(new Variable("ue")) -// ), -// new MetaRDLTerm( -// new MetaEvaluatableTermVariable(new Variable("te")), -// new MetaResource(new Variable("r"), new Variable("n")), -// new MetaRDLTerm( -// new MetaEvaluatableTermVariable(new Variable("se")), -// new MetaResource(new Variable("q"), new Variable("n")), -// new MetaEvaluatableTermVariable(new Variable("ue")) -// ) -// ) -// ), -// new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0")) -// ); -// -// private static final InferenceRule pseudoConstantness = new InferenceRule( -// "Pseudo-Constantness", -// List.of( -// new MetaDependencyFormula( -// new MetaRDLTerm( -// new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), -// new MetaResource(new Variable("r"), new Variable("n")) -// ) -// ) -// ), -// new MetaEquationFormula( -// new MetaRDLTerm( -// new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), -// new MetaResource(new Variable("r"), new Variable("n")), -// new MetaResource(new Variable("r"), new Variable("n")) -// ), -// new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")) -// ), -// new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0")) -// ); + + public static final InferenceRule uncurrying = new InferenceRule( + "Uncurrying", + List.of( + new MetaDependencyFormula( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")), + new MetaEvaluatableTermVariable(new Variable("re"), new Variable("n")) + ), + new MetaEvaluatableTermVariable(new Variable("pe"), ExpressionUitls.parse("n-1")) + ), + new MetaEquationFormula( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("pe"), ExpressionUitls.parse("n-1")), + new MetaEvaluatableTermVariable(new Variable("x")), + new MetaEvaluatableTermVariable(new Variable("y")) + ), + new MetaEvaluatableTermVariable(new Variable("te")) + ), + new MetaEquationFormula( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("qe"), ExpressionUitls.parse("n-1")), + new MetaEvaluatableTermVariable(new Variable("x2")), + new MetaEvaluatableTermVariable(new Variable("y2")) + ), + new MetaEvaluatableTermVariable(new Variable("ue")) + ) + ), + new MetaEquationFormula( + new MetaRDLTerm( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")), + new MetaEvaluatableTermVariable(new Variable("re"), new Variable("n")), + new MetaEvaluatableTermVariable(new Variable("ue")) + ), + new MetaEvaluatableTermVariable(new Variable("pe"), ExpressionUitls.parse("n-1")), + new MetaEvaluatableTermVariable(new Variable("te")) + ), + new MetaRDLTerm( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")), + new MetaEvaluatableTermVariable(new Variable("re"), new Variable("n")), + new MetaEvaluatableTermVariable(new Variable("qe"), ExpressionUitls.parse("n-1")) + ), + new MetaEvaluatableTermVariable(new Variable("pe"), ExpressionUitls.parse("n-1")), + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaEvaluatableTermVariable(new Variable("qe"), ExpressionUitls.parse("n-1")), + new MetaEvaluatableTermVariable(new Variable("ue")) + ) + ) + ); + // // //======================Dependency Axioms============================= // @@ -366,6 +428,28 @@ new MetaResource(new Variable("p")) ) ); + + public static final InferenceRule uncurriedMapping = new InferenceRule( + "Uncurried Mapping", + List.of( + new MetaDependencyFormula( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("re")) + ), + new MetaEvaluatableTermVariable(new Variable("pe"), ExpressionUitls.parse("n-1")) + ) + ), + new MetaDependencyFormula( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("re")), + new MetaEvaluatableTermVariable(new Variable("te"), ExpressionUitls.parse("n-1")) + ), + new MetaEvaluatableTermVariable(new Variable("pe"), ExpressionUitls.parse("n-1")), + new MetaEvaluatableTermVariable(new Variable("te"), ExpressionUitls.parse("n-1")) + ) + ); private static final List axioms = List.of( diff --git a/src/main/java/models/terms/meta/MetaDynamicTerm.java b/src/main/java/models/terms/meta/MetaDynamicTerm.java index bee1554..6e1e54c 100644 --- a/src/main/java/models/terms/meta/MetaDynamicTerm.java +++ b/src/main/java/models/terms/meta/MetaDynamicTerm.java @@ -1,5 +1,6 @@ package models.terms.meta; +import java.util.ArrayList; import java.util.HashSet; import java.util.List; import java.util.Map; @@ -21,6 +22,7 @@ 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); @@ -34,6 +36,7 @@ public MetaDynamicTerm(MetaTermGenerator dependingTermGenerator, MetaRDLTerm dependedTerm) { this(dependingTermGenerator, (MetaTermGenerator) (index, depht, isLast) -> dependedTerm); + isStaticSize = true; } public MetaDynamicTerm(MetaTermGenerator dependingTermGenerator, MetaTermPairGenerator termPairGenerator) { @@ -48,25 +51,22 @@ 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 binding, int depth) { switch (this.termType) { case META_DEPENDENCY: - return dependencySubstitute(binding); + return dependencyGenerate(binding).substitute(binding); case META_DEPENDENCY_TERM: - break; + return dependencyTermGenerate(binding).substitute(binding); 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<>(); @@ -124,7 +124,7 @@ 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); + result = termPair.argTerm().isMatchedBy(anotherArgumentTerms.get(i), result, depth + 1); if (result.isEmpty()) { return result; } @@ -166,7 +166,54 @@ 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 binding, int maxRecursion, int depth) { + MetaRDLTerm dependingTerm = dependingTermGenerator.generate(0, depth, depth == maxRecursion - 1); + List termPairs = new ArrayList<>(); + TermPair termPair = termPairGenerator.generate(0, depth, depth == maxRecursion - 1); + termPairs.add(termPair.dependedTerm()); + termPairs.add(termPair.argTerm()); + for (int i = 0; i < searchMaxTermPairIndex(binding, depth, depth == maxRecursion - 1); i++) { + TermPair pair = termPairGenerator.generate(0, depth, depth == maxRecursion - 1); + termPairs.add(pair.dependedTerm()); + termPairs.add(pair.argTerm()); + } + if (depth == maxRecursion - 1) { + return new MetaRDLTerm(dependingTerm, termPairs); + } + List 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 binding, int depth, boolean isLast) { + if (isStaticSize) return 0; int ok = -1; int ng = 100; while (Math.abs(ok - ng) > 1) { @@ -183,6 +230,24 @@ return ok; } + private int searchMaxTermPairIndex(Map 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 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 binding) { int ok = -1; int ng = 100; @@ -199,4 +264,22 @@ } return dependencyRecursionGenerate(binding, ok, 0); } + + public MetaRDLTerm dependencyTermGenerate(Map binding) { + int ok = -1; + int ng = 100; + while (Math.abs(ok - ng) > 1) { + int mid = (ok + ng) / 2; + MetaRDLTerm generatedTerm = dependencyTermRecursionGenerate(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 dependencyTermRecursionGenerate(binding, ok, 0); + } + } diff --git a/src/main/java/utils/ExpressionUitls.java b/src/main/java/utils/ExpressionUitls.java index 7981932..c6313a4 100644 --- a/src/main/java/utils/ExpressionUitls.java +++ b/src/main/java/utils/ExpressionUitls.java @@ -9,6 +9,13 @@ import models.algebra.Term; import models.algebra.Variable; import models.dataConstraintModel.DataConstraintModel; +import models.dataFlowModel.DataTransferModel; +import parser.Parser; +import parser.Parser.TokenStream; +import parser.exceptions.ExpectedColon; +import parser.exceptions.ExpectedDoubleQuotation; +import parser.exceptions.ExpectedRightBracket; +import parser.exceptions.WrongJsonExpression; public class ExpressionUitls { @@ -68,4 +75,18 @@ return Integer.parseInt((String) constant.getValue()); } + private static TokenStream stream = new Parser.TokenStream(); + private static Parser parser = new Parser(stream); + private static DataTransferModel model = new DataTransferModel(); + + public static Expression parse(String expr) { + stream.addLine(expr); + try { + return parser.parseTerm(stream, model); + } catch (ExpectedRightBracket | WrongJsonExpression | ExpectedColon | ExpectedDoubleQuotation e) { + e.printStackTrace(); + return null; + } + } + } diff --git a/src/test/java/inferencerule/DependencyAxiomTest.java b/src/test/java/inferencerule/DependencyAxiomTest.java index 834cfe0..e693aa8 100644 --- a/src/test/java/inferencerule/DependencyAxiomTest.java +++ b/src/test/java/inferencerule/DependencyAxiomTest.java @@ -10,6 +10,7 @@ import models.formulas.DependencyFormula; import models.formulas.EquationFormula; import models.formulas.Formula; +import models.terms.Dependency; import models.terms.DependencyTerm; import models.terms.Resource; import utils.Utils; @@ -21,6 +22,9 @@ Resource c = new Resource("c", Utils.INT, 1); Resource d = new Resource("d", Utils.INT, 1); Resource e = new Resource("e", Utils.INT, 1); + Resource f = new Resource("f", Utils.INT, 2); + Resource g = new Resource("g", Utils.INT, 2); + Resource h = new Resource("h", Utils.INT, 2); @Test void IdentityMappingTest() { @@ -65,4 +69,16 @@ assertFalse(result.contains(d3)); } + @Test + void UncurriedMappingTest() { + Dependency d1 = new Dependency(f, g); + Dependency d2 = new Dependency(d1, a); + DependencyTerm t1 = new DependencyTerm(f, g, b); + Dependency d3 = new Dependency(t1, a, b); + DependencyFormula df1 = new DependencyFormula(d2); + DependencyFormula df2 = new DependencyFormula(d3); + Set results = ProofSystem.uncurriedMapping.apply(List.of(df1), Set.of(b)); + assertTrue(results.contains(df2)); + } + } diff --git a/src/test/java/inferencerule/EqualityAxiomTest.java b/src/test/java/inferencerule/EqualityAxiomTest.java index 3d382bc..0617ca7 100644 --- a/src/test/java/inferencerule/EqualityAxiomTest.java +++ b/src/test/java/inferencerule/EqualityAxiomTest.java @@ -10,6 +10,7 @@ import models.formulas.DependencyFormula; import models.formulas.EquationFormula; import models.formulas.Formula; +import models.terms.Dependency; import models.terms.DependencyTerm; import models.terms.Resource; import utils.Utils; @@ -23,6 +24,11 @@ Resource e = new Resource("e", Utils.INT, 1); Resource f = new Resource("f", Utils.INT, 1); Resource g = new Resource("g", Utils.INT, 1); + Resource h = new Resource("h", Utils.INT, 2); + Resource i = new Resource("i", Utils.INT, 2); + Resource j = new Resource("j", Utils.INT, 2); + Resource k = new Resource("k", Utils.INT, 2); + Resource l = new Resource("l", Utils.INT, 1); @Test void ReflexivityTest() { @@ -104,4 +110,53 @@ assertEquals(f2, result); } + @Test + void RightNormalizationTest() { + Dependency d1 = new Dependency(a, b); + Dependency d2 = new Dependency(c, d); + DependencyTerm t1 = new DependencyTerm(a, b, c); + DependencyTerm t2 = new DependencyTerm(t1, d, e); + DependencyTerm t3 = new DependencyTerm(c, d, e); + DependencyTerm t4 = new DependencyTerm(a, b, t3); + + DependencyFormula df1 = new DependencyFormula(d1); + DependencyFormula df2 = new DependencyFormula(d2); + EquationFormula eq1 = new EquationFormula(t2, t4); + Set result = ProofSystem.rightNormalization.apply(List.of(df1, df2), Set.of(e)); + assertTrue(result.contains(eq1)); + + } + + @Test + void PseudoConstantnessTest() { + Dependency d1 = new Dependency(a, b); + DependencyTerm t1 = new DependencyTerm(a, b, b); + DependencyFormula df1 = new DependencyFormula(d1); + EquationFormula eq1 = new EquationFormula(t1, a); + Formula result = ProofSystem.pseudoConstantness.apply(List.of(df1)); + assertEquals(eq1, result); + } + + @Test + void UncurryingTest() { + Dependency d1 = new Dependency(h, i); + Dependency d2 = new Dependency(d1, a); + DependencyTerm t1 = new DependencyTerm(a, b, c); + DependencyTerm t2 = new DependencyTerm(d, e, f); + DependencyFormula df1 = new DependencyFormula(d2); + EquationFormula eq1 = new EquationFormula(t1, f); + EquationFormula eq2 = new EquationFormula(t2, l); + + DependencyTerm t3 = new DependencyTerm(h, i, l); + DependencyTerm t4 = new DependencyTerm(t3, a, f); + DependencyTerm t5 = new DependencyTerm(h, i, d); + DependencyTerm t6 = new DependencyTerm(t5, a, f, d, l); + EquationFormula eq3 = new EquationFormula(t4, t6); + + + Formula result = ProofSystem.uncurrying.apply(List.of(df1, eq1, eq2)); + assertEquals(result, eq3); + + } + } diff --git a/src/test/java/terms/meta/MetaDynamicTermTest.java b/src/test/java/terms/meta/MetaDynamicTermTest.java index fc1a8c0..ff9ef31 100644 --- a/src/test/java/terms/meta/MetaDynamicTermTest.java +++ b/src/test/java/terms/meta/MetaDynamicTermTest.java @@ -3,8 +3,10 @@ import org.junit.jupiter.api.Test; +import models.algebra.Constant; import models.algebra.Variable; import models.terms.Dependency; +import models.terms.DependencyTerm; import models.terms.Resource; import models.terms.meta.MatchConstraint; import models.terms.meta.MetaDynamicTerm; @@ -19,6 +21,17 @@ Resource b = new Resource("b", Utils.INT, 1); Resource c = new Resource("c", Utils.INT, 1); Resource d = new Resource("d", Utils.INT, 1); + Resource e = new Resource("e", Utils.INT, 1); + Resource f = new Resource("f", Utils.INT, 1); + Resource g = new Resource("g", Utils.INT, 1); + Resource h = new Resource("h", Utils.INT, 1); + Resource i = new Resource("i", Utils.INT, 3); + Resource j = new Resource("j", Utils.INT, 2); + Resource k = new Resource("k", Utils.INT, 2); + Resource l = new Resource("l", Utils.INT, 1); + Resource m = new Resource("m", Utils.INT, 1); + Resource n = new Resource("n", Utils.INT, 0); + Resource o = new Resource("o", Utils.INT, 0); @Test void GenerateTest1() { @@ -89,5 +102,59 @@ assertEquals(mt1.substitute(result.getBinding()), d2); } + @Test + void GenerateTest4() { + 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("z" + depth))); + } + }, + new MetaResource(new Variable("y")), + new MetaResource(new Variable("z")) + ); + + DependencyTerm t1 = new DependencyTerm(a, b, c); + DependencyTerm t2 = new DependencyTerm(t1, d, e); + DependencyTerm t3 = new DependencyTerm(t2, d, e); + assertTrue(! mt1.isMatchedBy(t1).isEmpty()); + assertTrue(! mt1.isMatchedBy(t2).isEmpty()); + assertTrue(! mt1.isMatchedBy(t3).isEmpty()); + + MatchConstraint result = mt1.isMatchedBy(t3).iterator().next(); + assertTrue(! mt1.dependencyTermGenerate(result.getBinding()).isMatchedBy(t3, result).isEmpty()); + assertEquals(mt1.substitute(result.getBinding()), t3); + + } + + @Test + void GenerateTest5() { + MetaDynamicTerm mt1 = new MetaDynamicTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int index, int depth, boolean isLast) { + if (isLast) { + return new MetaResource(new Variable("x"), new Variable("m")); + } + return new MetaDynamicTerm(this, new MetaResource(new Variable("y" + depth), new Variable("m-" + (depth+1))), new MetaResource(new Variable("z" + depth), new Variable("m-" + (depth+1)))); + } + }, + new MetaResource(new Variable("y"), new Constant("0")), + new MetaResource(new Variable("z"), new Constant("0")) + ); + + DependencyTerm t1 = new DependencyTerm(i, j, k); + DependencyTerm t2 = new DependencyTerm(t1, l, m); + DependencyTerm t3 = new DependencyTerm(t2, n, o); + assertTrue(! mt1.isMatchedBy(t3).isEmpty()); + + MatchConstraint result = mt1.isMatchedBy(t3).iterator().next(); + assertTrue(! mt1.dependencyTermGenerate(result.getBinding()).isMatchedBy(t3, result).isEmpty()); + assertEquals(mt1.substitute(result.getBinding()), t3); + } }