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.
Grigorii Kirgizov