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

Support for unassigned logical variables in unification. Fix cycle not detected.

This commit is contained in:
Fedor Isakov 2019-01-25 11:37:18 +01:00
parent b523467c5f
commit e645ac8a70
2 changed files with 51 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
reactor/Core/src/jetbrains/mps/unification/TermGraphUnifier.kt
View File

@ -18,6 +18,7 @@ package jetbrains.mps.unification
import gnu.trove.list.array.TIntArrayList
import gnu.trove.map.hash.TIntObjectHashMap
import jetbrains.mps.logic.reactor.logical.Logical
import jetbrains.mps.unification.Substitution.FailureCause.CYCLE_DETECTED
import jetbrains.mps.unification.Substitution.FailureCause.SYMBOL_CLASH
import jetbrains.mps.unification.Term.Kind.*
@ -294,13 +295,15 @@ class TermGraphUnifier {
return wrapper.unwrap(origin[t])
}
private fun idSymbol(symbol: Any): Any {
return if (symbol is String) symbol.intern() else symbol
}
private fun idSymbol(symbol: Any): Any =
when (symbol) {
is String -> symbol.intern()
is Logical<*> -> symbol.findRoot()
else -> symbol
}
private fun Any?.eq (that: Any?): Boolean {
return if (this == null) that == null else this.equals(that)
}
}

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

@ -16,6 +16,9 @@
package jetbrains.mps.unification.test;
import jetbrains.mps.logic.reactor.core.LogicalImpl;
import jetbrains.mps.logic.reactor.logical.MetaLogical;
import jetbrains.mps.unification.Substitution;
import jetbrains.mps.unification.Term;
import jetbrains.mps.unification.TermWrapper;
import org.jetbrains.annotations.NotNull;
@ -543,4 +546,44 @@ public class SolverTests {
}
@Test
public void joinedLogicals() throws Exception {
MetaLogical<Term> X = new MetaLogical<>("X", Term.class);
MetaLogical<Term> Y = new MetaLogical<>("Y", Term.class);
MetaLogical<Term> Z = new MetaLogical<>("Z", Term.class);
LogicalImpl<Term> xLogical = new LogicalImpl<>(X);
LogicalImpl<Term> yLogical = new LogicalImpl<>(Y);
LogicalImpl<Term> zLogical = new LogicalImpl<>(Z);
Term left = term("foo", term("bar", logicalVar(yLogical)), logicalVar(zLogical));
Term right = term("foo", term("bar", logicalVar(xLogical)), logicalVar(zLogical));
assertUnifiesWithBindings(left, right,
new Substitution.Binding(logicalVar(xLogical), logicalVar(yLogical)));
xLogical.union(yLogical);
assertUnifiesWithBindings(left, right);
}
@Test
public void joinedLogicals_cycle() throws Exception {
MetaLogical<Term> X = new MetaLogical<>("X", Term.class);
MetaLogical<Term> Y = new MetaLogical<>("Y", Term.class);
MetaLogical<Term> Z = new MetaLogical<>("Z", Term.class);
LogicalImpl<Term> xLogical = new LogicalImpl<>(X);
LogicalImpl<Term> yLogical = new LogicalImpl<>(Y);
LogicalImpl<Term> zLogical = new LogicalImpl<>(Z);
Term left = logicalVar(yLogical);
Term right = term("foo", term("bar", logicalVar(xLogical)), logicalVar(zLogical));
assertUnifiesWithBindings(left, right,
new Substitution.Binding(left, right));
xLogical.union(yLogical);
assertUnificationFails(left, right,
CYCLE_DETECTED);
}
}