Cleanup reactor code, drop obsolete code:

old matching algorithm implementation,
store occurrences indexing,
propagation history.
This commit is contained in:
Fedor Isakov 2018-08-04 15:53:48 +02:00
parent 75c6dff551
commit faaa9f12d6
8 changed files with 3 additions and 1650 deletions

View File

@ -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)
}

View File

@ -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<Rule, MatchTrieSet>()
fun matches(activeOcc: ConstraintOccurrence, aux: OccurrenceIndex) : Iterable<Match> = object : Iterable<Match> {
override fun iterator(): Iterator<Match> {
val relevantRules = ruleIndex.forOccurrence(activeOcc).toList()
val tries = LazyIterable<Rule, MatchTrieSet>(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<ConstraintOccurrence>,
val discardedOccurrences: List<ConstraintOccurrence>) : 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<Any>).to(b.term().toValue())
}.toMap(HashMap<MetaLogical<*>, Any?>())
val meta2logical = HashMap<MetaLogical<*>, Logical<*>>()
override fun <V : Any> variable(meta: MetaLogical<V>): Logical<V> =
(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<V>
}
}
val patternPredicates: List<Predicate> 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<ConstraintOccurrence> = keptOccurrences
override fun matchHeadReplaced(): Iterable<ConstraintOccurrence> = 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<ConstraintOccurrence>, discarded: List<ConstraintOccurrence>) :
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<Term>)
} 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

View File

@ -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<ConstraintOccurrence?>
private set
internal lateinit var discardedOccurrences: Array<ConstraintOccurrence?>
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<Match>("matchesRule_${rule.tag()}") {
val kept = keptOccurrences.asList() as List<ConstraintOccurrence>
val discarded = discardedOccurrences.asList() as List<ConstraintOccurrence>
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()}"
}

View File

@ -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<BitSet> =
HashMap<MetaLogical<*>, 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<BitSet>().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<PartialMatchTrie>()
fun matches(activeOcc: ConstraintOccurrence, occIndex: OccurrenceIndex): Sequence<PartialMatch> {
val constraints = keptConstraints + discardedConstraints
val relevantTries = ArrayList<PartialMatchTrie>()
val copyTries = ArrayList<PartialMatchTrie>()
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<PartialMatch> = object : Sequence<PartialMatch> {
override fun iterator() = object : Iterator<PartialMatch> {
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?>("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>) : 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<MatchTrieNode> {
return profiler.profile<Iterable<MatchTrieNode>>("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<MatchTrieNode> {
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<Result, Iterable<ConstraintOccurrence>> {
return profiler.profile<Pair<Result, Iterable<ConstraintOccurrence>>> ("lookupAux_${cst.symbol()}") {
val fromArgs = ArrayList<ConstraintOccurrence>(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<Pair<Result, Iterable<ConstraintOccurrence>>> ("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<Any>): ArrayList<Any> {
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<Any> =
foldPath(ArrayList<Any>(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 <T> 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
}
}

View File

@ -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<Rule, PersList<List<IdWrapper<ConstraintOccurrence>>>>
constructor() {
this.recordedPropagation = Maps.of<Rule, PersList<List<IdWrapper<ConstraintOccurrence>>>> ()
}
private constructor(recorded : PersMap<Rule, PersList<List<IdWrapper<ConstraintOccurrence>>>>) {
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<List<IdWrapper<ConstraintOccurrence>>>()
return PropagationHistory(recordedPropagation.put(pm.rule, hist.prepend(idOccs)))
}
return this
}
}

View File

@ -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<ConstraintOccurrence>
fun forLogical(logical: Logical<*>): Iterable<ConstraintOccurrence>
fun forLogicalAndConstraint(logical: Logical<*>, cst:Constraint): Iterable<ConstraintOccurrence>
fun forTerm(term: Term): Iterable<ConstraintOccurrence>
fun forTermAndConstraint(term: Term, cst: Constraint): Iterable<ConstraintOccurrence>
fun forValue(value: Any): Iterable<ConstraintOccurrence>
}
/**
* 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<IdWrapper<Logical<*>>, IdHashSet<ConstraintOccurrence>>
var term2occurrences: TermTrie<ConstraintOccurrence>
var value2occurrences: PersMap<Any, IdHashSet<ConstraintOccurrence>>
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<ConstraintOccurrence> {
return (symbol2occurrences[symbol] ?: emptySet()).filter { co -> co.isStored() }
}
override fun forLogicalAndConstraint(logical: Logical<*>, cst: Constraint): Iterable<ConstraintOccurrence> {
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<ConstraintOccurrence> {
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<ConstraintOccurrence> {
return term2occurrences.lookupValues(term.withAny()).filter { it.isStored() }
}
override fun forTermAndConstraint(term: Term, cst: Constraint): Iterable<ConstraintOccurrence> {
return term2occurrences.lookupValues(term.withConstraint(cst)).filter { it.isStored() }
}
override fun forValue(value: Any): Iterable<ConstraintOccurrence> {
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"
}
}
}

View File

@ -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<String>("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<Int>("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<Int>("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<Int>("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<Int>("M", "N")
val (O, P) = metaLogical<Int>("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<Any>("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<Int>("M", "N")
val (O, P) = metaLogical<Int>("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<String>("b", "c")
val (x, y) = metaLogical<String>("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<String>("b", "c", "d")
val (x, y, z) = metaLogical<String>("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<ConstraintOccurrence>()
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<RuleIndex, OccurrenceIndex> =
this.indices(occurrence.toList())
private fun Builder.indices(stored: List<ConstraintOccurrence>): Pair<RuleIndex, OccurrenceIndex> {
val aux = object : OccurrenceIndex {
override fun forSymbol(symbol: ConstraintSymbol): Iterable<ConstraintOccurrence> =
stored.filter { co -> co.constraint().symbol() == symbol }
override fun forLogical(logical: Logical<*>): Iterable<ConstraintOccurrence> =
stored.filter { co ->
co.arguments().any { it is Logical<*> && it.isBound && it.findRoot() == logical.findRoot() }
}
override fun forLogicalAndConstraint(logical: Logical<*>, cst: Constraint): Iterable<ConstraintOccurrence> =
stored.filter { co ->
co.arguments().any { it is Logical<*> && it.isBound && it.findRoot() == logical.findRoot() }
}
override fun forTerm(term: Term): Iterable<ConstraintOccurrence> =
stored.filter { co ->
co.arguments().any { it is Term && Unification.unify(it, term).isSuccessful }
}
override fun forTermAndConstraint(term: Term, cst: Constraint): Iterable<ConstraintOccurrence> =
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<ConstraintOccurrence> =
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 }
}

View File

@ -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<Pair<Logical<*>, 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<String>("foo")
val bar = logical<String>("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<String>("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<Term>("foo")
val bar = logical<Term>("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<Term>("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<Term>("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")))
}
}