diff --git a/reactor/code/src/jetbrains/mps/unification/Unification.java b/reactor/code/src/jetbrains/mps/unification/Unification.java index fa92dfd7..de82be01 100644 --- a/reactor/code/src/jetbrains/mps/unification/Unification.java +++ b/reactor/code/src/jetbrains/mps/unification/Unification.java @@ -64,6 +64,9 @@ public class Unification { while(scit.hasNext() && tcit.hasNext()) { if (!unifClosure(scit.next(), tcit.next())) return false; } + if (scit.hasNext() != tcit.hasNext()) { + return false; // children lists are of different size + } } else { return false; // symbol clash diff --git a/reactor/tests/src/jetbrains/mps/unification/SolverTests.java b/reactor/tests/src/jetbrains/mps/unification/SolverTests.java index 5f8c0a4f..29777bb8 100644 --- a/reactor/tests/src/jetbrains/mps/unification/SolverTests.java +++ b/reactor/tests/src/jetbrains/mps/unification/SolverTests.java @@ -60,20 +60,20 @@ public class SolverTests { bind(var("Y"), term("c")) ); assertUnifiesWithBindings( - parse("a{b X Y Z}"), - parse("a{X Y Z b{e}}"), + parse("a{b{c} X Y Z}"), + parse("a{X Y Z b{c}}"), - bind(var("X"), term("b")), - bind(var("Y"), term("b")), - bind(var("Z"), term("b")) + bind(var("X"), parse("b{c}")), + bind(var("Y"), parse("b{c}")), + bind(var("Z"), parse("b{c}")) ); assertUnifiesWithBindings( - parse("a{b Z Y X}"), - parse("a{Z Y X b{e}}"), + parse("a{b{c} Z Y X}"), + parse("a{Z Y X b{c}}"), - bind(var("X"), term("b")), - bind(var("Y"), term("b")), - bind(var("Z"), term("b")) + bind(var("X"), parse("b{c}")), + bind(var("Y"), parse("b{c}")), + bind(var("Z"), parse("b{c}")) ); } @@ -149,7 +149,7 @@ public class SolverTests { @Test public void test8() throws Exception { assertUnifiesWithBindings( - parseTerm("a{b{c d} e{f g} }"), + parseTerm("a{b{c d} e{f} }"), parseTerm("a{b{X Y} e{Z} }"), bind(var("X"), parseTerm("c")), @@ -158,13 +158,32 @@ public class SolverTests { ); } + @Test + public void test9() throws Exception { + assertUnifiesWithBindings( + parseTerm("a{b{c d} e{X} }"), + parseTerm("a{b{X Y} e{Z} }"), + + bind(var("X"), parseTerm("c")), + bind(var("Y"), parseTerm("d")), + bind(var("Z"), parseTerm("c")) + ); + } + @Test public void testFail1() throws Exception { assertUnifificationFails( term("a"), term("b") ); + } + @Test + public void testFail2() throws Exception { + assertUnifificationFails( + parse("a{b c}"), + parse("a{X}") + ); } }