3813 add selected hooks for INT, BOOL, MAP, LIST #3828
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
jberthold
commented
Apr 24, 2024
booster/library/Booster/Builtin.hs
Outdated
Comment on lines
195
to
200
| intTerm :: Integer -> Term | ||
| intTerm = DomainValue SortInt . pack . show | ||
|
|
||
| readIntTerm :: Term -> Maybe Integer | ||
| readIntTerm (DomainValue SortInt val) = readMaybe (unpack val) | ||
| readIntTerm _other = Nothing |
There was a problem hiding this comment.
Obviously these hooks would be faster if we had an internal type holding an Integer, instead of reading and showing the values for every operation.
Currently the IMP-sum-to-n test is still 30% faster with the LLVM backend than it is without.
|
A tiny bit of slowdown in KEVM (if not measurement noise)
|
|
With one more (previously-missing) hook
Results for MX Backend are showing improvements:
(The |
jberthold
force-pushed
the
3813-map-update-hook-and-hook-refactoring
branch
from
503e19d to
34a5867
Compare
Update the key-value association of an internal `KMap` with a new value if the key is (syntactically) present (assumes bottom-up evaluation). Otherwise: * If the map has an opaque part, no result is returned; * If the map has unevaluated key data, no result is returned; * Otherwise, the key is certain to be absent in the map. A new association pair is added to the list
jberthold
force-pushed
the
3813-map-update-hook-and-hook-refactoring
branch
from
34a5867 to
e095e9c
Compare
jberthold
force-pushed
the
3813-map-update-hook-and-hook-refactoring
branch
from
92e7232 to
e86bae4
Compare
geo2a
reviewed
Apr 30, 2024
| @@ -2,88 +2,6 @@ | |||
| {"tag":"simplification","result":{"tag":"success","rule-id":"f310443b160236f56d095576a7500c11d1e98ee7af349b0bbf7a34b5e444d300"},"origin":"booster"} | |||
| {"tag":"simplification","result":{"tag":"failure","reason":"RuleNotPreservingDefinedness","rule-id":"3b51b2998e8ebe79b88550ea9d27ca95003744019b16b93d17a55f6f9bcaa12a"},"origin":"booster"} | |||
| {"tag":"simplification","result":{"tag":"failure","reason":"RuleNotPreservingDefinedness","rule-id":"1170b8c2f6d770eecb12b2ffb28275ed94ae1451d0ae3f2b42e570cd198099fa"},"origin":"booster"} | |||
| {"tag":"simplification","result":{"tag":"failure","reason":"Failed match","rule-id":"c2682318552299808618ea1106c22cf9df82485521eaf5e58844a16e0d4550e4"},"origin":"booster"} | |||
There was a problem hiding this comment.
Am I right to understand that we are evaluating certain things with the hooks, whereas before we attempted to apply rules from domains.md?
There was a problem hiding this comment.
Correct, the hook is tried first (if one exists), and if the hook returns a result, no equations are tried.
|
|
…k-and-hook-refactoring
Comment on lines
+76
to
+78
| readIntTerm :: Term -> Maybe Integer | ||
| readIntTerm (DomainValue SortInt val) = readMaybe (unpack val) | ||
| readIntTerm _other = Nothing |
There was a problem hiding this comment.
definitely not the scope of this PR, but perhaps we should make an issue about making ints an internalised value?
There was a problem hiding this comment.
#3848 created to track this
jberthold
commented
May 2, 2024
geo2a
approved these changes
May 2, 2024
|
Re-tested with latest version of
|
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Context: #3813
Adds a number of hooks (as per documentation in https://github.com/runtimeverification/haskell-backend/blob/master/docs/hooks.md) and splits the
Booster.Builtinmodule into several parts.Bool: all hooked operations implementedInt: selected binary and unary operations and comparisonsList:get(indexing) andsizeMap: all hooked operations exceptremoveAllandkeys(which would require using internal sets)