You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Previously, the `add_equation` logic handled multiple concerns at the
same time in a relatively convoluted way, in part due to the need to
accomodate both basic and advanced meet algorithms in the same code.
With the removal of the basic meet (#3726), we can considerably simplify
the code.
This commit refactors `add_equation` by decomposing it into smaller,
well-defined steps and recognizing that concrete types and aliases need
to be handled differently.
This restructuring clarifies the process of adding an equation:
1. Compute the canonical of the LHS with
`get_canonical_simple_ignoring_name_mode`
2. Check if the type is a concrete type or an alias, which is then
resolved to its current canonical (`add_equation_on_canonical`).
3. If an alias, merge the two canonical simples in the Aliases
structure, then call `record_demotion` to update the typing env,
transferring the existing concrete type from the demoted element to
its new canonical element.
4. If a concrete type, perform the `meet` with the existing concrete
type, then call `replace_concrete_equation` if a more precise
concrete type is found. `replace_concrete_equation` automatically
demotes to a constant instead if the concrete type is a singleton
(without going through `record_demotion`, since we have already
computed the `meet`).
Additionally, `Type_grammar.recover_const_alias` is renamed to
`must_be_singleton`, which better captures its behavior.
Overall, this should be easier to read and maintain. It also facilitates
extensions; for instance, the improved relations tracking for the
match-in-match heuristics will rely on `record_demotion` and
`add_alias_between_canonicals`.
0 commit comments