diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/Justified.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/Justified.kt index 6f7f2a63..887279f6 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/Justified.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/Justified.kt @@ -28,13 +28,20 @@ typealias Evidence = Int /** * [Justifications] is a set of [Evidence]s. */ -typealias Justifications = TIntSet - -fun emptyJustifications(): Justifications = TIntHashSet(1) -fun justsOf(vararg elements: Evidence): Justifications = TIntHashSet(elements) -fun justsFromCollection(collection: Collection): Justifications = TIntHashSet(collection) -fun justsCopy(other: Justifications): Justifications = TIntHashSet(other) - +data class Justifications(private val evidenceSet: TIntSet) { + companion object { + fun empty() = Justifications (TIntHashSet(1)) + fun of(vararg elements: Evidence) = Justifications(TIntHashSet(elements)) + fun of(collection: Collection) = Justifications(TIntHashSet(collection)) + fun copy(other: Justifications) = Justifications(TIntHashSet(other.evidenceSet)) + } + fun addAll(that: Justifications) { evidenceSet.addAll(that.evidenceSet) } + fun add(evidence: Evidence) { evidenceSet.add(evidence) } + fun contains(evidence: Evidence) = evidenceSet.contains(evidence) + fun forEach(action: (Evidence) -> Boolean) { + evidenceSet.forEach(action) + } +} /** * A logical entity whose existence is supported by some 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 c5fcec72..7bece4b7 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 @@ -164,7 +164,7 @@ internal class ConstraintsProcessing( // By default share justifications (as a small optimization) val evidence = nextEvidence() - val justifications = justsCopy(savedJustifications).apply { add(evidence) } + val justifications = Justifications.copy(savedJustifications).apply { add(evidence) } return Occurrence( this, logicalContext, arguments, evidence, 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 368f5cda..5ba1cf16 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 @@ -141,7 +141,7 @@ interface MatchJournal : EvidenceSource { val occ: Occurrence } - open class Pos(val chunk: Chunk, val entriesCount: Int) { + class Pos(val chunk: Chunk, val entriesCount: Int) { override fun equals(other: Any?) = other is Pos 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 e6195bf2..ce6a2cd9 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 @@ -34,7 +34,7 @@ internal open class MatchJournalImpl( val trace: EvaluationTrace = EvaluationTrace.NULL ) : MatchJournal { - private abstract class ChunkImpl : Chunk { + private sealed class ChunkImpl : Chunk { var entries: MutableList = mutableListOf() override fun entries(): List = entries override fun addEntry(e: Chunk.Entry) = entries.add(e) @@ -54,7 +54,7 @@ internal open class MatchJournalImpl( private object CornerChunk : ChunkImpl() { override val evidence: Evidence = -1 - override fun justifications(): Justifications = emptyJustifications() + override fun justifications() = Justifications.empty() } @@ -209,70 +209,12 @@ internal open class MatchJournalImpl( throw IllegalStateException() } - - /** - * Provides [MatchJournal] look-ahead traverse. - */ - abstract private class AbstractChunkIterator(private val iter: ListIterator) : ChunkIterator - { - protected var __next: ChunkImpl - protected var __current: ChunkImpl - - init { - __current = iter.next() - __next = iter.next() - iter.previous() - - assert(__current is CornerChunk) - } - - final override val current: Chunk get() = __current - - final override fun atStart(): Boolean = __current is CornerChunk - final override fun atEnd(): Boolean = __next is CornerChunk - - protected fun updateNext() { - assert(iter.hasNext()) { "journal iterator must always have next chunk (maybe the final)" } - __next = iter.next() - iter.previous() // iterator always points between stored chunks - } - - protected fun nextImpl(): Chunk { - __current = iter.next() - assert(__current === __next) - updateNext() - return __current - } - } - - internal infix fun ChunkIterator.assertAt(pos: Pos) { - if (!(this at pos)) - throw IllegalStateException("Position wasn't found in journal: $pos") - } - - - internal class StoreViewImpl(occurrences: Sequence) : StoreView { - - val allOccurrences = occurrences.toSet() - - val allSymbols = allOccurrences.map { co -> co.constraint().symbol() }.toSet() - - override fun constraintSymbols(): Iterable = allSymbols - - override fun allOccurrences(): Iterable = allOccurrences - - override fun occurrences(symbol: ConstraintSymbol): Iterable = - allOccurrences.filter { co -> co.constraint().symbol() == symbol }.toSet() - - } - - /** * Provides [MatchJournal] modification and look-ahead traverse with [Chunk] replay. * Represents [MatchJournal] state: additions & removals happen at pointed-to position. * [Cursor] points at position between [current] & [initial]. */ - private inner class Cursor(private val iter: MutableListIterator) : AbstractChunkIterator(iter){ + private inner class Cursor(private val iter: MutableListIterator) : ChunkIterator { /** * Replays [Chunk]s while iterating */ @@ -312,6 +254,40 @@ internal open class MatchJournalImpl( this assertAt pastPos } + private var __next: ChunkImpl + private var __current: ChunkImpl + + init { + __current = iter.next() + __next = iter.next() + iter.previous() + + assert(__current is CornerChunk) + } + + override val current: Chunk get() = __current + + override fun atStart(): Boolean = __current is CornerChunk + override fun atEnd(): Boolean = __next is CornerChunk + + private fun updateNext() { + assert(iter.hasNext()) { "journal iterator must always have next chunk (maybe the final)" } + __next = iter.next() + iter.previous() // iterator always points between stored chunks + } + + private fun nextImpl(): Chunk { + __current = iter.next() + assert(__current === __next) + updateNext() + return __current + } + + infix fun assertAt(pos: Pos) { + if (!(this at pos)) + throw IllegalStateException("Position wasn't found in journal: $pos") + } + } /** @@ -348,13 +324,13 @@ internal open class MatchJournalImpl( } } - // returns new collection of justifications internal fun RuleMatch.collectJustifications(vararg withEvidence: Evidence): Justifications = - justsOf(*withEvidence).also { allJss -> - this.allHeads().forEach { allJss.addAll(it.justifications()) } + Justifications.of(*withEvidence).also { justifications -> + this.allHeads().forEach { justifications.addAll(it.justifications()) } } internal fun MutableList.push(element: E) = this.add(element) internal fun MutableList.pop() = this.removeAt(this.size - 1) internal fun MutableList.peek() = this.last() + diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/StoreViewImpl.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/StoreViewImpl.kt new file mode 100644 index 00000000..f0be03bb --- /dev/null +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/StoreViewImpl.kt @@ -0,0 +1,37 @@ +/* + * Copyright 2014-2024 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.Occurrence +import jetbrains.mps.logic.reactor.evaluation.ConstraintOccurrence +import jetbrains.mps.logic.reactor.evaluation.StoreView +import jetbrains.mps.logic.reactor.program.ConstraintSymbol + +internal class StoreViewImpl(occurrences: Sequence) : StoreView { + + val allOccurrences = occurrences.toSet() + + val allSymbols = allOccurrences.map { co -> co.constraint().symbol() }.toSet() + + override fun constraintSymbols(): Iterable = allSymbols + + override fun allOccurrences(): Iterable = allOccurrences + + override fun occurrences(symbol: ConstraintSymbol): Iterable = + allOccurrences.filter { co -> co.constraint().symbol() == symbol }.toSet() + +} \ No newline at end of file diff --git a/reactor/Test/test/RulesHelper.kt b/reactor/Test/test/RulesHelper.kt index b659ad29..320ccd44 100644 --- a/reactor/Test/test/RulesHelper.kt +++ b/reactor/Test/test/RulesHelper.kt @@ -1,8 +1,5 @@ import jetbrains.mps.logic.reactor.core.* import jetbrains.mps.logic.reactor.core.internal.* -import jetbrains.mps.logic.reactor.evaluation.PredicateInvocation -import jetbrains.mps.logic.reactor.evaluation.Solver -import jetbrains.mps.logic.reactor.evaluation.StoreView import jetbrains.mps.logic.reactor.logical.Logical import jetbrains.mps.logic.reactor.logical.LogicalContext import jetbrains.mps.logic.reactor.logical.MetaLogical @@ -102,7 +99,7 @@ fun equals(left: Any, right: Any): ConjBuilder.() -> Unit = { fun occurrence(id: String, vararg args: Any): Occurrence = MockConstraint(ConstraintSymbol.symbol(id, args.size)) - .occurrence(listOf(* args), 0, justsOf(0), noLogicalContext) + .occurrence(listOf(* args), 0, Justifications.of(0), noLogicalContext) fun justifiedOccurrence(id: String, evidence: Evidence, justifications: Justifications, principal: Boolean, vararg args: Any): Occurrence = MockConstraint(ConstraintSymbol.symbol(id, args.size), principal) @@ -115,7 +112,7 @@ fun justifiedOccurrence(id: String, hist: MatchJournal, vararg args: Any): Occur justifiedOccurrence(id, hist.evidence(), hist.justifications(), false, * args) fun principalOccurrenceInit(id: String, vararg args: Any): Occurrence = - justifiedOccurrence(id, 0, justsFromCollection(setOf(0)), true, * args) + justifiedOccurrence(id, 0, Justifications.of(setOf(0)), true, * args) fun sym0(id: String): ConstraintSymbol = ConstraintSymbol(id, 0) diff --git a/reactor/Test/test/TestStoreAwareJournal.kt b/reactor/Test/test/TestStoreAwareJournal.kt index 089d170c..49bf0488 100644 --- a/reactor/Test/test/TestStoreAwareJournal.kt +++ b/reactor/Test/test/TestStoreAwareJournal.kt @@ -1,7 +1,5 @@ import jetbrains.mps.logic.reactor.core.* import jetbrains.mps.logic.reactor.core.internal.* -import jetbrains.mps.logic.reactor.program.Constraint -import jetbrains.mps.logic.reactor.program.Rule import org.junit.Test import org.junit.Assert.* @@ -75,7 +73,7 @@ class TestStoreAwareJournal { { with(JournalDispatcherHelper(Dispatcher(RuleIndex(rules)))) { - hist.justifications() shouldBe justsOf(0) // initial chunk + hist.justifications() shouldBe Justifications.of(0) // initial chunk logExpand(principalOccurrenceInit("foo")) val fooMatches = d.matches() @@ -84,7 +82,7 @@ class TestStoreAwareJournal { // log first 'foo' match hist.logMatch(fooMatches.first()) - hist.justifications() shouldBe justsOf(0,1) + hist.justifications() shouldBe Justifications.of(0,1) logExpandJustified("bar") d.matches().count() shouldBe 0 @@ -92,13 +90,13 @@ class TestStoreAwareJournal { // log second 'foo' match hist.logMatch(fooMatches.elementAt(1)) - hist.justifications() shouldBe justsOf(0,2) + hist.justifications() shouldBe Justifications.of(0,2) logExpandJustified("qux") d.matches().count() shouldBe 1 logFirstMatch() - hist.justifications() shouldBe justsOf(0,1,2,3) + hist.justifications() shouldBe Justifications.of(0,1,2,3) } } }