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 8f441d06..5c6a9d53 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/Controller.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/Controller.kt @@ -41,13 +41,8 @@ class Controller( private val frameStack = FrameStack(storeView) - private val matcher = Matcher(ruleIndex, profiler) - private var dispatchFringe = Dispatcher(ruleIndex).fringe() - // persistent (functional) object. reassigned on update - private var propHistory = PropagationHistory() - internal fun currentFrame(): Frame = frameStack.current fun storeView(): StoreView = frameStack.current.store.view() @@ -131,13 +126,6 @@ class Controller( failure = null } - // propHistory is now functional (persistent) - // we must reassign the field on every rule triggering - // and store on the stack the last value before rule activation in order to undo in case of failure - val savedPropHistory = propHistory - // TODO: prophistory -// this.propHistory = propHistory.record(match) - val savedFrame = frameStack.current frameStack.push() @@ -152,10 +140,6 @@ class Controller( } catch (ex: EvaluationFailureException) { failure = ex - - // abrupt termination: restore the state - this.propHistory = savedPropHistory - frameStack.reset(savedFrame) } diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/Matcher.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/Matcher.kt deleted file mode 100644 index cea8d2c9..00000000 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/Matcher.kt +++ /dev/null @@ -1,195 +0,0 @@ -/* - * Copyright 2014-2017 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.Constraint -import jetbrains.mps.logic.reactor.program.Predicate -import jetbrains.mps.logic.reactor.program.Rule -import jetbrains.mps.logic.reactor.util.LazyIterable -import jetbrains.mps.logic.reactor.util.Profiler -import jetbrains.mps.unification.Substitution -import jetbrains.mps.unification.Term -import jetbrains.mps.unification.TermWrapper -import com.github.andrewoma.dexx.collection.List as PersList - -/** - * @author Fedor Isakov - */ - -class Matcher(val ruleIndex: RuleIndex, - val profiler: Profiler? = null) -{ - - private val rule2matchTrieSet = HashMap() - - fun matches(activeOcc: ConstraintOccurrence, aux: OccurrenceIndex) : Iterable = object : Iterable { - - override fun iterator(): Iterator { - - val relevantRules = ruleIndex.forOccurrence(activeOcc).toList() - - val tries = LazyIterable(relevantRules) { rule -> - rule2matchTrieSet[rule] ?: MatchTrieSet(rule, profiler).apply { - rule2matchTrieSet[rule] = this - } - }.asSequence() - - return tries.flatMap { matchTrieSet -> - matchTrieSet.matches(activeOcc, aux) - }.map { partialMatch -> - partialMatch.complete(profiler) - }.filter { match -> - match.successful - }.iterator() - } - - } - -} - -class Match(val rule: Rule, - val substitution: Substitution, - val keptOccurrences: List, - val discardedOccurrences: List) : MatchRule -{ - - val logicalContext: LogicalContext by lazy(LazyThreadSafetyMode.NONE) { - object : LogicalContext { - - // invariant: the variables in substitution bindings can only be instances of MetaLogical - val meta2subs = substitution.bindings().map { b -> - (b.`var`().symbol() as MetaLogical).to(b.term().toValue()) - }.toMap(HashMap, Any?>()) - - val meta2logical = HashMap, Logical<*>>() - - override fun variable(meta: MetaLogical): Logical = - (meta2logical[meta] ?: meta2subs[meta]?.let { value -> - when (value) { - is Logical<*> -> value - is LogicalOwner -> value.logical() - else -> LogicalImpl(value) - } - } ?: meta.logical().also { - logical -> meta2logical[meta] = logical }) as Logical - - } - } - - val patternPredicates: List by lazy(LazyThreadSafetyMode.NONE) { - (rule.headKept() + rule.headReplaced()).zip(keptOccurrences + discardedOccurrences).flatMap { p -> - p.first.patternPredicates(p.second.arguments()) }.toList() - } - - val successful: Boolean - get() = substitution.isSuccessful - - val isPropagation: Boolean - get() = !keptOccurrences.isEmpty() && discardedOccurrences.isEmpty() - - override fun rule(): Rule = rule - - override fun matchHeadKept(): Iterable = keptOccurrences - - override fun matchHeadReplaced(): Iterable = discardedOccurrences - - override fun logicalContext(): LogicalContext = logicalContext -} - -/** Function term with arguments == constraints converted to terms. May contain variables. */ -class RuleTerm(rule: Rule) : - Function( - rule.tag(), - (rule.headKept() + rule.headReplaced()).map { c -> ConstraintPatternTerm(c) }) {} - -/** Function term with arguments == constraint arguments converted to terms. - * MetaLogical arguments are term variables. - * Everything else is either a term or a constant wrapping the value. */ -class ConstraintPatternTerm(constraint: Constraint) : - Function( - constraint.symbol(), - constraint.arguments().mapIndexed { idx: Int, arg: Any? -> arg.asTerm() }) {} - -/** Function term with arguments == terms corresponding to constraint occurrences. Never contains variables. */ -class MatchTerm(rule: Rule, kept: List, discarded: List) : - Function(rule.tag(), (kept + discarded).map { co -> ConstraintOccurrenceTerm(co) }) {} - -/** Function term with arguments == constraint occurrence arguments converted to terms. - * Logical arguments are constants wrapping the logical itself. - * Everything else is either a term or a constant wrapping the value. - * Never contains variable terms. */ -class ConstraintOccurrenceTerm(occurrence: ConstraintOccurrence) : - Function( - occurrence.constraint().symbol(), - occurrence.arguments().mapIndexed { idx: Int, arg: Any? -> arg.asTerm() }) {} - - -/** Wraps the terms for the internal representation of the unification algorithm. - * When unifying constraint and occurrence terms we are interested in bindings of the meta logicals, - * so these are represented as variables. - * In addition, the logicals are either represented as constants (unbound ones) or their values. - * When unwrapping, the reverse transformation takes place, so that the unification result binds meta logicals - * to logicals, and not to their values. */ -class MatchTermWrapper() : TermWrapper { - - override fun wrap(orig: Term): Term = - if (orig.`is`(Term.Kind.VAR)) { - val symbol = orig.symbol() - when (symbol) { - is MetaLogical<*> -> orig - is Logical<*> -> symbol.let { logical -> - if (logical.isBound && logical.findRoot().value() is Term) { - WrapGroundLogical(logical as Logical) - - } else { - WrapFreeLogical(logical) - } - } - else -> WrapConstant(orig) - } - - } else { - orig - } - - override fun unwrap(wrapper: Term): Term = when (wrapper) { - is WrapConstant -> wrapper.orig - is WrapFreeLogical -> Constant(wrapper.logical) - is WrapGroundLogical -> Constant(wrapper.logical) - else -> wrapper - } - -} - -fun Any?.asTerm(): Term = when (this) { - is MetaLogical<*> -> Variable(this) - is Logical<*> -> Variable(this) -// is Logical<*> -> if (this.isBound) this.findRoot().value().asTerm() else Constant(this.findRoot()) - is Term -> this // wrapped before unification - is Any -> Constant(this) - else -> throw NullPointerException() -} - -// FIXME: "unpacking" the logicals -fun Term.toValue(): Any? = if (this is Constant) this.symbol() else this - diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/PartialMatch.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/PartialMatch.kt deleted file mode 100644 index 851fe0b7..00000000 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/PartialMatch.kt +++ /dev/null @@ -1,78 +0,0 @@ -/* - * Copyright 2014-2017 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.program.Rule -import jetbrains.mps.logic.reactor.util.Profiler -import jetbrains.mps.logic.reactor.util.profile -import jetbrains.mps.unification.Substitution -import jetbrains.mps.unification.Unification - -internal class PartialMatch(val rule: Rule) { - - internal lateinit var keptOccurrences: Array - private set - - internal lateinit var discardedOccurrences: Array - private set - - private lateinit var substitution: Substitution - - constructor(rule: Rule, keptSize: Int, discardedSize: Int) : - this(rule) - { - this.keptOccurrences = arrayOfNulls(keptSize) - this.discardedOccurrences = arrayOfNulls(discardedSize) - } - - - fun complete(profiler: Profiler? = null): Match { - return profiler.profile("matchesRule_${rule.tag()}") { - - val kept = keptOccurrences.asList() as List - val discarded = discardedOccurrences.asList() as List - - this.substitution = Unification.unify(MatchTerm(rule, kept, discarded), RuleTerm(rule), MatchTermWrapper()) - - if (substitution.isSuccessful) { - Match(rule, substitution, kept, discarded) - } - else - Match(rule, substitution, emptyList(), emptyList()) - - } - } - - internal fun keep(occ: ConstraintOccurrence, idx: Int): PartialMatch { - val match = PartialMatch(rule) - match.keptOccurrences = this.keptOccurrences.copyOf() - match.keptOccurrences[idx] = occ - match.discardedOccurrences = this.discardedOccurrences - return match - } - - internal fun discard(occ: ConstraintOccurrence, idx: Int): PartialMatch { - val match = PartialMatch(rule) - match.keptOccurrences = this.keptOccurrences - match.discardedOccurrences = this.discardedOccurrences.copyOf() - match.discardedOccurrences[idx] = occ - return match - } - - override fun toString(): String = "${keptOccurrences.toList()} \\ ${discardedOccurrences.toList()}" -} \ No newline at end of file diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/PartialMatchTrie.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/PartialMatchTrie.kt deleted file mode 100644 index f54a1fac..00000000 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/PartialMatchTrie.kt +++ /dev/null @@ -1,447 +0,0 @@ -/* - * Copyright 2014-2017 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.MetaLogical -import jetbrains.mps.logic.reactor.program.Constraint -import jetbrains.mps.logic.reactor.program.Rule -import jetbrains.mps.logic.reactor.util.Profiler -import jetbrains.mps.logic.reactor.util.profile -import jetbrains.mps.unification.Term -import jetbrains.mps.unification.Unification -import java.util.* -import kotlin.collections.ArrayList -import com.github.andrewoma.dexx.collection.Map as PersMap - -/** - * @author Fedor Isakov - */ -internal class MatchTrieSet(val rule: Rule, val profiler: Profiler?) { - - private val keptConstraints = rule.headKept().toCollection(ArrayList(4)) - - private val discardedConstraints = rule.headReplaced().toCollection(ArrayList(4)) - - // for each slot keep a set of "related" slots, that is the slots with matching (meta-)logicals - // this map is built only once per rule - private val relatedSlots: List = - HashMap, BitSet>().let { meta2slots -> - - (keptConstraints + discardedConstraints).forEachIndexed { slot, cst -> - cst.arguments().forEach { arg -> - if (arg is MetaLogical<*>) { - val bs = meta2slots[arg] ?: BitSet().apply { meta2slots[arg] = this } - bs.set(slot) - } - } - } - - ArrayList().apply { - (keptConstraints + discardedConstraints).forEachIndexed { slot, cst -> - val bs = BitSet() - cst.arguments().forEach { arg -> - if (arg is MetaLogical<*>) { - bs.or(meta2slots[arg]) - } - } - bs.clear(slot) - add(bs) - } - } - - } - - val tries = ArrayList() - - fun matches(activeOcc: ConstraintOccurrence, occIndex: OccurrenceIndex): Sequence { - val constraints = keptConstraints + discardedConstraints - - val relevantTries = ArrayList() - val copyTries = ArrayList() - for (t in tries) { - if (!t.vacant.isEmpty) { - copyTries.add(t) - for (idx in t.vacant.stream()) { - if (constraints[idx].probablyMatches(activeOcc)) { - relevantTries.add(PartialMatchTrie(activeOcc, occIndex, t)) - copyTries.removeAt(copyTries.size - 1) - break - } - } - } - } - if (relevantTries.isEmpty()) { - relevantTries.add(PartialMatchTrie(activeOcc, occIndex, null)) - } - - this.tries.clear() - this.tries.addAll(copyTries) - this.tries.addAll(relevantTries) - - return relevantTries.asSequence().flatMap { t -> t.matches() } - } - - inner class PartialMatchTrie(val activeOcc: ConstraintOccurrence, - val occIndex: OccurrenceIndex, - prototype: PartialMatchTrie?) - { - private val root: RootMatchTrieNode = RootMatchTrieNode(prototype?.root) - - val vacant = BitSet() - - fun matches(): Sequence = object : Sequence { - - override fun iterator() = object : Iterator { - - val firstRoot: MatchTrieNode? = root.firstChild - - var next: PartialMatch? = null - - override fun hasNext(): Boolean { - if (next == null) { - this.next = calcNext() - } - return (next != null) - } - - override fun next(): PartialMatch { - if (next == null) { - this.next = calcNext() - } - if (next != null) { - val tmp: PartialMatch = next!! - this.next = calcNext() - return tmp - } - throw NoSuchElementException() - } - - private fun calcNext(): PartialMatch? { - return profiler.profile("partialMatch_calcNext") { - // the search always starts at the first root - if (firstRoot == null) { - return null - } - var mtn: MatchTrieNode? = firstRoot - - while (mtn != null) { - if (mtn.isSeen) { - if (mtn.nextSibling == null) { - mtn.parent?.setSeen() - } - mtn = mtn.nextSibling ?: mtn.parent - - } else if (mtn.isLeaf) { - mtn.setSeen() - vacant.clear() - return mtn.match - - } else if (mtn.firstChild == null) { - mtn.setSeen() - vacant.or(mtn.vacantSlots) - vacant.andNot(mtn.relatedFirstVacantSlots) - - } else { - mtn = mtn.firstChild - } - } - - return null - } - } - } - - } - - private abstract inner class BaseMatchTrieNode() { - - var _firstChild: MatchTrieNode? = null - - protected fun copyChildren(copyFrom: BaseMatchTrieNode, parent: MatchTrieNode?) { - copyFrom._firstChild?.firstAlive()?.let { copyFirst -> - - val first = MatchTrieNode(parent, copyFirst) - var prev = first - var copyNext = copyFirst.nextSibling?.firstAlive() - - while (copyNext != null) { - val next = MatchTrieNode(parent, copyNext) - prev._nextSibling = next - prev = next - copyNext = copyNext.nextSibling?.firstAlive() - } - - this._firstChild = first - } - } - - protected fun buildNode(siblings: Iterable) : MatchTrieNode? { - var first: MatchTrieNode? = null - var prev: MatchTrieNode? = null - for (next in siblings) { - if (first == null) { - first = next - } - prev?._nextSibling = next - prev = next - } - - return first - } - - } - - private inner class RootMatchTrieNode(copyFrom: RootMatchTrieNode? = null) : BaseMatchTrieNode() { - - init { - if (copyFrom != null) { copyChildren(copyFrom, null) } - } - - val firstChild: MatchTrieNode? - get() { - if (_firstChild == null) { - this._firstChild = buildNode(calcRoots()) - } - return _firstChild - } - - private fun calcRoots(): Iterable { - return profiler.profile>("partialMatch_calcRoots") { - - keptConstraints.withIndex().filter {(_, cst) -> - cst.probablyMatches(activeOcc)}.map {(idx, cst) -> - MatchTrieNode(null, true, cst, activeOcc, idx) - } + - discardedConstraints.withIndex().filter {(_, cst) -> - cst.probablyMatches(activeOcc)}.map {(idx, cst) -> - MatchTrieNode(null, false, cst, activeOcc, idx) - } - - } - } - - } - - private inner class MatchTrieNode(val parent: MatchTrieNode?, - val keepConstraint: Boolean, - val constraint: Constraint, - val occurrence: ConstraintOccurrence, - val index: Int) : BaseMatchTrieNode() - { - - constructor(parent: MatchTrieNode?, copyFrom: MatchTrieNode) : - this(parent, copyFrom.keepConstraint, copyFrom.constraint, copyFrom.occurrence, copyFrom.index) - { - copyChildren(copyFrom, this) - } - - val firstChild: MatchTrieNode? - get() { - if (_firstChild == null) { - this._firstChild = buildNode(calcChildren()) - } - return _firstChild - } - - var _nextSibling: MatchTrieNode? = null - - val nextSibling: MatchTrieNode? - get() = _nextSibling - - private var _isSeen: Boolean = false - - val isSeen: Boolean - get() = _isSeen - - val vacantSlots: BitSet by lazy(LazyThreadSafetyMode.NONE) { - val result = BitSet() - result.set(0, keptConstraints.size + discardedConstraints.size) - foldPath(result) { bits, mtn -> - val slot = if (mtn.keepConstraint) mtn.index else mtn.index + keptConstraints.size - bits.clear(slot) - bits - } - result - } - - val relatedFirstVacantSlots: BitSet by lazy(LazyThreadSafetyMode.NONE) { - val result = vacantSlots.clone() as BitSet - result.and(relatedSlots[if (keepConstraint) index else index + keptConstraints.size]) - result - } - - val isLeaf: Boolean - get() = vacantSlots.isEmpty - - val match: PartialMatch by lazy(LazyThreadSafetyMode.NONE) { - val parentMatch = parent?.match ?: PartialMatch(rule, keptConstraints.size, discardedConstraints.size) - if (keepConstraint) parentMatch.keep(occurrence, index) - else parentMatch.discard(occurrence, index) - } - - fun setSeen() { - this._isSeen = true - } - - private fun calcChildren(): Iterable { - val nextSlots = if (!relatedFirstVacantSlots.isEmpty) relatedFirstVacantSlots else vacantSlots - val nextSlot = nextSlots.nextSetBit(0) - if (nextSlot < 0) { - return emptyList() - } - - val keep = nextSlot < keptConstraints.size - val nextIdx = if (keep) nextSlot else nextSlot - keptConstraints.size - val nextCst = if (keep) keptConstraints[nextSlot] else discardedConstraints[nextIdx] - - return if (nextCst.probablyMatches(activeOcc) && !hasOccurrence(activeOcc)) { - arrayListOf(MatchTrieNode(this, keep, nextCst, activeOcc, nextIdx)) - - } - else { - val (result, auxOccurrences) = lookupAuxOccurrences(nextCst) - when (result) { - // FIXME: this optimization is causing major problems, drop it? - Result.DEFINITIVE -> null /*parent*/ - Result.NONE -> this - Result.INCONCLUSIVE -> null - }?.forEachInPath { mtn -> mtn.setSeen() } - - auxOccurrences.map { auxOcc -> MatchTrieNode(this, keep, nextCst, auxOcc, nextIdx) } - } - } - - // the first component indicates the quality of the result: - // DEFINITIVE indicates the only possible matches were returned - // INCONCLUSIVE may yield some (ir-)relevant results - // NONE means no results could have been found at all, so it's useless to attempt again with the same input - private fun lookupAuxOccurrences(cst: Constraint): Pair> { - return profiler.profile>> ("lookupAux_${cst.symbol()}") { - - val fromArgs = ArrayList(4) - for (arg in metaInstances(cst.arguments()) + cst.arguments().filter { arg -> !(arg is MetaLogical<*>) }) { - when (arg) { - is Logical<*> -> fromArgs.addAll(occIndex.forLogicalAndConstraint(arg, cst)) - - is Term -> fromArgs.addAll(occIndex.forTermAndConstraint(arg, cst)) - - is Any -> fromArgs.addAll(occIndex.forValue(arg)) - } - } - if (fromArgs.isNotEmpty()) { - Result.DEFINITIVE.to(fromArgs.filter { occ -> cst.probablyMatches(occ) && !hasOccurrence(occ) }) - - } else { - return profiler.profile>> ("lookupAux_default_${cst.symbol()}") { - - val hasRelated = relatedFirstVacantSlots == vacantSlots - val allArgsMetaLogicals = cst.arguments().all { a -> a is MetaLogical<*> } - val noArgs = cst.arguments().isEmpty() - - if (noArgs || (allArgsMetaLogicals && !hasRelated)) { - Result.INCONCLUSIVE.to(occIndex.forSymbol(cst.symbol()).filter { occ -> cst.probablyMatches(occ) && !hasOccurrence(occ) }) - - } - else { - // all candidate occurrences should have been found by this time; if not, then there's none - Result.NONE.to(emptyList()) - } - } - } - } - } - - fun firstAlive(): MatchTrieNode? { - var fca: MatchTrieNode? = this - while (!(fca?.occurrence?.isAlive() ?: true)) { - fca = fca?.nextSibling - } - return fca - } - - - private fun collectMetaInstances(meta: Collection<*>, list: ArrayList): ArrayList { - constraint.arguments().zip(occurrence.arguments()).forEach { p -> - if (p.first is MetaLogical<*> && meta.contains(p.first) && !list.contains(p.second)) { - list.add(p.second!!) - } - } - return list - } - - private fun metaInstances(meta: Collection<*>): List = - foldPath(ArrayList(4)) { list, mtn -> mtn.collectMetaInstances(meta, list) } - - private fun hasOccurrence(occ: ConstraintOccurrence): Boolean = - anyInPath { mtn -> mtn.occurrence === occ } // referential equality! - - private inline fun anyInPath(predicate: (MatchTrieNode) -> Boolean): Boolean = - foldPath(false) { b, mtn -> b || predicate(mtn) } - - private inline fun forEachInPath(proc: (MatchTrieNode) -> Unit) = - foldPath(Unit) { b, mtn -> proc(mtn) } - - private inline fun foldPath(initVal: T, step: (T, MatchTrieNode) -> T): T { - var mtn: MatchTrieNode? = this - var currVal = initVal - while(mtn != null) { - currVal = step(currVal, mtn) - mtn = mtn.parent - } - return currVal - } - - } - - } - - fun Constraint.probablyMatches(occ: ConstraintOccurrence): Boolean { - if (this.symbol() != occ.constraint().symbol()) { return false } - - val cstArgIt = this.arguments().iterator() - val occArgIt = occ.arguments().iterator() - while (cstArgIt.hasNext() && occArgIt.hasNext()) { - val cstArg = cstArgIt.next() - val occArg = occArgIt.next() - - if (cstArg is Term && occArg is Term) { - if (!Unification.unify(cstArg, occArg).isSuccessful) { return false } - } - - if (cstArg !is MetaLogical<*> && occArg !is Logical<*>) { - if (!(cstArg?.equals(occArg) ?: (occArg === null))) { return false } - } - } - - return true - } - - enum class Result { - DEFINITIVE, - INCONCLUSIVE, - NONE - } - -} - - - - - - diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/PropagationHistory.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/PropagationHistory.kt deleted file mode 100644 index 2eb0dac9..00000000 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/PropagationHistory.kt +++ /dev/null @@ -1,59 +0,0 @@ -/* - * Copyright 2014-2017 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 com.github.andrewoma.dexx.collection.ConsList -import com.github.andrewoma.dexx.collection.Maps -import com.github.andrewoma.dexx.collection.Map as PersMap -import com.github.andrewoma.dexx.collection.List as PersList -import jetbrains.mps.logic.reactor.evaluation.ConstraintOccurrence -import jetbrains.mps.logic.reactor.program.Rule -import jetbrains.mps.logic.reactor.util.IdWrapper - -internal class PropagationHistory { - - val recordedPropagation : PersMap>>> - - constructor() { - this.recordedPropagation = Maps.of>>> () - } - - private constructor(recorded : PersMap>>>) { - this.recordedPropagation = recorded - } - - fun isRecorded(m: Match): Boolean { - if (!m.isPropagation) return false - val test = m.keptOccurrences.map { occ -> IdWrapper(occ) }.sortedBy { idOcc -> idOcc.idHash }.toList() - - return recordedPropagation.get(m.rule)?.let { hist -> - hist.any { recorded -> recorded == test } // use the reference equality via IdWrapper - } ?: false - } - - fun record(pm: Match): PropagationHistory { - if (pm.isPropagation) { - val idOccs = pm.keptOccurrences.map { occ -> IdWrapper(occ) }.sortedBy { id -> id.idHash }.toList() - - val hist = recordedPropagation.get(pm.rule) ?: ConsList.empty>>() - - return PropagationHistory(recordedPropagation.put(pm.rule, hist.prepend(idOccs))) - } - return this - } - -} \ No newline at end of file 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 63af9e79..234cceee 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/Store.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/Store.kt @@ -52,7 +52,7 @@ interface StoreItem { var stored: Boolean - fun terminate(): Unit + fun terminate() } @@ -66,26 +66,10 @@ interface StoreKeeper { } -interface OccurrenceIndex { - - fun forSymbol(symbol: ConstraintSymbol): Iterable - - fun forLogical(logical: Logical<*>): Iterable - - fun forLogicalAndConstraint(logical: Logical<*>, cst:Constraint): Iterable - - fun forTerm(term: Term): Iterable - - fun forTermAndConstraint(term: Term, cst: Constraint): Iterable - - fun forValue(value: Any): Iterable - -} - /** * TODO: make this class persistent. */ -class Store : LogicalObserver, OccurrenceIndex { +class Store : LogicalObserver { val currentFrame: () -> StoreKeeper @@ -93,16 +77,10 @@ class Store : LogicalObserver, OccurrenceIndex { var logical2occurrences: PersMap>, IdHashSet> - var term2occurrences: TermTrie - - var value2occurrences: PersMap> - constructor(copyFrom: Store, currentFrame: () -> StoreKeeper) { this.currentFrame = currentFrame this.symbol2occurrences = copyFrom.symbol2occurrences this.logical2occurrences = copyFrom.logical2occurrences - this.term2occurrences = copyFrom.term2occurrences - this.value2occurrences = copyFrom.value2occurrences } constructor(copyFrom: StoreView, currentFrame: () -> StoreKeeper) { @@ -126,40 +104,15 @@ class Store : LogicalObserver, OccurrenceIndex { } this.logical2occurrences = l2o - this.term2occurrences = t2o - this.value2occurrences = v2o } constructor(currentFrame: () -> StoreKeeper) { this.currentFrame = currentFrame this.symbol2occurrences = Maps.of() this.logical2occurrences = Maps.of() - this.term2occurrences = TermTrie() - this.value2occurrences = Maps.of() } override fun valueUpdated(logical: Logical<*>) { - logical2occurrences[IdWrapper(logical.findRoot())]?.let { toMerge -> - val value = logical.findRoot().value() - when (value) { - is Term -> { - for (occ in toMerge) { - this.term2occurrences = term2occurrences.put(value.withConstraint(occ.constraint()), occ) - } - } - is Any -> { - var newSet = value2occurrences[value] ?: emptySet() - for (occ in toMerge) { - newSet = newSet.add(occ) - } - this.value2occurrences = value2occurrences.put(value, newSet) - } - else -> { - // never happens - throw NullPointerException() - } - } - } } override fun parentUpdated(logical: Logical<*>) { @@ -177,7 +130,7 @@ class Store : LogicalObserver, OccurrenceIndex { } } - fun store(occ: ConstraintOccurrence): Unit { + fun store(occ: ConstraintOccurrence) { val symbol = occ.constraint().symbol() this.symbol2occurrences = symbol2occurrences.put(symbol, @@ -193,17 +146,6 @@ class Store : LogicalObserver, OccurrenceIndex { logical2occurrences[argId]?.add(occ) ?: singletonSet(occ)) currentFrame().addObserver(value) { frame -> frame.store() } } - is Term -> { - this.term2occurrences = term2occurrences.put(value.withConstraint(occ.constraint()), occ) - } - is Any -> { - this.value2occurrences = value2occurrences.put(value, - value2occurrences[value]?.add(occ) ?: singletonSet(occ)) - } - else -> { - // never happens - throw NullPointerException() - } } } @@ -231,16 +173,6 @@ class Store : LogicalObserver, OccurrenceIndex { } } } - is Term -> { - // removing occurrences from the index is *very* expensive, - // so let's simply use the 'alive' flag to filter out terminated occurrences -// this.term2occurrences = term2occurrences.remove(arg, occ) - } - is Any -> { - value2occurrences[arg]?.remove(occ)?. let { newList -> - this.value2occurrences = value2occurrences.put(arg, newList) - } - } } } @@ -255,64 +187,14 @@ class Store : LogicalObserver, OccurrenceIndex { fun view(): StoreView = StoreViewImpl(allOccurrences()) - override fun forSymbol(symbol: ConstraintSymbol): Iterable { - return (symbol2occurrences[symbol] ?: emptySet()).filter { co -> co.isStored() } - } - - override fun forLogicalAndConstraint(logical: Logical<*>, cst: Constraint): Iterable { - return if (logical.isBound) { - val value = logical.findRoot().value() - when (value) { - is Term -> forTermAndConstraint(value, cst) - is Any -> forValue(value) - else -> throw NullPointerException() - } - - } else { - (logical2occurrences[IdWrapper(logical.findRoot())] ?: emptySet()).filter { co -> co.isStored() } - } - } - - override fun forLogical(logical: Logical<*>): Iterable { - return if (logical.isBound) { - val value = logical.findRoot().value() - when (value) { - is Term -> forTerm(value) - is Any -> forValue(value) - else -> throw NullPointerException() - } - - } else { - (logical2occurrences[IdWrapper(logical.findRoot())] ?: emptySet()).filter { co -> co.isStored() } - } - } - - override fun forTerm(term: Term): Iterable { - return term2occurrences.lookupValues(term.withAny()).filter { it.isStored() } - } - - override fun forTermAndConstraint(term: Term, cst: Constraint): Iterable { - return term2occurrences.lookupValues(term.withConstraint(cst)).filter { it.isStored() } - } - - override fun forValue(value: Any): Iterable { - return (value2occurrences[value] ?: emptySet()).filter { co -> co.isStored() } - } - private fun Term.withConstraint(cst: Constraint): Term = Function(CONSTRAINT, listOf(Function(cst.symbol(), emptyList()), this)) - private fun Term.withAny(): Term = Function(CONSTRAINT, listOf(Variable(ANY), this)) - private companion object { private val CONSTRAINT = object : Any() { override fun toString(): String = "CONSTRAINT" } - private val ANY = object : Any() { - override fun toString(): String = "ANY" - } - } } diff --git a/reactor/Test/test/TestMatcher.kt b/reactor/Test/test/TestMatcher.kt deleted file mode 100644 index 7b24d2d1..00000000 --- a/reactor/Test/test/TestMatcher.kt +++ /dev/null @@ -1,581 +0,0 @@ -import jetbrains.mps.logic.reactor.core.* -import jetbrains.mps.logic.reactor.evaluation.ConstraintOccurrence -import jetbrains.mps.logic.reactor.logical.Logical -import jetbrains.mps.logic.reactor.program.Constraint -import jetbrains.mps.logic.reactor.program.ConstraintSymbol -import jetbrains.mps.unification.Term -import jetbrains.mps.unification.Unification -import jetbrains.mps.unification.test.MockTermsParser.parseTerm -import org.junit.Assert.* -import org.junit.Test - -/** - * @author Fedor Isakov - */ - -class TestMatcher { - - @Test - fun matchSingle() { - programWithRules( - rule("main", - headReplaced( - constraint("main") - ), - body( - constraint("foo") - )) - ).let { builder -> - builder.indices().run { - Matcher(first).matching(occurrence("main"), second).let { matches -> - val match = matches.single() - assertEquals(match.rule, builder.rules.first()) - assertTrue(match.keptOccurrences.isEmpty()) - val occ = match.discardedOccurrences.single() - assert(occ.constraint().symbol().id() == "main") - } - } - } - } - - @Test - fun matchDiscardedKept() { - programWithRules( - rule("main1", - headReplaced( - constraint("main") - ), - body( - constraint("foo") - )), - rule("main2", - headKept( - constraint("main") - ), - body( - constraint("bar") - )) - ).let { builder -> - builder.indices().run { - Matcher(first).matching(occurrence("main"), second).let { matches -> - assertTrue(matches.all {m -> m.successful}) - assertEquals(builder.rules.toSet(), matches.map { m -> m.rule }.toSet()) - matches.forEach { m -> assertTrue(m.keptOccurrences.size + m.discardedOccurrences.size == 1) } - matches.flatMap { m -> - (m.keptOccurrences.toList() + m.discardedOccurrences.toList()) }.forEach { occ -> - assert(occ.constraint().symbol().id() == "main") - } - } - } - } - } - - @Test - fun matchComplementMissing() { - programWithRules( - rule("main1", - headKept( - constraint("main") - ), - headReplaced( - constraint("secondary") - ), - body( - constraint("foo") - )), - rule("main2", - headKept( - constraint("main") - ), - body( - constraint("bar") - )) - ).let { builder -> - builder.indices().run { - Matcher(first).matching(occurrence("main"), second).let { matches -> - assertTrue(matches.all {m -> m.successful}) - assertEquals(builder.rules.drop(1).toSet(), matches.map { m -> m.rule }.toSet()) - } - } - } - } - - @Test - fun matchComplementPresent() { - programWithRules( - rule("main1", - headKept( - constraint("main") - ), - headReplaced( - constraint("aux") - ), - body( - constraint("foo") - )), - rule("main2", - headKept( - constraint("main") - ), - body( - constraint("bar") - )) - ).let { builder -> - builder.indices(occurrence("aux")).run { - Matcher(first).matching(occurrence("main"), second).let { matches -> - assertTrue(matches.all {m -> m.successful}) - assertEquals(builder.rules.toSet(), matches.map { m -> m.rule }.toSet()) - } - } - } - } - - @Test - fun matchArgument() { - programWithRules( - rule("main1", - headKept( - constraint("main", "foo") - ), - body( - constraint("foo") - )), - rule("main2", - headKept( - constraint("main", "bar") - ), - body( - constraint("bar") - )) - ).let { builder -> - builder.indices().run{ - Matcher(first).matching(occurrence("main", "bar"), second).let { matches -> - assertTrue(matches.all {m -> m.successful}) - assertEquals(builder.rules.drop(1), matches.map { m -> m.rule }.toList()) - } - } - } - } - - @Test - fun noMatchArgument() { - programWithRules( - rule("main1", - headKept( - constraint("main", "foo") - ), - body( - constraint("foo") - )), - rule("main2", - headKept( - constraint("main", "bar") - ), - body( - constraint("bar") - )) - ).indices().run{ - Matcher(first).matching(occurrence("main", "qux"), second).let { matches -> - assertFalse(matches.any()) - } - } - } - - @Test - fun multipleHandlers() { - programWithHandlers( - handler("handler1", emptyList(), - rule("main1", - headKept( - constraint("foo") - )) - ), - handler("handler2", emptyList(), - rule("main2", - headKept( - constraint("bar") - )) - ) - ).indices().run { - Matcher(first).matching(occurrence("qux"), second).let { matches -> - assertFalse(matches.any()) - } - Matcher(first).matching(occurrence("foo"), second).let { matches -> - assertSame(1, matches.size) - } - Matcher(first).matching(occurrence("bar"), second).let { matches -> - assertSame(1, matches.size) - } - } - } - - @Test - fun metaLogical() { - val (A, B, C) = metaLogical("A", "B", "C") - val b = B.logical() - - programWithRules( - rule("main", - headKept( - constraint("foo", A, B) - ), - body( - constraint("bar", B) - ) - ) - ).indices().run { - Matcher(first).matches(occurrence("foo", "blah", b), second).first().run { - assert(successful) - assertEquals("blah", logicalContext.variable(A).findRoot().value()) - assertSame(b, logicalContext.variable(B)) - assertEquals(C.logical().metaLogical(), logicalContext.variable(C).metaLogical()) - } - } - - } - - @Test - fun matchMetaLogical() { - val (M, N) = metaLogical("M", "N") - - programWithRules( - rule("main1", - headKept( - constraint("foo", M) - ), - headReplaced( - constraint("foo", N) - ), - body( - constraint("bar") - )), - rule("main2", - headKept( - constraint("foo", M) - ), - headReplaced( - constraint("foo", M) - ), - body( - constraint("bar") - )) - ).run { - indices().run { - Matcher(first).matching(occurrence("foo", 1), second).let { matches -> - assertFalse(matches.any()) - } - } - - // same parameter -- 4 matches (all permutations) - indices(occurrence("foo", 42)).run { - Matcher(first).matching(occurrence("foo", 42), second).let { matches -> - assertTrue(matches.all {m -> m.successful}) - assertEquals(4, matches.count()) - assertTrue(matches.all { m -> m.allOccurrences().toSet().size == 2 }) - } - } - - indices(occurrence("foo", 42)).run { - Matcher(first).matching(occurrence("foo", 16), second).let { matches -> - assertTrue(matches.all {m -> m.successful}) - assertEquals(2, matches.count()) - assertEquals(listOf("main1", "main1"), matches.map { m -> m.rule.tag() }.toList()) - matches.map { m -> - setOf(M, N).map { lp -> - m.logicalContext.variable(lp).findRoot().value() - } - }.forEach { vals -> - assertEquals(setOf(42, 16), vals.toSet()) - } - assertTrue(matches.all { m -> m.allOccurrences().toSet().size == 2 }) - } - } - - val (x, y) = logical("x", "y") - x.set(123) - y.set(456) - - indices(occurrence("foo", x)).run { - Matcher(first).matching(occurrence("foo", y), second).let { matches -> - assertTrue(matches.all {m -> m.successful}) - assertEquals(2, matches.count()) - assertEquals(listOf("main1", "main1"), matches.map { m -> m.rule.tag() }.toList()) - assertTrue(matches.all { m -> m.allOccurrences().toSet().size == 2 }) - } - } - - val (v, w) = logical("v", "w") - w.findRoot().union(v) - - indices(occurrence("foo", v)).run { - Matcher(first).matching(occurrence("foo", w), second).let { matches -> - assertTrue(matches.all {m -> m.successful}) - assertEquals(2, matches.count()) - assertTrue(matches.all{ m -> m.allOccurrences().toSet().size == 2 }) - } - } - } - } - - @Test - fun matchOccurrenceArguments() { - val (M, N) = metaLogical("M", "N") - val (O, P) = metaLogical("O", "P") - - programWithRules( - rule("select_A_x", - headKept( - constraint("foo", "A", M) - ), - headReplaced( - constraint("foo", "A", N) - ), - body( - constraint("bar") - )), - rule("select_A_B", - headReplaced( - constraint("foo", "A", "B") - ), - body( - constraint("bar") - )), - rule("select_x_B", - headKept( - constraint("foo", M, "B") - ), - body( - constraint("bar") - )), - rule("select_B_x", - headKept( - constraint("foo", "B", M) - ), - body( - constraint("bar") - )), - rule("select_ALL", - headKept( - constraint("foo", O, P) - ), - body( - constraint("bar") - )) - ).indices().first.run { - val x = logical("X") - - assertEquals( - listOf(byTag("select_A_x"), byTag("select_A_B"), byTag("select_x_B"), byTag("select_ALL")), - forOccurrence(occurrence("foo", "A", x)).toList()) - assertEquals( - listOf(byTag("select_x_B"), byTag("select_B_x"), byTag("select_ALL")), - forOccurrence(occurrence("foo", "B", x)).toList()) - assertEquals( - listOf(byTag("select_B_x"), byTag("select_ALL")), - forOccurrence(occurrence("foo", "B", "C")).toList()) - - } - } - - @Test - fun matchOccurrenceTermArguments() { - val (M, N) = metaLogical("M", "N") - val (O, P) = metaLogical("O", "P") - - programWithRules( - rule("select_fg_x", - headKept( - constraint("foo", parseTerm("f{g}"), M) - ), - body( - constraint("bar") - )), - rule("select_abX_x", - headKept( - constraint("foo", parseTerm("a{b X}"), M) - ), - body( - constraint("bar") - )), - rule("select_aYcde_x", - headKept( - constraint("foo", parseTerm("a{Y c{d e}}"), M) - ), - body( - constraint("bar") - )), - rule("select_aYcdd_fg", - headKept( - constraint("foo", parseTerm("a{Y c{d d}}"), parseTerm("f{g}")) - ), - body( - constraint("bar") - )) - ).indices().first.run { - - assertEquals( - listOf(byTag("select_fg_x")), - forOccurrence(occurrence("foo", parseTerm("f{g}"), parseTerm("u"))).toList()) - assertEquals( - listOf(byTag("select_fg_x")), - forOccurrence(occurrence("foo", parseTerm("f{Z}"), parseTerm("u"))).toList()) - assertEquals( - listOf(byTag("select_abX_x"), byTag("select_aYcde_x")), - forOccurrence(occurrence("foo", parseTerm("a{b c{d Z}}"), parseTerm("u"))).toList()) - assertEquals( - listOf(byTag("select_aYcdd_fg")), - forOccurrence(occurrence("foo", parseTerm("a{d c{d d}}"), parseTerm("f{g}"))).toList()) - - } - } - - @Test - fun matchTermArguments() { - programWithRules( - rule("select_abcde", - headKept( - constraint("foo", parseTerm("a{b{h} c{d e}}")) - ), - body( - constraint("bar") - )), - rule("select_abcdf", - headKept( - constraint("foo", parseTerm("a{b{h} c{d f}}")) - ), - body( - constraint("bar") - )), - rule("select_agcde", - headKept( - constraint("foo", parseTerm("a{g{h} c{d e}}")) - ), - body( - constraint("bar") - )) - ).indices().first.run { - - assertEquals( - listOf(byTag("select_abcde")), - forOccurrence(occurrence("foo", parseTerm("a{b{h} c{d e}}"))).toList()) - assertEquals( - listOf(byTag("select_abcdf")), - forOccurrence(occurrence("foo", parseTerm("a{b{h} c{d f}}"))).toList()) - assertEquals( - listOf(byTag("select_agcde")), - forOccurrence(occurrence("foo", parseTerm("a{g{h} c{d e}}"))).toList()) - - } - } - - @Test - fun matchConstraintsWrongOrder() { - - val (b, c) = metaLogical("b", "c") - val (x, y) = metaLogical("x", "y") - - val program = programWithRules( - rule("foo2", - headKept( - constraint("foo", b, parseTerm("a{b}")), - constraint("foo", c, parseTerm("a{c}")) - ), - body( - constraint("done") - ) - ) - ) - - program.indices(occurrence("foo", x, parseTerm("a{c}"))).run { - Matcher(first).matching(occurrence("foo", y, parseTerm("a{b}")), second).let { matches -> - assertEquals("foo2", matches.single().rule.tag()) - } - } - program.indices(occurrence("foo", x, parseTerm("a{b}"))).run { - Matcher(first).matching(occurrence("foo", y, parseTerm("a{c}")), second).let { matches -> - assertEquals("foo2", matches.single().rule.tag()) - } - } - } - - @Test - fun matchConstraintsIncrementally() { - - val (b, c, d) = metaLogical("b", "c", "d") - val (x, y, z) = metaLogical("x", "y", "z") - - val program = programWithRules( - rule("expected", - headKept( - constraint("foo", d, parseTerm("a{d}")), - constraint("foo", b, parseTerm("a{b}")), - constraint("foo", c, parseTerm("a{c}")) - ), - body( - constraint("done") - ) - ) - ) - - val stored = ArrayList() - program.indices(stored).run { - val matcher = Matcher(first) - val occ1 = occurrence("foo", x, parseTerm("a{c}")) - stored.add(occ1) - matcher.matching(occ1, second).let { matches -> - assertTrue(matches.isEmpty()) - } - val occ2 = occurrence("foo", y, parseTerm("a{b}")) - stored.add(occ2) - matcher.matching(occ2, second).let { matches -> - assertTrue(matches.isEmpty()) - } - val occ3 = occurrence("foo", z, parseTerm("a{d}")) - stored.add(occ3) - matcher.matching(occ3, second).let { matches -> - assertEquals("expected", matches.single().rule.tag()) - } - } - } - - private fun Builder.indices(vararg occurrence: ConstraintOccurrence): Pair = - this.indices(occurrence.toList()) - - private fun Builder.indices(stored: List): Pair { - - val aux = object : OccurrenceIndex { - override fun forSymbol(symbol: ConstraintSymbol): Iterable = - stored.filter { co -> co.constraint().symbol() == symbol } - - override fun forLogical(logical: Logical<*>): Iterable = - stored.filter { co -> - co.arguments().any { it is Logical<*> && it.isBound && it.findRoot() == logical.findRoot() } - } - - override fun forLogicalAndConstraint(logical: Logical<*>, cst: Constraint): Iterable = - stored.filter { co -> - co.arguments().any { it is Logical<*> && it.isBound && it.findRoot() == logical.findRoot() } - } - - override fun forTerm(term: Term): Iterable = - stored.filter { co -> - co.arguments().any { it is Term && Unification.unify(it, term).isSuccessful } - } - - override fun forTermAndConstraint(term: Term, cst: Constraint): Iterable = - stored.filter { co -> - co.constraint().symbol() == cst.symbol() && co.arguments().any { it is Term && Unification.unify(it, term).isSuccessful } - } - - override fun forValue(value: Any): Iterable = - stored.filter { co -> co.arguments().contains(value) } - } - - return RuleIndex(handlers).to(aux) - } - - private fun Match.allOccurrences() = (keptOccurrences + discardedOccurrences) - - private fun Matcher.matching(activeOcc: ConstraintOccurrence, aux: OccurrenceIndex) = this.matches(activeOcc, aux).filter { m -> m.successful } - -} diff --git a/reactor/Test/test/TestOccurrenceStore.kt b/reactor/Test/test/TestOccurrenceStore.kt deleted file mode 100644 index 7e56f1a5..00000000 --- a/reactor/Test/test/TestOccurrenceStore.kt +++ /dev/null @@ -1,153 +0,0 @@ -import jetbrains.mps.logic.reactor.core.* -import jetbrains.mps.logic.reactor.logical.Logical -import jetbrains.mps.logic.reactor.program.ConstraintSymbol.symbol -import jetbrains.mps.logic.reactor.util.emptyConsList -import jetbrains.mps.unification.Term -import jetbrains.mps.unification.test.MockTermsParser.parseTerm -import org.junit.Test -import org.junit.Assert.* -import org.junit.Before - -/** - * @author Fedor Isakov - */ - -class TestOccurrenceStore { - - internal class MockProxy(val _store: () -> Store) : LogicalObserver, StoreKeeper { - - private var observerList = emptyConsList, LogicalObserver>>() - - override fun store(): Store = _store() - - override fun addObserver(logical: Logical<*>, obs: (StoreKeeper) -> LogicalObserver) { - if (!observerList.any { obs -> obs.first === logical }) { // referential equality! - logical.addObserver(this) - } - this.observerList = observerList.prepend(logical.to(obs(this))) - } - - override fun removeObserver(logical: Logical<*>, obs: (StoreKeeper) -> LogicalObserver) = TODO() - - override fun valueUpdated(logical: Logical<*>) { - for (obs in observerList) { - if (obs.first === logical) { // referential equality! - obs.second.valueUpdated(logical) - } - } - } - - override fun parentUpdated(logical: Logical<*>) { - for (obs in observerList) { - if (obs.first === logical) { // referential equality! - obs.second.parentUpdated(logical) - } - } - } - } - - lateinit var occstore: Store - - @Before - fun setup() { - occstore = Store { MockProxy { occstore } } - } - - @Test - fun testMergeLogicals() { - val foo = logical("foo") - val bar = logical("bar") - - val main = occurrence("main", foo) - occstore.store(main) - assertEquals(listOf(main), occstore.forLogical(foo)) - assertEquals(listOf(main), occstore.forSymbol(symbol("main", 1))) - - bar.union(foo) - assertEquals(listOf(main), occstore.forLogical(foo)) - assertEquals(listOf(main), occstore.forLogical(bar)) - - val bazz = logical("bazz") - val main2 = occurrence("main", bazz) - occstore.store(main2) - assertEquals(listOf(main2), occstore.forLogical(bazz)) - - bazz.union(bar) - assertEquals(setOf(main, main2), occstore.forLogical(bazz).toSet()) - assertEquals(occstore.forLogical(foo), occstore.forLogical(bazz)) - assertEquals(occstore.forLogical(bar), occstore.forLogical(bazz)) - - occstore.discard(main) - assertEquals(listOf(main2), occstore.forLogical(foo)) - assertEquals(listOf(main2), occstore.forLogical(bar)) - assertEquals(listOf(main2), occstore.forLogical(bazz)) - } - - @Test - fun testLateGroundLogical() { - val foo = logical("foo") - val bar = logical("bar") - - val cnst = occurrence("cnst", foo) - occstore.store(cnst) - assertEquals(listOf(cnst), occstore.forLogical(foo)) - assertEquals(listOf(cnst), occstore.forSymbol(symbol("cnst", 1))) - - foo.set(parseTerm("a{b c d{e}}")) - - assertEquals(listOf(cnst), occstore.forLogical(foo)) - assertEquals(listOf(cnst), occstore.forTerm(parseTerm("a{b c d{e}}"))) - - foo.union(bar) - assertEquals(listOf(cnst), occstore.forLogical(bar)) - } - - @Test - fun testEarlyGroundLogical() { - val foo = logical("foo") - - foo.set(parseTerm("a{b c d{e}}")) - - val cnst = occurrence("cnst", foo) - occstore.store(cnst) - - assertEquals(listOf(cnst), occstore.forLogical(foo)) - assertEquals(listOf(cnst), occstore.forSymbol(symbol("cnst", 1))) - assertEquals(listOf(cnst), occstore.forTerm(parseTerm("a{b c d{e}}"))) - } - - @Test - fun testIndependentlyGroundLogical() { - val foo = logical("foo") - - val cnst = occurrence("cnst", parseTerm("a{b c d{e}}")) - occstore.store(cnst) - - foo.set(parseTerm("a{b c d{e}}")) - - assertEquals(listOf(cnst), occstore.forSymbol(symbol("cnst", 1))) - assertEquals(listOf(cnst), occstore.forTerm(parseTerm("a{b c d{e}}"))) - assertEquals(listOf(cnst), occstore.forLogical(foo)) - } - - @Test - fun testValueIndex () { - val value = "foobar" - val main = occurrence("main", value) - occstore.store(main) - - assertEquals(listOf(main), occstore.forValue(value)) - } - - @Test - fun testTermIndex () { - val foo = occurrence("foo", parseTerm("a{b c}")) - occstore.store(foo) - - // TODO: more tests - assertEquals(listOf(foo), occstore.forTerm(parseTerm("a{b c}"))) - assertEquals(listOf(foo), occstore.forTerm(parseTerm("a{b Y}"))) - assertEquals(listOf(foo), occstore.forTerm(parseTerm("Z"))) - } - -}