-
Notifications
You must be signed in to change notification settings - Fork 28
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
Implement fold_into_reduce and reassociate_expr #558
Conversation
Codecov ReportAttention:
❗ Your organization needs to install the Codecov GitHub app to enable full functionality. Additional details and impacted files@@ Coverage Diff @@
## main #558 +/- ##
==========================================
+ Coverage 87.24% 87.26% +0.02%
==========================================
Files 82 82
Lines 19416 19487 +71
==========================================
+ Hits 16939 17006 +67
- Misses 2477 2481 +4 ☔ View full report in Codecov by Sentry. |
I updated the name to Some ideas:
|
They look the same because we simplify the parenthesis. My experience with languages that implements expression rewrites (like Coq) is that you just have to pay attention to these things when using the primitives. Then, you build hammer automations on top of it. |
I agree that we should build automation in the standard library, but at least the primitive definition should be consistent with what it is actually doing. The current documentation writes
which doesn't accurately describe the acceptable program. You could change the documentation to describe the left figure above, but I think it will be hard to write the documentation with syntax that is opaque to users (binop AST). |
We can change it to:
We also need to a better name that signifies what it does. |
Yeah I guess |
This PR implements two operations:
The primary reason behind this PR is being able to put assignments into reduction format which some analysis depends on (e.g. #557).