-
Notifications
You must be signed in to change notification settings - Fork 14
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
Remove Asrt.Star (fix #159) #316
base: master
Are you sure you want to change the base?
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]>
Remove
Asrt.Star
; what used to beAsrt.t
is nowAsrt.atom
(atomic assertions), andAsrt.t
is nowatom list
, avoiding the need for recursive functions when traversing assertions, and making the distinction much clearer and simpler.Rename
Asrt.GA
->Asrt.CorePred