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

Optimize and refactor TermGraphUnifier. Beautify the code. 

Avoid internalizing a (sub-)term that has not been unified with
 a variable, thus saving on unnecessary accounting.
This commit is contained in:
Fedor Isakov 2020-06-04 11:37:41 +02:00
parent 04c2dfb385
commit c24f4f75a4
1 changed files with 107 additions and 80 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -17,6 +17,7 @@
package jetbrains.mps.unification
import gnu.trove.list.array.TIntArrayList
import gnu.trove.map.hash.TIntIntHashMap
import gnu.trove.map.hash.TIntObjectHashMap
import jetbrains.mps.logic.reactor.logical.Logical
import jetbrains.mps.unification.Substitution.FailureCause.CYCLE_DETECTED
@ -53,6 +54,7 @@ import java.util.*
*/
typealias IntList = TIntArrayList
typealias IntIntHashMap = TIntIntHashMap
typealias IntAnyHashMap<V> = TIntObjectHashMap<V>
class TermGraphUnifier(private val wrapper: TermWrapper = TermWrapper.ID,
@ -65,57 +67,72 @@ class TermGraphUnifier(private val wrapper: TermWrapper = TermWrapper.ID,
}
fun unify(a: Term, b: Term): Substitution {
return if (unifClosure(toInner(a), toInner(b))) {
findSolution(toInner(a))
return if (unifClosure(toInt(a), toInt(b))) {
findSolution(a, Unification.EMPTY_SUBSTITUTION)
} else {
failedSubstitution(failureCause, *failureDetails)
}
}
private fun findSolution(s: Int): Substitution {
return findSolution(s, Unification.EMPTY_SUBSTITUTION)
}
private fun findSolution(s: Int, defSubs: Substitution) : Substitution {
val (_, z) = findSchema(s)
val vars = innerVars[find(z)]
if (isAcyclic(z)) { return defSubs } // not part of a cycle
if (isVisited(z)) { return failedSubstitution(CYCLE_DETECTED) } // there exists a cycle
private fun findSolution(term: Term, defSubs: Substitution) : Substitution {
var subs = defSubs
if (origin[z].`is`(FUN)) {
setVisited(z)
for (c in origin[z].arguments()) {
subs = findSolution(toInner(c), subs)
if (!subs.isSuccessful) break
}
clearVisited(z)
}
if (subs.isSuccessful) {
setAcyclic(z)
// avoid unnecessary instatiation
val success = if (subs is SuccessfulSubstitution) subs as SuccessfulSubstitution
else SuccessfulSubstitution(subs)
if (vars != null) {
for (v in vars) {
if (trivialBindings || v != z) {
// Keep the order of variables within a binding
if (origin[z].`is`(VAR) && origin[z].compareTo(origin[v]) < 0) {
success.addBinding(fromInner(z), fromInner(v))
} else {
success.addBinding(fromInner(v), fromInner(z))
}
}
// use the "shortcut" solution for terms that have not been internalized,
// meaning such terms have not gone through a unification, thus have not
// been assigned either class or schema
if (!isInternalized(term)) {
if (term.`is`(FUN)) {
for (c in term.arguments()) {
subs = findSolution(c, subs)
if (!subs.isSuccessful) break
}
} else {
// VAR or REF has to be processed recursively to account for
// possible cycles
toInt(term)
}
}
if (isInternalized(term)) {
val (_, z) = findSchema(toInt(term))
val vars = intVars[find(z)]
if (isAcyclic(z)) { return defSubs } // not part of a cycle
if (isVisited(z)) { return failedSubstitution(CYCLE_DETECTED) } // there exists a cycle
if (origin[z].`is`(FUN)) {
setVisited(z)
for (c in origin[z].arguments()) {
subs = findSolution(c, subs)
if (!subs.isSuccessful) break
}
clearVisited(z)
}
subs = success
if (subs.isSuccessful) {
setAcyclic(z)
// avoid unnecessary instatiation
val success = if (subs is SuccessfulSubstitution) subs as SuccessfulSubstitution
else SuccessfulSubstitution(subs)
if (vars != null) {
for (v in vars) {
if (trivialBindings || v != z) {
// Keep the order of variables within a binding
if (origin[z].`is`(VAR) && origin[z].compareTo(origin[v]) < 0) {
success.addBinding(fromInner(z), fromInner(v))
} else {
success.addBinding(fromInner(v), fromInner(z))
}
}
}
}
subs = success
}
}
return subs
@ -148,7 +165,7 @@ class TermGraphUnifier(private val wrapper: TermWrapper = TermWrapper.ID,
val zsit = origin[zs].arguments().iterator()
val ztit = origin[zt].arguments().iterator()
while (zsit.hasNext() && ztit.hasNext()) {
if (!unifClosure(toInner(zsit.next()), toInner(ztit.next()))) {
if (!unifClosure(toInt(zsit.next()), toInt(ztit.next()))) {
return false // arguments mismatch
}
}
@ -187,9 +204,9 @@ class TermGraphUnifier(private val wrapper: TermWrapper = TermWrapper.ID,
}
setSize(s, ssize + tsize)
prependVars(s, innerVars[t])
prependVars(s, intVars[t])
setKlass(t, s)
// copy the schema
val zs = schema(s)
val zt = schema(t)
@ -223,9 +240,9 @@ class TermGraphUnifier(private val wrapper: TermWrapper = TermWrapper.ID,
private fun prependVars(t: Int, vars: TIntArrayList?) {
if (vars?.isEmpty ?: true) { return }
val newVars = IntList(innerVars[t] ?: EMPTY_LIST)
val newVars = IntList(intVars[t] ?: EMPTY_LIST)
newVars.addAll(vars)
innerVars.put (t, newVars)
intVars.put (t, newVars)
}
@ -241,36 +258,35 @@ class TermGraphUnifier(private val wrapper: TermWrapper = TermWrapper.ID,
private fun getRef(zs: Int): Int =
if (origin[zs].`is`(REF))
toInner(origin[zs].get())
toInt(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
return if (backref.containsKey(key)) {
backref[key] !!
private fun toInt(term: Term): Int {
val key = intKey(term)
return if (terms.containsKey(key)) {
terms[key]
} else {
val wrapped = wrapper.wrap(term)
val next = origin.size
origin.add(wrapped)
// initialize internal structures
innerSchema.add(next)
innerClass.add(next)
innerSize.add(1)
innerAcyclic.add(0)
innerVisited.add(0)
terms.put(key, next)
initData(next)
if (wrapped.`is`(VAR)) {
innerVars.put(next, IntList(intArrayOf(next)))
intVars.put(next, IntList(intArrayOf(next)))
}
backref.put(key, next)
next
}
}
private fun isInternalized(term: Term): Boolean = terms.containsKey(intKey(term))
private fun intKey(term: Term) =
// Variables with matching symbols are all treated as a single term.
System.identityHashCode(if (term.`is`(VAR)) idSymbol(term.symbol()) else term)
private fun fromInner(t: Int): Term {
return wrapper.unwrap(origin[t])
}
@ -286,36 +302,47 @@ class TermGraphUnifier(private val wrapper: TermWrapper = TermWrapper.ID,
return if (this == null) that == null else this.equals(that)
}
private fun klass(t: Int): Int = innerClass[t]
private fun initData(nextId: Int) {
// initialize internal structures
intSchema.add(nextId)
intClass.add(nextId)
intSize.add(1)
intAcyclic.add(0)
intVisited.add(0)
}
private fun setKlass(t: Int, klass: Int): Unit { innerClass[t] = klass }
private fun schema(t: Int): Int = intSchema[t]
private fun schema(t: Int): Int = innerSchema[t]
private fun setSchema(t: Int, schema: Int) { intSchema[t] = schema }
private fun setSchema(t: Int, schema: Int): Unit { innerSchema[t] = schema }
private fun klass(t: Int): Int = intClass[t]
private fun size(t: Int): Int = innerSize[t]
private fun setKlass(t: Int, klass: Int) { intClass[t] = klass }
private fun setSize(t: Int, size: Int): Unit { innerSize[t] = size }
private fun size(t: Int): Int = intSize[t]
private fun isAcyclic(t: Int): Boolean = innerAcyclic[t] != 0
private fun setSize(t: Int, size: Int) { intSize[t] = size }
private fun setAcyclic(t: Int): Unit { innerAcyclic[t] = 1 }
private fun isAcyclic(t: Int): Boolean = (intAcyclic[t]) != 0
private fun isVisited(t: Int): Boolean = innerVisited[t] != 0
private fun setAcyclic(t: Int) { intAcyclic[t] = 1 }
private fun setVisited(t: Int): Unit { innerVisited[t] = 1 }
private fun isVisited(t: Int): Boolean = intVisited[t] != 0
private fun clearVisited(t: Int): Unit { innerVisited[t] = 0 }
private fun setVisited(t: Int) { intVisited[t] = 1 }
private fun clearVisited(t: Int) { intVisited[t] = 0 }
private var failureCause: Substitution.FailureCause = Substitution.FailureCause.UKNOWN
private var failureDetails = emptyArray<Any?>()
private val backref = IdentityHashMap<Any?, Int>()
private val innerVars = IntAnyHashMap<IntList?>()
private val origin = ArrayList<Term>()
private val innerClass = IntList()
private val innerSchema = IntList()
private val innerSize = IntList()
private val innerAcyclic = IntList()
private val innerVisited = IntList()
}
private val terms = IntIntHashMap()
private val intVars = IntAnyHashMap<IntList?>()
private val intClass = IntList()
private val intSchema = IntList()
private val intSize = IntList()
private val intAcyclic = IntList()
private val intVisited = IntList()
}