Add new incr stage for rewinding logical unification (MPSCR-67 & MPSCR-21)
For this several notions are introduced. Logical variable is called "principal" if it is used in principal occurrences and at some point during evaluation is unified or bound. Principal occurrence is called "volatile" if it uses principal logicals. PrincipalObserverDispatcher's task is to track volatile occurrences by enabling uni observers on all free logicals in principal occ-s. RewindVolatileOccurrencesStage then on events of incremental usage of volatile occurrences (e.g. match on it, or continued activation) resets journal cursor to the position of initial occurrence activation, where it can be re-evaluated with fresh, unaffected, logicals. It's the only stage that goes backwards in journal. So in this way unification is incrementally cancelled. link to MPSCR-62 (docs)
This commit is contained in:
Grigorii Kirgizov
parent
eb1e646cd4
commit
98ee9f4da2
|
|
@ -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) {
|
||||
|
|
|
|||
|
|
@ -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 {
|
||||
|
|
|
|||
|
|
@ -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<Any>,
|
||||
private val activationSink: ContinuedActivationSink,
|
||||
private val stateCleaner: ConstraintsProcessing.ProgramStateCleaner,
|
||||
private val trace: EvaluationTrace
|
||||
): IncrementalStage {
|
||||
): IncrementalStage, InvalidatingInfo {
|
||||
|
||||
private val invalidJustifications = mutableListOf<Justified>()
|
||||
|
||||
|
|
@ -62,9 +74,13 @@ internal class InvalidationStage(
|
|||
|
||||
fun invalidatedRules(): List<Any> = invalidRuleIdsAll.toList()
|
||||
|
||||
override fun isInvalid(entity: Justified): Boolean =
|
||||
entity.justifiedByAny(invalidJustifications)
|
||||
|
||||
fun receive(invalid: Iterable<Justified>) { 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<Rule>,
|
||||
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<MatchCandidate>()
|
||||
private val activationCandidates = PriorityQueue<MatchCandidate>{
|
||||
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<Int, MutableCollection<RuleMatchEx>> = hashMapOf()
|
||||
|
||||
|
||||
fun onNext(reader: ChunkReader): Collection<AdditionStage.MatchCandidate> {
|
||||
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<RuleMatchEx>): List<RuleMatchEx> {
|
||||
val currentMatches = mutableListOf<RuleMatchEx>()
|
||||
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<ExecPos> = HashSet<ExecPos>()
|
||||
|
||||
|
||||
private fun ExecPos.isInvalid() = with(invalidatingInfo) {
|
||||
isInvalid(reactivated)
|
||||
}
|
||||
|
||||
fun onNext(reader: ChunkReader): Collection<Occurrence> {
|
||||
val continued = mutableListOf<Occurrence>()
|
||||
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<Occurrence>) =
|
||||
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 <E> MutableList<E>.top(): E = this.last()
|
||||
private fun <E> MutableList<E>.pop(): E = this.removeAt(this.size - 1)
|
||||
private fun <E> MutableList<E>.push(element: E): Boolean = this.add(element)
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
// 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<MatchJournal.MatchChunk> = PriorityQueue(journalIndex.chunkComparator)
|
||||
|
||||
private val seen = hashSetOf<MatchJournal.Chunk>()
|
||||
|
||||
fun receive(occs: Sequence<Occurrence>): 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<MatchJournal.MatchChunk> {
|
||||
val reevaluated = mutableListOf<MatchJournal.MatchChunk>()
|
||||
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) }
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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<MatchJournal.Chunk>
|
||||
|
|
|
|||
|
|
@ -144,7 +144,7 @@ interface MatchJournal : Iterable<MatchJournal.Chunk>, 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<MatchJournal.Chunk>, 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]
|
||||
*/
|
||||
|
|
|
|||
|
|
@ -392,23 +392,38 @@ internal open class MatchJournalImpl(
|
|||
val last: E get() = if (l is LinkedList<E>) l.last else l.last()
|
||||
}
|
||||
|
||||
private class IndexImpl(chunks: Iterable<Chunk>): MatchJournal.Index
|
||||
private class IndexImpl(chunks: List<Chunk>): MatchJournal.Index
|
||||
{
|
||||
private val chunkOrder = HashMap<Id<Chunk>, Int>()
|
||||
private val occChunks = HashMap<Int, OccChunk>()
|
||||
private val parentMatches = HashMap<OccChunk, MatchChunk>()
|
||||
|
||||
init {
|
||||
chunks.forEachIndexed { index, chunk ->
|
||||
var index: Int = chunks.size
|
||||
val orphansYet = hashSetOf<OccChunk>()
|
||||
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<Chunk> get() = compareBy<Chunk>(this::orderOfThrow)
|
||||
|
||||
|
|
|
|||
|
|
@ -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<Int, UnmodifiableLogicalObserver> = 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<Logical<*>> = 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<Logical<*>> {
|
||||
val unique = hashSetOf<Logical<*>>()
|
||||
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
|
||||
}
|
||||
|
||||
|
||||
|
|
@ -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<Int, LogicalBindObserver> = hashMapOf()
|
||||
private val triggered: HashSet<Int> = 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<Logical<*>> = 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<Logical<*>> {
|
||||
val unique = hashSetOf<Logical<*>>()
|
||||
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
|
||||
}
|
||||
|
|
@ -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<RuleMatchEx>): List<RuleMatchEx>
|
||||
|
||||
/**
|
||||
* 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<RuleMatchEx>): List<RuleMatchEx> = 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<Any>,
|
||||
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<Any> =
|
||||
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,
|
||||
|
|
|
|||
|
|
@ -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<Occurrence>,
|
||||
private val rules: Iterable<Rule>,
|
||||
private val frontState: DispatchingFrontState,
|
||||
val logicalState: LogicalState,
|
||||
val ruleIndex: RuleIndex) : SessionToken
|
||||
private val journalView: MatchJournal.View,
|
||||
private var store: Collection<Occurrence>,
|
||||
private val rules: Iterable<Rule>,
|
||||
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<Rule> = rules
|
||||
|
|
|
|||
|
|
@ -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 <T : Any> 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<Int>("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<Int>("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<Int>("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<Int>("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<Int>("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<Int>("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<Int>("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<Int>("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(
|
||||
|
|
|
|||
Loading…
Reference in New Issue