Skip to content
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

Add conversions of num/int/rat/real/word that evaluate expressions using Compute #119

Merged
merged 1 commit into from
Nov 20, 2024

Conversation

aqjune-aws
Copy link
Contributor

This patch adds conversions of num/int/rat/real/word that use the Compute module to evaluate expressions.
They are named *_COMPUTE_CONV and uses the 'weak' reduction (Compute.WEAK_CBV_CONV).
Additionally, an if-then-else expression is configured to be reduced only when the branch is constant.

These new conversions are different from

  • *_RED_CONV because *_RED_CONV cannot recursively traverse subexpression (e.g., NUM_RED_CONV cannot reduce `1 + (2 + 3)`)
  • Also different from *_REDUCE_CONV because *_REDUCE_CONV tries to recursively reduce every subexpression (e.g., `if unknown_cond then 1 + 2 else 3 + 4`, `\x. x + (1 + 2)`).

…ing Compute

This patch adds conversions of num/int/rat/real/word that use the Compute module to
evaluate expressions.
They are named `*_COMPUTE_CONV` and uses the 'weak' reduction (`Compute.WEAK_CBV_CONV`).
Additionally, an if-then-else expression is configured to be reduced only when the branch is constant.

These new conversions are different from

- `*_RED_CONV` because `*_RED_CONV` cannot
  recursively traverse subexpression (e.g., `NUM_RED_CONV` cannot reduce `` `1 + (2 + 3)` ``)
- Also different from `*_REDUCE_CONV` because `*_REDUCE_CONV` tries to
  recursively reduce every subexpression (e.g.,
  `` `if unknown_cond then 1 + 2 else 3 + 4` ``, `` `\x. x + (1 + 2)` ``).

This also makes github workflow fail if any command fails.
@aqjune-aws
Copy link
Contributor Author

I refactored this patch a bit in order to make *_RED_CONV and *_COMPUTE_CONV rely on the same list of (pattern, conversion)s.

@jrh13
Copy link
Owner

jrh13 commented Nov 20, 2024

This is great, thank you! I like the way the xxx_COMPUTE_CONV and the existing xxx_RED_CONV are factored through a common pattern+conversion list. I've tried out a few examples and it all works smoothly, as well as saving a lot of computation in cases where the reduction strategy is more efficient.

@jrh13 jrh13 merged commit 4eef6f6 into jrh13:master Nov 20, 2024
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants