In case evaluation fails and the state of activated occurrences is
reset to some previously stored state, the trace view does not
get updated and contains some stale information. This patch fixes it.
A propagaition rule must ignore reactivated occurrence.
Although it is possible that other occurrences are waiting,
and they can be erroneously selected if precautions are not taken.
The default tell protocol assumes an exception is to be thrown
in case predicate is not satisfied. This may lead to unnecessary
exceptions being thrown in a situation where a simple failure
status would have been sufficient.
Introduce feedback basis to track dependencies on rules.
Index journal chunks by evidence for quick lookup.
The feedback basis is the collection of principal rules tags
from the justifications of the current match.
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)
Rename NonIncrementalProcessing -> DefaultProcessing
Add GroundProcessing as common superclass to handle OccurrenceContractObserver
Add another test for this occurrence contract logic.
Allows to carry logically connected information in one object.
Needed for subsequent changes to ConstraintOccurrence, which
must have better information on source rule: rule template name.
Used by occurrence cache.
CachedOccurrencesProcessing simply activates occurrences
passed to it as input before proceeding with 'main'.
Use it instead of PreambleProcessing (that works with journal).
This should help if 'main' doesn't lead to duplicate activations
of these occurrences. So coderules program must be aware of
occurrence cache and should not include rules for cached occ-s.
Relevant for Incremental strategy.
Allows to more precisely track invalidated types of nodes.
Type of node is invalidated if rules with this origin
were invalidated during incremental processing.
Introduced to discern incremental strategies: Full,Preamble,Default.
because how SessionToken is used and stored depends on it.
EvaluationSessionImpl now simply dispatches to it.
Also rename 'IncrementalProcessing' to 'ProcessingStrategy'.
Incremental algorithm is stricter now in relation to
how it reads MatchJournal and operates on it.
Previously each incremental stage required full traversal.
Now all stages run on each chunk in a single traversal.
Separate journal traversal from incremental logic required for each Chunk.
The test substructuralTS_indirectResourceDependency is not doing what it's intended
to be doing b/c of apparenly wrongly understood contract of the `also()` method.
It is not supposed to pass the result of the computation to the "chained" method.
Compare `T.also(block: (T) -> Unit): T` and `T.let(block: (T) -> R): R`.
After having fixed the code, the test no longer passes.
Previously only logicals directly used ar occurrence args
were observed. Now terms in occurrence args are traversed
recursively and all contained logicals are observed.
Also clear occurrence contract observers on discarding occ-s.
Introduce a generic way to clear observers in LogicalState.
Instead of simple allowed/not option sometimes Unsafe
is useful. 'Unsafe' status may be present when there're
few "bad" rules.
With this level end code may resolve to go with
incrementality without strict guarantees.
It seems to reflect the exact information needed: there's
one-to-one correspondence between feedback and its match.
While using rule unique tag as feedback key in TypesIndex
relied on several assumptions.
Also there's less use of MatchJournal information with this.
Previously parent principal match was passed to FeedbackConsumer.
Matches which discard principal occurrences must be handled specially
on incremental execution. Imagine such match inserted in journal
before other matches with the same occurrence in head.
Because inserted match discards the occurrence, following matches
can't match on it. They must be invalidated. (Relevant for MPSCR-62)
See tests for substructuralTS.
Commit refactors machinery of `dropDiscardingMatchesFor` in
ConstraintsProcessing that was incomplete, as revealed by MPSCR-64.
Relaxes small memory opt introduced in commit a2675351:
Now justifications in Occurrences are not shared with their
activating matches. See JustifiedOccurrenceCreator.
Introduced machinery requires that Occurrences had their own
Evidence (because `dropDiscarding` invalidates by Occurrences).
Previously algorithm was invalidating Chunks only by Evidence
from rule matches, that's why only RuleMatches had to have
unique Evidence, while Occurrences could bear less info.
In short, this change restricts information algo needs from journal.
It restricts how far invalidation stage goes into journal.
Previously it fed ExecQueue with position arbitrarily far in 'past',
whereas now it feeds the closest valid position (the 'present').
Refine interface of RuleMatchEx to use Occurrence,
move one of its function as ext fun (as in TODO).
Fix duplication of extension functions for IncrSpec.
Ensure some contracts in ExecutionQueue.
Some constraints could be missed: those which
are activated and discarded in the same Chunk.
Dispatcher weren't cleared from them
and stale matches could remain in its state.
Through these matches their invalidated heads
could get into incremental execution queue
which led to assert violation in MatchJournalImpl.reset
Fixes IncrClassHierarchy.modifyClsHierarchyTypeParams test.
Key point is that changes to rules causing their
regeneration must be reflected in program.
There appeared to be cases when it's not true.
It's a case of non-principal rules with origins.
Such rules are called "weak principal" rules.
Matches of weak principal rules are not recorded
in Journal (as is for principal rules), but instead
they become part of their parent MatchChunk.
(In essense, tags of weak principal rules are
recorded in parent chunk).
With this, when a weak principal rule changes,
matches of all principal rules whose computation
depends on them are correctly invalidated.
(Example rules: findHierarchy_Classifier)
Relevant for MPSCR-62.
Some time ago "mixed" matches (with both principal and non-principal heads)
were allowed and are handled by Journal. So now principal constraints
can lead to non-principal matches, which renders assert invalid.
(Relevant for MPSCR-62)
DataProvider is an abstract way to associate any data with the
runtime object, such as Supervisor.
Predicate solvers that ought to be stateful may make use of
DataProvider to access the internal state.
Previously it was done twice: at Occurence creation
and in ConstraintsProcessing.processActivated.
Occurrences now constructed in 'dead' state (without observers).
Fedor Isakov