-
-
Notifications
You must be signed in to change notification settings - Fork 40
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
StratifiedRules: Integer literals #2706
Conversation
Codecov Report
@@ Coverage Diff @@
## main #2706 +/- ##
==========================================
+ Coverage 78.48% 78.50% +0.01%
==========================================
Files 460 461 +1
Lines 15876 15885 +9
Branches 2595 2562 -33
==========================================
+ Hits 12461 12471 +10
+ Misses 3415 3414 -1
... and 1 file with indirect coverage changes 📣 We’re building smart automated test selection to slash your CI/CD build times. Learn more |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nice!
@@ -55,6 +58,8 @@ abstract class RewriterImpl(@unused private val ctx: SolverContext) extends Rewr | |||
case _ => "O@" | |||
} | |||
|
|||
val intValueCache: IntValueCache = new IntValueCache |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I was a bit surprised to see this declaration between function definitions. Is not it a standard practice to put the values and attributes in from of a class definition?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
in the front, i assume
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Code LGTM
I'm concerned though that neither the linked issue nor the current PR description provide context for an uninitiated reader (e.g., a future collaborator, ourselves in 5 years from now, ...) to understand why this PR exists in the first place.
I think these should mention the larger narrative under which these changes are introduced.
@@ -55,6 +58,8 @@ abstract class RewriterImpl(@unused private val ctx: SolverContext) extends Rewr | |||
case _ => "O@" | |||
} | |||
|
|||
val intValueCache: IntValueCache = new IntValueCache |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
in the front, i assume
The issue is part of https://github.com/informalsystems/apalache/milestone/75, and that milestone links back to the relevant ADR. If this is too obscure, I can start adding more context to individual issues, but then you'd likely have the same description literally copy-pasted for each stratified rule. |
If you hadn't told me, I wouldn't have found that. Why not provide a shortcut, for example by linking to the relevant ADR from the PR and/or issue?
Please do. |
make fmt-fix
(or had formatting run automatically on all files edited)./unreleased/
for any new functionalitycloses #2705
In addition, tweaks the interface of
SubstStratifiedRule
, to avoid implementing an unnecessary do-nothing unit method, and adds a previously missingBOOLEAN
set test.