From c7fb0502cceb510c5a3677965b49100fe2695672 Mon Sep 17 00:00:00 2001 From: Fedor Isakov Date: Tue, 10 Mar 2020 14:18:03 +0100 Subject: [PATCH] Dereference all refs within term on unification. Method findSolution now walks all refs inside a term. This guarantees no "hidden" cycles, but also breaks the "cyclic term" feature. --- .../mps/unification/TermGraphUnifier.kt | 63 +++++++++---------- .../mps/unification/test/SolverTests.java | 58 +++++++++-------- 2 files changed, 63 insertions(+), 58 deletions(-) diff --git a/reactor/Core/src/jetbrains/mps/unification/TermGraphUnifier.kt b/reactor/Core/src/jetbrains/mps/unification/TermGraphUnifier.kt index 9df260ca..2e95de2d 100644 --- a/reactor/Core/src/jetbrains/mps/unification/TermGraphUnifier.kt +++ b/reactor/Core/src/jetbrains/mps/unification/TermGraphUnifier.kt @@ -58,7 +58,7 @@ typealias IntAnyHashMap = TIntObjectHashMap class TermGraphUnifier { companion object { - val EMPTY =TIntArrayList.wrap(kotlin.IntArray(0)) + val EMPTY_LIST = TIntArrayList.wrap(kotlin.IntArray(0)) } private var wrapper: TermWrapper @@ -97,7 +97,8 @@ class TermGraphUnifier { } private fun findSolution(s: Int, defSubs: Substitution) : Substitution { - val z = innerSchema[find(s)] + val (_, z) = findSchema(s) + val vars = innerVars[find(z)] if (innerAcyclic[z]) { return defSubs } // not part of a cycle if (innerVisited[z]) { return failedSubstitution(CYCLE_DETECTED) } // there exists a cycle @@ -105,22 +106,21 @@ class TermGraphUnifier { var subs = defSubs if (origin[z].`is`(FUN)) { innerVisited.set(z) - for (c in origin[z].arguments()) { - subs = findSolution(toInner(c), subs) + val (_, zc) = findSchema(toInner(c)) + subs = findSolution(zc, subs) if (!subs.isSuccessful) break } - - innerVisited.set(z) + innerVisited.clear(z) } if (subs.isSuccessful) { innerAcyclic.set(z) // avoid unnecessary instatiation - val success = if (subs is SuccessfulSubstitution) subs else SuccessfulSubstitution(subs) + val success = if (subs is SuccessfulSubstitution) subs as SuccessfulSubstitution + else SuccessfulSubstitution(subs) - val vars = innerVars[find(z)] if (vars != null) { for (v in vars) { if (v != z) { @@ -143,23 +143,10 @@ class TermGraphUnifier { private fun unifClosure(a: Int, b: Int): Boolean { - var s = find(a) - var t = find(b) + if (find(a) == find(b)) { return true } - if (s == t) { return true } - - var zs = innerSchema[s] - var zt = innerSchema[t] - - while (origin[zs].`is`(REF)) { - s = union(s, getRef(zs)) - zs = innerSchema[s] - } - - while (origin[zt].`is`(REF)) { - t = union(t, getRef(zt)) - zt = innerSchema[t] - } + val (s, zs) = findSchema(a) + val (t, zt) = findSchema(b) // a VAR always matches another term if (origin[zs].`is`(VAR) || origin[zt].`is`(VAR)) { @@ -188,14 +175,13 @@ class TermGraphUnifier { // fail if different arguments count return zsit.hasNext() == ztit.hasNext() - + } else { // something's wrong with the input throw IllegalStateException("invalid input") } } - private fun union(a: Int, b: Int): Int { var s = find(a) var t = find(b) @@ -230,13 +216,14 @@ class TermGraphUnifier { if (origin[zs].`is`(REF)) { innerSchema[s] = zt - } else if (origin[zs].`is`(VAR) && !(origin[zt].`is`(VAR))) { + } else if (origin[zs].`is`(VAR) && (origin[zt].`is`(FUN))) { innerSchema[s] = zt } return s } + private fun find(t: Int): Int { var repr = innerClass[t] if (repr == t) { return repr } @@ -257,19 +244,31 @@ class TermGraphUnifier { return repr } - private fun prependVars(t: Int, vars: TIntArrayList?) { if (vars?.isEmpty ?: true) { return } - val newVars = IntList(innerVars[t] ?: EMPTY) + val newVars = IntList(innerVars[t] ?: EMPTY_LIST) newVars.addAll(vars) innerVars.put (t, newVars) } - private fun getRef(zs: Int): Int { - return if (origin[zs].`is`(REF)) toInner(origin[zs].get()) else zs + + private fun findSchema(s: Int): Pair { + var t = find(s) + var zt = innerSchema[t] + while (origin[zt].`is`(REF)) { + t = union(t, getRef(zt)) + zt = innerSchema[t] + } + return t to zt } + private fun getRef(zs: Int): Int = + if (origin[zs].`is`(REF)) + toInner(origin[zs].get()) + else + zs + private fun toInner(term: Term): Int { // Variables with matching symbols are all treated as a single term. val key = if (term.`is`(VAR)) idSymbol(term.symbol()) else term @@ -298,7 +297,7 @@ class TermGraphUnifier { private fun idSymbol(symbol: Any): Any = when (symbol) { is String -> symbol.intern() - is Logical<*> -> symbol.findRoot() + is Logical<*> -> symbol.findRoot() else -> symbol } diff --git a/reactor/Test/test/jetbrains/mps/unification/test/SolverTests.java b/reactor/Test/test/jetbrains/mps/unification/test/SolverTests.java index 58f68646..9d5b730b 100644 --- a/reactor/Test/test/jetbrains/mps/unification/test/SolverTests.java +++ b/reactor/Test/test/jetbrains/mps/unification/test/SolverTests.java @@ -23,6 +23,7 @@ import jetbrains.mps.unification.Substitution; import jetbrains.mps.unification.Term; import jetbrains.mps.unification.TermWrapper; import org.jetbrains.annotations.NotNull; +import org.junit.Ignore; import org.junit.Test; import java.util.Collection; @@ -288,7 +289,9 @@ public class SolverTests { ); } + // FIXME cyclic terms are no longer supported @Test + @Ignore public void testCyclicVar() throws Exception { assertUnifiesWithBindings( MockTermsParser.parseTerm("@1 a{b ^1}"), @@ -576,32 +579,36 @@ 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 -// ); + assertUnificationFails( + MockTermsParser.parseTerm("X"), + MockTermsParser.parseTerm("f{^X}"), - // pass + 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 {@1 f{X} g{^1}}"), + MockTermsParser.parseTerm("t { f{Y} Y }"), + + CYCLE_DETECTED + ); + assertUnificationFails( + MockTermsParser.parseTerm("t { f{^X} X }"), + MockTermsParser.parseTerm("t { Y g{^Y} }"), + + CYCLE_DETECTED + ); assertUnificationFails( MockTermsParser.parseTerm("t { ^X Y }"), MockTermsParser.parseTerm("t { Y f{X} }"), @@ -620,7 +627,6 @@ public class SolverTests { CYCLE_DETECTED ); - // fixme: infinitely cycles !! assertUnificationFails( MockTermsParser.parseTerm("t { ^X ^Y }"), MockTermsParser.parseTerm("t { Y f{X} }"),