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 019871a3..c508699b 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,6 +20,8 @@ import jetbrains.mps.logic.reactor.core.* import jetbrains.mps.logic.reactor.evaluation.EvaluationTrace import jetbrains.mps.logic.reactor.program.IncrementalProgramSpec import jetbrains.mps.logic.reactor.evaluation.SessionToken +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 @@ -94,37 +96,44 @@ internal class ConstraintsProcessing(private var dispatchingFront: Dispatcher.Di // Remove chunk from the journal it.remove() - // 'Undo' all activated in this chunk occurrences - chunk.activatedLog().forEach { - dispatchingFront = dispatchingFront.forget(it) - } - if (chunk is MatchJournal.MatchChunk) { - trace.invalidate(chunk.match) - invalidatedRulesTags.add(chunk.ruleUniqueTag) + val validOccs = invalidateChunk(chunk, justificationRoots) - dispatchingFront = dispatchingFront.forget(chunk.match as RuleMatchEx) + activationQueue.offerAll(lastValidChunk.toPos(), validOccs) - // Valid head occurrences could match more rules - // without this match, so need to reactivate them. - // E.g. occurrences discarded in this match on - // previous run but revived here can match more rules. - val matchedOccs = chunk.match.allHeads() - val validOccs = matchedOccs.filter { occ -> - !occ.justifiedByAny(justificationRoots) - } - // By definition of Chunk and principal rule, - // all occurrences from the head are principal. - assert(chunk.match.allHeads().all { it.isPrincipal }) - - activationQueue.offerAll(lastValidChunk.toPos(), validOccs.asIterable()) - } } else { lastValidChunk = chunk } } } + private fun invalidateChunk(chunk: MatchJournal.Chunk, invalidJustifications: Collection): Iterable { + // 'Undo' all activated in this chunk occurrences + chunk.activatedLog().forEach { + dispatchingFront = dispatchingFront.forget(it) + } + + val validOccs: Sequence + if (chunk is MatchJournal.MatchChunk) { + trace.invalidate(chunk.match) + invalidatedRulesTags.add(chunk.ruleUniqueTag) + dispatchingFront = dispatchingFront.forget(chunk.match as RuleMatchEx) + + // Valid head occurrences could match more rules + // without this match, so need to reactivate them. + // E.g. occurrences discarded in this match on + // previous run but revived here can match more rules. + validOccs = chunk.match.allHeads().filter { occ -> + !occ.justifiedByAny(invalidJustifications) + } + // By definition of Chunk and principal rule, + // all occurrences from the head are principal. + assert(chunk.match.allHeads().all { it.isPrincipal }) + + } else validOccs = emptySequence() + return validOccs.asIterable() + } + fun addRuleMatches(rules: Iterable) { val activationCandidates = mutableListOf() @@ -207,14 +216,10 @@ internal class ConstraintsProcessing(private var dispatchingFront: Dispatcher.Di fun processActivated(controller: Controller, active: Occurrence, parent: MatchJournal.MatchChunk, inStatus: FeedbackStatus) : FeedbackStatus { push() - val activationChunk: MatchJournal.OccChunk? if (!active.stored) { active.stored = true - activationChunk = logActivation(active) + logActivation(active) active.revive(logicalState) - } else { - // defined (not null) & needed only for incremental execution - activationChunk = journalIndex.activatingChunkOf(active) } assert(active.alive) @@ -233,12 +238,6 @@ internal class ConstraintsProcessing(private var dispatchingFront: Dispatcher.Di } val outStatus = currentMatches.fold(inStatus) { status, match -> - if (activationChunk != null && !isFront()) { - if (match.discards(active)) { - dropDiscardingMatchesFor(activationChunk, invalidatedRulesTags) - } - } - // TODO: paranoid check. should be isAlive() instead // FIXME: move this check elsewhere if (status.operational && active.stored && match.allStored()) { @@ -255,6 +254,7 @@ internal class ConstraintsProcessing(private var dispatchingFront: Dispatcher.Di return outStatus } + @Deprecated("obsolete machinery, superseded by MPSCR-65") private fun dropDiscardingMatchesFor(ancestor: MatchJournal.OccChunk, droppedRuleTags: MutableSet) = this.dropDescendantsWhile(ancestor) { chunk -> if (chunk is MatchJournal.MatchChunk && chunk.match.discards(ancestor.occ)) { @@ -283,15 +283,30 @@ internal class ConstraintsProcessing(private var dispatchingFront: Dispatcher.Di } } .also { trace.trigger(match) } - .also { - accept(controller, match) - } - .then { - controller.processBody(match, parent, it) - } + .also { continueReplacedHeads(match, parent) } + .also { accept(controller, match) } + .then { controller.processBody(match, parent, it) } .also { trace.finish(match) } + private fun continueReplacedHeads(match: RuleMatchEx, parent: MatchJournal.MatchChunk) { + if (!isFront() && match.isPrincipal) { + profiler.profile("continueReplaced") { + + val invalidJustifications = match.matchHeadReplaced().filter { it.isPrincipal } + if (invalidJustifications.isNotEmpty()) { + + val pos = currentPos() + dropDescendants(invalidJustifications) { + val validOccs = invalidateChunk(it, invalidJustifications) + activationQueue.offerAll(pos, validOccs) + } + + } + } + } + } + private fun accept(controller: Controller, match: RuleMatchEx) { profiler.profile("logMatch") { @@ -327,6 +342,39 @@ internal class ConstraintsProcessing(private var dispatchingFront: Dispatcher.Di } } + + /** + * Incapsulates logic for deriving [Evidence] and [Justifications] for a new [Occurrence]. + */ + inner class JustifiedOccurrenceCreator { + val savedEvidence: Evidence = evidence() + val savedJustifications: Justifications = justifications() + + fun Constraint.occurrence( + observable: LogicalStateObservable, + arguments: List<*>, + logicalContext: LogicalContext, + ruleUniqueTag: Any? = null + ): Occurrence { + + // By default share justifications (as a small optimization) + var evidence = savedEvidence + var justifications = savedJustifications + + // For principal occurrences create new + if (ispec.isPrincipal(this)) { + evidence = nextEvidence() + justifications = justsCopy(savedJustifications).apply { add(evidence) } + } + + return Occurrence( + observable, this, logicalContext, arguments, + evidence, justifications, ruleUniqueTag + ) + } + } + + 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/ContinuedActivationQueue.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/ContinuedActivationQueue.kt index a44178bd..b7c9ef82 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/ContinuedActivationQueue.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/ContinuedActivationQueue.kt @@ -35,7 +35,9 @@ internal class ContinuedActivationQueue( } private fun ExecPos.assertValid() { - assert(continueFrom.chunk.justifiedBy(reactivated) || journalIndex.compare(continueFrom, reactivated.toPos()) >= 0) + val isAncestor = continueFrom.chunk.justifiedBy(reactivated) + val isPredecessor = journalIndex.compare(continueFrom, reactivated.toPos()) >= 0 + assert(isAncestor || isPredecessor) } diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/ControllerImpl.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/ControllerImpl.kt index af21fa5f..326b47cd 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/ControllerImpl.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/ControllerImpl.kt @@ -80,7 +80,7 @@ internal class ControllerImpl ( // FIXME noLogicalContext val context = Context(NORMAL(), noLogicalContext, null, trace) - activateConstraint(constraint, processing.initialChunk(), processing.evidence(), processing.justifications(), context) + activateConstraint(constraint, processing.initialChunk(), processing.JustifiedOccurrenceCreator(), context) return context.currentStatus() } @@ -166,14 +166,13 @@ internal class ControllerImpl ( // fixme: fails in lambdacalc because of reactivated occurrences // (parents ain't tracked correctly in this case) // assert(newParent === processing.parentChunk()) + // todo: remove tracking parent in Controller once above issue is fixed - val currentJustifications = processing.justifications() - val currentEvidence = processing.evidence() + val occCreator = processing.JustifiedOccurrenceCreator() for (item in body) { val itemOk = when (item) { - // Occurrence just inherits evidence and justifications of its activating rule match - is Constraint -> activateConstraint(item, newParent, currentEvidence, currentJustifications, context) + is Constraint -> activateConstraint(item, newParent, occCreator, context) is Predicate -> tellPredicate(item, context) else -> throw IllegalArgumentException("unknown item ${item}") } @@ -229,15 +228,17 @@ internal class ControllerImpl ( return context.currentStatus() } - private fun activateConstraint(constraint: Constraint, parent: MatchJournal.MatchChunk, evidence: Evidence, justifications: Justifications, context: Context) : Boolean { + private fun activateConstraint(constraint: Constraint, parent: MatchJournal.MatchChunk, creator: ConstraintsProcessing.JustifiedOccurrenceCreator, context: Context) : Boolean { val args = supervisor.instantiateArguments(constraint.arguments(), context.logicalContext, context) return context.eval { status -> profiler.profile("activate_${constraint.symbol()}") { - constraint.occurrence(logicalStateObservable(), args, evidence, justifications, context.logicalContext, context.ruleUniqueTag).let { occ -> - trace.activate(occ) - processing.processActivated(this, occ, parent, status) + with(creator) { + constraint.occurrence(logicalStateObservable(), args, context.logicalContext, context.ruleUniqueTag).let { occ -> + trace.activate(occ) + processing.processActivated(this@ControllerImpl, occ, parent, status) + } } } 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 1c570ed7..bdd054fb 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 @@ -82,8 +82,16 @@ interface MatchJournal : MutableIterable, EvidenceSource { * Transitively removes descendants of removed chunks. * Only erases future chunks and leaves journal [currentPos] intact. */ + @Deprecated("obsolete machinery, superseded by [dropDescendants] & MPSCR-65") fun dropDescendantsWhile(ancestor: Chunk, dropIf: (Chunk) -> Boolean) + /** + * Removes [Chunk]s dependent on any of [invalidated], + * applying [forEachDropped] for each removed [Chunk]. + * Only erases future chunks, leaving journal position [currentPos] intact. + */ + fun dropDescendants(invalidated: Collection, forEachDropped: (Chunk) -> Unit) + /** * Replay activated and discarded occurrences logged in journal between current * and provided positions. Advances journal position to specified position. @@ -131,6 +139,11 @@ interface MatchJournal : MutableIterable, EvidenceSource { * Length of the indexed [MatchJournal] */ val size: Int + + // some context functions + infix fun Pos.before(other: Pos): Boolean = compare(this, other) <= 0 + + infix fun Pos.after(other: Pos): Boolean = compare(this, other) >= 0 } /** @@ -243,3 +256,11 @@ private fun Iterable.allOccurrences(): List, forEachDropped: (Chunk) -> Unit) { + if (invalidated.isEmpty()) return + + val start = current + while (posPtr.hasNext()) { + current = posPtr.next() + if (current.justifiedByAny(invalidated)) { + // no need to 'resetOccurrences' because journal position is left intact + posPtr.remove() + forEachDropped(current) + } + } + + // rollback to the start + while (current !== start) { + current = posPtr.previous() + } + // make ptr point right after 'current' in case we changed anything + if (posPtr.hasNext()) posPtr.next() + } + private fun resetOccurrences(occSpecs: List) = // assume occSpecs are ordered in order of processing // so, iterate over reversed list @@ -434,13 +455,6 @@ internal open class MatchJournalImpl( } } -// NB: returns same collection of justifications, not copy -fun MatchJournal.justifications() = this.currentPos().chunk.justifications() -fun MatchJournal.evidence() = this.currentPos().chunk.evidence -// todo: this should be more correct -//fun MatchJournal.justifications() = this.parentChunk().justifications() -//fun MatchJournal.evidence() = this.parentChunk().evidence - // returns new collection of justifications fun RuleMatch.collectJustifications(vararg withEvidence: Evidence): Justifications = justsOf(*withEvidence).also { allJss ->