diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/Controller.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/Controller.kt index 425ee6e2..df808d11 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/Controller.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/Controller.kt @@ -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 } diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/Dispatcher.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/Dispatcher.kt index 308c7991..1f562389 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/Dispatcher.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/Dispatcher.kt @@ -54,29 +54,34 @@ class Dispatcher (val ruleIndex: RuleIndex) { constructor(pred: DispatchFringe, matching: Iterable) { 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 = 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) + }) } diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/MatchRuleImpl.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/MatchRuleImpl.kt index 2ab087bf..a6c59653 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/MatchRuleImpl.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/MatchRuleImpl.kt @@ -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, val headReplaced: MutableIterable) : MatchRule { diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/MatchingProbe.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/MatchingProbe.kt index 93b947e2..67cb7783 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/MatchingProbe.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/MatchingProbe.kt @@ -31,10 +31,12 @@ interface MatchingProbe { fun matches() : Collection + fun consumed(matchRule: MatchRule): MatchingProbe + fun expand(occ: ConstraintOccurrence) : MatchingProbe fun expand(occ: ConstraintOccurrence, mask: BitSet) : MatchingProbe fun contract(occ: ConstraintOccurrence): MatchingProbe - + } \ No newline at end of file diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/OccurrenceMatcher.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/OccurrenceMatcher.kt index 6d3fd5d9..f0413bb5 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/OccurrenceMatcher.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/OccurrenceMatcher.kt @@ -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? = diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/ReteNetwork.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/ReteNetwork.kt index 862d382c..e4362341 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/ReteNetwork.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/ReteNetwork.kt @@ -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 = 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 } diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/RuleMatcher.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/RuleMatcher.kt index 5ec07f87..3abeef91 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/RuleMatcher.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/RuleMatcher.kt @@ -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, - val seen: IdHashSet, - val genId: Int) : MatchingProbe { + fun probe(): MatchingProbe = RuleMatchFringe(listOf(MatchNode(emptySubst())), + Sets.of(), + Sets.of(), + 0) + inner class RuleMatchFringe(val nodes: List, + val seen: PersSet>, + val consumed: PersSet?>>, + val genId: Int) : MatchingProbe + { override fun rule(): Rule = rule - override fun matches(): Collection = - nodes.filter { rn -> - rn is ActiveFringeNode && rn.complete && rn.genId == genId }.map { rn -> - (rn as ActiveFringeNode).toMatchRule() } + override fun matches(): Collection { + 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() - 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(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(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?> = + arrayListOf(* arrayOfNulls?>(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 = - unrelatedOrNull(occ)?.run { - ArrayList().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 = + unrelatedOrNull(occ)?.let { n -> + ArrayList().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 fold(init: T, action: (T, ActiveFringeNode) -> T): T { + inline protected fun 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 foldUntilNull(init: T, action: (T, ActiveFringeNode) -> T?): T? { + inline protected fun 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?> = + (parent.signature.clone() as ArrayList?>) + .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 = - 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()))) } } diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/Store.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/Store.kt index 8d9aeeab..2dcb3a8e 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/Store.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/Store.kt @@ -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() } } } diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/util/IdHashSet.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/util/IdHashSet.kt index aa972176..c614a552 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/util/IdHashSet.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/util/IdHashSet.kt @@ -72,6 +72,6 @@ class IdHashSet : AbstractSet { } @Suppress("UNCHECKED_CAST") -fun emptySet(): IdHashSet = IdHashSet.EMPTY_SET as IdHashSet +fun emptyIdSet(): IdHashSet = IdHashSet.EMPTY_SET as IdHashSet -fun singletonSet(e: E): IdHashSet = emptySet().add(e) \ No newline at end of file +fun singletonIdSet(e: E): IdHashSet = emptyIdSet().add(e) \ No newline at end of file diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/util/PersistentTermTrie.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/util/PersistentTermTrie.kt index 3b871bfc..a1212512 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/util/PersistentTermTrie.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/util/PersistentTermTrie.kt @@ -235,7 +235,7 @@ class PersistentTermTrie() : TermTrie { { constructor(symbol: Any, arity: Int) : - this(symbol, arity, Maps.of(), emptySet()) + this(symbol, arity, Maps.of(), emptyIdSet()) constructor(copyFrom: PathNode, setValues: IdHashSet) : this(copyFrom.symbol, copyFrom.arity, copyFrom.next, setValues) diff --git a/reactor/Test/test/TestController.kt b/reactor/Test/test/TestController.kt index 568fece0..abe7f651 100644 --- a/reactor/Test/test/TestController.kt +++ b/reactor/Test/test/TestController.kt @@ -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("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("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() { diff --git a/reactor/Test/test/TestRuleMatcher.kt b/reactor/Test/test/TestRuleMatcher.kt index 25680813..1797464f 100644 --- a/reactor/Test/test/TestRuleMatcher.kt +++ b/reactor/Test/test/TestRuleMatcher.kt @@ -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.shouldBe(that: B) = assertEquals(that, this) + @Test + fun testOccurrenceMatchLogical() { + val (X, Y) = metaLogical("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("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("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()) - } \ No newline at end of file