Instead of storing information about expression depths in the
solver state (which gets recomputed for salvage) let's track
it directly in constraint system, which also gives solver
access to it when needed e.g. for fixes.
We've been running doxygen with the autobrief option for a couple of
years now. This makes the \brief markers into our comments
redundant. Since they are a visual distraction and we don't want to
encourage more \brief markers in new code either, this patch removes
them all.
Patch produced by
for i in $(git grep -l '\\brief'); do perl -pi -e 's/\\brief //g' $i & done
If sibling components failed, there is no reason to establish new
scope since remaining containers are not really going to be taken
but fail fast instead.
Instead of printing `trying` for type variable and `assuming`
for disjunction choices, unify it so `BindingStep` logs
`attempting {type variable, disjunction choice}`.
Instead of asserting in the solver loop, let's move all of that
logic into `SolverStep::transitionTo(StepState)` and verify state
transition validity there.
Instead of using `TypeChecker` and related APIs directly every time,
let's just abstract it all away to easily check if solver is running
in debug mode and to produce indented logger.
Eagerly check if optimal solution has already been found even if
current binding attempt has failed, because otherwise it might
check too many bindings which would result in ambiguity.
Before this change some of the type variables, especially the ones
that have been previously bound haven't been associated with any
of the component steps, so it had to be done by scope once per step,
but now such recording is done once per split.
Orphaned constraints can be re-introduced to the system by `setup`
of the component, and all of them could be returned back by
`SplitterStep::resume` there so no need to use destructor for that.
Also, orphan constraints have to be registered as regular constraints
by components as well as marked as "orphaned".
Extract choice attempting logic into `DisjunctionStep::attemptChoice`
and start recording taken choices in constraint system when
requested by disjunction.
Execute components with fewer disjunction constraints first,
to make sure that if one of the components fails we do the
smallest amount of work possible.
First of all, let the splitter transfer constraints from inactive
work-list to associated components. Also start tracking components
to reinstate constraints back to constraint system when everything
is done, this allows to execute component steps in any desirable order.
Introduce a notion of `StepState` with some valid transitions,
and split monolithic `take(bool)` into three phases - `setup`, `take`, and
`resume`.
* `setup` - is preliminary state before the step has been taken
for the first time.
* `take` - represents actual logic of the step, results in either
step being done or suspended.
* `resume` - `take` might split steps into smaller ones to make
incremental progress towards the target, which means
that the main step has to be suspended. `resume` is
triggered when all of the "follow-up" steps have been
executed and are "done".
If "split" step produced a single component, there is no reason
to allocate a scope for it and modify constraint system,
because all of the existing type variables and constraints
are related to it anyway, so scope would just end up doing
useless work.
Similar to `DisjunctionStep` `TypeVariableStep` attempts
its choices one-by-one, and if any of the choices match
it makes type variable as a whole successfully solved.
Since type variable attempts choices it means that it
can only produce "split" steps as a follow-up.
`DisjunctionStep` attempts all of the viable choices,
at least one of the choices has to succeed for disjunction
to be considered a success.
`DisjunctionStep` attempts each choice and generates followup
`SplitterStep` to see if applying choice to constraint system
resulted in any simplification.
Failure propagation is crucial for splitter and component steps
because that's the only signal for them to figure out if they
could be completely solved or have to fail.
For example, if one of the component steps created by "split"
fails it would cascade to the rest of the pending component steps
receiving "fail" signal and ultimately result in failure of the
"split" when it's re-taken.
* `SplitterStep` is responsible for running connected components
algorithm to determine how many independent sub-systems there are.
Once that's done it would create one `ComponentStep` per such
sub-system, and move to try to solve each and then merge partial
solutions produced by components into complete solution(s).
* `ComponentStep` represents a set of type variables and related
constraints which could be solved independently. It's further
simplified into "binding" steps which attempt type variable and
disjunction choices.
* "Binding" steps such as `TypeVariableStep` and `DisjunctionStep`
are responsible for trying type binding choices in attempt to
simplify the system and produce a solution. After attempting each
choice they introduce a new "split" step to compute more work.
The idea so to split solving into non-recursive steps,
represented by `SolverStep`, each of the steps is resposible
for a unit of work e.g. attempting type variable or
disjunction bindings/choices.
Each step could produce more work via "follow-up" steps,
complete "partial" solution when it's done, or error which
terminates solver loop.
