Add conversions of num/int/rat/real/word that evaluate expressions using Compute #119
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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)`
)*_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)`
).