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 Value.compare #210

Open
filipeom opened this issue Sep 11, 2024 · 2 comments
Open

Fix Value.compare #210

filipeom opened this issue Sep 11, 2024 · 2 comments

Comments

@filipeom
Copy link
Member

No description provided.

@hra687261
Copy link
Contributor

Can you give more details on what the issue with it is?

@filipeom
Copy link
Member Author

filipeom commented Sep 16, 2024

Yes of course. In Value.compare the case when two values are not of the same type is undefined and just does: assert false.

smtml/src/ast/value.ml

Lines 46 to 49 in 30dc99f

| ( ( True | False | Unit | Int _ | Real _ | Str _ | Num _ | List _ | App _
| Nothing )
, _ ) ->
assert false

This isn't a massive issue because we don't have a Expr.compare yet. But even if we had to have an Expr.compare we we could just use the hash-consing tags to provide a total ordering.

But in any case, the function is wrong and we should fix it at some point.

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

No branches or pull requests

2 participants