-
Notifications
You must be signed in to change notification settings - Fork 22
Remove Asrt.Star (fix #159) #316
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
Conversation
|
I think if you fix this problem, it will also fix #301 |
Ah yes interesting you seem to have stumbled upon similar things... When I have more time (🫠) I'll look; what's odd is that the version that works doesn't sort the assertions, so I'm not certain how sorting then (Types>Pure>CorePred>Wand) causes the issue; will update And yes sure I'll rename it to Additional note: running Gillian-JS with this causes a stack overflow so something somewhere isn't tail-recursive anymore... |
|
JS works but something is still odd for Gillian-C, which ends up verifying less branches than it used to, possibly due to ordering issues. Will leave as is for now and maybe come back later to it... |
|
The tests pass which is a miracle but from diffing some of my local tests I get a few mismatches so not ready to merge yet fyi |
|
@giltho @NatKarmios fyi this is ready for review :) After some evaluation, I get:
|
Co-Authored-By: Sacha Ayoun <[email protected]>
NatKarmios
left a comment
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
lgtm :)
|
Looks like the CI failed spuriously because a dependency failed to download? I'll rerun. |

Remove
Asrt.Star; what used to beAsrt.tis nowAsrt.atom(atomic assertions), andAsrt.tis nowatom list, avoiding the need for recursive functions when traversing assertions, and making the distinction much clearer and simpler.Rename
Asrt.GA->Asrt.CorePred