diff --git a/src/main/java/Main.java b/src/main/java/Main.java index f8508b2..1f2f61e 100644 --- a/src/main/java/Main.java +++ b/src/main/java/Main.java @@ -8,8 +8,11 @@ import models.algebra.Expression; import models.algebra.Type; import models.algebra.Variable; +import models.terms.Dependency; +import models.terms.Resource; import models.terms.meta.MetaDynamicDependency; import models.terms.meta.MetaDynamicDependencyTerm; +import models.terms.meta.MetaEvaluatableTermVariable; import models.terms.meta.MetaRDLTerm; import models.terms.meta.MetaResource; import models.terms.meta.MetaTermGenerator; @@ -24,6 +27,7 @@ sandbox2(); sandbox3(); sandbox4(); + sandbox5(); } @@ -77,4 +81,26 @@ System.out.println(t1.generate(0, 5, 0, null)); System.out.println(t2.generate(0, 3, 2, null)); } + + static void sandbox5() { + MetaDynamicDependency md1 = new MetaDynamicDependency(new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + int maxOrder = (Integer) context.get("maxOrder"); + if (curDepth < maxDepth && curIndex == 0) { + return new MetaDynamicDependency(this); + } + if (curIndex == 0) { + return new MetaEvaluatableTermVariable(new Variable("s"), new Constant("" + maxOrder)); + } + return new MetaEvaluatableTermVariable(new Variable("v" + curDepth), new Constant("" + (maxOrder - (maxDepth - curDepth)))); + }}); + System.out.println(md1.generate(2, 3, Map.of("maxOrder", 4)).toStringWithOrder()); + Dependency d1 = new Dependency(new Resource("s", 4), new Resource("t", 4)); + Dependency d2 = new Dependency(d1, new Resource("v3", 3)); + Dependency d3 = new Dependency(d2, new Resource("v2", 2)); + Dependency d4 = new Dependency(d3, new Resource("v1", 1)); + System.out.println(d3); + System.out.println(md1.isMatchedBy(d3, Map.of("maxOrder", 4))); + } } diff --git a/src/main/java/inference/InferenceRule.java b/src/main/java/inference/InferenceRule.java index c7f09c7..f8e16ff 100644 --- a/src/main/java/inference/InferenceRule.java +++ b/src/main/java/inference/InferenceRule.java @@ -128,7 +128,7 @@ for (MatchConstraint con: result) { try { int maxIndex = conclusionMaxIndexCalculator != null ? conclusionMaxIndexCalculator.calculate(assumptions) : 0; - int maxDepth = conclusionMaxDepthCalculator != null ? conclusionMaxDepthCalculator.calculate(assumptions) : 0; + int maxDepth = conclusionMaxDepthCalculator != null ? conclusionMaxDepthCalculator.calculate(assumptions) : 1; subRes.add(conclusion.substitution(con.getBinding(), Map.of("maxIndex", maxIndex, "maxDepth", maxDepth))); } catch (SubstituteFailedException e) { continue; diff --git a/src/main/java/inference/ProofSystem.java b/src/main/java/inference/ProofSystem.java index d68fac9..624f162 100644 --- a/src/main/java/inference/ProofSystem.java +++ b/src/main/java/inference/ProofSystem.java @@ -12,7 +12,9 @@ import java.util.Set; import java.util.stream.Collectors; +import inference.axioms.CompositeMapping; import inference.axioms.RightSubstitution; +import inference.axioms.UncurriedMapping; import models.algebra.Variable; import models.formulas.DependencyFormula; import models.formulas.EquationFormula; @@ -26,6 +28,7 @@ import models.terms.meta.MetaEvaluatableTermVariable; import models.terms.meta.MetaRDLTerm; import models.terms.meta.MetaTermGenerator; +import models.terms.meta.OrderConstraint; import utils.Product; public class ProofSystem { @@ -203,7 +206,56 @@ // //======================Dependency Axioms============================= // - + public static final InferenceRule identityMapping = new InferenceRule( + "Identity Mapping", + List.of( + new MetaEquationFormula( + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaEvaluatableTermVariable(new Variable("se")) + ) + ), + List.of(), + new MetaDependencyFormula( + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaEvaluatableTermVariable(new Variable("se")) + ), + null, + null, + null, + null + ); + + public static final InferenceRule compositeMapping = new CompositeMapping(); + + public static final InferenceRule constantMapping = new InferenceRule( + "Constant Mapping", + List.of(), + List.of(), + new MetaDependencyFormula( + new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")), + new MetaEvaluatableTermVariable(new Variable("re"), new Variable("m")) + ), + new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m")), + null, + null, + null + ); + + public static final InferenceRule uncurriedMapping = new UncurriedMapping(); + + /* + * new InferenceRule( + "", + List.of(), + List.of(), + null, + null, + null, + null, + null + ); + */ + private static final List axioms = List.of( // reflexivity, // symmetry, diff --git a/src/main/java/inference/axioms/CompositeMapping.java b/src/main/java/inference/axioms/CompositeMapping.java new file mode 100644 index 0000000..035272d --- /dev/null +++ b/src/main/java/inference/axioms/CompositeMapping.java @@ -0,0 +1,105 @@ +package inference.axioms; + +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.DependencyFormula; +import models.formulas.Formula; +import models.formulas.meta.MetaDependencyFormula; +import models.formulas.meta.MetaFormula; +import models.terms.meta.MatchConstraint; +import models.terms.meta.MetaDynamicDependency; +import models.terms.meta.MetaEvaluatableTermVariable; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaTermGenerator; + +public class CompositeMapping extends InferenceRule { + + public CompositeMapping() { + super("Compsite Mapping"); + this.assumptions.add( + new MetaDependencyFormula( + new MetaDynamicDependency( + (ci, cd, mi, md, context) -> new MetaEvaluatableTermVariable(new Variable("te" + (ci - 2))), + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("te")) + ) + ) + ); + this.assumptions.add( + new MetaDependencyFormula( + new MetaDynamicDependency( + (ci, cd, mi, md, context) -> new MetaEvaluatableTermVariable(new Variable("ue" + (ci - 1))), + new MetaEvaluatableTermVariable(new Variable("te")) + ) + ) + ); + this.conclusion = new MetaDependencyFormula( + new MetaDynamicDependency( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth,Map context) { + curIndex -= 1; + int firstAssumptionSize = (Integer) context.get("firstAssumptionSize") - 2; + if (curIndex < firstAssumptionSize) { + return new MetaEvaluatableTermVariable(new Variable("te" + (curIndex))); + } + return new MetaEvaluatableTermVariable(new Variable("ue" + (curIndex - firstAssumptionSize))); + } + + }, + new MetaEvaluatableTermVariable(new Variable("se")) + ) + ); + conclusionMaxIndexCalculator = (assumptions) -> ((DependencyFormula) assumptions.get(0)).getDependency().getMaxIndex() - 2 + ((DependencyFormula) assumptions.get(1)).getDependency().getMaxIndex() - 1 + 1; + } + + protected Set apply(List assumptions, MatchConstraint constraint) { + if (assumptions.size() < getAssumptionSize()) { + return new HashSet<>(); + } + + Set result = new HashSet<>(); + result.add(constraint); + for (int i = 0; i < getAssumptionSize(); i++) { + result = this.assumptions.get(i).isMatchedBy(assumptions.get(i), result); + if (result.isEmpty()) { + return new HashSet<>(); + } + } + if (this.repetitionAssumptions.size() != 0 && (assumptions.size() - this.assumptions.size()) % this.repetitionAssumptions.size() != 0) { + return new HashSet<>(); + } + if (this.repetitionAssumptions.size() != 0) { + 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 new HashSet<>(); + } + } + } + } + Set subRes = new HashSet<>(); + for (MatchConstraint con: result) { + try { + int maxIndex = conclusionMaxIndexCalculator != null ? conclusionMaxIndexCalculator.calculate(assumptions) : 0; + int maxDepth = conclusionMaxDepthCalculator != null ? conclusionMaxDepthCalculator.calculate(assumptions) : 1; + int firstAssumptionSize = ((DependencyFormula) assumptions.get(0)).getDependency().getMaxIndex(); + subRes.add(conclusion.substitution(con.getBinding(), Map.of("maxIndex", maxIndex, "maxDepth", maxDepth, "firstAssumptionSize", firstAssumptionSize))); + } catch (SubstituteFailedException e) { + continue; + } + } + return subRes; + } + +} diff --git a/src/main/java/inference/axioms/UncurriedMapping.java b/src/main/java/inference/axioms/UncurriedMapping.java new file mode 100644 index 0000000..5854252 --- /dev/null +++ b/src/main/java/inference/axioms/UncurriedMapping.java @@ -0,0 +1,166 @@ +package inference.axioms; + +import java.util.HashMap; +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.Constant; +import models.algebra.Variable; +import models.formulas.DependencyFormula; +import models.formulas.Formula; +import models.formulas.meta.MetaDependencyFormula; +import models.formulas.meta.MetaEquationFormula; +import models.formulas.meta.MetaFormula; +import models.terms.Dependency; +import models.terms.RDLTerm; +import models.terms.Resource; +import models.terms.meta.MatchConstraint; +import models.terms.meta.MetaDependency; +import models.terms.meta.MetaDependencyTerm; +import models.terms.meta.MetaDynamicDependency; +import models.terms.meta.MetaEvaluatableTermVariable; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaTermGenerator; + +public class UncurriedMapping extends InferenceRule { + + public UncurriedMapping() { + super("Uncurried Mapping"); + this.assumptions.add( + new MetaDependencyFormula( + new MetaDynamicDependency(new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + int maxOrder = (Integer) context.get("maxOrder"); + context.put("" + curDepth, curIndex + 1); + context.put("maxDepth", Math.max((Integer) context.getOrDefault("maxDepth", 0), curDepth + 1)); + if (curIndex == 0 && curDepth == maxDepth - 1) { + return new MetaDependency( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")) + ); + } + if (curDepth < maxDepth && curIndex == 0) { + return new MetaDynamicDependency(this); + } + return new MetaEvaluatableTermVariable(new Variable("v" + curDepth), new Constant("" + (maxOrder - (maxDepth - curDepth)))); + } + }) + ) + ); + this.assumptions.add(new MetaEquationFormula( + new MetaDependencyTerm( + new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), + new MetaEvaluatableTermVariable(new Variable("xxx")), + new MetaEvaluatableTermVariable(new Variable("yyy")) + ), + new MetaEvaluatableTermVariable(new Variable("ue"), new Variable("m")) + )); + this.conclusion = new MetaDependencyFormula( + new MetaDynamicDependency(new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + int maxOrder = (Integer) context.get("maxOrder"); + int uOrder = (Integer) context.get("uOrder"); + int maxIdx = (Integer) context.get("" + curDepth); + if (curIndex >= maxIdx) { + return null; + } + if (curIndex == 0 && curDepth == maxDepth - 1) { + return new MetaDependencyTerm( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), + new MetaEvaluatableTermVariable(new Variable("ue"), new Variable("m")) + ); + } + if (curDepth < maxDepth - 1 && curIndex == 0) { + return new MetaDynamicDependency(this); + } + if (curDepth == uOrder && curIndex == 1) { + return new MetaEvaluatableTermVariable(new Variable("ue"), new Variable("m")); + } + return new MetaEvaluatableTermVariable(new Variable("v" + curDepth), new Constant("" + (maxOrder - (maxDepth - curDepth)))); + } + }) + ); + } + + + protected Set apply(List assumptions, MatchConstraint constraint) { + Map context = new HashMap<>(); + if (assumptions.size() < getAssumptionSize()) { + return new HashSet<>(); + } + + Set result = new HashSet<>(); + result.add(constraint); + if (! (assumptions.get(0) instanceof DependencyFormula)) { + return new HashSet<>(); + } + Dependency dep = ((DependencyFormula)assumptions.get(0)).getDependency(); + int maxOrder = 0; + while (true) { + RDLTerm d2 = dep.getDependingTerm(); + if (d2 instanceof Resource) { + maxOrder = dep.getDependedTerms().iterator().next().getOrder(); + break; + } + dep = (Dependency) d2; + } + + for (int i = 0; i < getAssumptionSize(); i++) { + context.put("maxOrder", maxOrder); + result = this.assumptions.get(i).isMatchedBy(assumptions.get(i), result, context); + if (result.isEmpty()) { + return new HashSet<>(); + } + } + + Set ng = new HashSet<>(); + int m = 0; + for (MatchConstraint matchConstraint : result) { + int n = matchConstraint.getOrderConstraint().get(new Variable("n")).getOrder(); + m = matchConstraint.getOrderConstraint().get(new Variable("m")).getOrder(); + if (n != maxOrder) { + ng.add(matchConstraint); + continue; + } + } + context.put("" + m, (Integer) context.get("" + m) + 1); + + if (this.repetitionAssumptions.size() != 0 && (assumptions.size() - this.assumptions.size()) % this.repetitionAssumptions.size() != 0) { + return new HashSet<>(); + } + if (this.repetitionAssumptions.size() != 0) { + 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 new HashSet<>(); + } + } + } + } + Set subRes = new HashSet<>(); + for (MatchConstraint con: result) { + try { + int maxIndex = conclusionMaxIndexCalculator != null ? conclusionMaxIndexCalculator.calculate(assumptions) : 10000; + int uOrder = con.getBinding().get(new Variable("ue")).getOrder(); + context.put("maxIndex", maxIndex); + context.put("uOrder", uOrder); + subRes.add(conclusion.substitution(con.getBinding(), context)); + } catch (SubstituteFailedException e) { + continue; + } + } + return subRes; + } + +} diff --git a/src/main/java/models/formulas/meta/MetaDependencyFormula.java b/src/main/java/models/formulas/meta/MetaDependencyFormula.java index 300d0ef..e0095f7 100644 --- a/src/main/java/models/formulas/meta/MetaDependencyFormula.java +++ b/src/main/java/models/formulas/meta/MetaDependencyFormula.java @@ -50,12 +50,12 @@ } @Override - public Set isMatchedBy(Formula formula, MatchConstraint constraint) { + public Set isMatchedBy(Formula formula, MatchConstraint constraint, Map context) { if (! (formula instanceof DependencyFormula)) { return new HashSet<>(); } DependencyFormula dep = (DependencyFormula) formula; - return dependency.isMatchedBy(dep.getDependency(), constraint); + return dependency.isMatchedBy(dep.getDependency(), constraint, context); } diff --git a/src/main/java/models/formulas/meta/MetaEquationFormula.java b/src/main/java/models/formulas/meta/MetaEquationFormula.java index 5edee3d..ca3c2bb 100644 --- a/src/main/java/models/formulas/meta/MetaEquationFormula.java +++ b/src/main/java/models/formulas/meta/MetaEquationFormula.java @@ -34,14 +34,14 @@ } @Override - public Set isMatchedBy(Formula formula, MatchConstraint constraint) { + public Set isMatchedBy(Formula formula, MatchConstraint constraint, Map context) { Set result = new HashSet<>(); if (! (formula instanceof EquationFormula)) { return result; } EquationFormula eq = (EquationFormula) formula; - result = leftSideHand.isMatchedBy(eq.getLeftSideHand(), constraint); - return rightSideHand.isMatchedBy(eq.getRightSideHand(), result); + result = leftSideHand.isMatchedBy(eq.getLeftSideHand(), constraint, context); + return rightSideHand.isMatchedBy(eq.getRightSideHand(), result, context); } @Override diff --git a/src/main/java/models/formulas/meta/MetaFormula.java b/src/main/java/models/formulas/meta/MetaFormula.java index f6befda..3cbc04f 100644 --- a/src/main/java/models/formulas/meta/MetaFormula.java +++ b/src/main/java/models/formulas/meta/MetaFormula.java @@ -18,7 +18,16 @@ return isMatchedBy(formula, new MatchConstraint(new HashMap<>(), new HashMap<>())); } - public abstract Set isMatchedBy(Formula formula, MatchConstraint constraint); + public Set isMatchedBy(Formula formula, Map context) { + return isMatchedBy(formula, MatchConstraint.createDefault(), context); + } + + public abstract Set isMatchedBy(Formula formula, MatchConstraint constraint, Map context); + + public Set isMatchedBy(Formula formula, MatchConstraint constraint) { + return isMatchedBy(formula, constraint, new HashMap<>()); + } + public Set isMatchedBy(Formula formula, Set constraints) { Set result = new HashSet<>(); @@ -28,6 +37,14 @@ return result; } + public Set isMatchedBy(Formula formula, Set constraints, Map context) { + Set result = new HashSet<>(); + for (MatchConstraint constraint: constraints) { + result.addAll(isMatchedBy(formula, constraint, context)); + } + return result; + } + public abstract Formula substitution(Map binding, Map context); public abstract Set getSubTerms(Class clazz); diff --git a/src/main/java/models/terms/meta/MetaDependency.java b/src/main/java/models/terms/meta/MetaDependency.java index 8342e29..857186b 100644 --- a/src/main/java/models/terms/meta/MetaDependency.java +++ b/src/main/java/models/terms/meta/MetaDependency.java @@ -44,7 +44,7 @@ } @Override - public Set isMatchedBy(RDLTerm another, MatchConstraint constraint) { + public Set isMatchedBy(RDLTerm another, MatchConstraint constraint, Map context) { Set result = new HashSet<>(); if (! another.getClass().isAssignableFrom(this.termType.getBaseTermClass())) { return result; diff --git a/src/main/java/models/terms/meta/MetaDependencyTerm.java b/src/main/java/models/terms/meta/MetaDependencyTerm.java index ec17a2f..525cbd2 100644 --- a/src/main/java/models/terms/meta/MetaDependencyTerm.java +++ b/src/main/java/models/terms/meta/MetaDependencyTerm.java @@ -1,7 +1,5 @@ package models.terms.meta; -import com.google.common.collect.TreeMultiset; - import java.util.ArrayList; import java.util.Arrays; import java.util.HashSet; @@ -12,6 +10,8 @@ import java.util.stream.Collectors; import java.util.stream.IntStream; +import com.google.common.collect.TreeMultiset; + import exceptions.SubstituteFailedException; import exceptions.SyntaxException; import models.algebra.Variable; @@ -57,7 +57,7 @@ } @Override - public Set isMatchedBy(RDLTerm another, MatchConstraint constraint) { + public Set isMatchedBy(RDLTerm another, MatchConstraint constraint, Map context) { Set result = new HashSet<>(); if (! another.getClass().isAssignableFrom(this.termType.getBaseTermClass())) { return result; diff --git a/src/main/java/models/terms/meta/MetaDynamicDependency.java b/src/main/java/models/terms/meta/MetaDynamicDependency.java index 569003a..fc837ff 100644 --- a/src/main/java/models/terms/meta/MetaDynamicDependency.java +++ b/src/main/java/models/terms/meta/MetaDynamicDependency.java @@ -2,7 +2,6 @@ import java.util.ArrayList; import java.util.Arrays; -import java.util.HashMap; import java.util.List; import java.util.Map; import java.util.Set; @@ -53,6 +52,9 @@ } for (int i = staticSize; i < maxIndex - 1; i++) { RDLTerm generatedTerm = termGenerator.generate(i + 1, depth, maxIndex, maxDepth, context); + if (generatedTerm == null) { + break; + } while (generatedTerm instanceof MetaDynamicTerm dynamicTerm) { generatedTerm = dynamicTerm.generate(depth + 1, maxIndex, maxDepth, context); } @@ -63,10 +65,10 @@ @Override - public Set isMatchedBy(RDLTerm another, MatchConstraint constraint) { + public Set isMatchedBy(RDLTerm another, MatchConstraint constraint, Map context) { int maxIndex = another.getMaxIndex(); int maxDepth = another.getMaxDepth(); - MetaRDLTerm metaDep = generate(maxIndex, maxDepth, new HashMap<>()); + MetaRDLTerm metaDep = generate(maxIndex, maxDepth, context); return metaDep.isMatchedBy(another, constraint); } diff --git a/src/main/java/models/terms/meta/MetaDynamicDependencyTerm.java b/src/main/java/models/terms/meta/MetaDynamicDependencyTerm.java index aeb528e..8a55608 100644 --- a/src/main/java/models/terms/meta/MetaDynamicDependencyTerm.java +++ b/src/main/java/models/terms/meta/MetaDynamicDependencyTerm.java @@ -1,16 +1,15 @@ 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 com.google.common.collect.TreeMultiset; + import exceptions.SubstituteFailedException; import exceptions.SyntaxException; import models.algebra.Variable; @@ -82,7 +81,13 @@ } for (int i = 0; i < (maxIndex - index) / 2; i++) { RDLTerm dependedTerm = generator.generate(i * 2 + 1, depth, maxIndex, maxDepth, context); + if (dependedTerm == null) { + break; + } RDLTerm argTerm = generator.generate(i * 2 + 2, depth, maxIndex, maxDepth, context); + if (argTerm == null) { + break; + } while (dependedTerm instanceof MetaDynamicTerm dynamicTerm) { dependedTerm = dynamicTerm.generate(depth + 1, maxIndex, maxDepth, context); } @@ -96,10 +101,10 @@ } @Override - public Set isMatchedBy(RDLTerm another, MatchConstraint constraint) { + public Set isMatchedBy(RDLTerm another, MatchConstraint constraint, Map context) { int maxIndex = another.getMaxIndex(); int maxDepth = another.getMaxDepth(); - MetaRDLTerm metaTerm = generate(maxIndex, maxDepth, new HashMap<>()); + MetaRDLTerm metaTerm = generate(maxIndex, maxDepth, context); return metaTerm.isMatchedBy(another, constraint); } diff --git a/src/main/java/models/terms/meta/MetaRDLTerm.java b/src/main/java/models/terms/meta/MetaRDLTerm.java index 02d7a3d..c8827ba 100644 --- a/src/main/java/models/terms/meta/MetaRDLTerm.java +++ b/src/main/java/models/terms/meta/MetaRDLTerm.java @@ -32,15 +32,31 @@ return isMatchedBy(another, MatchConstraint.createDefault()); } + public Set isMatchedBy(RDLTerm another, Map context) { + return isMatchedBy(another, MatchConstraint.createDefault(), context); + } + public Set isMatchedBy(RDLTerm another, Set constraints) { Set result = new HashSet<>(); for (MatchConstraint constraint : constraints) { - result.addAll(isMatchedBy(another, constraint)); + result.addAll(isMatchedBy(another, constraint, new HashMap<>())); } return result; } - abstract public Set isMatchedBy(RDLTerm another, MatchConstraint constraint); + public Set isMatchedBy(RDLTerm another, Set constraints, Map context) { + Set result = new HashSet<>(); + for (MatchConstraint constraint : constraints) { + result.addAll(isMatchedBy(another, constraint, context)); + } + return result; + } + + public Set isMatchedBy(RDLTerm another, MatchConstraint constraint) { + return isMatchedBy(another, constraint, new HashMap<>()); + } + + abstract public Set isMatchedBy(RDLTerm another, MatchConstraint constraint, Map context); public RDLTerm substitute(Map binding) { diff --git a/src/main/java/models/terms/meta/MetaResource.java b/src/main/java/models/terms/meta/MetaResource.java index 8b59887..2385c19 100644 --- a/src/main/java/models/terms/meta/MetaResource.java +++ b/src/main/java/models/terms/meta/MetaResource.java @@ -28,7 +28,7 @@ } @Override - public Set isMatchedBy(RDLTerm another, MatchConstraint constraint) { + public Set isMatchedBy(RDLTerm another, MatchConstraint constraint, Map context) { Set result = new HashSet<>(); Map binding = constraint.getBinding(); Map orderConstraint = constraint.getOrderConstraint(); diff --git a/src/main/java/models/terms/meta/MetaVariable.java b/src/main/java/models/terms/meta/MetaVariable.java index 8c8f717..34fa8b6 100644 --- a/src/main/java/models/terms/meta/MetaVariable.java +++ b/src/main/java/models/terms/meta/MetaVariable.java @@ -75,7 +75,7 @@ } @Override - public Set isMatchedBy(RDLTerm another, MatchConstraint constraint) { + public Set isMatchedBy(RDLTerm another, MatchConstraint constraint, Map context) { Set result = new HashSet<>(); Map binding = constraint.getBinding(); Map orderConstraint = constraint.getOrderConstraint(); diff --git a/src/test/java/inferencerule/DependencyAxiomTest.java b/src/test/java/inferencerule/DependencyAxiomTest.java index 9b62347..f84dd16 100644 --- a/src/test/java/inferencerule/DependencyAxiomTest.java +++ b/src/test/java/inferencerule/DependencyAxiomTest.java @@ -1,6 +1,17 @@ package inferencerule; +import static org.junit.jupiter.api.Assertions.*; + +import java.util.Set; + +import org.junit.jupiter.api.Test; + +import inference.ProofSystem; +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; public class DependencyAxiomTest { @@ -9,8 +20,64 @@ Resource c = new Resource("c", 1); Resource d = new Resource("d", 1); Resource e = new Resource("e", 1); - Resource f = new Resource("f", 2); - Resource g = new Resource("g", 2); - Resource h = new Resource("h", 2); + Resource f = new Resource("f", 1); + Resource g = new Resource("g", 1); + Resource h = new Resource("h", 1); + Resource i = new Resource("i", 2); + Resource j = new Resource("j", 2); + Resource k = new Resource("k", 2); + + @Test + void IdentityMappingTest() { + Set res = ProofSystem.identityMapping.apply(new EquationFormula(a, b)); + assertTrue(res.contains(new DependencyFormula(a, b))); + } + + @Test + void CompositeMappingTest() { + Set res = ProofSystem.compositeMapping.apply(new DependencyFormula(a, b), new DependencyFormula(b, c)); + assertTrue(res.contains(new DependencyFormula(a, c))); + + res = ProofSystem.compositeMapping.apply(new DependencyFormula(a, b, c), new DependencyFormula(c, d, e, f)); + assertTrue(res.contains(new DependencyFormula(a, b, d, e, f))); + } + + @Test + void ConstantMappingTest() { + //todo + } + + @Test + void UncurriedMappingTest() { + Set res = ProofSystem.uncurriedMapping.apply( + new DependencyFormula(new Dependency(i, j), a), + new EquationFormula(new DependencyTerm(j, h, c), b) + ); + assertTrue(res.contains(new DependencyFormula(new DependencyTerm(i, j, b), a, b))); + + Resource a4 = new Resource("a4", 4); + Resource b4 = new Resource("b4", 4); + Resource x= new Resource("y", 4); + Resource y = new Resource("x", 4); + Resource a3 = new Resource("a3", 3); + Resource a2 = new Resource("a2", 2); + Resource a1 = new Resource("a1", 1); + Resource c2 = new Resource("c2", 2); + + Dependency d4 = new Dependency(b4, a4); + Dependency d3 = new Dependency(d4, a3); + Dependency d2 = new Dependency(d3, a2); + Dependency d1 = new Dependency(d2, a1); + + res = ProofSystem.uncurriedMapping.apply( + new DependencyFormula(d1), + new EquationFormula(new DependencyTerm(a4, x, y), c2) + ); + DependencyTerm t1 = new DependencyTerm(b4, a4, c2); + Dependency d33 = new Dependency(t1, a3); + Dependency d22 = new Dependency(d33, a2, c2); + Dependency d11 = new Dependency(d22, a1); + assertTrue(res.contains(new DependencyFormula(d11))); + } }