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

SAW-core translator: lets in lambda bodies #1524

Merged
merged 4 commits into from
Nov 30, 2021

Conversation

eddywestbrook
Copy link
Contributor

It looks like the SAW core to Coq translator had a small bug, where the the translator was not inserting let-bindings for duplicated terms inside the bodies of lambda-abstractions. More specifically, translateTerm was being called to translate the bodies of lambda-abstractions instead of translateTermLet. This was probably just an oversight at some point, as the translator does call translateTermLet on the bodies of pi-abstractions. This PR fixes this issue.

Also addressed in this PR: when the SAW core unit type is translated to Coq, it needs to be explicitly coerced to be a Type, otherwise Coq can sometimes think it needs to be Set, which can cause type errors in weird corner cases. One of these weird corner cases was exposed by the above altered translation of lambda-abstractions, so this PR addresses this problem as well, by adding a new Ascription constructor to the Coq AST type and using it to explicitly ascribe Type to the unit type.

…ings for repeated terms; added a type ascription term to the Coq AST; changed the translation of the unit type to give it an explicit ascription to sort Type rather than Set
@eddywestbrook
Copy link
Contributor Author

Crap, this PR accidentally has some other Heapster stuff in it. I'll parcel those off into their own PR, so this one can just be about the Coq translator.

@eddywestbrook
Copy link
Contributor Author

Ok, the Heapster-related changes have been merged into master now, so the only diffs to look at for this are specifically the Coq translator ones.

@eddywestbrook eddywestbrook added the subsystem: saw-core-coq Issues related to converting saw-core to Gallina for use with the Coq/Rocq theorem prover label Nov 30, 2021
Copy link
Contributor

@brianhuffman brianhuffman left a comment

Choose a reason for hiding this comment

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

Looks good to me.

@eddywestbrook eddywestbrook added the PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run label Nov 30, 2021
@eddywestbrook eddywestbrook merged commit 4bbb352 into master Nov 30, 2021
@mergify mergify bot deleted the saw-core-coq/lets-in-lambda-bodies branch November 30, 2021 22:06
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run subsystem: saw-core-coq Issues related to converting saw-core to Gallina for use with the Coq/Rocq theorem prover
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants