From 2a0d4ef0767ab31f6865a3852ffebf0803041074 Mon Sep 17 00:00:00 2001 From: Grigorii Kirgizov Date: Mon, 27 Jul 2020 15:33:29 +0300 Subject: [PATCH] Observe all unbound logicals inside Occurrence to check contract (MPSCR-66) Previously only logicals directly used ar occurrence args were observed. Now terms in occurrence args are traversed recursively and all contained logicals are observed. Also clear occurrence contract observers on discarding occ-s. Introduce a generic way to clear observers in LogicalState. --- .../reactor/core/LogicalStateObservable.kt | 3 + .../core/internal/ConstraintsProcessing.kt | 39 ++----- .../reactor/core/internal/LogicalState.kt | 14 +++ .../internal/OccurrenceContractObserver.kt | 108 ++++++++++++++++++ .../logic/reactor/core/internal/TermWalker.kt | 35 +++++- reactor/Test/test/RulesHelper.kt | 3 + 6 files changed, 171 insertions(+), 31 deletions(-) create mode 100644 reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/OccurrenceContractObserver.kt diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/LogicalStateObservable.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/LogicalStateObservable.kt index 481132eb..6669bd51 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/LogicalStateObservable.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/LogicalStateObservable.kt @@ -27,6 +27,9 @@ interface LogicalStateObservable { fun addForwardingObserver(logical: Logical<*>, observer: ForwardingLogicalObserver) fun removeForwardingObserver(logical: Logical<*>, observer: ForwardingLogicalObserver) + = removeForwardingObserversWhere(logical, observer::equals) + + fun removeForwardingObserversWhere(logical: Logical<*>, where: (ForwardingLogicalObserver) -> Boolean) } diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/ConstraintsProcessing.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/ConstraintsProcessing.kt index 997d6f4f..b4f2164e 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/ConstraintsProcessing.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/ConstraintsProcessing.kt @@ -20,12 +20,13 @@ import jetbrains.mps.logic.reactor.core.* import jetbrains.mps.logic.reactor.evaluation.EvaluationTrace import jetbrains.mps.logic.reactor.program.IncrementalSpec import jetbrains.mps.logic.reactor.evaluation.SessionToken -import jetbrains.mps.logic.reactor.logical.Logical import jetbrains.mps.logic.reactor.logical.LogicalContext import jetbrains.mps.logic.reactor.program.Constraint import jetbrains.mps.logic.reactor.program.Rule import jetbrains.mps.logic.reactor.util.Profiler import jetbrains.mps.logic.reactor.util.profile +import kotlin.collections.ArrayList +import kotlin.collections.HashSet /** @@ -52,6 +53,9 @@ internal class ConstraintsProcessing(private var dispatchingFront: Dispatcher.Di private val activationQueue: ContinuedActivationQueue = ContinuedActivationQueue(journalIndex, RuleOrdering(ruleIndex)) + private val occurrenceContractObserver: OccurrenceContractObserver? = + if (ispec.assertLevel().assertContracts()) OccurrenceContractObserver(logicalState, ispec) else null + private val invalidFeedbackKeys: MutableSet = mutableSetOf() private data class MatchCandidate(val rule: Rule, val occChunk: MatchJournal.OccChunk) @@ -110,6 +114,7 @@ internal class ConstraintsProcessing(private var dispatchingFront: Dispatcher.Di private fun invalidateChunk(chunk: MatchJournal.Chunk, invalidJustifications: Collection): Iterable { // 'Undo' all activated in this chunk occurrences + // todo: need clearing observers in logicalState for occurrences we drop? chunk.activatedLog().forEach { dispatchingFront = dispatchingFront.forget(it) } @@ -222,9 +227,7 @@ internal class ConstraintsProcessing(private var dispatchingFront: Dispatcher.Di logActivation(active) active.revive(logicalState) - if (ispec.assertLevel().assertContracts()) { - active.addContractObservers(logicalState) - } + occurrenceContractObserver?.onActivated(active) } assert(active.alive) @@ -338,6 +341,8 @@ internal class ConstraintsProcessing(private var dispatchingFront: Dispatcher.Di occ.terminate(logicalState) + occurrenceContractObserver?.onDiscarded(occ) + } trace.discard(occ) @@ -378,32 +383,6 @@ internal class ConstraintsProcessing(private var dispatchingFront: Dispatcher.Di } } - - private fun Occurrence.addContractObservers(observable: LogicalStateObservable) { - if (this.isPrincipal) { - UnmodifiableLogicalObserver(this, observable) - } - } - - internal class UnmodifiableLogicalObserver(val source: Occurrence, observable: LogicalStateObservable): ForwardingLogicalObserver { - init { - for (a in HashSet(source.arguments)) { // avoid duplicate subscriptions - if (a is Logical<*>) { - observable.addForwardingObserver(a, this) - } - } - } - - override fun valueUpdated(logical: Logical<*>, controller: Controller) = doCheckContract(logical, controller) - - override fun parentUpdated(logical: Logical<*>, controller: Controller) = doCheckContract(logical, controller) - - private fun doCheckContract(logical: Logical<*>, controller: Controller) = - checkContract(false) { - "$logical can't be unified because it's used in principal occurrence $source" - } - } - private fun MatchJournal.MatchChunk.dependsOnAny(utags: Iterable): Boolean = utags.contains(this.ruleUniqueTag) || utags.any { utag -> dependsOnRule(utag) } diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/LogicalState.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/LogicalState.kt index 21812247..8b5f9ed2 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/LogicalState.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/LogicalState.kt @@ -105,6 +105,13 @@ class LogicalState : LogicalStateObservable, LogicalObserver } } + override fun removeForwardingObserversWhere(logical: Logical<*>, where: (ForwardingLogicalObserver) -> Boolean) { + currentFrame().removeForwardingObserversWhere(logical, where) + if (!currentFrame().isObserving(logical)) { + logical.removeObserver(this) + } + } + override fun valueUpdated(logical: Logical<*>) { // forward to the top frame with added transient state (Controller) currentFrame().valueUpdated(logical, controller!!) @@ -163,6 +170,13 @@ class LogicalStateFrame : LogicalStateObservable, ForwardingLogicalObserver } } + override fun removeForwardingObserversWhere(logical: Logical<*>, where: (ForwardingLogicalObserver) -> Boolean) { + observers[logical]?.apply { + removeIf(where) + if (isEmpty()) observers.remove(logical) + } + } + fun observed(): Sequence> = observers.keys.asSequence() // observers.keys().asSequence().map { it.wrapped } diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/OccurrenceContractObserver.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/OccurrenceContractObserver.kt new file mode 100644 index 00000000..74e1c0e2 --- /dev/null +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/OccurrenceContractObserver.kt @@ -0,0 +1,108 @@ +/* + * Copyright 2014-2020 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.internal + +import jetbrains.mps.logic.reactor.core.Controller +import jetbrains.mps.logic.reactor.core.ForwardingLogicalObserver +import jetbrains.mps.logic.reactor.core.LogicalStateObservable +import jetbrains.mps.logic.reactor.core.Occurrence +import jetbrains.mps.logic.reactor.logical.Logical +import jetbrains.mps.logic.reactor.program.IncrementalSpec +import jetbrains.mps.unification.Term +import kotlin.collections.HashSet + + +internal class OccurrenceContractObserver(private val observable: LogicalStateObservable, override val ispec: IncrementalSpec): IncrSpecHolder { + private val observers: HashMap = hashMapOf() + + fun onActivated(occ: Occurrence) { + if (occ.isPrincipal) { + observers[occ.identity] = UnmodifiableLogicalObserver(occ, observable) + } + } + + fun onDiscarded(occ: Occurrence) { + // NB: works between incremental sessions only if this instance is preserved between them + // observers.remove(occ.identity)?.removeObservers(observable) + + occ.removeContractObservers(observable) + observers.remove(occ.identity) + } +} + +internal fun Occurrence.removeContractObservers(observable: LogicalStateObservable) { + for (observedLogical in this.usedUnboundLogicals()) { + observable.removeForwardingObserversWhere(observedLogical) { observer -> + observer is UnmodifiableLogicalObserver && observer.source.identity == this.identity + } + } +} + +internal class UnmodifiableLogicalObserver(val source: Occurrence, observable: LogicalStateObservable): ForwardingLogicalObserver { + private val observed: HashSet> = HashSet() + + private fun observe(arg: Logical<*>, observable: LogicalStateObservable) { + if (!observed.contains(arg)) { + observable.addForwardingObserver(arg, this) + observed.add(arg) + } + } + + init { + for (unboundLogical in source.usedUnboundLogicals()) { + observe(unboundLogical, observable) + } + } + + fun removeObservers(observable: LogicalStateObservable) { + for (logical in observed) { + observable.removeForwardingObserver(logical, this) + } + observed.clear() + } + + override fun valueUpdated(logical: Logical<*>, controller: Controller) = doCheckContract(logical, controller) + + override fun parentUpdated(logical: Logical<*>, controller: Controller) = doCheckContract(logical, controller) + + private fun doCheckContract(logical: Logical<*>, controller: Controller) = + checkContract(false) { + "$logical can't be unified because it's used in principal occurrence $source" + } +} + +internal fun Occurrence.usedUnboundLogicals(): Set> { + val unique = hashSetOf>() + for (arg in arguments) { + + val argLogicals = when (arg) { + is Logical<*> -> + if (!arg.isBound) listOf(arg) + else when(val value = arg.findRoot().value()) { + is Term -> value.unboundLogicals() + else -> emptyList() + } + is Term -> arg.unboundLogicals() + else -> emptyList() + } + + unique.addAll(argLogicals) + } + return unique +} + + diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/TermWalker.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/TermWalker.kt index ba704637..2d5fe8a6 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/TermWalker.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/TermWalker.kt @@ -30,7 +30,14 @@ class TermWalker(vararg visitors: TermVisitor) { @Throws(Exception::class) abstract fun visit(t: T): MutableCollection +// abstract fun visit(t: T): Collection + } + class SimpleVisitor( + kind: Term.Kind, + private inline val f: (T) -> MutableCollection + ) : TermVisitor(kind) { + override fun visit(t: T) = f(t) } private val visitorMap: MutableMap> = EnumMap(Term.Kind::class.java) @@ -74,4 +81,30 @@ class TermWalker(vararg visitors: TermVisitor) { companion object { private val SINGLETON = Any() } -} \ No newline at end of file +} + +internal fun Term.unboundLogicals(): Collection> = logicalsWhere { !it.isBound } + +internal inline fun Term.logicalsWhere(crossinline where: (Logical<*>) -> Boolean): Collection> { + val collected = arrayListOf>() + + TermWalker( + TermWalker.SimpleVisitor(Term.Kind.FUN) { t -> + t.arguments() + }, + TermWalker.SimpleVisitor(Term.Kind.REF) { ref -> + if (ref.get() !== ref) { + Collections.singletonList(ref.get()) + } + Collections.emptyList() + }, + TermWalker.SimpleVisitor(Term.Kind.VAR) { v -> + if (v is LogicalOwner && where(v.logical())) { + collected.add(v.logical()) + } + Collections.emptyList() + } + ).walk(this) + + return collected +} diff --git a/reactor/Test/test/RulesHelper.kt b/reactor/Test/test/RulesHelper.kt index 26f957b5..58a3d973 100644 --- a/reactor/Test/test/RulesHelper.kt +++ b/reactor/Test/test/RulesHelper.kt @@ -230,6 +230,9 @@ class MockController : Controller { override fun removeForwardingObserver(logical: Logical<*>, observer: ForwardingLogicalObserver) { } + + override fun removeForwardingObserversWhere(logical: Logical<*>, where: (ForwardingLogicalObserver) -> Boolean) { + } } override fun storeView(): StoreView {