diff --git a/reactor/code/src/jetbrains/mps/unification/Unification.java b/reactor/code/src/jetbrains/mps/unification/Unification.java index ac7f0440..2df9f9da 100644 --- a/reactor/code/src/jetbrains/mps/unification/Unification.java +++ b/reactor/code/src/jetbrains/mps/unification/Unification.java @@ -309,7 +309,15 @@ public class Unification { } private void addBinding(Var v, Node n) { - myBindings.addFirst(new Binding(v, n)); + Binding bng; + if (n.isVar() && n.asVar().compareTo(v) < 0) { + bng = new Binding(n.asVar(), v); + } + else { + bng = new Binding(v, n); + } + + myBindings.addFirst(bng); } } diff --git a/reactor/tests/src/jetbrains/mps/unification/test/SolverTests.java b/reactor/tests/src/jetbrains/mps/unification/test/SolverTests.java index c6a5f74e..085882a7 100644 --- a/reactor/tests/src/jetbrains/mps/unification/test/SolverTests.java +++ b/reactor/tests/src/jetbrains/mps/unification/test/SolverTests.java @@ -39,7 +39,7 @@ public class SolverTests { var("Y"), var("X"), - bind(var("Y"), var("X")) + bind(var("X"), var("Y")) ); } @@ -69,11 +69,12 @@ public class SolverTests { ); assertUnifiesWithBindings( parse("a{b{c} Z Y X}"), - parse("a{Z Y X b{c}}"), + parse("a{Z Y X b{W}}"), bind(var("X"), parse("b{c}")), bind(var("Y"), parse("b{c}")), - bind(var("Z"), parse("b{c}")) + bind(var("Z"), parse("b{c}")), + bind(var("W"), parse("c")) ); } @@ -90,14 +91,14 @@ public class SolverTests { parse("a{X}"), parse("a{Y}"), - bind(var("Y"), var("X")) + bind(var("X"), var("Y")) ); assertUnifiesWithBindings( parse("a{b{X} c{Y}}"), parse("a{b{V} c{W}}"), - bind(var("X"), var("V")), - bind(var("Y"), var("W")) + bind(var("V"), var("X")), + bind(var("W"), var("Y")) ); } @@ -170,6 +171,38 @@ public class SolverTests { ); } + @Test + public void test10() throws Exception { + assertUnifiesWithBindings( + parseTerm("a{b{c Y} e{X} }"), + parseTerm("a{X e{b{Z d}} }"), + + bind(var("X"), parseTerm("b{c Y}")), + bind(var("Y"), parseTerm("d")), + bind(var("Z"), parseTerm("c")) + ); + } + + @Test + public void test11() throws Exception { + assertUnifiesWithBindings( + parseTerm("a{b{c d} e{f g{b{c d}}} }"), + parseTerm("a{X e{f g{X }} }"), + + bind(var("X"), parseTerm("b{c d}")) + ); + } + + @Test + public void test12() throws Exception { + assertUnifiesWithBindings( + parse("node{name{foo} child{X}}"), + parse("node{name{foo} child{Y}}"), + + bind(var("X"), var("Y")) + ); + } + @Test public void testFail1() throws Exception { assertUnifificationFails(