Implement incremental handling of discarded principal occurrences (MPSCR-65)

Matches which discard principal occurrences must be handled specially
on incremental execution. Imagine such match inserted in journal
before other matches with the same occurrence in head.
Because inserted match discards the occurrence, following matches
can't match on it. They must be invalidated. (Relevant for MPSCR-62)
See tests for substructuralTS.

Commit refactors machinery of `dropDiscardingMatchesFor` in
ConstraintsProcessing that was incomplete, as revealed by MPSCR-64.

Relaxes small memory opt introduced in commit a2675351:
Now justifications in Occurrences are not shared with their
activating matches. See JustifiedOccurrenceCreator.
Introduced machinery requires that Occurrences had their own
Evidence (because `dropDiscarding` invalidates by Occurrences).
Previously algorithm was invalidating Chunks only by Evidence
from rule matches, that's why only RuleMatches had to have
unique Evidence, while Occurrences could bear less info.

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<Justified>): Iterable<Occurrence> {
+        // 'Undo' all activated in this chunk occurrences
+        chunk.activatedLog().forEach {
+            dispatchingFront = dispatchingFront.forget(it)
+        }
+
+        val validOccs: Sequence<Occurrence>
+        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<Rule>) {
 
         val activationCandidates = mutableListOf<MatchCandidate>()
@@ -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<Any>) =
         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<Any>): Boolean =
         utags.contains(this.ruleUniqueTag) || utags.any { utag -> dependsOnRule(utag) }
 

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

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<FeedbackStatus>("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)
+                    }
                 }
 
             }

reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/MatchJournal.kt

@@ -82,8 +82,16 @@ interface MatchJournal : MutableIterable<MatchJournal.Chunk>, 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<Justified>, 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<MatchJournal.Chunk>, 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<MatchJournal.Chunk.Entry>.allOccurrences(): List<Occurrence
     return set.map { it.wrapped }
 }
 
+
+// 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
+

reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/MatchJournalImpl.kt

@@ -309,6 +309,27 @@ internal open class MatchJournalImpl(
         if (posPtr.hasNext()) posPtr.next()
     }
 
+    override fun dropDescendants(invalidated: Collection<Justified>, 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<Chunk.Entry>) =
         // 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 ->