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 45ff9234..b865a8bc 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 @@ -141,7 +141,13 @@ internal class ConstraintsProcessing( if (operational) action(this) else this private fun processMatch(controller: Controller, match: RuleMatchEx, parent: MatchJournal.MatchChunk, inStatus: FeedbackStatus) : FeedbackStatus = - controller.offerMatch(match, inStatus) + inStatus + .let { + //fixme: refactor this abort logic? + if (incrementalProcessing.offerMatch(match)) { + controller.offerMatch(match, inStatus) + } else inStatus.abort(DetailedFeedback("incremental processing omitted match")) + } .let { when (it) { is FeedbackStatus.ABORTED -> { // guard is not satisfied @@ -149,15 +155,15 @@ internal class ConstraintsProcessing( return it.recover() // return from the enclosing method } - is FeedbackStatus.FAILED -> { // guard failed + is FeedbackStatus.FAILED -> { // guard failed return it.recover() // return from the enclosing method } else -> it } } - .also { trace.trigger(match) } .also { incrementalProcessing.processMatch(match) } + .also { trace.trigger(match) } .also { accept(controller, match) } .then { controller.processBody(match, parent, it) } .also { trace.finish(match) } @@ -188,7 +194,6 @@ internal class ConstraintsProcessing( profiler.profile("terminateOccurrence") { occ.terminate(logicalState) - incrementalProcessing.processDiscarded(occ, logicalState) } @@ -202,7 +207,7 @@ internal class ConstraintsProcessing( fun erase(occurrence: Occurrence) { dispatchingFront = dispatchingFront.forget(occurrence) occurrence.terminate(logicalState) - incrementalProcessing.processDiscarded(occurrence, logicalState) + incrementalProcessing.processInvalidated(occurrence, logicalState) } fun erase(match: RuleMatchEx) { diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/EvaluationSessionImpl.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/EvaluationSessionImpl.kt index bfb22478..280306fc 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/EvaluationSessionImpl.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/EvaluationSessionImpl.kt @@ -55,7 +55,8 @@ internal data class SessionParts( val logicalState: LogicalState, val controller: ControllerImpl, val processing: ConstraintsProcessing, - val strategy: ProcessingStrategy + val strategy: ProcessingStrategy, + val principalObservers: PrincipalObserverDispatcher ) { val frontState: DispatchingFrontState get() = processing.getFrontState() } @@ -102,11 +103,11 @@ internal class EvaluationSessionImpl private constructor ( override fun firstSession(): SessionParts = getSession(null) - override fun nextSession(token: SessionToken): SessionParts = getSession(token) + override fun nextSession(token: SessionToken): SessionParts = getSession(token as SessionTokenImpl) - private fun getSession(token: SessionToken?): SessionParts { + private fun getSession(token: SessionTokenImpl?): SessionParts { val ruleIndex = token - ?.let { (it as SessionTokenImpl).ruleIndex } + ?.let { it.ruleIndex } ?.also { it.updateIndexFromRules(program.rules()) } ?: RuleIndex(program.rules()) @@ -114,24 +115,24 @@ internal class EvaluationSessionImpl private constructor ( val logicalState = LogicalState() val dispatchingFront = Dispatcher(ruleIndex).front() - val processingStrategy = GroundProcessing(incrementality) + // todo: remove this option + val principalObservers: PrincipalObserverDispatcher = + if (incrementality.assertLevel().assertContracts()) + LogicalBindObserverDispatcher() + else + PrincipalObserverDispatcher.EMPTY + val processingStrategy = GroundProcessing(incrementality, principalObservers) + val processing = ConstraintsProcessing(dispatchingFront, journal, logicalState, incrementality, trace, profiler) processing.setStrategy(processingStrategy) val controller = ControllerImpl(supervisor, processing, incrementality, trace, profiler) - return SessionParts(program.preambleInfo(), ruleIndex, journal, logicalState, controller, processing, processingStrategy) + return SessionParts(program.preambleInfo(), ruleIndex, journal, logicalState, controller, processing, processingStrategy, principalObservers) } override fun endSession(session: SessionParts): SessionToken = with(session) { - SessionTokenImpl( - journal.view(), - emptyList(), - ruleIndex.toRules(), - emptyFrontState(), - logicalState, - ruleIndex - ) + SessionTokenImpl(journal.view(), emptyList(), ruleIndex.toRules(), emptyFrontState(), ruleIndex, logicalState, principalObservers.apply { clearTriggerReceiver() }) } override fun runSession(session: SessionParts, main: Constraint): EvaluationResult = with(session) { @@ -155,21 +156,24 @@ internal class EvaluationSessionImpl private constructor ( val front = Dispatcher(ruleIndex, tkn.getFrontState()).front() val processing = ConstraintsProcessing(front, journal, logicalState, incrementality, trace, profiler) + val principalObservers = tkn.principalObservers val processingStrategy = IncrementalProcessing( - incrementality, journal, program.newRules(), program.droppedRules(), processing.getStateCleaner(), ruleIndex, trace + incrementality, journal, program.newRules(), program.droppedRules(), + processing.getStateCleaner(), ruleIndex, principalObservers, trace ) processing.setStrategy(processingStrategy) val controller = ControllerImpl(supervisor, processing, incrementality, trace, profiler) - return SessionParts(program.preambleInfo(), ruleIndex, journal, logicalState, controller, processing, processingStrategy) + return SessionParts(program.preambleInfo(), ruleIndex, journal, logicalState, controller, processing, processingStrategy, principalObservers) } override fun endSession(session: SessionParts): SessionToken = with(session) { val histView = journal.view() processing.resetStore() // clear observers val principalState = sessionState(frontState).resetLookup() - return SessionTokenImpl(histView, emptyList(), ruleIndex.toRules(), principalState, logicalState, ruleIndex) + principalObservers.clearTriggerReceiver() + return SessionTokenImpl(histView, emptyList(), ruleIndex.toRules(), principalState, ruleIndex, logicalState, principalObservers) } /** @@ -202,7 +206,7 @@ internal class EvaluationSessionImpl private constructor ( val controller = ControllerImpl(supervisor, processing, incrementality, trace, profiler) - return SessionParts(program.preambleInfo(), ruleIndex, journal, logicalState, controller, processing, processingStrategy) + return SessionParts(program.preambleInfo(), ruleIndex, journal, logicalState, controller, processing, processingStrategy, tkn.principalObservers) } override fun endSession(session: SessionParts): SessionToken = with(session) { @@ -213,10 +217,11 @@ internal class EvaluationSessionImpl private constructor ( outputOccurrences.forEach{ it.terminate(logicalState) } processing.resetStore() // clear observers logicalState.reset() + principalObservers.clearTriggerReceiver() val rules = ruleIndex.toRules().filter(preambleInfo::inPreamble) - SessionTokenImpl(histView, outputOccurrences, rules, emptyFrontState(), LogicalState(), ruleIndex) + SessionTokenImpl(histView, outputOccurrences, rules, emptyFrontState(), ruleIndex, LogicalState()) } private fun MatchJournal.View.filterOccurrences(without: OccurrenceStore = emptyStore()): OccurrenceStore { diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/IncrementalStage.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/IncrementalStage.kt index 20b9cbfb..bf8709c8 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/IncrementalStage.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/IncrementalStage.kt @@ -35,21 +35,33 @@ internal interface IncrementalStage: IncrSpecHolder { } +/** + * Used for pruning invalid internal state in impls of [IncrementalStage]. + */ +internal interface InvalidatingInfo { + fun isInvalid(entity: Justified): Boolean + + companion object Empty: InvalidatingInfo { + override fun isInvalid(entity: Justified): Boolean = false + } +} /** * Invalidation stage includes several activities: - * - removing chunks (i.e. principal matches) corresponding to - * removed rules and chunks depending on them from journal - * - reactivating occurrences that led to invalidated matches - * - pruning invalidated occurrences and matches from Dispatcher's state + * - removing from chunks (i.e. principal matches) that correspond + * to rules removed from program, their dependent chunks, and those + * dependent on additional invalidated [Justified] entities from [receive]; + * - reactivating occurrences that led to invalidated matches (through [activationSink]); + * - pruning invalidated occurrences and matches from [Dispatcher.DispatchingFront]'s state. */ internal class InvalidationStage( override val ispec: IncrementalSpec, + private val posTracker: PosTracking, private val invalidRuleIds: Set, private val activationSink: ContinuedActivationSink, private val stateCleaner: ConstraintsProcessing.ProgramStateCleaner, private val trace: EvaluationTrace -): IncrementalStage { +): IncrementalStage, InvalidatingInfo { private val invalidJustifications = mutableListOf() @@ -62,9 +74,13 @@ internal class InvalidationStage( fun invalidatedRules(): List = invalidRuleIdsAll.toList() + override fun isInvalid(entity: Justified): Boolean = + entity.justifiedByAny(invalidJustifications) fun receive(invalid: Iterable) { invalidJustifications.addAll(invalid) } + fun receive(invalid: Justified) { invalidJustifications.add(invalid) } + /** * Invalidates next chunk, if needed. * Doesn't remove the [Chunk] from the [Journal]. @@ -97,8 +113,13 @@ internal class InvalidationStage( with (chunk.match) { trace.invalidate(this) + // Don't accidentaly invalidate new rules. + // New rules themselves remain valid, only their effects must be cleared. + if (posTracker.isOld(chunk)) { + invalidRuleIdsAll.add(rule().uniqueTag()) + } + // So invalidate feedback they produced invalidFeedbackKeys.add(feedbackKey) - invalidRuleIdsAll.add(rule().uniqueTag()) stateCleaner.erase(this as RuleMatchEx) @@ -134,6 +155,7 @@ internal class AdditionStage( override val ispec: IncrementalSpec, private val addedRules: Iterable, private val activationSink: ContinuedActivationSink, + private val invalidatingInfo: InvalidatingInfo, private val ruleOrdering: RuleOrdering, private val ruleIndex: RuleIndex, private val trace: EvaluationTrace @@ -150,7 +172,6 @@ internal class AdditionStage( ): MatchCandidate -// private val activationCandidates = mutableListOf() private val activationCandidates = PriorityQueue{ lhs, rhs -> ruleOrdering.compare(lhs.rule, rhs.rule) } @@ -195,6 +216,12 @@ internal class AdditionStage( val candidateRule = candidate.rule val occChunk = candidate.occChunk + // Relevant for when rewind happenned + if (invalidatingInfo.isInvalid(occChunk)) { + aIt.remove() + continue + } + val pos = if (ruleOrdering.canBeInserted(candidateRule, occChunk, reader.next) || reader.atEnd()) reader.current.toPos() @@ -211,9 +238,77 @@ internal class AdditionStage( } +// todo; extract more restricted interface (w/o rewind) for use in stages +internal class PosTracking( + private val journalIndex: MatchJournal.Index, + private val journal: MatchJournal, + initPos: MatchJournal.Pos = journal.initialChunk().toPos() +) { + + /** + * Serves as a reference point for determining [isFuture] and [isPast]. + * Contract: [MatchJournal.Index.isKnown] is always `true` for [lastVisited]. + * Updated on each [onNext]. + */ + private var lastVisited: MatchJournal.Pos = initPos + + /** + * Contract: [MatchJournal.Index.isKnown] is always `true` for [front]. + * Updated only on [rewind], not on each [onNext]. + */ + private var front: MatchJournal.Pos = initPos + + + private fun updateReferencePos(current: MatchJournal.Chunk) { + if (journalIndex.isKnown(current)) { + lastVisited = current.toPos() + } + } + + fun rewind(pos: MatchJournal.Pos) = with(journalIndex) { + assert(isKnown(pos.chunk)) + assert(pos before lastVisited) + + journal.resetCursor(pos) + + if (lastVisited after front) { // rewind can happen inside another rewind and appear inferior + front = lastVisited + } + lastVisited = pos + } + + /** + * Tracks [MatchJournal] position as a reference point for [isFuture]. + */ + fun onNext(reader: ChunkReader): Unit = + updateReferencePos(reader.current) + + + fun isOld(chunk: MatchJournal.Chunk): Boolean = + journalIndex.isKnown(chunk) + fun isOld(occ: Occurrence): Boolean = + journalIndex.isKnown(occ) + + fun isNew(chunk: MatchJournal.Chunk): Boolean = + !journalIndex.isKnown(chunk) + fun isNew(occ: Occurrence): Boolean = + !journalIndex.isKnown(occ) + + + fun isFront(): Boolean = + with(journalIndex) { lastVisited afterOrEq front } + + fun isFuture(pos: MatchJournal.Pos): Boolean = + with(journalIndex) { pos after lastVisited } + + fun isPast(pos: MatchJournal.Pos): Boolean = + with(journalIndex) { pos before lastVisited } +} + + internal class PostponeMatchesStage( override val ispec: IncrementalSpec, - journal: MatchJournal, // todo: remove this dependency, needed only for initial chunk + private val posTracker: PosTracking, private val journalIndex: MatchJournal.Index, private val ruleOrdering: RuleOrdering ): IncrementalStage { @@ -228,14 +323,10 @@ internal class PostponeMatchesStage( } - private var lastKnownPos: MatchJournal.Pos = journal.initialChunk().toPos() - private val postponedMatches: MutableMap> = hashMapOf() fun onNext(reader: ChunkReader): Collection { - updateBasisPos(reader.current) - return (reader.current as? MatchJournal.OccChunk)?.let { occChunk -> postponedMatches.remove(occChunk.identity)?.map { PostponedMatch(it, occChunk) } } ?: emptyList() @@ -251,22 +342,21 @@ internal class PostponeMatchesStage( postponeFutureMatches(matches).withPostponedMatches(active) /** - * Determines, filters out, and postpones future matches. Returns only current matches. + * Determines, filters out, and postpones future matches. + * Returns only current matches. * - * Future match is a match, which has heads that are not yet activated - * according to [MatchJournal] position tracked in [lastKnownPos]. + * Future match is a match, which has heads that are not yet + * activated according to current [MatchJournal] position. */ fun postponeFutureMatches(matches: List): List { val currentMatches = mutableListOf() for (m in matches) { - // Returns null for matches with occurrences only from this session // because journalIndex indexes only previous session. val occChunk = journalIndex.activationPos(m) - val pos = occChunk?.toPos() - - if (pos != null && isFuturePos(pos)) { + if (occChunk != null && posTracker.isFuture(occChunk.toPos())) { postponedMatches.getOrPut(occChunk.identity, ::mutableListOf).add(m) + } else { currentMatches.add(m) } @@ -284,29 +374,13 @@ internal class PostponeMatchesStage( (this + postponed).sortedWith(ruleOrdering.matchComparator) } ?: this - - /** - * Tracks [MatchJournal] position as a reference point for distinguishing - * future matches and current matches (see [postponeFutureMatches] for details). - */ - private fun updateBasisPos(current: MatchJournal.Chunk) { - if (journalIndex.isKnown(current)) { - lastKnownPos = current.toPos() - } - } - - /** - * Defines the notion of 'future' position (and, hence, of 'future match'). - */ - private fun isFuturePos(pos: MatchJournal.Pos): Boolean = - with(journalIndex) { pos after lastKnownPos } - private val MatchJournal.OccChunk.identity get() = this.occ.identity } internal class ContinueOccurrencesStage( override val ispec: IncrementalSpec, + private val invalidatingInfo: InvalidatingInfo, private val journalIndex: MatchJournal.Index ): IncrementalStage, ContinuedActivationSink { @@ -328,8 +402,7 @@ internal class ContinueOccurrencesStage( } assert({ // lazily - // fixme: no good way to assert it for unknown (i.e. new, from this session) chunks - if (journalIndex.isKnown(continueFrom.chunk)) { + if (!isNew(continueFrom.chunk)) { // can't assert it for new chunks (i.e. those from this session) val isAncestor = continueFrom.chunk.justifiedBy(reactivated) val isPredecessor = journalIndex.compare(continueFrom, reactivated.toPos()) >= 0 isAncestor || isPredecessor @@ -343,15 +416,31 @@ internal class ContinueOccurrencesStage( private val seen: MutableSet = HashSet() + private fun ExecPos.isInvalid() = with(invalidatingInfo) { + isInvalid(reactivated) + } + fun onNext(reader: ChunkReader): Collection { val continued = mutableListOf() + while (queue.isNotEmpty()) { + if (queue.top().isInvalid()) { + queue.pop() + continue + } + if (!(reader at queue.top())) break - while (queue.isNotEmpty() && reader at queue.top()) { - continued.add(queue.pop().reactivatedOcc) + continued.add( queue.pop().reactivatedOcc ) } return continued } + fun onRewind(reader: ChunkReader) = with(journalIndex) { + val nextPos = reader.next.toPos() + seen.removeIf { seenPos -> + isNew(seenPos.continueFrom.chunk) || seenPos.continueFrom afterOrEq nextPos + } + } + override fun offerAll(continueFromPos: MatchJournal.Pos, occs: Iterable) = occs.mapNotNull(journalIndex::activatingChunkOf) .sortedWith(journalIndex.chunkComparator) @@ -359,12 +448,80 @@ internal class ContinueOccurrencesStage( override fun offer(continueFromPos: MatchJournal.Pos, ancestor: MatchJournal.OccChunk): Boolean = ExecPos(continueFromPos, ancestor).let { - it.assertValid() - if (seen.add(it)) queue.push(it) else false + when { + seen.add(it) -> { + it.assertValid() + queue.push(it) + } + else -> false + } } + private fun isNew(chunk: MatchJournal.Chunk) = !journalIndex.isKnown(chunk) private fun MutableList.top(): E = this.last() private fun MutableList.pop(): E = this.removeAt(this.size - 1) private fun MutableList.push(element: E): Boolean = this.add(element) -} \ No newline at end of file +} + + +// fixme: docs +internal class RewindVolatileOccurrencesStage( + override val ispec: IncrementalSpec, + private val posTracker: PosTracking, + private val journalIndex: MatchJournal.Index, + private val invalidated: InvalidatingInfo, + private val principalObserver: PrincipalObserverDispatcher +): IncrementalStage { + + private val toRewind: PriorityQueue = PriorityQueue(journalIndex.chunkComparator) + + private val seen = hashSetOf() + + fun receive(occs: Sequence): Boolean = + occs.filter(::takeVolatile) + .mapNotNull(journalIndex::activatingChunkOf) + .mapNotNull(journalIndex::matchChunkOf) + .filter(seen::add) + .toList().let(toRewind::addAll) + + fun maybeReset(reader: ChunkReader): MatchJournal.Pos? = + if (needRewind()) { + toRewind.peek()!!.toPos() + } else null + + fun reevaluate(reader: ChunkReader): Iterable { + val reevaluated = mutableListOf() + while (toRewind.isNotEmpty()) { + if (reader atNext toRewind.peek()!!) { + reevaluated.add(toRewind.remove()!!) + } else break + } + return reevaluated + } + + fun needRewind(): Boolean = peek()?.let { + posTracker.isPast(it.toPos()) + } ?: false + + /** + * Checked peek() for [toRewind] which prunes stale positions. + */ + private fun peek(): MatchJournal.MatchChunk? { + while (toRewind.isNotEmpty()) { + val top = toRewind.peek()!! + if (invalidated.isInvalid(top)) { + toRewind.remove() + continue + } + return top + } + return null + } + + private fun takeVolatile(occ: Occurrence) = + // NB: only occurrences from previous session are considered + journalIndex.isKnown(occ) && + with(principalObserver) { removeTriggered(occ) } + +} diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/JournalIterator.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/JournalIterator.kt index 3495286a..f91fae13 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/JournalIterator.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/JournalIterator.kt @@ -26,6 +26,9 @@ interface ChunkReader { infix fun at(pos: MatchJournal.Pos) = current === pos.chunk infix fun at(chunk: MatchJournal.Chunk) = current === chunk + + infix fun atNext(pos: MatchJournal.Pos) = next === pos.chunk + infix fun atNext(chunk: MatchJournal.Chunk) = next === chunk } interface JournalIterator: ChunkReader, Iterator diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/MatchJournal.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/MatchJournal.kt index d657fb89..f09b4969 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/MatchJournal.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/MatchJournal.kt @@ -144,7 +144,7 @@ interface MatchJournal : Iterable, EvidenceSource { fun isKnown(occ: Occurrence): Boolean = activatingChunkOf(occ) != null /** - * Returns [Chunk] where [occ] was activated. + * Returns [Chunk] corresponding to [occ] activation. * Returns null for non-principal occurrences & those not from indexed session. */ fun activatingChunkOf(occ: Occurrence): OccChunk? @@ -155,6 +155,12 @@ interface MatchJournal : Iterable, EvidenceSource { */ fun activationPos(match: RuleMatchEx): OccChunk? + /** + * Returns [MatchChunk] corresponding to [RuleMatch] where [occ] was activated. + * Returns null for non-principal occurrences & those not from indexed session. + */ + fun matchChunkOf(occChunk: OccChunk): MatchChunk? + /** * Length of the indexed [MatchJournal] */ diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/MatchJournalImpl.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/MatchJournalImpl.kt index f1899d35..fb8bb066 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/MatchJournalImpl.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/MatchJournalImpl.kt @@ -392,23 +392,38 @@ internal open class MatchJournalImpl( val last: E get() = if (l is LinkedList) l.last else l.last() } - private class IndexImpl(chunks: Iterable): MatchJournal.Index + private class IndexImpl(chunks: List): MatchJournal.Index { private val chunkOrder = HashMap, Int>() private val occChunks = HashMap() + private val parentMatches = HashMap() init { - chunks.forEachIndexed { index, chunk -> + var index: Int = chunks.size + val orphansYet = hashSetOf() + chunks.reversed().forEach { chunk -> if (!(chunk is CornerChunk)) { - chunkOrder[Id(chunk)] = index + chunkOrder[Id(chunk)] = --index } - if (chunk is OccChunk) { - occChunks[chunk.occ.identity] = chunk + + when (chunk) { + is OccChunk -> { + occChunks[chunk.occ.identity] = chunk + + orphansYet.add(chunk) + } + is MatchChunk -> orphansYet.removeIf{ orphan -> + // first met justifying MatchChunk is parent + if (orphan.justifiedBy(chunk)) { + parentMatches[orphan] = chunk + true + } else false + } } } } - override val size: Int = chunks.count() + override val size: Int = chunks.size override fun isKnown(chunk: Chunk): Boolean = chunkOrder.containsKey(Id(chunk)) @@ -417,9 +432,11 @@ internal open class MatchJournalImpl( override fun activationPos(match: RuleMatchEx): OccChunk? = // The latest matched occurrence from match's head is (by definition) // the occurrence which activated this match. - match.signature().mapNotNull { occSig -> - occSig?.let { activatingChunkOf(it.wrapped) } - }.maxBy { orderOf(it)!! } // compare positions: find latest + match.allHeads() + .mapNotNull(this::activatingChunkOf) + .maxBy { orderOf(it)!! } // compare positions: find latest + + override fun matchChunkOf(occChunk: OccChunk): MatchChunk? = parentMatches[occChunk] override val chunkComparator: Comparator get() = compareBy(this::orderOfThrow) 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 deleted file mode 100644 index 506af991..00000000 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/OccurrenceContractObserver.kt +++ /dev/null @@ -1,115 +0,0 @@ -/* - * 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 - - -/** - * Ensures important contract of incremental algorithm. - * - * Contract states that arguments of principal [Occurrence]s - * must be immutable, that is, logicals can't be unified - * with either ground or free other logicals. - */ -internal class OccurrenceContractObserver(override val ispec: IncrementalSpec): IncrSpecHolder { - private val observers: HashMap = hashMapOf() - - fun onActivated(occ: Occurrence, observable: LogicalStateObservable) { - if (occ.isPrincipal) { - observers[occ.identity] = UnmodifiableLogicalObserver(occ, observable) - } - } - - fun onDiscarded(occ: Occurrence, observable: LogicalStateObservable) { - // 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/PrincipalObserverDispatcher.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/PrincipalObserverDispatcher.kt new file mode 100644 index 00000000..362afa74 --- /dev/null +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/PrincipalObserverDispatcher.kt @@ -0,0 +1,179 @@ +/* + * 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.unification.Term + + +typealias ObserverTriggeredHandler = (Occurrence) -> Boolean + +interface PrincipalObserverDispatcher { + + fun onActivated(occ: Occurrence, observable: LogicalStateObservable) + fun onInvalidated(occ: Occurrence, observable: LogicalStateObservable) + + fun setTriggerReceiver(receiver: ObserverTriggeredHandler) + fun clearTriggerReceiver() + fun isObserving(occ: Occurrence): Boolean + fun isTriggered(occ: Occurrence): Boolean + fun removeTriggered(occ: Occurrence): Boolean + + + companion object EMPTY : PrincipalObserverDispatcher { + override fun onActivated(occ: Occurrence, observable: LogicalStateObservable) { } + override fun onInvalidated(occ: Occurrence, observable: LogicalStateObservable) { } + override fun setTriggerReceiver(receiver: ObserverTriggeredHandler) { } + override fun clearTriggerReceiver() { } + override fun isObserving(occ: Occurrence): Boolean = false + override fun isTriggered(occ: Occurrence): Boolean = false + override fun removeTriggered(occ: Occurrence): Boolean = false + } +} + +/** + * Ensures important contract of incremental algorithm. + * + * Contract states that arguments of principal [Occurrence]s + * must be immutable, that is, logicals can't be unified + * with either ground or free other logicals. + */ +internal class LogicalBindObserverDispatcher : PrincipalObserverDispatcher { + + private var receiver: ObserverTriggeredHandler = { false } + + private val observing: HashMap = hashMapOf() + private val triggered: HashSet = hashSetOf() + + override fun toString(): String = + "${javaClass.name}(observed: ${observing.size}, triggered: ${triggered.size})" + + override fun setTriggerReceiver(receiver: ObserverTriggeredHandler) { this.receiver = receiver } + + override fun clearTriggerReceiver() { receiver = { false } } + + override fun onActivated(occ: Occurrence, observable: LogicalStateObservable) { + if (observing.containsKey(occ.identity)) return + + LogicalBindObserver(this, occ, observable).let { + if (it.observes) { + observing[occ.identity] = it + } + } + } + + override fun onInvalidated(occ: Occurrence, observable: LogicalStateObservable) { + // NB: works between incremental sessions only if this instance is preserved between them + observing.remove(occ.identity)?.removeObservers(observable) + } + + override fun isObserving(occ: Occurrence): Boolean = observing.containsKey(occ.identity) + + override fun isTriggered(occ: Occurrence): Boolean = triggered.contains(occ.identity) + + override fun removeTriggered(occ: Occurrence): Boolean = triggered.remove(occ.identity) + + + fun onTrigger(source: Occurrence, logical: Logical<*>) { + observing.remove(source.identity) // logical observers are already removed + if (!receiver(source)) { + // if receiver didn't accept occurrence, + // then remember it for later requests + triggered.add(source.identity) + } + +// checkContract(false) { +// "$logical can't be unified because it's used in principal occurrence $source" +// } + } + + private inner class LogicalBindObserver( + private val logicalDispatcher: LogicalBindObserverDispatcher, + val source: Occurrence, + observable: LogicalStateObservable + ): ForwardingLogicalObserver { + + private val observed: MutableSet> = hashSetOf() + + init { + for (unboundLogical in source.usedUnboundLogicals()) { + observe(unboundLogical, observable) + } + } + + private fun observe(arg: Logical<*>, observable: LogicalStateObservable) { + if (!observed.contains(arg)) { + observable.addForwardingObserver(arg, this) + observed.add(arg) + } + } + + fun removeObservers(observable: LogicalStateObservable) { + for (logical in observed) { + observable.removeForwardingObserver(logical, this) + } + observed.clear() + } + + val observes: Boolean = observed.isNotEmpty() + + + override fun valueUpdated(logical: Logical<*>, controller: Controller) = onUpdated(logical, controller) + + override fun parentUpdated(logical: Logical<*>, controller: Controller) = onUpdated(logical, controller) + + private fun onUpdated(logical: Logical<*>, controller: Controller) { + removeObservers(controller.logicalStateObservable()) + logicalDispatcher.onTrigger(source, logical) + } + } + + + + private fun Occurrence.removeContractObservers(observable: LogicalStateObservable) { + for (observedLogical in this.usedUnboundLogicals()) { + observable.removeForwardingObserversWhere(observedLogical) { observer -> + observer is LogicalBindObserver && observer.source.identity == this.identity + } + } + } +} + + +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/ProcessingStrategy.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/ProcessingStrategy.kt index 891e4ae2..53e22fff 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/ProcessingStrategy.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/ProcessingStrategy.kt @@ -45,7 +45,14 @@ internal interface ProcessingStrategy { fun run(processing: ConstraintsProcessing, controller: Controller, main: Constraint): FeedbackStatus /** - * Pre-process accepted match before general processing in [Controller.processBody]. + * Called before [Controller.offerMatch]. + * Can omit match by returning false. + */ + fun offerMatch(match: RuleMatchEx): Boolean + + /** + * Pre-process accepted match (i.e. after [Controller.offerMatch]) + * before general processing in [Controller.processBody]. */ fun processMatch(match: RuleMatchEx) @@ -56,17 +63,19 @@ internal interface ProcessingStrategy { fun processOccurrenceMatches(active: Occurrence, matches: List): List /** - * Called on new activated [Occurrence]. Allows to handle program's - * logical state, e.g. add processing-specific observers with [observable]. + * Called on new activated [Occurrence]. + * Allows to handle program's logical state, + * e.g. add processing-specific observers with [observable]. */ fun processActivated(active: Occurrence, observable: LogicalStateObservable): Unit + // fixme: essentially InvalidationStage.invalidateChunk redirects back here -- unnecessary circle /** - * Called for each replaced [Occurrence] in match's head. - * It's a pair method for [processActivated] to discharge its effects, - * e.g. for clearing program logical state. + * Called for invalidated [Occurrence]s. + * It's a pair method for [processActivated] to discharge + * its effects, e.g. to clear program logical state. */ - fun processDiscarded(occ: Occurrence, observable: LogicalStateObservable): Unit + fun processInvalidated(occ: Occurrence, observable: LogicalStateObservable): Unit } @@ -85,31 +94,35 @@ internal open class DefaultProcessing: ProcessingStrategy { override fun run(processing: ConstraintsProcessing, controller: Controller, main: Constraint) = controller.activate(main) + override fun offerMatch(match: RuleMatchEx): Boolean = true + override fun processMatch(match: RuleMatchEx) {} override fun processOccurrenceMatches(active: Occurrence, matches: List): List = matches override fun processActivated(active: Occurrence, observable: LogicalStateObservable) {} - override fun processDiscarded(occ: Occurrence, observable: LogicalStateObservable) {} + override fun processInvalidated(occ: Occurrence, observable: LogicalStateObservable) {} } /** * Processing strategy that observes logical vars and ensures basic incremental contract. */ -internal open class GroundProcessing(override val ispec: IncrementalSpec): DefaultProcessing(), IncrSpecHolder { - - private val occurrenceContractObserver: OccurrenceContractObserver? = - if (ispec.assertLevel().assertContracts()) OccurrenceContractObserver(ispec) else null +internal open class GroundProcessing( + override val ispec: IncrementalSpec, + private val principalObservers: PrincipalObserverDispatcher = PrincipalObserverDispatcher.EMPTY +): DefaultProcessing(), IncrSpecHolder { override fun processActivated(active: Occurrence, observable: LogicalStateObservable) { - occurrenceContractObserver?.onActivated(active, observable) + if (active.isPrincipal) { + principalObservers.onActivated(active, observable) + } } - override fun processDiscarded(occ: Occurrence, observable: LogicalStateObservable) { + override fun processInvalidated(occ: Occurrence, observable: LogicalStateObservable) { if (occ.isPrincipal) { - occurrenceContractObserver?.onDiscarded(occ, observable) + principalObservers.onInvalidated(occ, observable) } } @@ -141,16 +154,33 @@ internal class IncrementalProcessing( droppedRules: Iterable, stateCleaner: ConstraintsProcessing.ProgramStateCleaner, ruleIndex: RuleIndex, + principalObservers: PrincipalObserverDispatcher, trace: EvaluationTrace -): GroundProcessing(ispec) { +): GroundProcessing(ispec, principalObservers) { private val journalIndex = journal.index() private val ruleOrdering = RuleOrdering(ruleIndex) + private val invalidatingInfo = InvalidatingInfoDispatcher() - private val continuator = ContinueOccurrencesStage(ispec, journalIndex) - private val invalidator = InvalidationStage(ispec, droppedRules.toSet(), continuator, stateCleaner, trace) - private val adder = AdditionStage(ispec, newRules, continuator, ruleOrdering, ruleIndex, trace) - private val postponer = PostponeMatchesStage(ispec, journal, journalIndex, ruleOrdering) + private val posTracker = PosTracking(journalIndex, journal) + private val continuator = ContinueOccurrencesStage(ispec, invalidatingInfo, journalIndex) + private val invalidator = InvalidationStage(ispec, posTracker, droppedRules.toSet(), continuator, stateCleaner, trace) + private val adder = AdditionStage(ispec, newRules, continuator, invalidatingInfo, ruleOrdering, ruleIndex, trace) + private val postponer = PostponeMatchesStage(ispec, posTracker, journalIndex, ruleOrdering) + private val rewinder = RewindVolatileOccurrencesStage(ispec, posTracker, journalIndex, invalidatingInfo, principalObservers) + + init { + // lateinit to break constructor cycle + invalidatingInfo.src = invalidator + + principalObservers.setTriggerReceiver(this::receiveBindTriggered) + } + + private class InvalidatingInfoDispatcher : InvalidatingInfo { + lateinit var src: InvalidatingInfo + + override fun isInvalid(entity: Justified): Boolean = src.isInvalid(entity) + } override fun invalidatedFeedback(): FeedbackKeySet = @@ -159,6 +189,13 @@ internal class IncrementalProcessing( override fun invalidatedRules(): List = invalidator.invalidatedRules() + override fun offerMatch(match: RuleMatchEx) = + !match.allHeads().filter { it.isPrincipal }.toList().let { + if (it.isNotEmpty()) { + rewinder.receive(it.asSequence()) + } else false + } + override fun processMatch(match: RuleMatchEx) = continueReplacedHeadsImpl(match) @@ -170,24 +207,36 @@ internal class IncrementalProcessing( var status: FeedbackStatus = FeedbackStatus.NORMAL() val cursor = journal.cursor while (true) { + posTracker.onNext(cursor) + + rewinder.rewind(cursor) invalidate(cursor) val postponedMatches = postponer.onNext(cursor) adder.receive(postponedMatches) - adder.onNext(cursor) + // Adder step must work on the incremental front. + // If rewind happened, then must skip this. + if (posTracker.isFront()) { adder.onNext(cursor) } + // fixme: pass inStatus? status = continuator.runContinued(processing, controller, cursor) - if (!status.operational) break - // continuator may request invalidating more chunks val haveChanges = invalidate(cursor) - if (cursor.atEnd()) break - if (!haveChanges) cursor.next() + if (!status.operational) break + if (!rewinder.needRewind() && cursor.atEnd()) break + // These changes (if present) must operate on + // current cursor position, so don't advance it. + if (!rewinder.needRewind() && !haveChanges) cursor.next() } return status } + private fun receiveBindTriggered(occ: Occurrence): Boolean = + if (journalIndex.isKnown(occ)) { + invalidator.receive(occ) + true + } else false private fun continueReplacedHeadsImpl(match: RuleMatchEx) { if (requiresIncrementalProcessing(match)) { @@ -202,12 +251,37 @@ internal class IncrementalProcessing( } else matches + private fun RewindVolatileOccurrencesStage.rewind(cursor: ChunkReader): Boolean = + maybeReset(cursor)?.let { rewindPos -> + // This is the only place where journal can be reset to past + // fixme: modifying not through cursor; not the cleanest way + posTracker.rewind(rewindPos) + // fixme: modifying not through cursor; not the cleanest way + + // Some stages on rewind need to take actions (e.g. clear internal state) + continuator.onRewind(cursor) + + reevaluate(cursor).let { + // will invalidate these chunks and reevaluate them + invalidator.receive(it) + } + true + } ?: false + + private fun invalidate(cursor: RemovingJournalIterator): Boolean { var haveChanges = false - while (invalidator.onNext(cursor)) { - cursor.removeNext() - haveChanges = true - } + do { + // handle all new chunks that were invalidated by rewind + if (posTracker.isNew(cursor.next)) { + invalidator.receive(listOf(cursor.next)) + } + + if (invalidator.onNext(cursor)) { + cursor.removeNext() + haveChanges = true + } else break + } while (true) return haveChanges } @@ -240,8 +314,8 @@ internal class PreambleProcessing( private val journalIndex = journal.index() private val ruleOrdering = RuleOrdering(ruleIndex) - private val continuator = ContinueOccurrencesStage(ispec, journalIndex) - private val adder = AdditionStage(ispec, newRules, continuator, ruleOrdering, ruleIndex, trace) + private val continuator = ContinueOccurrencesStage(ispec, InvalidatingInfo.Empty, journalIndex) + private val adder = AdditionStage(ispec, newRules, continuator, InvalidatingInfo.Empty, ruleOrdering, ruleIndex, trace) override fun run(processing: ConstraintsProcessing, controller: Controller, main: Constraint): FeedbackStatus { var status: FeedbackStatus = FeedbackStatus.NORMAL() @@ -269,7 +343,7 @@ internal class PreambleProcessing( * it can get them from [MatchJournal] and output for putting into cache. * * It requires that program in question adheres to incremental contracts. - * Importantly, one ensured by [OccurrenceContractObserver]. + * Importantly, one ensured by [LogicalBindObserverDispatcher]. */ internal class CachedOccurrencesProcessing( ispec: IncrementalSpec, diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/SessionTokenImpl.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/SessionTokenImpl.kt index 2daa4e69..cf43d097 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/SessionTokenImpl.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/SessionTokenImpl.kt @@ -24,12 +24,14 @@ import jetbrains.mps.logic.reactor.evaluation.SessionToken import jetbrains.mps.logic.reactor.program.Rule data class SessionTokenImpl( - private val journalView: MatchJournal.View, - private var store: Collection, - private val rules: Iterable, - private val frontState: DispatchingFrontState, - val logicalState: LogicalState, - val ruleIndex: RuleIndex) : SessionToken + private val journalView: MatchJournal.View, + private var store: Collection, + private val rules: Iterable, + private val frontState: DispatchingFrontState, + val ruleIndex: RuleIndex, + val logicalState: LogicalState, + val principalObservers: PrincipalObserverDispatcher = PrincipalObserverDispatcher.EMPTY +) : SessionToken { override fun getJournalView(): MatchJournalView = journalView override fun getRules(): Iterable = rules diff --git a/reactor/Test/test/TestIncrementalProgram.kt b/reactor/Test/test/TestIncrementalProgram.kt index 33e761a6..7c3861d5 100644 --- a/reactor/Test/test/TestIncrementalProgram.kt +++ b/reactor/Test/test/TestIncrementalProgram.kt @@ -4,6 +4,7 @@ import jetbrains.mps.logic.reactor.core.ReactorLifecycle import jetbrains.mps.logic.reactor.core.RulesDiff import jetbrains.mps.logic.reactor.core.internal.MatchJournal import jetbrains.mps.logic.reactor.evaluation.* +import jetbrains.mps.logic.reactor.logical.Logical import jetbrains.mps.logic.reactor.program.Constraint import jetbrains.mps.logic.reactor.program.ConstraintSymbol import jetbrains.mps.logic.reactor.program.IncrementalContractViolationException @@ -92,6 +93,8 @@ class TestIncrementalProgram { private fun EvaluationResult.lastChunkSymbols() = this.lastChunk().activatedLog().constraintSymbols() + private fun ConstraintOccurrence.firstValue(): Any? = (arguments().first() as? Logical<*>)?.value() + private fun PredicateInvocation.eq(left: T, right: T) = invocationContext().tellEquals(left, right) @@ -1541,18 +1544,19 @@ class TestIncrementalProgram { } } + @Ignore("feature is superseded") @Test(expected = EvaluationFailureException::class) fun violatePrincipalLogicalContract() { val progSpec = MockIncrProgSpec( setOf("main", "produceBound"), - setOf(sym1("foo")) + setOf(sym0("main"), sym1("foo")) ).withContractChecks() val (X, Y) = metaLogical("X", "Y") programWithRules( rule("main", headReplaced( - constraint("main") + pconstraint("main") ), body( pconstraint("foo", X) @@ -1575,41 +1579,28 @@ class TestIncrementalProgram { ).launch("violate contract assertion", progSpec) { result -> //NB: this check isn't supposed to be even run because of exception - //result.storeView().constraintSymbols() shouldBe setOf(sym1("foo"), sym1("hasBound")) + result.storeView().constraintSymbols() shouldBe setOf(sym1("foo"), sym1("hasBound")) } } - @Test(expected = EvaluationFailureException::class) - fun violatePrincipalLogicalContractOnRelaunch() { + @Test + fun inference_insertLogicalUni_2() { val progSpec = MockIncrProgSpec( setOf("main", "produceBound"), - setOf(sym1("foo")) - ).withContractChecks() + setOf(sym0("main"), sym1("foo")) + ) val (X, Y) = metaLogical("X", "Y") - val fooMatch = - rule("produceBound", - headKept( - pconstraint("foo", X) - ), - body( - statement({ x, y -> eq(x,y) }, X, Y), - constraint("hasBound", Y) - )) - programWithRules( rule("main", headReplaced( - constraint("main") + pconstraint("main") ), body( pconstraint("foo", X) )), - - // place for inserting 'fooMatch' rule - rule("bindVar", headKept( constraint("hasBound", Y) @@ -1624,16 +1615,379 @@ class TestIncrementalProgram { }.let { (builder, evalRes) -> builder - .insertRulesAt(1, fooMatch) + .insertRulesAt(1, + rule("produceBound", + headKept( + pconstraint("foo", X) + ), + body( + statement({ x, y -> eq(x,y) }, X, Y), + constraint("hasBound", Y) + )) + + ) .relaunch("violate contract assertion", progSpec, evalRes.token()) { result -> - //NB: this check isn't supposed to be even run because of exception - //result.storeView().constraintSymbols() shouldBe setOf(sym1("foo"), sym1("hasBound")) + result.storeView().constraintSymbols() shouldBe setOf(sym1("foo"), sym1("hasBound")) } } } + @Test + fun inference_rewindLogicalBind() { + val progSpec = MockIncrProgSpec( + setOf("main", "bindVar", "beforeBind"), + setOf(sym0("main"), sym1("foo")) + ).withContractChecks() + + val X = metaLogical("X") + + programWithRules( + rule("main", + headReplaced( + pconstraint("main") + ), + body( + pconstraint("foo", X) + )), + rule("bindVar", + headKept( + pconstraint("foo", X) + ), + body( + statement({ x -> x.set(42) }, X) + )) + + ).launch("normal run", progSpec) { result -> + + result.storeView().constraintSymbols() shouldBe setOf(sym1("foo")) + result.storeView().occurrences(sym1("foo")).first().firstValue() shouldBe 42 + + }.let { (builder, evalRes) -> + builder + .insertRulesAt(1, + rule("beforeBind", + headKept( + pconstraint("foo", X) + ), + guard( + expression({ x -> !x.isBound }, X) + ), + body( + constraint("expected" ) + )) + ) + .relaunch("relaunch", progSpec, evalRes.token()) { result -> + + result.storeView().constraintSymbols() shouldBe setOf(sym0("expected"), sym1("foo")) + result.storeView().occurrences(sym1("foo")).first().firstValue() shouldBe 42 + } + } + } + + /** + * Opposite to previous test [inference_insertLogicalBind] + */ + @Test + fun inference_insertLogicalBind() { + val progSpec = MockIncrProgSpec( + setOf("main", "bindVar", "checkFresh"), + setOf(sym0("main"), sym1("foo")) + ).withContractChecks() + + val X = metaLogical("X") + + programWithRules( + rule("main", + headReplaced( + pconstraint("main") + ), + body( + pconstraint("foo", X) + )), + rule("checkFresh", + headReplaced( + pconstraint("foo", X) + ), + guard( + expression({ x -> !x.isBound }, X) + ), + body( + constraint("unexpected" ) + )) + + ).launch("normal run", progSpec) { result -> + + result.storeView().constraintSymbols() shouldBe setOf(sym0("unexpected")) + + }.let { (builder, evalRes) -> + builder + .insertRulesAt(1, + rule("bindVar", + headKept( + pconstraint("foo", X) + ), + body( + statement({ x -> x.set(42) }, X) + )) + ) + .relaunch("relaunch", progSpec, evalRes.token()) { result -> + + result.storeView().constraintSymbols() shouldBe setOf(sym1("foo")) + result.storeView().occurrences(sym1("foo")).first().firstValue() shouldBe 42 + } + } + } + + @Test + fun inference_rewindLogicalBind_indirectUni() { + val progSpec = MockIncrProgSpec( + setOf("main", "produceBound", "beforeProduceBound"), + setOf(sym0("main"), sym1("foo")) + ).withContractChecks() + + val (X, Y) = metaLogical("X", "Y") + + programWithRules( + rule("main", + headReplaced( + pconstraint("main") + ), + body( + pconstraint("foo", X) + )), + rule("produceBound", + headKept( + pconstraint("foo", X) + ), + body( + statement({ x, y -> eq(x,y) }, X, Y), + constraint("hasBound", Y) + )), + rule("bindVar", + headKept( + constraint("hasBound", Y) + ), + body( + statement({ y -> y.set(42) }, Y) + )) + + ).launch("normal run", progSpec) { result -> + + result.storeView().constraintSymbols() shouldBe setOf(sym1("foo"), sym1("hasBound")) + result.storeView().occurrences(sym1("foo")).first().firstValue() shouldBe 42 + + }.let { (builder, evalRes) -> + builder + .insertRulesAt(1, + rule("beforeProduceBound", + headKept( + pconstraint("foo", X) + ), + guard( + expression({ x -> !x.isBound }, X) + ), + body( + constraint("expected" ) + )) + ) + .relaunch("relaunch", progSpec, evalRes.token()) { result -> + + result.storeView().constraintSymbols() shouldBe setOf(sym0("expected"), sym1("foo"), sym1("hasBound")) + result.storeView().occurrences(sym1("foo")).first().firstValue() shouldBe 42 + } + } + } + + @Test + fun inference_rewindLogicalBind_onDiscarded() { + val progSpec = MockIncrProgSpec( + setOf("main", "bindVar", "beforeBind"), + setOf(sym0("main"), sym1("foo")) + ).withContractChecks() + + val X = metaLogical("X") + + programWithRules( + rule("main", + headReplaced( + pconstraint("main") + ), + body( + pconstraint("foo", X) + )), + rule("bindVar", + headReplaced( + pconstraint("foo", X) + ), + body( + statement({ x -> x.set(42) }, X), + constraint("expectedValue", X) + )) + + ).launch("normal run", progSpec) { result -> + + result.storeView().constraintSymbols() shouldBe setOf(sym1("expectedValue")) + result.storeView().occurrences(sym1("expectedValue")).first().firstValue() shouldBe 42 + + }.let { (builder, evalRes) -> + builder + .insertRulesAt(1, + rule("beforeBind", + headKept( + pconstraint("foo", X) + ), + guard( + expression({ x -> !x.isBound }, X) + ), + body( + constraint("expected" ) + )) + ) + .relaunch("relaunch", progSpec, evalRes.token()) { result -> + + result.storeView().constraintSymbols() shouldBe setOf(sym0("expected"), sym1("expectedValue")) + result.storeView().occurrences(sym1("expectedValue")).first().firstValue() shouldBe 42 + } + } + } + + @Test + fun inference_rewindLogicalBind_indirectMatch() { + val progSpec = MockIncrProgSpec( + setOf("main", "produceBound", "beforeProduceBound", "runFoo"), + setOf(sym0("main"), sym1("foo"), sym0("runFoo")) + ).withContractChecks() + + val (X, Y) = metaLogical("X", "Y") + + programWithRules( + rule("main", + headKept( + pconstraint("main") + ), + body( + pconstraint("foo", X) + )), + rule("beforeProduceBound", + headReplaced( + pconstraint("runFoo") + ), + headKept( + pconstraint("foo", X) + ), + guard( + expression({ x -> !x.isBound }, X) + ), + body( + constraint("expected" ) + )), + rule("produceBound", + headKept( + pconstraint("foo", X) + ), + body( + statement({ x, y -> eq(x,y) }, X, Y), + constraint("hasBound", Y) + )), + rule("bindVar", + headKept( + constraint("hasBound", Y) + ), + body( + statement({ y -> y.set(42) }, Y) + )) + + ).launch("normal run", progSpec) { result -> + + result.storeView().constraintSymbols() shouldBe setOf(sym0("main"), sym1("foo"), sym1("hasBound")) + result.storeView().occurrences(sym1("foo")).first().firstValue() shouldBe 42 + + }.let { (builder, evalRes) -> + builder + .insertRulesAt(0, + rule("runFoo", + headKept( + pconstraint("main") + ), + body( + pconstraint("runFoo") + )) + ) + .relaunch("relaunch", progSpec, evalRes.token()) { result -> + + result.storeView().constraintSymbols() shouldBe setOf(sym0("main"), sym0("expected"), sym1("foo"), sym1("hasBound")) + result.storeView().occurrences(sym1("foo")).first().firstValue() shouldBe 42 + } + } + } + + @Test + fun inference_insertLogicalUni_affectFuture() { + val progSpec = MockIncrProgSpec( + setOf("main", "produceBound", "uniVars", "bindVar", "checkFresh"), + setOf(sym0("main"), sym1("foo"), sym1("bar")) + ).withContractChecks() + + val (X, Y) = metaLogical("X", "Y") + + programWithRules( + rule("main", + headReplaced( + pconstraint("main") + ), + body( + pconstraint("bar", Y), + pconstraint("foo", X) + )), + rule("bindVar", + headKept( + pconstraint("bar", Y) + ), + body( + statement({ y -> y.set(42) }, Y) + )), + rule("checkFresh", + headKept( + pconstraint("foo", X) + ), + guard( + expression({ x -> !x.isBound }, X) + ), + body( + constraint("unexpected") + )) + + ).launch("normal run", progSpec) { result -> + + result.storeView().constraintSymbols() shouldBe setOf(sym1("foo"), sym1("bar"), sym0("unexpected")) + result.storeView().occurrences(sym1("bar")).first().firstValue() shouldBe 42 + result.storeView().occurrences(sym1("foo")).first().firstValue() shouldBe null + + }.let { (builder, evalRes) -> + builder + .insertRulesAt(1, + rule("uniVars", + headKept( + pconstraint("foo", X), + pconstraint("bar", Y) + ), + body( + statement({ x, y -> eq(x,y) }, X, Y) + )) + ) + .relaunch("relaunch", progSpec, evalRes.token()) { result -> + + result.storeView().constraintSymbols() shouldBe setOf(sym1("foo"), sym1("bar")) + result.storeView().occurrences(sym1("bar")).first().firstValue() shouldBe 42 + result.storeView().occurrences(sym1("foo")).first().firstValue() shouldBe 42 + } + } + } + + + @Test fun expectTypeGenericNonprincipal() { val progSpec = MockIncrProgSpec(