Establish the contract of OccurrenceMatcher to fail appropriately on unassigned logicals.
Fix processing of reactivated constraints in RuleMatcher, fix propagation history. Minor code refactorings. Tests.
This commit is contained in:
parent
fc1fcaaf9d
commit
181ccedd95
|
|
@ -86,12 +86,12 @@ class Controller(
|
|||
trace.reactivate(active)
|
||||
}
|
||||
|
||||
val activatedDF = dispatchFringe.activated(active)
|
||||
this.dispatchFringe = activatedDF
|
||||
val activatedFringe = dispatchFringe.expand(active)
|
||||
this.dispatchFringe = activatedFringe
|
||||
|
||||
var state : ProcessingState = instate
|
||||
|
||||
for (match in dispatchFringe.matches().toList()) {
|
||||
for (match in activatedFringe.matches().toList()) {
|
||||
if (!state.operational) break
|
||||
|
||||
// TODO: paranoid check. should be isAlive() instead
|
||||
|
|
@ -121,10 +121,11 @@ class Controller(
|
|||
continue
|
||||
}
|
||||
|
||||
this.dispatchFringe = dispatchFringe.consume(match)
|
||||
trace.trigger(match)
|
||||
|
||||
for (occ in match.matchHeadReplaced()) {
|
||||
this.dispatchFringe = dispatchFringe.discarded(occ)
|
||||
this.dispatchFringe = dispatchFringe.contract(occ)
|
||||
frameStack.current.store.discard(occ)
|
||||
trace.discard(occ)
|
||||
}
|
||||
|
|
@ -153,7 +154,7 @@ class Controller(
|
|||
|
||||
if (state is FAILED) {
|
||||
trace.failure(state.failure)
|
||||
|
||||
|
||||
if (!altIt.hasNext()) {
|
||||
// last alternative
|
||||
if (failureHandler != null) {
|
||||
|
|
@ -168,7 +169,7 @@ class Controller(
|
|||
if (state is FAILED) {
|
||||
frameStack.reset(savedFrame)
|
||||
}
|
||||
|
||||
|
||||
} else {
|
||||
break
|
||||
}
|
||||
|
|
|
|||
|
|
@ -54,29 +54,34 @@ class Dispatcher (val ruleIndex: RuleIndex) {
|
|||
|
||||
constructor(pred: DispatchFringe, matching: Iterable<MatchingProbe>) {
|
||||
this.rule2probe = pred.rule2probe
|
||||
matching.forEach { fringe ->
|
||||
this.rule2probe = rule2probe.put(fringe.rule(), fringe)
|
||||
allMatches.addAll(fringe.matches())
|
||||
matching.forEach { probe ->
|
||||
this.rule2probe = rule2probe.put(probe.rule(), probe)
|
||||
allMatches.addAll(probe.matches())
|
||||
}
|
||||
}
|
||||
|
||||
constructor(pred: DispatchFringe, consumedMatch: MatchRule) {
|
||||
this.rule2probe = pred.rule2probe
|
||||
pred.rule2probe[consumedMatch.rule()]?.let {
|
||||
this.rule2probe = rule2probe.put(consumedMatch.rule(), it.consumed(consumedMatch))
|
||||
}
|
||||
}
|
||||
|
||||
fun matches() : Iterable<MatchRule> = allMatches
|
||||
|
||||
fun activated(active: ConstraintOccurrence): DispatchFringe {
|
||||
return DispatchFringe(this,
|
||||
ruleIndex.forOccurrenceWithMask(active).mapNotNull { (rule, mask) ->
|
||||
rule2probe[rule]?.expand(active, mask)
|
||||
})
|
||||
}
|
||||
fun consume(matchRule: MatchRule) = DispatchFringe(this, matchRule)
|
||||
|
||||
fun discarded(discarded: ConstraintOccurrence): DispatchFringe {
|
||||
return DispatchFringe(this,
|
||||
ruleIndex.forOccurrence(discarded).mapNotNull { rule ->
|
||||
rule2probe[rule]
|
||||
}.map { probe ->
|
||||
probe.contract(discarded)
|
||||
})
|
||||
}
|
||||
fun expand(activated: ConstraintOccurrence) = DispatchFringe(this,
|
||||
ruleIndex.forOccurrenceWithMask(activated).mapNotNull { (rule, mask) ->
|
||||
rule2probe[rule]?.expand(activated, mask)
|
||||
})
|
||||
|
||||
fun contract(discarded: ConstraintOccurrence) = DispatchFringe(this,
|
||||
ruleIndex.forOccurrence(discarded).mapNotNull { rule ->
|
||||
rule2probe[rule]
|
||||
}.map { probe ->
|
||||
probe.contract(discarded)
|
||||
})
|
||||
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -24,7 +24,8 @@ 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,
|
||||
class MatchRuleImpl(val origin: Any,
|
||||
val rule: Rule,
|
||||
val subst: Subst,
|
||||
val headKept: MutableIterable<ConstraintOccurrence?>,
|
||||
val headReplaced: MutableIterable<ConstraintOccurrence?>) : MatchRule {
|
||||
|
|
|
|||
|
|
@ -31,10 +31,12 @@ interface MatchingProbe {
|
|||
|
||||
fun matches() : Collection<MatchRule>
|
||||
|
||||
fun consumed(matchRule: MatchRule): MatchingProbe
|
||||
|
||||
fun expand(occ: ConstraintOccurrence) : MatchingProbe
|
||||
|
||||
fun expand(occ: ConstraintOccurrence, mask: BitSet) : MatchingProbe
|
||||
|
||||
fun contract(occ: ConstraintOccurrence): MatchingProbe
|
||||
|
||||
|
||||
}
|
||||
|
|
@ -48,7 +48,7 @@ class OccurrenceMatcher(val contextSubst: Subst? = null) {
|
|||
if (cst.symbol() != occ.constraint().symbol()) return false
|
||||
|
||||
return zipWhileTrue(cst.arguments(), occ.arguments()) { cstarg, occarg ->
|
||||
matchAny(cstarg, occarg)
|
||||
ptnMatchAny(cstarg, occarg)
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -66,7 +66,7 @@ class OccurrenceMatcher(val contextSubst: Subst? = null) {
|
|||
* Respects substitutions for MetaLogical instances.
|
||||
* Returns either new substitution on successful match, or null.
|
||||
*/
|
||||
private fun matchAny(ptn: Any?, trg: Any?): Boolean =
|
||||
private fun ptnMatchAny(ptn: Any?, trg: Any?): Boolean =
|
||||
when (ptn) {
|
||||
is MetaLogical<*> -> {
|
||||
// recursion with existing substitution or new substitution
|
||||
|
|
@ -79,49 +79,83 @@ class OccurrenceMatcher(val contextSubst: Subst? = null) {
|
|||
else
|
||||
matchSubst!!.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
|
||||
ptn.`is`(Term.Kind.REF) -> ptnMatchAny(resolve(ptn), trg)
|
||||
else -> ptnMatchTerm(ptn, trg) // recursion into the term
|
||||
}
|
||||
else ->
|
||||
// compare two arbitrary values
|
||||
(ptn == trg)
|
||||
when {
|
||||
trg is Logical<*> -> ptnMatchAny(ptn, resolve(trg))
|
||||
else ->
|
||||
// compare two arbitrary values
|
||||
(ptn == trg)
|
||||
}
|
||||
}
|
||||
|
||||
private fun matchTerm(ptn: Term, trg: Any?): Boolean
|
||||
{
|
||||
private fun matchAny(left: Any?, right: Any?): Boolean =
|
||||
when (left) {
|
||||
is Logical<*> ->
|
||||
// match logical or its value
|
||||
matchLogical(left.findRoot(), right)
|
||||
is Term ->
|
||||
when {
|
||||
left.`is`(Term.Kind.REF) -> matchAny(resolve(left), right)
|
||||
else -> matchTerm(left, right) // recursion into the term
|
||||
}
|
||||
else ->
|
||||
when {
|
||||
right is Logical<*> -> matchAny(left, resolve(right))
|
||||
else -> // compare two arbitrary values
|
||||
(left == right)
|
||||
}
|
||||
}
|
||||
|
||||
private fun ptnMatchTerm(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 (ptn.`is`(Term.Kind.VAR)) return ptnMatchAny(ptn.get().symbol(), trgval)
|
||||
|
||||
if (!ptnMatchAny(ptn.get().symbol(), trgval.symbol())) return false
|
||||
|
||||
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)
|
||||
ptnMatchAny (ptnarg, trgarg)
|
||||
}
|
||||
}
|
||||
|
||||
private fun matchLogical(ptn: Logical<*>, trg: Any?): Boolean =
|
||||
private fun matchTerm(left: Term, right: Any?): Boolean {
|
||||
if (right == null) return false
|
||||
|
||||
val rval = resolve(right)
|
||||
if (!(rval is Term)) return false
|
||||
|
||||
if (!matchAny(left.get().symbol(), rval.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(left.get().arguments(), rval.arguments()) { larg, rarg ->
|
||||
matchAny (larg, rarg)
|
||||
}
|
||||
}
|
||||
|
||||
private fun matchLogical(left: Logical<*>, right: Any?): Boolean =
|
||||
when {
|
||||
trg is Logical<*> ->
|
||||
right is Logical<*> ->
|
||||
when {
|
||||
ptn.isBound -> matchAny(ptn.findRoot().value(), trg.findRoot().value())
|
||||
ptn.findRoot() === trg.findRoot() -> true // reference equality
|
||||
else -> false
|
||||
left.isBound -> matchAny(left.findRoot().value(),
|
||||
right.findRoot().value())
|
||||
left.findRoot() === right.findRoot() -> true // reference equality
|
||||
else -> false
|
||||
}
|
||||
ptn.isBound -> matchAny(ptn.findRoot().value(), trg)
|
||||
else -> false
|
||||
left.isBound -> matchAny(left.findRoot().value(), right)
|
||||
else -> false
|
||||
}
|
||||
|
||||
private fun resolve(obj: Any?): Any? =
|
||||
|
|
|
|||
|
|
@ -296,7 +296,8 @@ class ReteRuleMatcher(val rule: Rule) {
|
|||
val occList = occArray.toMutableList()
|
||||
val keptCount = rule.headKept().count()
|
||||
|
||||
matches.add(MatchRuleImpl(rule,
|
||||
matches.add(MatchRuleImpl(n,
|
||||
rule,
|
||||
allSubst,
|
||||
occList.subList(0, keptCount),
|
||||
occList.subList(keptCount, occList.size)))
|
||||
|
|
@ -344,6 +345,9 @@ class ReteRuleMatcher(val rule: Rule) {
|
|||
|
||||
override fun matches(): Collection<MatchRule> = generations.last().matches()
|
||||
|
||||
override fun consumed(matchRule: MatchRule): MatchingProbe {
|
||||
TODO("not implemented") //To change body of created functions use File | Settings | File Templates.
|
||||
}
|
||||
|
||||
fun indexOf(occurrence: ConstraintOccurrence): Int =
|
||||
seenOcc2Idx[occurrence] ?: (nextOccIdx++).also { idx -> seenOcc2Idx[occurrence] = idx }
|
||||
|
|
|
|||
|
|
@ -16,7 +16,9 @@
|
|||
|
||||
package jetbrains.mps.logic.reactor.core
|
||||
|
||||
import com.github.andrewoma.dexx.collection.Sets
|
||||
import com.github.andrewoma.dexx.collection.Map as PersMap
|
||||
import com.github.andrewoma.dexx.collection.Set as PersSet
|
||||
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
|
||||
|
|
@ -38,19 +40,28 @@ class RuleMatcher(val rule: Rule) {
|
|||
|
||||
val propagation = rule.headReplaced().count() == 0
|
||||
|
||||
fun probe(): MatchingProbe = MatchFringe(listOf(FringeNode(emptySubst())), emptySet(), 0)
|
||||
|
||||
inner class MatchFringe(val nodes: List<FringeNode>,
|
||||
val seen: IdHashSet<ConstraintOccurrence>,
|
||||
val genId: Int) : MatchingProbe {
|
||||
fun probe(): MatchingProbe = RuleMatchFringe(listOf(MatchNode(emptySubst())),
|
||||
Sets.of(),
|
||||
Sets.of(),
|
||||
0)
|
||||
|
||||
inner class RuleMatchFringe(val nodes: List<MatchNode>,
|
||||
val seen: PersSet<IdWrapper<ConstraintOccurrence>>,
|
||||
val consumed: PersSet<ArrayList<IdWrapper<ConstraintOccurrence>?>>,
|
||||
val genId: Int) : MatchingProbe
|
||||
{
|
||||
override fun rule(): Rule = rule
|
||||
|
||||
override fun matches(): Collection<MatchRule> =
|
||||
nodes.filter { rn ->
|
||||
rn is ActiveFringeNode && rn.complete && rn.genId == genId }.map { rn ->
|
||||
(rn as ActiveFringeNode).toMatchRule() }
|
||||
override fun matches(): Collection<MatchRule> {
|
||||
return nodes.filter { it is ActiveMatchNode && it.complete && it.genId == genId }
|
||||
.map { (it as ActiveMatchNode).toMatchRule() }
|
||||
}
|
||||
|
||||
override fun consumed(matchRule: MatchRule): MatchingProbe =
|
||||
RuleMatchFringe(nodes,
|
||||
seen,
|
||||
consumed.add(((matchRule as MatchRuleImpl).origin as ActiveMatchNode).signature),
|
||||
genId)
|
||||
|
||||
override fun expand(occ: ConstraintOccurrence): MatchingProbe =
|
||||
expand(occ, bitSetOfOnes(head.size))
|
||||
|
|
@ -59,74 +70,45 @@ class RuleMatcher(val rule: Rule) {
|
|||
* Expands the fringe by creating new leaf nodes that match the occurrence.
|
||||
* Mask specifies possible slots for the occurrence.
|
||||
*/
|
||||
override fun expand(occ: ConstraintOccurrence, mask: BitSet): MatchFringe {
|
||||
if (seen.contains(occ)) {
|
||||
// constraint occurrence is reactivated
|
||||
// there are nodes having occ in their paths
|
||||
// select complete (leaf) nodes and make them appear as if newly expanded
|
||||
// *unless* propagation (implement propagation history feature)
|
||||
if (propagation) return MatchFringe(nodes, seen, genId + 1)
|
||||
|
||||
val newNodes = ArrayList<FringeNode>()
|
||||
for (fn in nodes) {
|
||||
when (fn) {
|
||||
is ActiveFringeNode -> {
|
||||
// only leaf nodes
|
||||
// either unrelated, or the nodes already having occ
|
||||
fn.unrelatedOrCopy(occ, genId + 1)?.let { newNodes.add(it) }
|
||||
|
||||
// only non-leaf nodes
|
||||
// all unrelated, expanded on occ
|
||||
fn.unrelatedOrNull(occ)?.let {
|
||||
newNodes.addAll(it.expand(occ, genId + 1, fn.matchingVacant(mask)))
|
||||
}
|
||||
}
|
||||
|
||||
else -> {
|
||||
newNodes.add(fn)
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
if (newNodes.size == 1) {
|
||||
// only the root
|
||||
val rfn = newNodes.get(0)
|
||||
newNodes.addAll(rfn.expand(occ, genId + 1, rfn.matchingVacant(mask)))
|
||||
}
|
||||
|
||||
return MatchFringe(newNodes, seen, genId + 1)
|
||||
|
||||
} else {
|
||||
val newNodes = ArrayList<FringeNode>(nodes)
|
||||
for (fn in nodes) {
|
||||
newNodes.addAll(fn.expand(occ, genId + 1, fn.matchingVacant(mask)))
|
||||
}
|
||||
|
||||
return MatchFringe(newNodes, seen.add(occ), genId + 1)
|
||||
override fun expand(occ: ConstraintOccurrence, mask: BitSet): RuleMatchFringe {
|
||||
val reactivated = seen.contains(IdWrapper(occ))
|
||||
val newSeen = if (reactivated) seen else seen.add(IdWrapper(occ))
|
||||
val newNodes = ArrayList<MatchNode>(nodes)
|
||||
|
||||
val allSignatures = newNodes.map { it.signature }.toHashSet()
|
||||
for (n in nodes) {
|
||||
n.expand(occ, genId + 1, n.matchingVacant(mask))
|
||||
.filter { allSignatures.add(it.signature) || reactivated } // ensure reactivated have effect
|
||||
.filter { !(propagation && reactivated && consumed.contains(it.signature)) } // ...unless propagation
|
||||
.forEach { newNodes.add(it) }
|
||||
}
|
||||
|
||||
return RuleMatchFringe(newNodes, newSeen, consumed, genId + 1)
|
||||
}
|
||||
|
||||
override fun contract(occ: ConstraintOccurrence): MatchFringe {
|
||||
override fun contract(occ: ConstraintOccurrence): RuleMatchFringe {
|
||||
val newNodes = nodes.mapNotNull { it.unrelatedOrNull(occ) }
|
||||
return MatchFringe(newNodes, seen.remove(occ), genId + 1)
|
||||
return RuleMatchFringe(newNodes, seen, consumed,genId + 1)
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
open inner class FringeNode(val subst: Subst, val vacant: BitSet = bitSetOfOnes(head.size))
|
||||
open inner class MatchNode(val subst: Subst, val vacant: BitSet = bitSetOfOnes(head.size))
|
||||
{
|
||||
open val signature: ArrayList<IdWrapper<ConstraintOccurrence>?> =
|
||||
arrayListOf(* arrayOfNulls<IdWrapper<ConstraintOccurrence>?>(head.size))
|
||||
|
||||
/**
|
||||
* Returns the additional nodes built from this node on adding the occurrence.
|
||||
* If the occurrence is already in the path, return empty sequence.
|
||||
*/
|
||||
fun expand(occ: ConstraintOccurrence, genId: Int, matchingVacant: BitSet): List<ActiveFringeNode> =
|
||||
unrelatedOrNull(occ)?.run {
|
||||
ArrayList<ActiveFringeNode>().also { expanded ->
|
||||
for (idx in matchingVacant.allSetBits()) {
|
||||
OccurrenceMatcher(subst).let { matcher ->
|
||||
if (matcher.matches(head[idx], occ)) {
|
||||
expanded.add(ActiveFringeNode(matcher.substitution(), this, occ, idx, genId))
|
||||
fun expand(occ: ConstraintOccurrence, genId: Int, matchingVacant: BitSet): List<ActiveMatchNode> =
|
||||
unrelatedOrNull(occ)?.let { n ->
|
||||
ArrayList<ActiveMatchNode>().also { expanded ->
|
||||
for (headIdx in matchingVacant.allSetBits()) {
|
||||
OccurrenceMatcher(subst).run {
|
||||
if (matches(head[headIdx], occ)) {
|
||||
expanded.add(ActiveMatchNode(substitution(), n, occ, headIdx, genId))
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -137,17 +119,17 @@ class RuleMatcher(val rule: Rule) {
|
|||
/**
|
||||
* Returns this node if it doesn't have the occurrence in its path, null otherwise.
|
||||
*/
|
||||
open fun unrelatedOrNull(occ: ConstraintOccurrence): FringeNode? = this
|
||||
open fun unrelatedOrNull(occ: ConstraintOccurrence): MatchNode? = this
|
||||
|
||||
fun matchingVacant(mask: BitSet) = mask.copyApply { and(vacant) }
|
||||
|
||||
/**
|
||||
* Folds the path to the root.
|
||||
*/
|
||||
inline protected fun <T> fold(init: T, action: (T, ActiveFringeNode) -> T): T {
|
||||
inline protected fun <T> fold(init: T, action: (T, ActiveMatchNode) -> T): T {
|
||||
var rn = this
|
||||
var curr = init
|
||||
while (rn is ActiveFringeNode) {
|
||||
while (rn is ActiveMatchNode) {
|
||||
curr = action(curr, rn)
|
||||
rn = rn.parent
|
||||
}
|
||||
|
|
@ -157,10 +139,10 @@ class RuleMatcher(val rule: Rule) {
|
|||
/**
|
||||
* Folds the path to the root. If an iteration yields null, fold is stopped and null is returned.
|
||||
*/
|
||||
inline protected fun <T> foldUntilNull(init: T, action: (T, ActiveFringeNode) -> T?): T? {
|
||||
inline protected fun <T> foldUntilNull(init: T, action: (T, ActiveMatchNode) -> T?): T? {
|
||||
var rn = this
|
||||
var curr: T? = init
|
||||
while (rn is ActiveFringeNode) {
|
||||
while (rn is ActiveMatchNode) {
|
||||
curr = action(curr !!, rn)
|
||||
if (curr == null) return null
|
||||
rn = rn.parent
|
||||
|
|
@ -169,36 +151,34 @@ class RuleMatcher(val rule: Rule) {
|
|||
}
|
||||
}
|
||||
|
||||
inner class ActiveFringeNode(subst: Subst,
|
||||
val parent: FringeNode,
|
||||
val occ: ConstraintOccurrence,
|
||||
val idx: Int,
|
||||
val genId: Int) :
|
||||
FringeNode(subst, parent.vacant.clearBit(idx))
|
||||
inner class ActiveMatchNode(subst: Subst,
|
||||
val parent: MatchNode,
|
||||
val occurrence: ConstraintOccurrence,
|
||||
val headIndex: Int,
|
||||
val genId: Int) :
|
||||
MatchNode(subst, parent.vacant.clearBit(headIndex))
|
||||
{
|
||||
val complete = vacant.cardinality() == 0
|
||||
|
||||
fun occurrence(): ConstraintOccurrence = occ
|
||||
override val signature: ArrayList<IdWrapper<ConstraintOccurrence>?> =
|
||||
(parent.signature.clone() as ArrayList<IdWrapper<ConstraintOccurrence>?>)
|
||||
.also { it[headIndex] = IdWrapper(occurrence) }
|
||||
|
||||
fun constraint(): Constraint = head[idx]
|
||||
fun constraint(): Constraint = head[headIndex]
|
||||
|
||||
override fun unrelatedOrNull(occ: ConstraintOccurrence): ActiveFringeNode? =
|
||||
foldUntilNull(this) { acc, rn -> if (rn.occ === occ) null else acc }
|
||||
override fun unrelatedOrNull(occ: ConstraintOccurrence): ActiveMatchNode? =
|
||||
foldUntilNull(this) { acc, rn -> if (rn.occurrence === occ) null else acc }
|
||||
|
||||
/**
|
||||
* Returns this node if it doesn't have the occurrence in its path,
|
||||
* otherwise a copy of this node with the specified generation id.
|
||||
*/
|
||||
fun unrelatedOrCopy(occ: ConstraintOccurrence, copyGenId: Int): FringeNode? =
|
||||
unrelatedOrNull(occ) ?: ActiveFringeNode(subst, parent, occ, idx, copyGenId)
|
||||
|
||||
fun toMatchRule(): MatchRule {
|
||||
val matched: Array<ConstraintOccurrence?> =
|
||||
fold(arrayOfNulls(head.size)) { arr, rn -> arr[rn.idx] = rn.occ; arr }
|
||||
return MatchRuleImpl(rule,
|
||||
subst,
|
||||
ArrayList(matched.take(rule.headKept().count())),
|
||||
ArrayList(matched.takeLast(rule.headReplaced().count())))
|
||||
fold(arrayOfNulls(head.size)) { arr, rn -> arr[rn.headIndex] = rn.occurrence; arr }
|
||||
|
||||
return MatchRuleImpl(this,
|
||||
rule,
|
||||
subst,
|
||||
ArrayList(matched.take(rule.headKept().count())),
|
||||
ArrayList(matched.takeLast(rule.headReplaced().count())))
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -16,20 +16,14 @@
|
|||
|
||||
package jetbrains.mps.logic.reactor.core
|
||||
|
||||
import com.github.andrewoma.dexx.collection.DerivedKeyHashMap
|
||||
import com.github.andrewoma.dexx.collection.KeyFunction
|
||||
import com.github.andrewoma.dexx.collection.Maps
|
||||
import com.github.andrewoma.dexx.collection.internal.base.AbstractSet
|
||||
import jetbrains.mps.logic.reactor.evaluation.ConstraintOccurrence
|
||||
import jetbrains.mps.logic.reactor.evaluation.EvaluationSession
|
||||
import jetbrains.mps.logic.reactor.evaluation.StoreView
|
||||
import jetbrains.mps.logic.reactor.logical.Logical
|
||||
import jetbrains.mps.logic.reactor.logical.LogicalContext
|
||||
import jetbrains.mps.logic.reactor.program.Constraint
|
||||
import jetbrains.mps.logic.reactor.program.ConstraintSymbol
|
||||
import jetbrains.mps.unification.Term
|
||||
import jetbrains.mps.logic.reactor.util.*
|
||||
import java.util.*
|
||||
import com.github.andrewoma.dexx.collection.Map as PersMap
|
||||
import com.github.andrewoma.dexx.collection.Set as PersSet
|
||||
import com.github.andrewoma.dexx.collection.Vector as PersVector
|
||||
|
|
@ -94,8 +88,8 @@ class Store : LogicalObserver {
|
|||
copyFrom.allOccurrences().forEach { occ ->
|
||||
occ.arguments().forEach { arg ->
|
||||
when (arg) {
|
||||
is Logical<*> -> l2o = l2o.put(IdWrapper(arg.findRoot()), l2o[IdWrapper(arg.findRoot())]?.add(occ) ?: singletonSet(occ))
|
||||
is Any -> v2o = v2o.put(arg, v2o[arg]?.add(occ) ?: singletonSet(occ))
|
||||
is Logical<*> -> l2o = l2o.put(IdWrapper(arg.findRoot()), l2o[IdWrapper(arg.findRoot())]?.add(occ) ?: singletonIdSet(occ))
|
||||
is Any -> v2o = v2o.put(arg, v2o[arg]?.add(occ) ?: singletonIdSet(occ))
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -118,7 +112,7 @@ class Store : LogicalObserver {
|
|||
val logicalId = IdWrapper(logical)
|
||||
logical2occurrences[logicalId]?.let { toMerge ->
|
||||
val rootId = IdWrapper(logical.findRoot())
|
||||
var newSet = logical2occurrences[rootId] ?: emptySet()
|
||||
var newSet = logical2occurrences[rootId] ?: emptyIdSet()
|
||||
for (log in toMerge) {
|
||||
newSet = newSet.add(log)
|
||||
}
|
||||
|
|
@ -132,7 +126,7 @@ class Store : LogicalObserver {
|
|||
val symbol = occ.constraint().symbol()
|
||||
|
||||
this.symbol2occurrences = symbol2occurrences.put(symbol,
|
||||
symbol2occurrences[symbol]?.add(occ) ?: singletonSet(occ))
|
||||
symbol2occurrences[symbol]?.add(occ) ?: singletonIdSet(occ))
|
||||
|
||||
for (arg in occ.arguments()) {
|
||||
val value = if (arg is Logical<*> && arg.isBound) arg.findRoot().value() else arg
|
||||
|
|
@ -141,7 +135,7 @@ class Store : LogicalObserver {
|
|||
// free logical
|
||||
val argId = IdWrapper(value.findRoot())
|
||||
this.logical2occurrences = logical2occurrences.put(argId,
|
||||
logical2occurrences[argId]?.add(occ) ?: singletonSet(occ))
|
||||
logical2occurrences[argId]?.add(occ) ?: singletonIdSet(occ))
|
||||
currentFrame().addObserver(value) { frame -> frame.store() }
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -72,6 +72,6 @@ class IdHashSet<E> : AbstractSet<E> {
|
|||
}
|
||||
|
||||
@Suppress("UNCHECKED_CAST")
|
||||
fun <E> emptySet(): IdHashSet<E> = IdHashSet.EMPTY_SET as IdHashSet<E>
|
||||
fun <E> emptyIdSet(): IdHashSet<E> = IdHashSet.EMPTY_SET as IdHashSet<E>
|
||||
|
||||
fun <E> singletonSet(e: E): IdHashSet<E> = emptySet<E>().add(e)
|
||||
fun <E> singletonIdSet(e: E): IdHashSet<E> = emptyIdSet<E>().add(e)
|
||||
|
|
@ -235,7 +235,7 @@ class PersistentTermTrie<T>() : TermTrie<T> {
|
|||
{
|
||||
|
||||
constructor(symbol: Any, arity: Int) :
|
||||
this(symbol, arity, Maps.of(), emptySet())
|
||||
this(symbol, arity, Maps.of(), emptyIdSet())
|
||||
|
||||
constructor(copyFrom: PathNode<T>, setValues: IdHashSet<T>) :
|
||||
this(copyFrom.symbol, copyFrom.arity, copyFrom.next, setValues)
|
||||
|
|
|
|||
|
|
@ -6,8 +6,6 @@ import jetbrains.mps.logic.reactor.evaluation.*
|
|||
import jetbrains.mps.logic.reactor.logical.Logical
|
||||
import jetbrains.mps.logic.reactor.logical.LogicalContext
|
||||
import jetbrains.mps.logic.reactor.program.*
|
||||
import jetbrains.mps.logic.reactor.util.cons
|
||||
import org.jetbrains.kotlin.js.parser.parse
|
||||
import org.junit.After
|
||||
import org.junit.Assert.*
|
||||
import org.junit.Before
|
||||
|
|
@ -570,6 +568,56 @@ class TestController {
|
|||
}
|
||||
}
|
||||
|
||||
@Test
|
||||
fun propagationHistoryLogical() {
|
||||
val X = metaLogical<Int>("X")
|
||||
programWithRules(
|
||||
rule("main",
|
||||
headReplaced( constraint("main") ), body( constraint("foo", X),
|
||||
statement({ x -> eq(x, "doh") }, X)
|
||||
)
|
||||
),
|
||||
rule("foobar",
|
||||
headKept( constraint("foo", X) ),
|
||||
guard( expression ({ x -> x.isBound }, X) ),
|
||||
body( constraint("foobar") )
|
||||
)
|
||||
).controller().evaluate(occurrence("main")).run {
|
||||
assertEquals(setOf( ConstraintSymbol("foo", 1),
|
||||
ConstraintSymbol("foobar", 0)),
|
||||
constraintSymbols())
|
||||
assertEquals(1, occurrences(ConstraintSymbol("foo", 1)).count())
|
||||
assertEquals(1, occurrences(ConstraintSymbol("foobar", 0)).count())
|
||||
}
|
||||
}
|
||||
|
||||
@Test
|
||||
fun propagationHistoryLogical2() {
|
||||
val (X, Y) = metaLogical<Int>("X", "Y")
|
||||
programWithRules(
|
||||
rule("main",
|
||||
headReplaced( constraint("main") ), body( constraint("foo", X),
|
||||
constraint("bar", Y),
|
||||
statement({ x -> eq(x, "doh") }, X)
|
||||
)
|
||||
),
|
||||
rule("foobar",
|
||||
headKept( constraint("foo", X),
|
||||
constraint("bar", Y)
|
||||
),
|
||||
guard( expression ({ x -> x.isBound }, X) ),
|
||||
body( constraint("foobar") )
|
||||
)
|
||||
).controller().evaluate(occurrence("main")).run {
|
||||
assertEquals(setOf( ConstraintSymbol("foo", 1),
|
||||
ConstraintSymbol("bar", 1),
|
||||
ConstraintSymbol("foobar", 0)),
|
||||
constraintSymbols())
|
||||
assertEquals(1, occurrences(ConstraintSymbol("foo", 1)).count())
|
||||
assertEquals(1, occurrences(ConstraintSymbol("bar", 1)).count())
|
||||
assertEquals(1, occurrences(ConstraintSymbol("foobar", 0)).count())
|
||||
}
|
||||
}
|
||||
|
||||
@Test
|
||||
fun removeObserver() {
|
||||
|
|
|
|||
|
|
@ -1,4 +1,5 @@
|
|||
import jetbrains.mps.logic.reactor.core.*
|
||||
import jetbrains.mps.logic.reactor.program.ConstraintSymbol
|
||||
import jetbrains.mps.logic.reactor.program.ConstraintSymbol.symbol
|
||||
import jetbrains.mps.unification.Term
|
||||
import jetbrains.mps.unification.test.MockTerm.*
|
||||
|
|
@ -6,6 +7,7 @@ import jetbrains.mps.unification.test.MockTermsParser.*
|
|||
import org.junit.Assert.assertEquals
|
||||
import org.junit.Ignore
|
||||
import org.junit.Test
|
||||
import program.MockConstraint
|
||||
|
||||
/*
|
||||
* Copyright 2014-2018 JetBrains s.r.o.
|
||||
|
|
@ -32,6 +34,105 @@ class TestRuleMatcher {
|
|||
|
||||
infix fun <A, B> A.shouldBe(that: B) = assertEquals(that, this)
|
||||
|
||||
@Test
|
||||
fun testOccurrenceMatchLogical() {
|
||||
val (X, Y) = metaLogical<String>("X", "Y")
|
||||
val xLogical = X.logical()
|
||||
val yLogical = Y.logical()
|
||||
|
||||
val foobar = MockConstraint(ConstraintSymbol("foo", 1), "bar")
|
||||
val foox = MockConstraint(ConstraintSymbol("foo", 1), X)
|
||||
|
||||
// foo("bar") = foo("bar")
|
||||
OccurrenceMatcher().
|
||||
matches(foobar, occurrence("foo", "bar")) shouldBe true
|
||||
// foo("bar") != foo(X)
|
||||
OccurrenceMatcher().
|
||||
matches(foobar, occurrence("foo", xLogical)) shouldBe false
|
||||
// foo("bar") = foo(X = "bar")
|
||||
xLogical.set("bar")
|
||||
OccurrenceMatcher().
|
||||
matches(foobar, occurrence("foo", xLogical)) shouldBe true
|
||||
|
||||
// foo(X) = foo(Y)
|
||||
OccurrenceMatcher().
|
||||
matches(foox, occurrence("foo", yLogical)) shouldBe true
|
||||
// foo(X) = foo("bar")
|
||||
OccurrenceMatcher().
|
||||
matches(foox, occurrence("foo", "bar")) shouldBe true
|
||||
// foo(X) = foo(Y = "bar")
|
||||
yLogical.set("bar")
|
||||
OccurrenceMatcher().
|
||||
matches(foox, occurrence("foo", yLogical)) shouldBe true
|
||||
}
|
||||
|
||||
@Test
|
||||
fun testOccurrenceMatchTerm() {
|
||||
val (X, Y) = metaLogical<Term>("X", "Y")
|
||||
val xLogical = X.logical()
|
||||
val yLogical = Y.logical()
|
||||
|
||||
val foofh = MockConstraint(ConstraintSymbol("foo", 1), parseTerm("f { h }"))
|
||||
val foofx = MockConstraint(ConstraintSymbol("foo", 1), term("f", metaVar(X)))
|
||||
|
||||
// foo(f { h }) = foo(f { h })
|
||||
OccurrenceMatcher().
|
||||
matches(foofh, occurrence("foo", parseTerm("f { h }"))) shouldBe true
|
||||
// foo(f { h }) != foo(f { X })
|
||||
OccurrenceMatcher().
|
||||
matches(foofh, occurrence("foo", term("f", logicalVar(xLogical)))) shouldBe false
|
||||
// foo(f { h }) != foo(f { X = h })
|
||||
xLogical.set(term("h"))
|
||||
OccurrenceMatcher().
|
||||
matches(foofh, occurrence("foo", term("f", logicalVar(xLogical)))) shouldBe true
|
||||
|
||||
// foo(f { X }) = foo(f { h })
|
||||
OccurrenceMatcher().
|
||||
matches(foofx, occurrence("foo", parseTerm("f { h }"))) shouldBe true
|
||||
// foo(f { X }) = foo(f { Y })
|
||||
OccurrenceMatcher().
|
||||
matches(foofx, occurrence("foo", term("f", logicalVar(yLogical)))) shouldBe true
|
||||
// foo(f { X }) = foo(f { Y = h })
|
||||
xLogical.set(term("h"))
|
||||
OccurrenceMatcher().
|
||||
matches(foofx, occurrence("foo", term("f", logicalVar(yLogical)))) shouldBe true
|
||||
}
|
||||
|
||||
@Test
|
||||
fun testOccurrenceMatchConsistent() {
|
||||
val (X, Y, Z) = metaLogical<Term>("X", "Y", "Z")
|
||||
val xLogical = X.logical()
|
||||
val yLogical = Y.logical()
|
||||
val zLogical = Z.logical()
|
||||
|
||||
val foofx = MockConstraint(ConstraintSymbol("foo", 1), term("f", metaVar(X)))
|
||||
|
||||
// [X -> free] |- foo(f { X }) = foo(f { X })
|
||||
OccurrenceMatcher(arrayOf(X to logicalVar(xLogical)).toMap()).
|
||||
matches(foofx, occurrence("foo", term("f", logicalVar(xLogical)))) shouldBe true
|
||||
// [X -> free] |- foo(f { X }) != foo(f { Y })
|
||||
OccurrenceMatcher(arrayOf(X to logicalVar(xLogical)).toMap()).
|
||||
matches(foofx, occurrence("foo", term("f", logicalVar(yLogical)))) shouldBe false
|
||||
// [X -> free] |- foo(f { X }) != foo(f { h })
|
||||
OccurrenceMatcher(arrayOf(X to logicalVar(xLogical)).toMap()).
|
||||
matches(foofx, occurrence("foo", parseTerm("f { h }"))) shouldBe false
|
||||
// [X -> free] |- foo(f { X }) != foo(f { Y = h })
|
||||
yLogical.set(term("h"))
|
||||
OccurrenceMatcher(arrayOf(X to logicalVar(xLogical)).toMap()).
|
||||
matches(foofx, occurrence("foo", term("f", logicalVar(yLogical)))) shouldBe false
|
||||
|
||||
// [X -> h] |- foo(f { X }) = foo(f { h })
|
||||
OccurrenceMatcher(arrayOf(X to term("h")).toMap()).
|
||||
matches(foofx, occurrence("foo", parseTerm("f { h }"))) shouldBe true
|
||||
// [X -> h] |- foo(f { X }) != foo(f { Z })
|
||||
OccurrenceMatcher(arrayOf(X to term("h")).toMap()).
|
||||
matches(foofx, occurrence("foo", term("f", logicalVar(zLogical)))) shouldBe false
|
||||
// [X -> h] |- foo(f { X }) = foo(f { Z = h })
|
||||
zLogical.set(term("h"))
|
||||
OccurrenceMatcher(arrayOf(X to term("h")).toMap()).
|
||||
matches(foofx, occurrence("foo", term("f", logicalVar(zLogical)))) shouldBe true
|
||||
}
|
||||
|
||||
@Test
|
||||
fun testExpand() {
|
||||
with(programWithRules(
|
||||
|
|
@ -447,10 +548,10 @@ class TestRuleMatcher {
|
|||
{
|
||||
with(Dispatcher(RuleIndex(handlers)).fringe()) {
|
||||
|
||||
activated(occurrence("foo")) }.apply {
|
||||
expand(occurrence("foo")) }.apply {
|
||||
matches().count() shouldBe 0 }.run {
|
||||
|
||||
activated(occurrence("bar")) }.apply {
|
||||
expand(occurrence("bar")) }.apply {
|
||||
matches().count() shouldBe 1
|
||||
|
||||
with(matches().first()) {
|
||||
|
|
@ -489,10 +590,10 @@ class TestRuleMatcher {
|
|||
{
|
||||
with(Dispatcher(RuleIndex(handlers)).fringe()) {
|
||||
|
||||
activated(occurrence("foo")) }.apply {
|
||||
expand(occurrence("foo")) }.apply {
|
||||
matches().count() shouldBe 0 }.run {
|
||||
|
||||
activated(occurrence("bar", "a")) }.apply {
|
||||
expand(occurrence("bar", "a")) }.apply {
|
||||
matches().count() shouldBe 1
|
||||
|
||||
with(matches().first()) {
|
||||
|
|
@ -501,7 +602,7 @@ class TestRuleMatcher {
|
|||
|
||||
}
|
||||
}.run {
|
||||
activated(occurrence("bazz")) }.apply {
|
||||
expand(occurrence("bazz")) }.apply {
|
||||
matches().count() shouldBe 1
|
||||
|
||||
with(matches().first()) {
|
||||
|
|
@ -511,7 +612,7 @@ class TestRuleMatcher {
|
|||
|
||||
}
|
||||
}.run {
|
||||
activated(occurrence("bar", "b")) }.apply {
|
||||
expand(occurrence("bar", "b")) }.apply {
|
||||
matches().count() shouldBe 2
|
||||
|
||||
with(matches().drop(1).first()) {
|
||||
|
|
@ -558,16 +659,16 @@ class TestRuleMatcher {
|
|||
{
|
||||
with(Dispatcher(RuleIndex(handlers)).fringe()) {
|
||||
|
||||
activated(occurrence("blin")) }.apply {
|
||||
expand(occurrence("blin")) }.apply {
|
||||
matches().count() shouldBe 0 }.run {
|
||||
|
||||
activated(occurrence("bar")) }.apply {
|
||||
expand(occurrence("bar")) }.apply {
|
||||
matches().count() shouldBe 0 }.run {
|
||||
|
||||
activated(occurrence("bazz")) }.apply {
|
||||
expand(occurrence("bazz")) }.apply {
|
||||
matches().count() shouldBe 0 }.run {
|
||||
|
||||
activated(occurrence("foo")) }.apply {
|
||||
expand(occurrence("foo")) }.apply {
|
||||
matches().count() shouldBe 3 }.run {
|
||||
|
||||
matches().map { it.rule().tag() }.toList() shouldBe listOf("rule1", "rule2", "rule3")
|
||||
|
|
@ -608,18 +709,18 @@ class TestRuleMatcher {
|
|||
{
|
||||
with(Dispatcher(RuleIndex(handlers)).fringe()) {
|
||||
|
||||
activated(occurrence("foo")) }.apply {
|
||||
expand(occurrence("foo")) }.apply {
|
||||
matches().count() shouldBe 0 }.run {
|
||||
|
||||
activated(occurrence("bar")) }.apply {
|
||||
expand(occurrence("bar")) }.apply {
|
||||
matches().count() shouldBe 1
|
||||
matches().first().rule().tag() shouldBe "rule2" }.run {
|
||||
|
||||
activated(occurrence("bazz")) }.apply {
|
||||
expand(occurrence("bazz")) }.apply {
|
||||
matches().count() shouldBe 1
|
||||
matches().first().rule().tag() shouldBe "rule1" }.run {
|
||||
|
||||
activated(occurrence("blin")) }.apply {
|
||||
expand(occurrence("blin")) }.apply {
|
||||
matches().count() shouldBe 1
|
||||
matches().first().rule().tag() shouldBe "rule3"
|
||||
}
|
||||
|
|
@ -661,24 +762,24 @@ class TestRuleMatcher {
|
|||
val bar = occurrence("bar")
|
||||
with(Dispatcher(RuleIndex(handlers)).fringe()) {
|
||||
|
||||
activated(occurrence("foo")) }.apply {
|
||||
expand(occurrence("foo")) }.apply {
|
||||
matches().count() shouldBe 0 }.run {
|
||||
|
||||
activated(bar) }.apply {
|
||||
expand(bar) }.apply {
|
||||
matches().count() shouldBe 1
|
||||
matches().first().rule().tag() shouldBe "rule2" }.run {
|
||||
|
||||
activated(occurrence("bazz")) }.apply {
|
||||
expand(occurrence("bazz")) }.apply {
|
||||
matches().count() shouldBe 1
|
||||
matches().first().rule().tag() shouldBe "rule1" }.run {
|
||||
|
||||
discarded(bar) }.apply {
|
||||
contract(bar) }.apply {
|
||||
matches().count() shouldBe 0 }.run {
|
||||
|
||||
activated(occurrence("blin")) }.apply {
|
||||
expand(occurrence("blin")) }.apply {
|
||||
matches().count() shouldBe 0
|
||||
}.run {
|
||||
activated(bar) }.apply {
|
||||
expand(bar) }.apply {
|
||||
matches().count() shouldBe 3
|
||||
matches().map { it.rule().tag() }.toList() shouldBe listOf("rule1", "rule2", "rule3")
|
||||
}
|
||||
|
|
@ -686,5 +787,4 @@ class TestRuleMatcher {
|
|||
}
|
||||
|
||||
private fun Builder.ruleMatcher() = Matcher(rules.first())
|
||||
|
||||
}
|
||||
Loading…
Reference in New Issue