Refactored constraint simplification #276
Conversation
This commit refactors the implementation of subeffecting constraint simplification. The changes can be summarized as follows. - Introduced internal representation of constraints used by the simplification algorithm. - The simplification process is explicitly divided to several rules that can be combined used some combinators represented as higher-order functions. - Irrelevant constraints are recognized. - Added simplification rule: variant variables with no upper-bound are set to the join of their lower bounds. - Added simplification rule: redundant constraints are removed.
There was a problem hiding this comment.
Pull Request Overview
This PR refactors the constraint simplification algorithm for subeffecting constraints, introducing a cleaner internal representation and adding new simplification rules to improve the constraint solving process.
- Introduced internal constraint representation with explicit effect variables and formulas, separating the simplification algorithm into composable rules
- Added new simplification rules: variant variables with no upper-bound are set to the join of lower bounds, and redundant constraints are removed
- Enhanced API with compare functions for type variables and generalizable variables, and added functions to remove variables from effects
Reviewed Changes
Copilot reviewed 5 out of 5 changed files in this pull request and generated 7 comments.
Show a summary per file
| File | Description |
|---|---|
| src/Lang/ConEPriv/TVar.mli | Added compare function for type variables to support ordering |
| src/Lang/ConEPriv/Effct.mli | Added GVar.compare for ordering and remove_tvar/remove_gvar functions for variable removal from effects |
| src/Lang/ConEPriv/Effct.ml | Implemented remove operations for both map types, exposed GVar.Ordered module, and added remove_tvar/remove_gvar effect operations |
| src/Lang/ConE.mli | Exposed new comparison and removal functions in the public API |
| src/EffectInference/ConstrSimplify.ml | Complete refactoring of constraint simplification with new internal representation, expanded state tracking, and four composable simplification rules with proper iteration control |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
There was a problem hiding this comment.
Pull Request Overview
Copilot reviewed 5 out of 5 changed files in this pull request and generated 3 comments.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Foxinio
left a comment
Foxinio
left a comment
There was a problem hiding this comment.
I think this needs minor changes for future programmers reading this code
| let get_gvar eff = | ||
| match T.Effct.view eff with | ||
| | ([], [(gv, p)]) when IncrSAT.Formula.is_true p -> gv | ||
| | _ -> assert false |
There was a problem hiding this comment.
This function seems super unsafe. While I guess it is used correctly and is a nice shorthand wherever it's needed, I have three problems with it.
- It's used in so few places, there it can be replaced with a safer variant.
- If it was to fail, it should provide a better error description than assertion failed.
- While right now I believe it is used correctly, in the future it is bound to be used by someone who doesn't fully understand what it does.
There was a problem hiding this comment.
True. But it don't see how this "safer variant" could look like. To solve this issue, I could write explicitly the invariant maintained in the algorithm that guarantees that all calls to this function are safe. The error message can be improved too.
| | GVar of T.effct | ||
|
|
||
| (** Internal representation of a (normalized) constraint. *) | ||
| type constr = |
There was a problem hiding this comment.
Maybe I would add to documentation of this module, description that normalized constraint is always a relevant one.
There was a problem hiding this comment.
I don't think that this is important. The representation of normalized constraints admits irrelevant constraints, and none of the implemented simplification rules require only relevant constraints on its input. Irrelevant constraints are separated from relevant ones as an optimization, and no other parts of the implementation assumes that this optimization is enabled.
| mutable pgvs : T.GVar.Set.t; | ||
| mutable ngvs : T.GVar.Set.t; | ||
| mutable irr : Constr.t list (** Irrelevant constraints. *) | ||
| { scope : Scope.t; |
There was a problem hiding this comment.
in my opinion this should be called outer_scope, it would be longer to write, but it wouldn't bring up any wrong ideas.
There was a problem hiding this comment.
I disagree. I looked at the code again, and it seems that there is a convention to call the outer scope just scope in all places related to generalization (see for instance Lang.ConE.Type.collect_gvars). However, I can add a few comments that reminds that the scope means "outer scope".
forell
left a comment
forell
left a comment
There was a problem hiding this comment.
I really like the outcome of this refactor. I pointed out one comment that could be clarified, but otherwise I think these changes are good to go.
| [eff], or to [None] if it has multiple upper-bounds, or bounds are not | ||
| clear. Variables that have no upper-bound are not present in the map. *) |
There was a problem hiding this comment.
Before reading the implementation, it's unclear what is meant by "bounds are not clear" in this comment.
Foxinio
left a comment
Foxinio
left a comment
There was a problem hiding this comment.
I'm very happy with how these changes turned out
This PR refactors the implementation of subeffecting constraint simplification. The changes can be summarized as follows.