From 59a198db27bb8ffe9c5e4b30baecfd1fbdfd8099 Mon Sep 17 00:00:00 2001 From: Aron Zwaan Date: Mon, 17 Oct 2022 17:59:39 +0200 Subject: [PATCH] Fix inconsistent ordering between non-linear pattern vars and concrete terms. --- .../java/mb/nabl2/terms/matching/Pattern.java | 101 ++++++------------ .../terms/matching/TermPatternOrderTest.java | 14 ++- 2 files changed, 43 insertions(+), 72 deletions(-) diff --git a/nabl2.terms/src/main/java/mb/nabl2/terms/matching/Pattern.java b/nabl2.terms/src/main/java/mb/nabl2/terms/matching/Pattern.java index d60204c2d..e57f9e075 100644 --- a/nabl2.terms/src/main/java/mb/nabl2/terms/matching/Pattern.java +++ b/nabl2.terms/src/main/java/mb/nabl2/terms/matching/Pattern.java @@ -76,7 +76,7 @@ public MaybeNotInstantiated> 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. */ @@ -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. * * When used as an ordering (e.g., using asComparator) patterns are sorted such that more general patterns * appear after more specific. - * + * */ public Optional compare(Pattern p1, Pattern p2) { return Optional.ofNullable(compare(p1, p2, new AtomicInteger(), new HashMap<>(), new HashMap<>())); @@ -223,20 +223,8 @@ public Optional 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; @@ -248,78 +236,30 @@ public Optional 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; @@ -355,6 +295,25 @@ public Optional compare(Pattern p1, Pattern p2) { } } + private Integer compareVar(Pattern p1, Pattern p2, AtomicInteger pos, Map vars1, + Map 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 vars) { final @Nullable ITermVar v = vp.getVar(); if(v == null) { @@ -378,10 +337,10 @@ private void bind(@Nullable ITermVar v, Map 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 asComparator() { @@ -394,4 +353,4 @@ public java.util.Comparator asComparator() { } -} \ No newline at end of file +} diff --git a/nabl2.terms/src/test/java/mb/nabl2/terms/matching/TermPatternOrderTest.java b/nabl2.terms/src/test/java/mb/nabl2/terms/matching/TermPatternOrderTest.java index a7b7816a4..1d2bcba70 100644 --- a/nabl2.terms/src/test/java/mb/nabl2/terms/matching/TermPatternOrderTest.java +++ b/nabl2.terms/src/test/java/mb/nabl2/terms/matching/TermPatternOrderTest.java @@ -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) { @@ -140,4 +152,4 @@ private static void assertIncomparablePatterns(Pattern p1, Pattern p2) { assertFalse("Assymetric order", c2.isPresent()); } -} \ No newline at end of file +}