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

Requires in haskell is LHS #2690

Merged
merged 2 commits into from
Jun 29, 2022
Merged

Requires in haskell is LHS #2690

merged 2 commits into from
Jun 29, 2022

Conversation

radumereuta
Copy link
Contributor

Fixes: #2687

@radumereuta radumereuta requested a review from dwightguth June 28, 2022 21:00
@radumereuta radumereuta self-assigned this Jun 28, 2022
@radumereuta radumereuta requested a review from ehildenb June 28, 2022 21:00
Copy link
Collaborator

@dwightguth dwightguth left a comment

Choose a reason for hiding this comment

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

The change itself seems fine. I'm not sure the code that was there before was correct, but I guess if it's passing the tests it needs to pass, I could be mistaken. I'm just a little confused about whether it's better to treat the requires clause as "left-hand-side and right-hand side", which is what it is currently doing, or "left-hand-side only", which seems more intuitive.

I'm approving though as it seems to pass the test you wrote.

@ehildenb
Copy link
Member

I think the ML encoding is pretty much that requires clause is fully LHS, and ensures is RHS. It's encoded as LHS #And REQ #Implies \next RHS #And ENS if I understand correctly.

That's also how the pyk library treats it when building larger transition system structures like CFGs.

@ehildenb
Copy link
Member

And thank you for the fast turnaround @radumereuta

@rv-jenkins rv-jenkins merged commit 207ff55 into master Jun 29, 2022
@rv-jenkins rv-jenkins deleted the rhsVarsHaskell branch June 29, 2022 03:15
h0nzZik pushed a commit to h0nzZik/k that referenced this pull request Nov 24, 2022
…untimeverification#2038)

* haskell-backend/src/main/native/haskell-backend: 8585c190 - Add class Substitute (runtimeverification#2702)

* haskell-backend/src/main/native/haskell-backend: 4f00fdad5 - Profiles rewrite (runtimeverification#2690)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

[Bug] [kompile] - Reporting a requires clause variable as RHS
4 participants