Refine MatchHistory impl, extract interface for tests, add several tests.

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

@@ -20,73 +20,136 @@ import gnu.trove.set.TIntSet
 import gnu.trove.set.hash.TIntHashSet
 import jetbrains.mps.logic.reactor.core.Occurrence
 import jetbrains.mps.logic.reactor.evaluation.RuleMatch
-import org.jetbrains.kotlin.utils.mapToIndex
+import jetbrains.mps.logic.reactor.evaluation.StoreView
+import java.util.*
 
 
-internal class MatchHistory() {
+interface MatchHistory {
-
+    data class Chunk(val match: RuleMatch, val id: Int, val justifications: TIntSet) {
-    class Chunk(val match: RuleMatch, val id: Int, headJustifications: TIntSet) {
         data class Entry(val occ: Occurrence, val isDiscarded: Boolean = false)
 
         var occurrences: MutableList<Entry> = mutableListOf()
-        val justifications = headJustifications.also { it.add(id) }
     }
 
     class RemoveChunkIterator(val it: MutableListIterator<Chunk>): Iterator<Chunk> by it {
         fun remove() = it.remove()
     }
 
-    fun removeIterator() = RemoveChunkIterator(hist.listIterator())
+    interface HistoryPos {
+        fun chunk(): Chunk
+        fun occsRetained(): Int
+    }
 
 
-    fun logMatch(match: RuleMatchImpl) {
+    fun removeIterator(): RemoveChunkIterator
+    fun resetStore()
+    fun storeView(): StoreView
+
+    fun logMatch(match: RuleMatch)
+    fun logOccurence(occ: Occurrence)
+
+    fun current(): Chunk
+    fun currentPos(): HistoryPos
+    fun push()
+    fun reset(timepoint: HistoryPos)
+
+    fun rollTo(futurePos: HistoryPos)
+
+    companion object {
+        fun getMatchHistory(chunkIdSeed: Int = 0): MatchHistory = MatchHistoryImpl(chunkIdSeed)
+    }
+}
+
+
+internal class MatchHistoryImpl(chunkIdSeed: Int): MatchHistory {
+
+    override fun removeIterator() = MatchHistory.RemoveChunkIterator(hist.listIterator())
+
+    // Reset only store & history position, don't modify history
+    override fun resetStore() {
+        frameStack.reset(Frame(frameStack))
+        pos = hist.listIterator()
+    }
+
+    override fun storeView(): StoreView = frameStack.current.store.view()
+
+
+    override fun logMatch(match: RuleMatch) {
+        val m = match as RuleMatchImpl
         // If the set of justifications isn't empty, then we deal with principal constraint
         val justs = match.headJustifications()
         if (!justs.isEmpty) {
-            val newChunk = Chunk(match, nextChunkId++, justs)
+            justs.add(nextChunkId)
+            val newChunk = MatchHistory.Chunk(match, nextChunkId, justs)
             pos.add(newChunk)
+
+            ++nextChunkId
             current = newChunk
         }
 
         // Log discards
         match.forEachReplaced {occ ->
 //            this.dispatchFringe = dispatchFringe.contract(occ)
-            current.occurrences.add(Chunk.Entry(occ, true))
+            current.occurrences.add(MatchHistory.Chunk.Entry(occ, true))
             frameStack.current.store.discard(occ)
         }
     }
-    fun logOccurence(occ: Occurrence) {
+
-        current.occurrences.add(Chunk.Entry(occ))
+    override fun logOccurence(occ: Occurrence) {
+        current.occurrences.add(MatchHistory.Chunk.Entry(occ))
         frameStack.current.store.store(occ)
     }
 
 
-    data class HistoryPos(val frame: Frame, val chunk: Chunk, val occsRetained: Int = 0)
+    private data class HistoryPosImpl(val frame: Frame, val chunk: MatchHistory.Chunk, val occsRetained: Int = 0) : MatchHistory.HistoryPos {
+        override fun chunk(): MatchHistory.Chunk = chunk
+        override fun occsRetained(): Int = occsRetained
+    }
+
+    // FrameStack API: currentFrame/currentPos, push, reset
+    fun currentFrame() = frameStack.current
+
+    override fun current(): MatchHistory.Chunk = current
+
+    override fun currentPos(): MatchHistory.HistoryPos = HistoryPosImpl(frameStack.current, current, current.occurrences.size)
+
+    override fun push(): Unit { frameStack.push() }
 
-    // FrameStack API: currentFrame, push, reset
-    fun currentFrame() = HistoryPos(frameStack.current, current, current.occurrences.size)
-    fun push() = frameStack.push()
     // Throw away recently added chunks and reset store accordingly
     // NB: not checking that chunks are actually recently added
-    fun reset(timepoint: HistoryPos) {
+    override fun reset(timepoint: MatchHistory.HistoryPos) {
-        frameStack.reset(timepoint.frame)
+        val tp = timepoint as HistoryPosImpl
+        frameStack.reset(tp.frame)
 
-        while (timepoint.chunk != current && pos.hasPrevious()) {
+        while (tp.chunk != current && pos.hasPrevious()) {
-            pos.remove()
             current = pos.previous()
+            pos.remove()
         }
-        current.occurrences = current.occurrences.take(timepoint.occsRetained) as MutableList<Chunk.Entry>
+        current.occurrences = current.occurrences.take(tp.occsRetained) as MutableList<MatchHistory.Chunk.Entry>
     }
 
-    fun rollTo(chunk: Chunk) {
+
-        while (chunk != current && pos.hasNext()) {
+    override fun rollTo(futurePos: MatchHistory.HistoryPos) {
+        val fp = futurePos as HistoryPosImpl
+        while (pos.hasNext()) {
             current = pos.next()
-            rollChunk()
+            if (fp.chunk == current) {
+                rollOccurences(current.occurrences.take(fp.occsRetained))
+                break
+            }
+            rollOccurences(current.occurrences)
         }
     }
-    private fun rollChunk() {
+    fun rollTo(chunk: MatchHistory.Chunk) {
+        while (current != chunk && pos.hasNext()) {
+            current = pos.next()
+            rollOccurences(current.occurrences)
+        }
+    }
+
+    private fun rollOccurences(occSpecs: Iterable<MatchHistory.Chunk.Entry>) {
         // 'apply' all occurrences of current chunk to the store
-        for (occSpec in current.occurrences) {
+        for (occSpec in occSpecs) {
             if (occSpec.isDiscarded) {
                 frameStack.current.store.discard(occSpec.occ)
             } else {
@@ -95,28 +158,19 @@ internal class MatchHistory() {
         }
     }
 
-    // Reset only store & history position, don't modify history
-    fun resetStore() {
-        frameStack.reset(Frame(frameStack))
-        pos = hist.listIterator()
-    }
-
     // fixme: does belong to here?
 //    fun resetOrder() { order = hist.mapToIndex() }
 
 
-    private val hist: MutableList<Chunk> = mutableListOf()
+    private val hist: MutableList<MatchHistory.Chunk> = LinkedList<MatchHistory.Chunk>()
 //    private var order: Map<Chunk, Int> = emptyMap()
+    private val frameStack: FrameStack = FrameStack(null)
 
-    // FIXME: add framestack to the class
+    // FIXME: provide initial chunk? possibly initialized from StoreView, with empty justifications
-    // is it created along with MatchHistory? should be.
+    private lateinit var current: MatchHistory.Chunk
-    private val frameStack: FrameStack = FrameStack(null) //FIXME: ?provide storeView at construction
+    private var pos: MutableListIterator<MatchHistory.Chunk> = hist.listIterator()
 
-    private var pos: MutableListIterator<Chunk> = hist.listIterator()
+    private var nextChunkId: Int = chunkIdSeed;
-    // FIXME: provide initial chunk at construction
-    private lateinit var current: Chunk
-
-    private var nextChunkId: Int = 0;
 
 
 }

reactor/Core/src/jetbrains/mps/logic/reactor/program/Constraint.java

@@ -38,4 +38,5 @@ public interface Constraint extends AndItem {
      */
     Collection<? extends Predicate> patternPredicates(Collection<?> occurrenceArgs);
 
+    default boolean isPrincipal() { return false; }
 }

reactor/Test/src/program/MockConstraint.kt

@@ -8,10 +8,12 @@ import jetbrains.mps.logic.reactor.program.Predicate
  * @author Fedor Isakov
  */
 
-data class MockConstraint(val symbol: ConstraintSymbol, val arguments: List<Any>) : Constraint {
+data class MockConstraint(val symbol: ConstraintSymbol, val arguments: List<Any>, val principal: Boolean = false) : Constraint {
 
     constructor(symbol: ConstraintSymbol, vararg args: Any) : this(symbol, listOf(* args)) {}
 
+    constructor(symbol: ConstraintSymbol, principal: Boolean, vararg args: Any) : this(symbol, listOf(* args), principal) {}
+
     override fun arguments(): List<Any> = arguments
 
     override fun patternPredicates(args: Collection<*>): Collection<Predicate> = emptyList()
@@ -20,6 +22,8 @@ data class MockConstraint(val symbol: ConstraintSymbol, val arguments: List<Any>
 
     override fun argumentTypes(): List<Class<*>> = arguments.map { arg -> arg.javaClass }
 
+    override fun isPrincipal(): Boolean = principal
+
     override fun toString(): String = "${symbol()}(${arguments().joinToString()})"
 
 }

reactor/Test/test/RulesHelper.kt

@@ -1,3 +1,5 @@
+import gnu.trove.set.TIntSet
+import gnu.trove.set.hash.TIntHashSet
 import jetbrains.mps.logic.reactor.core.*
 import jetbrains.mps.logic.reactor.core.internal.FeedbackStatus
 import jetbrains.mps.logic.reactor.evaluation.PredicateInvocation
@@ -106,7 +108,11 @@ fun altBody(vararg content: ConjBuilder.() -> Unit): RuleBuilder.() -> Unit = {
 }
 
 fun constraint(id: String, vararg args: Any): ConjBuilder.() -> Unit = {
-    add(createConstraint(args, id))
+    add(createConstraint(args, id, false))
+}
+
+fun princConstraint(id: String, vararg args: Any): ConjBuilder.() -> Unit = {
+    add(createConstraint(args, id, true))
 }
 
 
@@ -117,6 +123,10 @@ fun equals(left: Any, right: Any): ConjBuilder.() -> Unit = {
 fun occurrence(id: String, vararg args: Any): Occurrence =
     MockConstraint(ConstraintSymbol.symbol(id, args.size)).occurrence(MockController(), listOf(* args))
 
+fun justifiedOccurrence(id: String, justs: TIntSet, vararg args: Any): Occurrence =
+    MockConstraint(ConstraintSymbol.symbol(id, args.size), true).occurrence(listOf(* args), { fooObservable }, justs)
+fun justifiedOccurrence(id: String, justs: Set<Int>, vararg args: Any): Occurrence = justifiedOccurrence(id, TIntHashSet(justs), * args)
+
 fun sym0(id: String): ConstraintSymbol =
     ConstraintSymbol(id, 0)
 
@@ -168,8 +178,8 @@ class MockController : Controller {
 class ConjBuilder(val type: Class<out AndItem>) {
     val constraints = ArrayList<AndItem>()
 
-    fun createConstraint(args: Array<out Any>, id: String): Constraint {
+    fun createConstraint(args: Array<out Any>, id: String, principal: Boolean): Constraint {
-        return MockConstraint(ConstraintSymbol(id, args.size), * args)
+        return MockConstraint(ConstraintSymbol(id, args.size), principal, * args)
     }
 
     fun add(item: AndItem): Unit {

reactor/Test/test/TestMatchHistory.kt

@@ -0,0 +1,303 @@
+import gnu.trove.set.hash.TIntHashSet
+import jetbrains.mps.logic.reactor.core.*
+import jetbrains.mps.logic.reactor.core.internal.createOccurrenceMatcher
+import jetbrains.mps.logic.reactor.core.internal.logical
+import jetbrains.mps.logic.reactor.core.internal.MatchHistory
+import jetbrains.mps.logic.reactor.program.ConstraintSymbol
+import jetbrains.mps.logic.reactor.program.ConstraintSymbol.symbol
+import org.junit.Test
+import org.junit.Assert.*
+
+/*
+ * Copyright 2014-2019 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.
+ */
+
+
+class TestMatchHistory {
+
+    @Test
+    fun testJustificationTracking() {
+        val hist = MatchHistory.getMatchHistory()
+
+        with(programWithRules(
+            rule("rule1",
+                headKept(
+                    constraint("main")
+                ),
+                body(
+                    constraint("foo")
+                )),
+            rule("rule2",
+                headKept(
+                    constraint("foo")
+                ),
+                body(
+                    constraint("bar")
+                )),
+            rule("rule3",
+                headKept(
+                    constraint("foo")
+                ),
+                body(
+                    constraint("qux")
+                )),
+            rule("rule4",
+                headReplaced(
+                    constraint("bar"),
+                    constraint("qux")
+                ),
+                body(
+//                    constraint("blin")
+                ))))
+        {
+
+            var d = Dispatcher(RuleIndex(handlers)).fringe()
+            val mainOcc = justifiedOccurrence("main", setOf(0))
+//            hist.logOccurence(mainOcc) // plays a role of the initial constraint, with no preceding RuleMatch
+            d = d.expand(mainOcc)
+
+            with(d.matches()) {
+                count() shouldBe 1
+
+                with(first()) {
+                    hist.logMatch(this)
+                    rule().tag() shouldBe "rule1"
+
+                    hist.current().justifications shouldBe TIntHashSet(setOf(0))
+                    val fooOcc = justifiedOccurrence("foo", hist.current().justifications)
+                    hist.logOccurence(fooOcc)
+                    d = d.expand(fooOcc)
+                }
+            }
+
+            with(d.matches()) {
+                count() shouldBe 2
+
+                with(elementAt(0)) {
+                    hist.logMatch(this)
+                    rule().tag() shouldBe "rule2"
+
+                    hist.current().justifications shouldBe TIntHashSet(setOf(0,1))
+                    val barOcc = justifiedOccurrence("bar", hist.current().justifications)
+                    hist.logOccurence(barOcc)
+                    d = d.expand(barOcc)
+
+                    with(d.matches()) {
+                        count() shouldBe 0
+                    }
+                }
+
+                with(elementAt(1)) {
+                    hist.logMatch(this)
+                    rule().tag() shouldBe "rule3"
+
+                    hist.current().justifications shouldBe TIntHashSet(setOf(0,2))
+                    val quxOcc = justifiedOccurrence("qux", hist.current().justifications)
+                    hist.logOccurence(quxOcc)
+                    d = d.expand(quxOcc)
+
+                    with(d.matches()) {
+                        count() shouldBe 1
+
+                        with(first()) {
+                            hist.logMatch(this)
+                            rule().tag() shouldBe "rule4"
+                        }
+                        hist.current().justifications shouldBe TIntHashSet(setOf(0,1,2,3))
+                    }
+                }
+            }
+        }
+    }
+
+
+    @Test
+    fun testResetThenRoll() {
+        val hist = MatchHistory.getMatchHistory()
+
+        with(programWithRules(
+            rule("rule1",
+                headKept(
+                    constraint("main")
+                ),
+                body(
+                    constraint("foo")
+                )),
+            rule("rule2",
+                headKept(
+                    constraint("foo")
+                ),
+                body(
+                    constraint("bar")
+                )),
+            rule("rule3",
+                headReplaced(
+                    constraint("bar"),
+                    constraint("foo")
+                ),
+                body(
+                    constraint("qux")
+                ))
+            ))
+        {
+
+            var d = Dispatcher(RuleIndex(handlers)).fringe()
+            val mainOcc = justifiedOccurrence("main", setOf(0))
+//            hist.logOccurence(mainOcc) // plays a role of the initial constraint, with no preceding RuleMatch
+            d = d.expand(mainOcc)
+
+            with(d.matches().first()) {
+                hist.logMatch(this)
+            }
+            val fooOcc = justifiedOccurrence("foo", hist.current().justifications)
+            hist.logOccurence(fooOcc)
+            d = d.expand(fooOcc)
+
+
+            with(d.matches().first()) {
+                hist.logMatch(this)
+            }
+            val barOcc = justifiedOccurrence("bar", hist.current().justifications)
+            hist.logOccurence(barOcc)
+            d = d.expand(barOcc)
+
+            with(d.matches().first()) {
+                hist.logMatch(this)
+            }
+            val quxOcc = justifiedOccurrence("qux", hist.current().justifications)
+            hist.logOccurence(quxOcc)
+            d = d.expand(quxOcc)
+
+            // 'rollTo' to the saved pos after full 'resetStore' must restore the store
+
+            val oldStore = hist.storeView().allOccurrences()
+            oldStore.count() shouldBe 1
+            val savedPos = hist.currentPos()
+
+            hist.resetStore()
+            hist.storeView().allOccurrences().count() shouldBe 0
+
+            hist.rollTo(savedPos)
+            hist.storeView().allOccurrences() shouldBe oldStore
+            hist.currentPos().chunk() shouldBe savedPos.chunk()
+            hist.currentPos().occsRetained() shouldBe savedPos.occsRetained()
+        }
+    }
+
+    @Test
+    fun testPushExecReset() {
+        val hist = MatchHistory.getMatchHistory()
+
+        with(programWithRules(
+            rule("rule1",
+                headKept(
+                    princConstraint("main")
+                ),
+                body(
+                    princConstraint("foo")
+                )),
+            rule("rule2",
+                headKept(
+                    princConstraint("foo")
+                ),
+                body(
+                    constraint("bar"),
+                    constraint("bazz"),
+                    princConstraint("qux")
+                )),
+            rule("rule3",
+                headReplaced(
+                    constraint("bar"),
+                    constraint("bazz")
+                ),
+                body(
+                    constraint("bazz")
+                )),
+            rule("rule4",
+            headKept(
+                princConstraint("qux"),
+                princConstraint("foo")
+            ),
+            body(
+                constraint("last")
+            ))
+        ))
+        {
+
+            var d = Dispatcher(RuleIndex(handlers)).fringe()
+            val mainOcc = justifiedOccurrence("main", setOf(0))
+            d = d.expand(mainOcc)
+
+            with(d.matches().first()) {
+                rule().tag() shouldBe "rule1"
+                hist.logMatch(this)
+            }
+            val fooOcc = justifiedOccurrence("foo", hist.current().justifications)
+            hist.logOccurence(fooOcc)
+            d = d.expand(fooOcc)
+
+
+            with(d.matches().first()) {
+                rule().tag() shouldBe "rule2"
+                hist.logMatch(this)
+            }
+            val barOcc = occurrence("bar")
+            val bazzOcc = occurrence("bazz")
+            val quxOcc = justifiedOccurrence("qux", hist.current().justifications)
+            hist.logOccurence(barOcc)
+            d = d.expand(barOcc)
+            hist.logOccurence(bazzOcc)
+            d = d.expand(bazzOcc)
+
+
+            val curChunk = hist.current()
+            with(d.matches().first()) {
+                rule().tag() shouldBe "rule3"
+                hist.logMatch(this)
+            }
+            // matched on rule with heads without justifications, should remain in the same chunk
+            hist.current() shouldBeSame curChunk
+
+            val bazzOcc2 = occurrence("bazz")
+            hist.logOccurence(bazzOcc2)
+            d = d.expand(bazzOcc2)
+
+            val oldStore = hist.storeView().allOccurrences()
+            val savedPos = hist.currentPos()
+            hist.push()
+
+
+            hist.logOccurence(quxOcc)
+            d = d.expand(quxOcc)
+
+
+            with(d.matches().first()) {
+                rule().tag() shouldBe "rule4"
+                hist.logMatch(this)
+            }
+            val lastOcc = occurrence("last")
+            hist.logOccurence(lastOcc)
+            d = d.expand(lastOcc)
+
+
+            assertNotEquals(oldStore, hist.storeView().allOccurrences())
+            hist.reset(savedPos)
+            assertEquals(oldStore, hist.storeView().allOccurrences())
+
+            hist.currentPos().chunk() shouldBe savedPos.chunk()
+            hist.currentPos().occsRetained() shouldBe savedPos.occsRetained()
+        }
+    }
+}