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

Simplify Steel.ST.Reference.with_local without EPushFrame/EPopFrame #276

Open
tahina-pro opened this issue Aug 3, 2022 · 0 comments
Open
Assignees

Comments

@tahina-pro
Copy link
Member

tahina-pro commented Aug 3, 2022

This is a follow-up issue to FStarLang/FStar#2664 .

@msprotz proposed an optimized implementation of Steel.ST.Reference.with_local without the need for anything like EPushFrame/EPopFrame, hoping to avoid unnecessary let res = ... bindings: following our discussion last week, Jonathan told me we shouldn't need push_frame and pop_frame at all, as soon as we could disable some pass in Karamel, except maybe in some cases related to Karamel hoisting a local variable declaration from within a nested if branch up to the beginning of a function.

Thanks Jonathan for your proposed Karamel test patch (FStarLang/FStar#2664 (comment)), I'll test it on my side.

@tahina-pro tahina-pro self-assigned this Aug 3, 2022
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

1 participant