Skip to content

Commit

Permalink
Fix inconsistent ordering between non-linear pattern vars and concret…
Browse files Browse the repository at this point in the history 
…e terms.
  • Loading branch information
@AZWN
AZWN committed Oct 17, 2022
1 parent 5836563 commit 59a198d
Show file tree
Hide file tree
Showing 2 changed files with 43 additions and 72 deletions.
101 changes: 30 additions & 71 deletions nabl2.terms/src/main/java/mb/nabl2/terms/matching/Pattern.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -76,7 +76,7 @@ public MaybeNotInstantiated<Optional<ISubstitution.Immutable>> match(ITerm term,

/**
* Match terms against a pattern and generate additional equalities that result from the match.
*
*
* Fresh variables are generated for unmatched variables in the patterns. As a result, the resulting substitution
* has entries for all the variables in the patterns, and no pattern variables escape in the equalities.
*/
Expand Down Expand Up @@ -188,7 +188,7 @@ public static class LeftRightOrder {

/**
* Compares two patterns for generality.
*
*
* If two patterns are comparable, it return an integer indicating which patterns is more general.
* <ul>
* <li>If the first pattern is more specific than the second, c < 0.
Expand All @@ -198,7 +198,7 @@ public static class LeftRightOrder {
* </ul>
* When used as an ordering (e.g., using asComparator) patterns are sorted such that more general patterns
* appear after more specific.
*
*
*/
public Optional<Integer> compare(Pattern p1, Pattern p2) {
return Optional.ofNullable(compare(p1, p2, new AtomicInteger(), new HashMap<>(), new HashMap<>()));
Expand All @@ -223,20 +223,8 @@ public Optional<Integer> compare(Pattern p1, Pattern p2) {
c = compare(it1.next(), it2.next(), pos, vars1, vars2);
}
return c;
} else if(p2 instanceof PatternVar) {
final PatternVar var2 = (PatternVar) p2;
if(boundAt(var2, vars2) >= 0) {
return 1;
} else {
bind(var2.getVar(), vars2, pos.getAndIncrement());
return -1;
}
} else if(p2 instanceof PatternAs) {
final PatternAs as2 = (PatternAs) p2;
bind(as2.getVar(), vars2, pos.get());
return compare(p1, as2.getPattern(), pos, vars1, vars2);
} else {
return null;
return compareVar(p1, p2, pos, vars1, vars2);
}
} else if(p1 instanceof ConsPattern) {
final ConsPattern cons1 = (ConsPattern) p1;
Expand All @@ -248,78 +236,30 @@ public Optional<Integer> compare(Pattern p1, Pattern p2) {
c = compare(cons1.getTail(), cons2.getTail(), pos, vars1, vars2);
}
return c;
} else if(p2 instanceof PatternVar) {
final PatternVar var2 = (PatternVar) p2;
if(boundAt(var2, vars2) >= 0) {
return 1;
} else {
bind(var2.getVar(), vars2, pos.getAndIncrement());
return -1;
}
} else if(p2 instanceof PatternAs) {
final PatternAs as2 = (PatternAs) p2;
bind(as2.getVar(), vars2, pos.get());
return compare(p1, as2.getPattern(), pos, vars1, vars2);
} else {
return null;
return compareVar(p1, p2, pos, vars1, vars2);
}
} else if(p1 instanceof NilPattern) {
if(p2 instanceof NilPattern) {
return 0;
} else if(p2 instanceof PatternVar) {
final PatternVar var2 = (PatternVar) p2;
if(boundAt(var2, vars2) >= 0) {
return 1;
} else {
bind(var2.getVar(), vars2, pos.getAndIncrement());
return -1;
}
} else if(p2 instanceof PatternAs) {
final PatternAs as2 = (PatternAs) p2;
bind(as2.getVar(), vars2, pos.get());
return compare(p1, as2.getPattern(), pos, vars1, vars2);
} else {
return null;
return compareVar(p1, p2, pos, vars1, vars2);
}
} else if(p1 instanceof StringPattern) {
final StringPattern string1 = (StringPattern) p1;
if(p2 instanceof StringPattern) {
final StringPattern string2 = (StringPattern) p2;
return string1.getValue().equals(string2.getValue()) ? 0 : null;
} else if(p2 instanceof PatternVar) {
final PatternVar var2 = (PatternVar) p2;
if(boundAt(var2, vars2) >= 0) {
return 1;
} else {
bind(var2.getVar(), vars2, pos.getAndIncrement());
return -1;
}
} else if(p2 instanceof PatternAs) {
final PatternAs as2 = (PatternAs) p2;
bind(as2.getVar(), vars2, pos.get());
return compare(p1, as2.getPattern(), pos, vars1, vars2);
} else {
return null;
return compareVar(p1, p2, pos, vars1, vars2);
}
} else if(p1 instanceof IntPattern) {
final IntPattern integer1 = (IntPattern) p1;
if(p2 instanceof IntPattern) {
final IntPattern integer2 = (IntPattern) p2;
return integer1.getValue() == integer2.getValue() ? 0 : null;
} else if(p2 instanceof PatternVar) {
final PatternVar var2 = (PatternVar) p2;
if(boundAt(var2, vars2) >= 0) {
return 1;
} else {
bind(var2.getVar(), vars2, pos.getAndIncrement());
return -1;
}
} else if(p2 instanceof PatternAs) {
final PatternAs as2 = (PatternAs) p2;
bind(as2.getVar(), vars2, pos.get());
return compare(p1, as2.getPattern(), pos, vars1, vars2);
} else {
return null;
return compareVar(p1, p2, pos, vars1, vars2);
}
} else if(p1 instanceof PatternVar) {
final PatternVar var1 = (PatternVar) p1;
Expand Down Expand Up @@ -355,6 +295,25 @@ public Optional<Integer> compare(Pattern p1, Pattern p2) {
}
}

private Integer compareVar(Pattern p1, Pattern p2, AtomicInteger pos, Map<ITermVar, Integer> vars1,
Map<ITermVar, Integer> vars2) {
if(p2 instanceof PatternVar) {
final PatternVar var2 = (PatternVar) p2;
if(boundAt(var2, vars2) == -1) {
bind(var2.getVar(), vars2, pos.getAndIncrement());
}
return -1;
} else if(p2 instanceof PatternAs) {
final PatternAs as2 = (PatternAs) p2;
bind(as2.getVar(), vars2, pos.get());
return compare(p1, as2.getPattern(), pos, vars1, vars2);
} else {
return null;
}
}

// Binding positions of variables.

private int boundAt(PatternVar vp, Map<ITermVar, Integer> vars) {
final @Nullable ITermVar v = vp.getVar();
if(v == null) {
Expand All @@ -378,10 +337,10 @@ private void bind(@Nullable ITermVar v, Map<ITermVar, Integer> vars, int pos) {

/**
* Return a comparator for patterns.
*
*
* Can be used to order patterns. It cannot not differentiate between incomparable patterns, and equivalent
* patterns: both return 0.
*
*
* Note: this comparator imposes orderings that are inconsistent with equals.
*/
public java.util.Comparator<Pattern> asComparator() {
Expand All @@ -394,4 +353,4 @@ public java.util.Comparator<Pattern> asComparator() {

}

}
}
14 changes: 13 additions & 1 deletion nabl2.terms/src/test/java/mb/nabl2/terms/matching/TermPatternOrderTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -110,6 +110,18 @@ public class TermPatternOrderTest {
assertFirstPatternMoreSpecificThanSecond(p1, p2);
}

@Test public void testNonLinearString() {
Pattern p1 = P.newTuple(P.newVar("x"), P.newVar("x"));
Pattern p2 = P.newTuple(P.newVar("x"), x);
assertFirstPatternMoreGeneralThanSecond(p1, p2);
}

@Test public void testNonLinearAsString() {
Pattern p1 = P.newTuple(P.newVar("x"), P.newVar("x"));
Pattern p2 = P.newTuple(P.newVar("x"), P.newAs("y", x));
assertFirstPatternMoreGeneralThanSecond(p1, p2);
}

//----------------------------------------------------------------------

private static void assertEquivalentPatterns(Pattern p1, Pattern p2) {
Expand Down Expand Up @@ -140,4 +152,4 @@ private static void assertIncomparablePatterns(Pattern p1, Pattern p2) {
assertFalse("Assymetric order", c2.isPresent());
}

}
}

0 comments on commit 59a198d

Please sign in to comment.