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

Fix the Ord instance for FP and FloatingPoint #701

Merged
merged 2 commits into from
Jun 6, 2024

Conversation

lsrcz
Copy link
Collaborator

@lsrcz lsrcz commented Jun 6, 2024

This pull request fixes the Ord instance for FP and FloatingPoint. The operator (>=) and (<=) will give True when comparing NaNs.

I originally thought that this comes from the underlying libBF library, as I've fixed a bug there yesterday. (GaloisInc/libBF-hs#32). However, after I switch to the fixed version, the bug is still there.

My theory for this bug in the sbv repo is that the instance derived by the compiler may look like this:

a <= b = not $ a > b

And the fix would be manually implementing the operators.

@lsrcz lsrcz added the Bug label Jun 6, 2024
@lsrcz lsrcz requested a review from LeventErkok June 6, 2024 20:43
FP eb0 sb0 v0 < FP eb1 sb1 v1 =
eb0 < eb1 || (eb0 == eb1 && (sb0 < sb1 || (sb0 == sb1 && v0 < v1)))
FP eb0 sb0 v0 <= FP eb1 sb1 v1 =
eb0 < eb1 || (eb0 == eb1 && (sb0 < sb1 || (sb0 == sb1 && v0 <= v1)))
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think we should we throw an error here if (eb0, sb0) /= (eb1, sb1), and if they're equal it should simply compare v0 and v1

My motivation is that if this gets called with a differing sized float, then that's really a type error. (i.e., it should never happen) Don't you think?

Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Also, we should bump libBF dependency to require >= 0.6.8 I suppose.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah that's a good idea. I implemented it like this just because this may be the original semantics, but fixed. Let me update it to throw errors.

For the libBF dependency, its (<) and (<=) are good, so we are able to implement a correct Ord instance even if the dependency is buggy.

@lsrcz
Copy link
Collaborator Author

lsrcz commented Jun 6, 2024

I've updated it to throw errors on comparing different precisions.

@LeventErkok LeventErkok merged commit 5740c01 into LeventErkok:master Jun 6, 2024
2 checks passed
@LeventErkok
Copy link
Owner

Great!

I'll make a stylistic change (I don't like otherwise, my pet peeve), and will bump the libBF dependency.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants