Minor code reorganization and refactoring. Extract MatchingProbe interface.

This commit is contained in:
Fedor Isakov 2018-10-04 10:53:00 +02:00
parent 834010e2d1
commit bc69a2e291
8 changed files with 277 additions and 178 deletions

View File

@ -26,34 +26,36 @@ import jetbrains.mps.logic.reactor.program.Rule
* @author Fedor Isakov
*/
typealias Matcher = RuleMatcher
class Dispatcher (val ruleIndex: RuleIndex) {
private val rule2matcher = HashMap<Rule, RuleMatcher>()
private val rule2matcher = HashMap<Rule, Matcher>()
init {
ruleIndex.forEach { rule ->
val matcher = RuleMatcher(rule)
val matcher = Matcher(rule)
rule2matcher.put(rule, matcher);
}
}
inner class DispatchFringe {
private var rule2fringe: PersMap<Rule, RuleMatcher.MatchFringe>
private var rule2probe: PersMap<Rule, MatchingProbe>
private val allMatches = arrayListOf<MatchRule>()
constructor() {
this.rule2fringe = Maps.of()
this.rule2probe = Maps.of()
rule2matcher.entries.forEach { e ->
this.rule2fringe = rule2fringe.put(e.key, e.value.fringe())
this.rule2probe = rule2probe.put(e.key, e.value.probe())
}
}
constructor(pred: DispatchFringe, matching: Iterable<RuleMatcher.MatchFringe>) {
this.rule2fringe = pred.rule2fringe
constructor(pred: DispatchFringe, matching: Iterable<MatchingProbe>) {
this.rule2probe = pred.rule2probe
matching.forEach { fringe ->
this.rule2fringe = rule2fringe.put(fringe.rule(), fringe)
this.rule2probe = rule2probe.put(fringe.rule(), fringe)
allMatches.addAll(fringe.matches())
}
}
@ -63,16 +65,16 @@ class Dispatcher (val ruleIndex: RuleIndex) {
fun activated(active: ConstraintOccurrence): DispatchFringe {
return DispatchFringe(this,
ruleIndex.forOccurrenceWithMask(active).mapNotNull { (rule, mask) ->
rule2fringe[rule]?.expand(active, mask)
rule2probe[rule]?.expand(active, mask)
})
}
fun discarded(discarded: ConstraintOccurrence): DispatchFringe {
return DispatchFringe(this,
ruleIndex.forOccurrence(discarded).mapNotNull { rule ->
rule2fringe[rule]
rule2probe[rule]
}.map { fringe ->
fringe.cleanup(discarded)
fringe.contract(discarded)
})
}

View File

@ -0,0 +1,55 @@
/*
* Copyright 2014-2018 JetBrains s.r.o.
*
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
* You may obtain a copy of the License at
*
* http://www.apache.org/licenses/LICENSE-2.0
*
* Unless required by applicable law or agreed to in writing, software
* distributed under the License is distributed on an "AS IS" BASIS,
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
* See the License for the specific language governing permissions and
* limitations under the License.
*/
package jetbrains.mps.logic.reactor.core
import jetbrains.mps.logic.reactor.evaluation.ConstraintOccurrence
import jetbrains.mps.logic.reactor.evaluation.MatchRule
import jetbrains.mps.logic.reactor.logical.Logical
import jetbrains.mps.logic.reactor.logical.LogicalContext
import jetbrains.mps.logic.reactor.logical.LogicalOwner
import jetbrains.mps.logic.reactor.logical.MetaLogical
import jetbrains.mps.logic.reactor.program.Rule
class MatchRuleImpl(val rule: Rule,
val subst: Subst,
val headKept: MutableIterable<ConstraintOccurrence?>,
val headReplaced: MutableIterable<ConstraintOccurrence?>) : MatchRule {
private val logicalContext = object : LogicalContext {
val meta2logical = HashMap<MetaLogical<*>, Logical<*>>()
override fun <V : Any> variable(meta: MetaLogical<V>): Logical<V> =
(meta2logical[meta] ?: subst[meta]?.let { value ->
when (value) {
is Logical<*> -> value
is LogicalOwner -> value.logical()
else -> LogicalImpl(value)
}
} ?: meta.logical().also { logical -> meta2logical[meta] = logical }) as Logical<V>
}
override fun rule(): Rule = rule
override fun matchHeadKept(): MutableIterable<ConstraintOccurrence?> = headKept
override fun matchHeadReplaced(): MutableIterable<ConstraintOccurrence?> = headReplaced
override fun logicalContext(): LogicalContext = logicalContext
}

View File

@ -0,0 +1,40 @@
/*
* Copyright 2014-2018 JetBrains s.r.o.
*
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
* You may obtain a copy of the License at
*
* http://www.apache.org/licenses/LICENSE-2.0
*
* Unless required by applicable law or agreed to in writing, software
* distributed under the License is distributed on an "AS IS" BASIS,
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
* See the License for the specific language governing permissions and
* limitations under the License.
*/
package jetbrains.mps.logic.reactor.core
import jetbrains.mps.logic.reactor.evaluation.ConstraintOccurrence
import jetbrains.mps.logic.reactor.evaluation.MatchRule
import jetbrains.mps.logic.reactor.program.Rule
import java.util.*
/**
* @author Fedor Isakov
*/
interface MatchingProbe {
fun rule() : Rule
fun matches() : Collection<MatchRule>
fun expand(occ: ConstraintOccurrence) : MatchingProbe
fun expand(occ: ConstraintOccurrence, mask: BitSet) : MatchingProbe
fun contract(occ: ConstraintOccurrence): MatchingProbe
}

View File

@ -0,0 +1,132 @@
/*
* Copyright 2014-2018 JetBrains s.r.o.
*
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
* You may obtain a copy of the License at
*
* http://www.apache.org/licenses/LICENSE-2.0
*
* Unless required by applicable law or agreed to in writing, software
* distributed under the License is distributed on an "AS IS" BASIS,
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
* See the License for the specific language governing permissions and
* limitations under the License.
*/
package jetbrains.mps.logic.reactor.core
import jetbrains.mps.logic.reactor.evaluation.ConstraintOccurrence
import jetbrains.mps.logic.reactor.logical.Logical
import jetbrains.mps.logic.reactor.logical.LogicalOwner
import jetbrains.mps.logic.reactor.logical.MetaLogical
import jetbrains.mps.logic.reactor.program.Constraint
import jetbrains.mps.unification.Term
typealias Subst = Map<MetaLogical<*>, Any>
fun emptySubst() = HashMap<MetaLogical<*>, Any>(4)
class OccurrenceMatcher(contextSubst: Subst = emptySubst()) {
private val matchSubst = HashMap(contextSubst)
fun substitution(): Subst = matchSubst
/**
* Matches constraint and occurrence.
* Recursively processes all arguments, including terms.
* Returns substitution of MetaLogical instances on success, null otherwise.
*/
fun matches(cst: Constraint, occ: ConstraintOccurrence): Boolean
{
if (cst.symbol() != occ.constraint().symbol()) return false
return zipWhileTrue(cst.arguments(), occ.arguments()) { cstarg, occarg ->
matchAny(cstarg, occarg)
}
}
/**
* Returns true for matching left and right parameters, false otherwise.
*/
fun match(left: Any?, right: Any?): Boolean {
return matchAny(left, right)
}
/**
* Matches target against pattern.
* Recursively iterates terms.
* Respects substitutions for MetaLogical instances.
* Returns either new substitution on successful match, or null.
*/
private fun matchAny(ptn: Any?, trg: Any?): Boolean =
when (ptn) {
is MetaLogical<*> ->
// recursion with existing substitution or new substitution
if (matchSubst.containsKey(ptn))
matchSubst[ptn].let { matchAny(it, trg) }
else
matchSubst.apply { put(ptn, trg) }.run { true }
is Logical<*> ->
// match logical or its value
matchLogical(ptn.findRoot(), trg)
is Term ->
when {
ptn.`is`(Term.Kind.REF) -> matchAny(resolve(ptn), trg)
else -> matchTerm(ptn, trg) // recursion into the term
}
else ->
// compare two arbitrary values
(ptn == trg)
}
private fun matchTerm(ptn: Term, trg: Any?): Boolean
{
if (trg == null) return false
val trgval = resolve(trg)
if (!(trgval is Term)) return false
if (ptn.`is`(Term.Kind.VAR)) return matchAny(ptn.get().symbol(), trgval)
if (!matchAny(ptn.get().symbol(), trgval.symbol())) return false
// FIXME: reversing the order of arguments leads to infinite cycle
// Example: two terms of the form f(... V_1 ...) and f(... V_2 ...) where
// V_1 is bound to g(... W_1 ...), V_2 -> g(... W_2 ...), W_1 -> f(... V_1 ...), and W_2 -> f(... V_2 ...)
return zipWhileTrue(ptn.get().arguments(), trgval.arguments()) { ptnarg, trgarg ->
matchAny (ptnarg, trgarg)
}
}
private fun matchLogical(ptn: Logical<*>, trg: Any?): Boolean =
when {
trg is Logical<*> ->
when {
ptn.isBound -> matchAny(ptn.findRoot().value(), trg.findRoot().value())
ptn.findRoot() === trg.findRoot() -> true // reference equality
else -> false
}
ptn.isBound -> matchAny(ptn.findRoot().value(), trg)
else -> false
}
private fun resolve(obj: Any?): Any? =
when (obj) {
is LogicalOwner -> if (obj.logical().isBound) resolve(obj.logical()) else obj
is Logical<*> -> resolve(obj.findRoot().value())
is Term -> if (obj.`is`(Term.Kind.REF)) resolve(obj.get()) else obj
else -> obj
}
private inline fun<S,T> zipWhileTrue(first: Iterable<S>, second: Iterable<T>, action: (S, T) -> Boolean): Boolean {
val firstIt = first.iterator()
val secondIt = second.iterator()
while(firstIt.hasNext() && secondIt.hasNext()) {
if (!action(firstIt.next(), secondIt.next())) return false
}
return true
}
}

View File

@ -21,26 +21,16 @@ import com.github.andrewoma.dexx.collection.List as PersList
import com.github.andrewoma.dexx.collection.Vector as PersVector
import jetbrains.mps.logic.reactor.evaluation.ConstraintOccurrence
import jetbrains.mps.logic.reactor.evaluation.MatchRule
import jetbrains.mps.logic.reactor.logical.Logical
import jetbrains.mps.logic.reactor.logical.LogicalContext
import jetbrains.mps.logic.reactor.logical.LogicalOwner
import jetbrains.mps.logic.reactor.logical.MetaLogical
import jetbrains.mps.logic.reactor.program.Constraint
import jetbrains.mps.logic.reactor.program.Rule
import jetbrains.mps.logic.reactor.util.*
import jetbrains.mps.unification.Term
import java.util.*
import kotlin.collections.ArrayList
import kotlin.collections.HashMap
/**
* @author Fedor Isakov
*/
private typealias Subst = Map<MetaLogical<*>, Any>
private fun emptySubst() = HashMap<MetaLogical<*>, Any>(4)
class RuleMatcher(val rule: Rule) {
val head = rule.headKept().toCollection(ArrayList(4)).apply {
@ -48,24 +38,28 @@ class RuleMatcher(val rule: Rule) {
val propagation = rule.headReplaced().count() == 0
fun fringe() = MatchFringe(listOf(FringeNode(emptySubst())), emptySet(), 0)
fun probe(): MatchingProbe = MatchFringe(listOf(FringeNode(emptySubst())), emptySet(), 0)
inner class MatchFringe(val nodes: List<FringeNode>,
val seen: IdHashSet<ConstraintOccurrence>,
val genId: Int) {
val genId: Int) : MatchingProbe {
fun rule(): Rule = rule
override fun rule(): Rule = rule
fun matches(): Collection<MatchRule> =
override fun matches(): Collection<MatchRule> =
nodes.filter { rn ->
rn is ActiveFringeNode && rn.complete && rn.genId == genId }.map { rn ->
(rn as ActiveFringeNode).toMatchRule() }
override fun expand(occ: ConstraintOccurrence): MatchingProbe =
expand(occ, bitSetOfOnes(head.size))
/**
* Expands the fringe by creating new leaf nodes that match the occurrence.
* Mask specifies possible slots for the occurrence.
*/
fun expand(occ: ConstraintOccurrence, mask: BitSet? = null): MatchFringe {
override fun expand(occ: ConstraintOccurrence, mask: BitSet): MatchFringe {
if (seen.contains(occ)) {
// constraint occurrence is reactivated
// there are nodes having occ in their paths
@ -97,7 +91,6 @@ class RuleMatcher(val rule: Rule) {
} else {
val newNodes = ArrayList<FringeNode>(nodes)
for (fn in nodes) {
// TODO: mask can't be null in normal circumstances
newNodes.addAll(fn.expand(occ, genId + 1, fn.matchingVacant(mask)))
}
@ -105,7 +98,7 @@ class RuleMatcher(val rule: Rule) {
}
}
fun cleanup(occ: ConstraintOccurrence): MatchFringe {
override fun contract(occ: ConstraintOccurrence): MatchFringe {
val newNodes = nodes.mapNotNull { it.unrelatedOrNull(occ) }
return MatchFringe(newNodes, seen.remove(occ), genId + 1)
}
@ -138,7 +131,7 @@ class RuleMatcher(val rule: Rule) {
*/
open fun unrelatedOrNull(occ: ConstraintOccurrence): FringeNode? = this
fun matchingVacant(mask: BitSet?) = mask?.copyApply { and(vacant) } ?: vacant
fun matchingVacant(mask: BitSet) = mask.copyApply { and(vacant) }
/**
* Folds the path to the root.
@ -194,137 +187,12 @@ class RuleMatcher(val rule: Rule) {
fun toMatchRule(): MatchRule {
val matched: Array<ConstraintOccurrence?> =
fold(arrayOfNulls(head.size)) { arr, rn -> arr[rn.idx] = rn.occ; arr }
return FringeMatchRule(rule,
subst,
ArrayList(matched.take(rule.headKept().count())),
ArrayList(matched.takeLast(rule.headReplaced().count())))
return MatchRuleImpl(rule,
subst,
ArrayList(matched.take(rule.headKept().count())),
ArrayList(matched.takeLast(rule.headReplaced().count())))
}
}
private class FringeMatchRule(val rule: Rule,
val subst: Subst,
val headKept: MutableIterable<ConstraintOccurrence?>,
val headReplaced: MutableIterable<ConstraintOccurrence?>) : MatchRule {
private val logicalContext = object : LogicalContext {
val meta2logical = HashMap<MetaLogical<*>, Logical<*>>()
override fun <V : Any> variable(meta: MetaLogical<V>): Logical<V> =
(meta2logical[meta] ?: subst[meta]?.let { value ->
when (value) {
is Logical<*> -> value
is LogicalOwner -> value.logical()
else -> LogicalImpl(value)
}
} ?: meta.logical().also { logical -> meta2logical[meta] = logical }) as Logical<V>
}
override fun rule(): Rule = rule
override fun matchHeadKept(): MutableIterable<ConstraintOccurrence?> = headKept
override fun matchHeadReplaced(): MutableIterable<ConstraintOccurrence?> = headReplaced
override fun logicalContext(): LogicalContext = logicalContext
}
private class OccurrenceMatcher(contextSubst: Subst) {
private val matchSubst = HashMap(contextSubst)
fun substitution(): Subst = matchSubst
/**
* Matches constraint and occurrence.
* Recursively processes all arguments, including terms.
* Returns substitution of MetaLogical instances on success, null otherwise.
*/
fun matches(cst: Constraint, occ: ConstraintOccurrence): Boolean
{
if (cst.symbol() != occ.constraint().symbol()) return false
return zipWhileTrue(cst.arguments(), occ.arguments()) { cstarg, occarg ->
matchAny(cstarg, occarg)
}
}
/**
* Matches target against pattern.
* Recursively iterates terms.
* Respects substitutions for MetaLogical instances.
* Returns either new substitution on successful match, or null.
*/
private fun matchAny(ptn: Any?, trg: Any?): Boolean =
when (ptn) {
is MetaLogical<*> ->
// recursion with existing substitution or new substitution
if (matchSubst.containsKey(ptn))
matchSubst[ptn].let { matchAny(it, trg) }
else
matchSubst.apply { put(ptn, trg) }.run { true }
is Logical<*> ->
// match logical or its value
matchLogical(ptn.findRoot(), trg)
is Term ->
when {
ptn.`is`(Term.Kind.REF) -> matchAny(resolve(ptn), trg)
else -> matchTerm(ptn, trg) // recursion into the term
}
else ->
// compare two arbitrary values
(ptn == trg)
}
private fun matchTerm(ptn: Term, trg: Any?): Boolean
{
if (trg == null) return false
val trgval = resolve(trg)
if (!(trgval is Term)) return false
if (ptn.`is`(Term.Kind.VAR)) return matchAny(ptn.get().symbol(), trgval)
if (!matchAny(ptn.get().symbol(), trgval.symbol())) return false
// FIXME: reversing the order of arguments leads to infinite cycle
// Example: two terms of the form f(... V_1 ...) and f(... V_2 ...) where
// V_1 is bound to g(... W_1 ...), V_2 -> g(... W_2 ...), W_1 -> f(... V_1 ...), and W_2 -> f(... V_2 ...)
return zipWhileTrue(ptn.get().arguments(), trgval.arguments()) { ptnarg, trgarg ->
matchAny (ptnarg, trgarg)
}
}
private fun matchLogical(ptn: Logical<*>, trg: Any?): Boolean =
when {
trg is Logical<*> ->
when {
ptn.isBound -> matchAny(ptn.findRoot().value(), trg.findRoot().value())
ptn.findRoot() === trg.findRoot() -> true // reference equality
else -> false
}
ptn.isBound -> matchAny(ptn.findRoot().value(), trg)
else -> false
}
private fun resolve(obj: Any?): Any? =
when (obj) {
is LogicalOwner -> if (obj.logical().isBound) resolve(obj.logical()) else obj
is Logical<*> -> resolve(obj.findRoot().value())
is Term -> if (obj.`is`(Term.Kind.REF)) resolve(obj.get()) else obj
else -> obj
}
private inline fun<S,T> zipWhileTrue(first: Iterable<S>, second: Iterable<T>, action: (S, T) -> Boolean): Boolean {
val firstIt = first.iterator()
val secondIt = second.iterator()
while(firstIt.hasNext() && secondIt.hasNext()) {
if (!action(firstIt.next(), secondIt.next())) return false
}
return true
}
}
}

View File

@ -28,11 +28,17 @@ inline fun BitSet.copyApply (f: BitSet.() -> Unit): BitSet =
fun bitSetOfOnes(size: Int): BitSet =
BitSet(size).apply { set(0, size) }
fun bitSet(setBit: Int): BitSet=
BitSet().apply { set(setBit) }
fun bitSet(setBits: Iterable<Int>): BitSet=
BitSet().apply { setBits.forEach { set(it) } }
fun BitSet.setBit(bit: Int): BitSet =
BitSet.valueOf(this.toLongArray()).apply { set(bit) }
(clone() as BitSet).apply { set(bit) }
fun BitSet.clearBit(bit: Int): BitSet =
BitSet.valueOf(this.toLongArray()).apply { clear(bit) }
(clone() as BitSet).apply { clear(bit) }
fun BitSet.allSetBits(): Iterable<Int> = object : Iterable<Int> {
override fun iterator(): Iterator<Int> = object : Iterator<Int> {

View File

@ -1,7 +1,4 @@
import jetbrains.mps.logic.reactor.core.Dispatcher
import jetbrains.mps.logic.reactor.core.RuleIndex
import jetbrains.mps.logic.reactor.core.RuleMatcher
import jetbrains.mps.logic.reactor.core.logical
import jetbrains.mps.logic.reactor.core.*
import jetbrains.mps.logic.reactor.program.ConstraintSymbol.symbol
import jetbrains.mps.unification.Term
import jetbrains.mps.unification.test.MockTerm.*
@ -46,7 +43,7 @@ class TestRuleMatcher {
constraint("qux")
))))
{
with(RuleMatcher(rules.first()).fringe()) {
with(ruleMatcher().probe()) {
expand(occurrence("foo")) }.apply {
matches().size shouldBe 0 }.run {
@ -74,7 +71,7 @@ class TestRuleMatcher {
))))
{
val foo = occurrence("foo")
with(RuleMatcher(rules.first()).fringe()) {
with(ruleMatcher().probe()) {
expand(foo) }.apply {
matches().size shouldBe 0 }.run {
@ -100,7 +97,7 @@ class TestRuleMatcher {
constraint("qux")
))))
{
with(RuleMatcher(rules.first()).fringe()) {
with(ruleMatcher().probe()) {
expand(occurrence("foo", parseTerm("f{g g}"))) }.apply {
matches().size shouldBe 0 }.run {
@ -126,7 +123,7 @@ class TestRuleMatcher {
constraint("qux")
))))
{
with(RuleMatcher(rules.first()).fringe()) {
with(ruleMatcher().probe()) {
val termh = parseTerm("h{k}")
expand(occurrence("foo", term("f", parseTerm("g"), ref(termh)))) }.apply {
@ -150,7 +147,7 @@ class TestRuleMatcher {
))))
{
val bara = occurrence("bar", "a")
with(RuleMatcher(rules.first()).fringe()) {
with(ruleMatcher().probe()) {
expand(occurrence("foo")) }.apply {
matches().size shouldBe 0 }.run {
@ -159,7 +156,7 @@ class TestRuleMatcher {
expand(occurrence("bar", "b")) }.apply {
matches().size shouldBe 0 }.run {
cleanup(bara) }.apply {
contract(bara) }.apply {
matches().size shouldBe 0 }.run {
expand(occurrence("bazz")) }.apply {
@ -194,7 +191,7 @@ class TestRuleMatcher {
constraint("qux")
))))
{
with(RuleMatcher(rules.first()).fringe()) {
with(ruleMatcher().probe()) {
expand(occurrence("foo", "a")) }.run {
expand(occurrence("bazz", "b")) }.run {
@ -260,7 +257,7 @@ class TestRuleMatcher {
constraint("qux")
))))
{
with(RuleMatcher(rules.first()).fringe()) {
with(ruleMatcher().probe()) {
expand(occurrence("foo", parseTerm("f{g{h}}"))) }.apply {
matches().size shouldBe 0
}.run {
@ -290,7 +287,7 @@ class TestRuleMatcher {
constraint("qux")
))))
{
with(RuleMatcher(rules.first()).fringe()) {
with(ruleMatcher().probe()) {
expand(occurrence("bar", parseTerm("h{k}"), parseTerm("h{k}"))) }.apply {
matches().size shouldBe 0 }.run {
@ -317,7 +314,7 @@ class TestRuleMatcher {
constraint("qux")
))))
{
with(RuleMatcher(rules.first()).fringe()) {
with(ruleMatcher().probe()) {
expand(occurrence("foo", term("f", ref(logicalVar(yLogical)), term("h")))) }.apply {
matches().size shouldBe 0 }.run {
@ -344,7 +341,7 @@ class TestRuleMatcher {
constraint("qux")
))))
{
with(RuleMatcher(rules.first()).fringe()) {
with(ruleMatcher().probe()) {
expand(occurrence("foo", term("f", logicalVar(yLogical), term("g")))) }.apply {
matches().size shouldBe 0 }.run {
@ -375,7 +372,7 @@ class TestRuleMatcher {
{
val occ2reactivate = occurrence("bazz", term("k", logicalVar(yLogical)))
with(RuleMatcher(rules.first()).fringe()) {
with(ruleMatcher().probe()) {
expand(occ2reactivate) }.apply {
matches().size shouldBe 0
yLogical.findRoot().value() shouldBe null
@ -658,7 +655,6 @@ class TestRuleMatcher {
}
}
private fun Builder.ruleMatcher() = Matcher(rules.first())
}