Commit 3934685e authored by Sarah Grebing's avatar Sarah Grebing

Bugfix

parent a7b1ed25
Pipeline #19956 failed with stages
in 2 minutes and 13 seconds
...@@ -19,7 +19,7 @@ public class KeyTermMatcher extends KeyTermBaseVisitor<Matchings, MatchPath> { ...@@ -19,7 +19,7 @@ public class KeyTermMatcher extends KeyTermBaseVisitor<Matchings, MatchPath> {
private String randomName; private String randomName;
MatchPath peek; // MatchPath peek;
private List<Integer> currentposition = new ArrayList<>(); private List<Integer> currentposition = new ArrayList<>();
...@@ -42,18 +42,11 @@ public class KeyTermMatcher extends KeyTermBaseVisitor<Matchings, MatchPath> { ...@@ -42,18 +42,11 @@ public class KeyTermMatcher extends KeyTermBaseVisitor<Matchings, MatchPath> {
public Matchings matchesSequent(Sequent sequent, Sequent pattern) { public Matchings matchesSequent(Sequent sequent, Sequent pattern) {
MatchPath.MPSequent mps = MatchPathFacade.create(sequent); MatchPath.MPSequent mps = MatchPathFacade.create(sequent);
// MatchPath.MPSequent mps = new MatchPath.MPSequent(sequent);
Matchings ms = matchesSemisequent( Matchings ms = matchesSemisequent(
// new MatchPath.MPSemiSequent(mps, sequent.succedent(), false),
MatchPathFacade.createSuccedent(mps), MatchPathFacade.createSuccedent(mps),
pattern.succedent()); pattern.succedent());
//peek = new MatchPath.MPSemiSequent(mps, sequent.succedent(), true);
Matchings ma = matchesSemisequent( Matchings ma = matchesSemisequent(
MatchPathFacade.createAntecedent(mps), MatchPathFacade.createAntecedent(mps),
// new MatchPath.MPSemiSequent(mps, sequent.antecedent(), true),
pattern.antecedent()); pattern.antecedent());
return reduceConform(ms, ma); return reduceConform(ms, ma);
...@@ -98,14 +91,6 @@ public class KeyTermMatcher extends KeyTermBaseVisitor<Matchings, MatchPath> { ...@@ -98,14 +91,6 @@ public class KeyTermMatcher extends KeyTermBaseVisitor<Matchings, MatchPath> {
return ret; return ret;
} }
/* private MatchPath.MPTerm create(MatchPath.MPSequentFormula sf) {
return new MatchPath.MPTerm(sf, sf.getUnit().formula(), MatchPath.SEQUENT_FORMULA_ROOT);
}
private MatchPath.MPSequentFormula create(MatchPath.MPSemiSequent peek, int pos) {
return new MatchPath.MPSequentFormula(peek, peek.getUnit().get(pos), pos);
}
*/
/** /**
* Visit a '...'MatchPath'...' structure * Visit a '...'MatchPath'...' structure
...@@ -116,7 +101,7 @@ public class KeyTermMatcher extends KeyTermBaseVisitor<Matchings, MatchPath> { ...@@ -116,7 +101,7 @@ public class KeyTermMatcher extends KeyTermBaseVisitor<Matchings, MatchPath> {
@DispatchOn(EllipsisOp.class) @DispatchOn(EllipsisOp.class)
public Matchings visitEllipsisOp(Term pattern, MatchPath subject) { public Matchings visitEllipsisOp(Term pattern, MatchPath subject) {
Matchings matchings = new Matchings(); Matchings matchings = new Matchings();
subTerms((MatchPath.MPTerm) peek).forEach(sub -> { subTerms((MatchPath.MPTerm) subject).forEach(sub -> {
Matchings s = visit(pattern.sub(0), sub); Matchings s = visit(pattern.sub(0), sub);
matchings.addAll(s); matchings.addAll(s);
}); });
...@@ -236,7 +221,7 @@ public class KeyTermMatcher extends KeyTermBaseVisitor<Matchings, MatchPath> { ...@@ -236,7 +221,7 @@ public class KeyTermMatcher extends KeyTermBaseVisitor<Matchings, MatchPath> {
if (matchings != NO_MATCH) { if (matchings != NO_MATCH) {
String name = pattern.sub(0).op().name().toString(); String name = pattern.sub(0).op().name().toString();
for (Map<String, MatchPath> a : matchings) { for (Map<String, MatchPath> a : matchings) {
a.put(name, peek); a.put(name, subject);
} }
} }
return matchings; return matchings;
...@@ -251,7 +236,8 @@ public class KeyTermMatcher extends KeyTermBaseVisitor<Matchings, MatchPath> { ...@@ -251,7 +236,8 @@ public class KeyTermMatcher extends KeyTermBaseVisitor<Matchings, MatchPath> {
if (subject.getUnit().subs().size() != pattern.subs().size()) { if (subject.getUnit().subs().size() != pattern.subs().size()) {
return NO_MATCH; return NO_MATCH;
} }
if(pattern.equals(subject1.getUnit()))
return EMPTY_MATCH;
for (int i = 0; i < subject.getUnit().subs().size(); i++) { for (int i = 0; i < subject.getUnit().subs().size(); i++) {
Term tt = subject.getUnit().sub(i); Term tt = subject.getUnit().sub(i);
Term pt = pattern.sub(i); Term pt = pattern.sub(i);
...@@ -268,6 +254,7 @@ public class KeyTermMatcher extends KeyTermBaseVisitor<Matchings, MatchPath> { ...@@ -268,6 +254,7 @@ public class KeyTermMatcher extends KeyTermBaseVisitor<Matchings, MatchPath> {
//region helper //region helper
private String getBindingName(Name name) { private String getBindingName(Name name) {
if (name.toString().equals("?")) if (name.toString().equals("?"))
return getRandomName(); return getRandomName();
return name.toString(); return name.toString();
......
...@@ -42,8 +42,8 @@ public class KeyMatcherFacadeTest { ...@@ -42,8 +42,8 @@ public class KeyMatcherFacadeTest {
@Test @Test
public void matchSeq() throws Exception { public void matchSeq() throws Exception {
shouldMatch("p ==>", "p ==>");
shouldMatch("==> pred(a), q", "==> pred(?X:S), q"); shouldMatch("==> pred(a), q", "==> pred(?X:S), q");
shouldMatch("==> p, q", "==> ?X:Formula"); shouldMatch("==> p, q", "==> ?X:Formula");
shouldMatch("==> p, q", "==> p, q"); shouldMatch("==> p, q", "==> p, q");
shouldMatch("==> p, q", "==> q, p"); shouldMatch("==> p, q", "==> q, p");
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment