diff --git a/src/main/java/exceptions/ReplaceFailedException.java b/src/main/java/exceptions/ReplaceFailedException.java new file mode 100644 index 0000000..01ce665 --- /dev/null +++ b/src/main/java/exceptions/ReplaceFailedException.java @@ -0,0 +1,5 @@ +package exceptions; + +public class ReplaceFailedException extends RuntimeException { + +} diff --git a/src/main/java/inference/DependencyAxiom.java b/src/main/java/inference/DependencyAxiom.java new file mode 100644 index 0000000..ecfff8e --- /dev/null +++ b/src/main/java/inference/DependencyAxiom.java @@ -0,0 +1,69 @@ +package inference; + +import java.util.ArrayDeque; +import java.util.ArrayList; +import java.util.Deque; +import java.util.HashSet; +import java.util.List; +import java.util.Set; + +import models.Position; +import models.formulas.DependencyFormula; +import models.formulas.Formula; +import models.terms.Dependency; +import models.terms.RDLTerm; +import models.terms.meta.MatchConstraint; +import utils.Permutation; + +public class DependencyAxiom extends InferenceRule{ + + int targetAssumptionIndex = 0; + + public DependencyAxiom(String name) { + super(name); + } + + @Override + public Set derive(List assumptions, Set existTerms) { + if (missingVariables.size() == 0) { + return recursionDerive(assumptions, MatchConstraint.createDefault()); + } else { + Set result = new HashSet<>(); + for (List terms: Permutation.permutation(existTerms, missingVariables.size())) { + for (MatchConstraint constraint: missingVariableFill(terms)) { + if (defaultOrderConstraint != null && (! defaultOrderConstraint.check(constraint.getOrderConstraint()))) continue; + result.addAll(recursionDerive(assumptions, constraint)); + } + } + return result; + } + } + + public Set recursionDerive(List assumptions, MatchConstraint constraint) { + Set result = new HashSet<>(); + Deque q = new ArrayDeque<>(); + q.add(new Position()); + Dependency baseTerm = ((DependencyFormula) assumptions.get(targetAssumptionIndex)).getDependency(); + while (! q.isEmpty()) { + Position curPos = q.pollFirst(); + RDLTerm curTerm = baseTerm; + for (int i = 1; i < curPos.getPath(i); i++) { + curTerm = (RDLTerm) curTerm.getChild(curPos.getPath(i)); + } + if (curTerm instanceof Dependency d) { + List assumptionsCopy = new ArrayList(assumptions); + assumptionsCopy.set(targetAssumptionIndex, new DependencyFormula(d)); + for (Formula derived: super.derive(assumptionsCopy, constraint.clone())) { + if (derived instanceof DependencyFormula df) { + result.add(new DependencyFormula(baseTerm.replace(curPos, df.getDependency()))); + } + } + } + for (int i = 0; i < curTerm.getChildren().size(); i++) { + q.add(curPos.addPath(i)); + } + } + return result; + } + +} diff --git a/src/main/java/inference/InferenceRule.java b/src/main/java/inference/InferenceRule.java index f13d1c7..c9a7ecd 100644 --- a/src/main/java/inference/InferenceRule.java +++ b/src/main/java/inference/InferenceRule.java @@ -57,18 +57,7 @@ } else { Set result = new HashSet<>(); for (List terms: Permutation.permutation(existTerms, missingVariables.size())) { - Set constraints = new HashSet<>(); - constraints.add(MatchConstraint.createDefault()); - boolean flg = false; - for (int i = 0; i < missingVariables.size(); i++) { - constraints = missingVariables.get(i).isMatchedBy(terms.get(i), constraints); - if (constraints.isEmpty()) { - flg = true; - break; - } - } - if (flg) continue; - for (MatchConstraint constraint: constraints) { + for (MatchConstraint constraint: missingVariableFill(terms)) { if (defaultOrderConstraint != null && (! defaultOrderConstraint.check(constraint.getOrderConstraint()))) continue; result.addAll(derive(assumptions, constraint)); } @@ -94,6 +83,16 @@ return result; } + protected Set missingVariableFill(List terms) { + Set constraints = new HashSet<>(); + constraints.add(MatchConstraint.createDefault()); + for (int i = 0; i < missingVariables.size(); i++) { + constraints = missingVariables.get(i).isMatchedBy(terms.get(i), constraints); + if (constraints.isEmpty()) return new HashSet<>(); + } + return constraints; + } + protected Set assumptionMatch(Listassumptions, MatchConstraint constraint) { Set matchResult = new HashSet<>(); matchResult.add(constraint); diff --git a/src/main/java/inference/axioms/UncurriedMapping.java b/src/main/java/inference/axioms/UncurriedMapping.java index ef26ff7..3a33527 100644 --- a/src/main/java/inference/axioms/UncurriedMapping.java +++ b/src/main/java/inference/axioms/UncurriedMapping.java @@ -6,7 +6,7 @@ import java.util.Set; import exceptions.SubstituteFailedException; -import inference.InferenceRule; +import inference.DependencyAxiom; import models.Position; import models.algebra.Variable; import models.formulas.Formula; @@ -19,7 +19,7 @@ import models.terms.meta.MetaTermGenerator; import utils.ExpressionUtils; -public class UncurriedMapping extends InferenceRule { +public class UncurriedMapping extends DependencyAxiom { public UncurriedMapping() { super("Uncurried Mapping"); diff --git a/src/main/java/models/Position.java b/src/main/java/models/Position.java index 5c4386a..5d4b247 100644 --- a/src/main/java/models/Position.java +++ b/src/main/java/models/Position.java @@ -44,7 +44,7 @@ return paths.size(); } - private int getPath(int index) { + public int getPath(int index) { if (index >= size()) { return -1; } diff --git a/src/main/java/models/terms/Dependency.java b/src/main/java/models/terms/Dependency.java index 8a25375..6b2ecb8 100644 --- a/src/main/java/models/terms/Dependency.java +++ b/src/main/java/models/terms/Dependency.java @@ -1,14 +1,15 @@ package models.terms; -import com.google.common.collect.TreeMultiset; - import java.util.ArrayList; import java.util.Arrays; import java.util.List; import java.util.stream.Collectors; +import com.google.common.collect.TreeMultiset; + import exceptions.SyntaxException; import lombok.Getter; +import models.Position; @Getter public class Dependency extends RDLTerm{ @@ -32,6 +33,10 @@ } } + public Dependency(RDLTerm dependingTerm, TreeMultiset dependedTerms) { + this(dependingTerm, new ArrayList<>(dependedTerms)); + } + public Dependency(RDLTerm dependingTerm, EvaluatableTerm ...dependedTerms) { this(dependingTerm, Arrays.asList(dependedTerms)); } @@ -42,6 +47,28 @@ } @Override + public RDLTerm replace(Position targetPosition, RDLTerm term, Position curPosition) { + if (targetPosition.equals(curPosition)) { + return term; + } else { + int nextPath = targetPosition.getPath(curPosition.size()); + if (nextPath == 0) { + return new Dependency(dependingTerm.replace(targetPosition, term, curPosition.addPath(nextPath)), this.dependedTerms); + } else { + List dependedTerms = new ArrayList<>(); + for (int i = 1; i < getChildren().size(); i++) { + if (i == nextPath) { + dependedTerms.add((EvaluatableTerm) ((RDLTerm) getChild(i)).replace(targetPosition, term, curPosition.addPath(i))); + } else { + dependedTerms.add((EvaluatableTerm) getChild(i)); + } + } + return new Dependency(dependingTerm, dependedTerms); + } + } + } + + @Override public int getMaxIndex() { return 1 + dependedTerms.size(); } diff --git a/src/main/java/models/terms/DependencyTerm.java b/src/main/java/models/terms/DependencyTerm.java index 1acfd5b..2949ec5 100644 --- a/src/main/java/models/terms/DependencyTerm.java +++ b/src/main/java/models/terms/DependencyTerm.java @@ -1,14 +1,15 @@ package models.terms; -import com.google.common.collect.TreeMultiset; - import java.util.ArrayList; import java.util.Arrays; import java.util.List; import java.util.TreeMap; +import com.google.common.collect.TreeMultiset; + import exceptions.SyntaxException; import lombok.Getter; +import models.Position; @Getter public class DependencyTerm extends EvaluatableTerm{ @@ -107,6 +108,24 @@ return new Dependency(dependingTerm, dependedTerms); } + @Override + public RDLTerm replace(Position targetPosition, RDLTerm term, Position curPosition) { + if (targetPosition.equals(curPosition)) { + return term; + } else { + int nextPath = targetPosition.getPath(curPosition.size()); + List children = new ArrayList<>(); + for (int i = 1; i < getChildren().size(); i++) { + children.add((EvaluatableTerm) getChild(i)); + } + if (nextPath == 0) { + return new DependencyTerm((EvaluatableTerm) dependingTerm.replace(targetPosition, term, curPosition.addPath(nextPath)), children); + } else { + children.set(nextPath - 1, (EvaluatableTerm) children.get(nextPath - 1).replace(targetPosition, term, curPosition.addPath(nextPath))); + return new DependencyTerm(dependingTerm, children); + } + } + } @Override public int getMaxIndex() { diff --git a/src/main/java/models/terms/RDLTerm.java b/src/main/java/models/terms/RDLTerm.java index 4c30b56..4eb68b5 100644 --- a/src/main/java/models/terms/RDLTerm.java +++ b/src/main/java/models/terms/RDLTerm.java @@ -1,6 +1,7 @@ package models.terms; import lombok.Getter; +import models.Position; import models.algebra.Symbol; import models.algebra.Term; @@ -22,6 +23,12 @@ public abstract Dependency getDependency(); + public abstract RDLTerm replace(Position targetPosition, RDLTerm term, Position curPosition); + + public RDLTerm replace(Position targetPosition, RDLTerm term) { + return replace(targetPosition, term, new Position()); + } + public abstract int getMaxIndex(); public abstract int getMaxDepth(); diff --git a/src/main/java/models/terms/Resource.java b/src/main/java/models/terms/Resource.java index 5603097..51f08a0 100644 --- a/src/main/java/models/terms/Resource.java +++ b/src/main/java/models/terms/Resource.java @@ -1,6 +1,8 @@ package models.terms; +import exceptions.ReplaceFailedException; import lombok.Getter; +import models.Position; @Getter public class Resource extends EvaluatableTerm { @@ -18,6 +20,14 @@ } @Override + public RDLTerm replace(Position targetPosition, RDLTerm term, Position curPosition) { + if (targetPosition.equals(curPosition)) { + return term; + } + throw new ReplaceFailedException(); + } + + @Override public int getMaxIndex() { return 1; } diff --git a/src/main/java/models/terms/ResourceConstant.java b/src/main/java/models/terms/ResourceConstant.java index 105590b..bb9b72b 100644 --- a/src/main/java/models/terms/ResourceConstant.java +++ b/src/main/java/models/terms/ResourceConstant.java @@ -1,6 +1,8 @@ package models.terms; +import exceptions.ReplaceFailedException; import lombok.Getter; +import models.Position; import models.algebra.Type; @Getter @@ -27,6 +29,14 @@ } @Override + public RDLTerm replace(Position targetPosition, RDLTerm term, Position curPosition) { + if (targetPosition.equals(curPosition)) { + return term; + } + throw new ReplaceFailedException(); + } + + @Override public int getMaxIndex() { return 1; } diff --git a/src/main/java/models/terms/meta/MatchConstraint.java b/src/main/java/models/terms/meta/MatchConstraint.java index aed9a0b..f78f5cc 100644 --- a/src/main/java/models/terms/meta/MatchConstraint.java +++ b/src/main/java/models/terms/meta/MatchConstraint.java @@ -55,6 +55,10 @@ return new HashMap<>(this.context); } + public MatchConstraint clone() { + return new MatchConstraint(this); + } + public static MatchConstraint createDefault() { return new MatchConstraint(new HashMap<>(), new HashMap<>(), new HashMap<>()); } diff --git a/src/main/java/models/terms/meta/MetaRDLTerm.java b/src/main/java/models/terms/meta/MetaRDLTerm.java index f9d20dc..edfa5fe 100644 --- a/src/main/java/models/terms/meta/MetaRDLTerm.java +++ b/src/main/java/models/terms/meta/MetaRDLTerm.java @@ -5,6 +5,7 @@ import java.util.Map; import java.util.Set; +import exceptions.ReplaceFailedException; import lombok.Getter; import models.Position; import models.algebra.Variable; @@ -67,6 +68,10 @@ protected abstract Set isMatchedBy(RDLTerm another, MatchConstraint constraint, Position position); + @Override + public RDLTerm replace(Position targetPosition, RDLTerm term, Position curPosition) { + throw new ReplaceFailedException(); + } public RDLTerm substitute(Map binding) { return substitute(binding, new HashMap<>(), new Position()); diff --git a/src/test/java/terms/DependencyTermTest.java b/src/test/java/terms/DependencyTermTest.java index 058cdd6..a8592c8 100644 --- a/src/test/java/terms/DependencyTermTest.java +++ b/src/test/java/terms/DependencyTermTest.java @@ -5,9 +5,9 @@ import org.junit.jupiter.api.Test; import exceptions.SyntaxException; +import models.Position; import models.terms.DependencyTerm; import models.terms.Resource; -import utils.Utils; public class DependencyTermTest { @@ -97,4 +97,13 @@ } + @Test + void ReplaceTest() { + DependencyTerm t1 = new DependencyTerm(a, b, c); + assertEquals(t1.replace(new Position(0, 1), d), new DependencyTerm(a, d, c)); + + DependencyTerm t2 = new DependencyTerm(t1, d, e); + assertEquals(t2.replace(new Position(0, 0, 0), t1), new DependencyTerm(new DependencyTerm(t1, b, c), d, e)); + } + } diff --git a/src/test/java/terms/DependencyTest.java b/src/test/java/terms/DependencyTest.java index 382cbc1..e7c8200 100644 --- a/src/test/java/terms/DependencyTest.java +++ b/src/test/java/terms/DependencyTest.java @@ -4,9 +4,9 @@ import org.junit.jupiter.api.Test; import exceptions.SyntaxException; +import models.Position; import models.terms.Dependency; import models.terms.Resource; -import utils.Utils; public class DependencyTest { @@ -91,4 +91,19 @@ } + @Test + void ReplaceTest() { + Dependency d1 = new Dependency(a, b); + Dependency d2 = (Dependency) d1.replace(new Position(0, 0), c); + assertEquals(d2, new Dependency(c, b)); + + Dependency d3 = new Dependency(d1, c); + Dependency d4 = (Dependency) d3.replace(new Position(0, 0, 1), d); + assertEquals(d4, new Dependency(new Dependency(a, d), c)); + + assertEquals(d3.replace(new Position(0, 1), c), new Dependency(d1, c)); + assertEquals(d3.replace(new Position(0, 0), c), new Dependency(c, c)); + + } + }