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.
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).
Commit also aligns Observable/Observer interfaces a bit.
Side note: the current role of LogicalState is to only
forward events from Logical to Observers with augmented
information (i.e. providing Controller to handle event).
Problem lies in that journal doesn't track all justifications
for reactivated occurrences. For a parent of such occurrence
its original activating match is considered, while
justifications from the Reactivating match aren't tracked.
So, this information about immediate reactivating parent is lost.
lambdacalc lang typesystem heavily uses reactivation, so it fails.
Now Evidence isn't unique for each Chunk: Occurrence Chunks fully
share evidence and justifications with their activating match.
So, less collections of justifications are created, approx. 2 times less.
Relates to machinery introduced in MPSCR-47.
Previously parent match was maintained in Controller on Java call stack.
Now this stack of parent matches is maintained manually in MatchJournal.
So MatchJournal gains new invariant: parentChunk()
returns correct parent after each logMatch() call.
Several tests fail, also need to maintain this
invariant after logActivation() calls.
Processing a match may fail because of unification went wrong.
To avoid these transient failures to propagate to program trace,
context can optionally abort instead of fail, which is then
recovered from.
Such cases arise when non-principal rules can match on principal occurrences
(for example, capture_Classifier rule in BaseLanguage typesystem).
We don't want to lost justifications provided by these occurrences,
so store them in the nearest relevant chunk --- which is a parent match chunk.
With this the invalidation of the tracked principal occurrences will lead to invalidation
of this relevant match and so to invalidation of any effects produced by non-principal rules,
because they're logged exactly under the chunk of that relevant match.
See tests from previous commits for example.
Such machinery is needed inside ControllerImpl.processBody
to provide nearest relevant match to feedback handling.
Also required for a fix for MPSCR-47.
Also enables back one assertion in incremental processing on rm stage.
Make Occurrence a Justified entity and drop .justifications() from
ConstraintOccurrence.java because justifications are used only internally.
A single justification is now called Evidence (typealias to Int),
so Justified entities are justified by Evidence-s.
In some cases replay could 'overshoot' because the position replayed to was invalidated.
The natural way is to replay to the last descendant of such activated occurrence
and continue execution from here.
Behavior was incorrect in the case of discarding rules.
Several discarding matches could appear on the same occurrence,
beacuase newer incremental matches were inserted before later one,
thus seeing their occurrence as still active and stored.
StateFrameStack adds no functionality but requires too much processing.
Rename StateFrameStack -> LogicalState.
Rename ProcessingStateImpl -> ConstraintsProcessing.
Simplify occurrence's logical observer.
Introduce transient dependency on controller to LogicalState.
Keep logical state as part of session token, avoid re-initializing
all logical observers.
Make replaying of match journal independent of controller.
Introduce a reactive scheme: alpha node has "dependent" nodes which
it can invalidate transitively. Drop block initiates invalidation,
intro block actually drops the nodes.
Instead of just reporting the times each probe has been called,
collect and calculate the actual time taken by each probe location from
the whole backtrace pool.
Grigorii Kirgizov