natas_hw
/
mps-coderules
mirror of https://github.com/JetBrains/mps-coderules
0
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Add tests for unification of terms with var refs

This commit is contained in:
Grigorii Kirgizov 2020-03-06 13:54:21 +03:00
parent f71d734853
commit df1750fee6
1 changed files with 60 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

60
reactor/Test/test/jetbrains/mps/unification/test/SolverTests.java
View File

@ -319,6 +319,12 @@ public class SolverTests {
bind(var("X"), var("Y"))
);
assertUnifiesWithBindings(
MockTermsParser.parseTerm("f{^X}"),
MockTermsParser.parseTerm("f{ Y}"),
bind(var("X"), var("Y"))
);
assertUnifiesWithBindings(
MockTermsParser.parseTerm("a{b ^X}"),
MockTermsParser.parseTerm("a{b c{d}}"),
@ -568,6 +574,60 @@ public class SolverTests {
);
}
@Test
public void testFailCyclicVarRef() throws Exception {
// assertUnificationFails(
// MockTermsParser.parseTerm("X"),
// MockTermsParser.parseTerm("f{^X}"),
//
// CYCLE_DETECTED
// );
// assertUnificationFails(
// MockTermsParser.parseTerm("f{X}"),
// MockTermsParser.parseTerm("f{f{^X}}"),
//
// CYCLE_DETECTED
// );
// assertUnificationFails(
// MockTermsParser.parseTerm("t {@1 f{X} g{^1}}"),
// MockTermsParser.parseTerm("t { f{X} X }"),
//
// CYCLE_DETECTED
// );
// assertUnificationFails(
// MockTermsParser.parseTerm("t { f{^X} X }"),
// MockTermsParser.parseTerm("t { Y g{^Y} }"),
//
// CYCLE_DETECTED
// );
// pass
assertUnificationFails(
MockTermsParser.parseTerm("t { ^X Y }"),
MockTermsParser.parseTerm("t { Y f{X} }"),
CYCLE_DETECTED
);
assertUnificationFails(
MockTermsParser.parseTerm("t { X Y }"),
MockTermsParser.parseTerm("t { f{Y} ^X }"),
CYCLE_DETECTED
);
assertUnificationFails(
MockTermsParser.parseTerm("t { ^X Y }"),
MockTermsParser.parseTerm("t { f{Y} ^X }"),
CYCLE_DETECTED
);
// fixme: infinitely cycles !!
assertUnificationFails(
MockTermsParser.parseTerm("t { ^X ^Y }"),
MockTermsParser.parseTerm("t { Y f{X} }"),
CYCLE_DETECTED
);
}
@Test
public void joinedLogicals() throws Exception {