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

Rise's capture avoiding substitution is bugged #164

Open
Bastacyclop opened this issue Apr 27, 2021 · 0 comments
Open

Rise's capture avoiding substitution is bugged #164

Bastacyclop opened this issue Apr 27, 2021 · 0 comments
Labels
bug Something isn't working

Comments

@Bastacyclop
Copy link
Member

Bastacyclop commented Apr 27, 2021

In #145 I found out that our capture-avoiding substitution was bugged. The condition to alpha-rename should be FV(expression) contains x and not FV(b) contains x:

case Lambda(x, b) =>
// See https://www.cs.cornell.edu/courses/cs3110/2019sp/textbook/interp/subst_lambda.html
if (x =~= `for`) return_(e)
// FIXME: should be !(FV(expression) contains x)
if (!(FV(b) contains x))
super.expr(e)
else {
val newX = Identifier(freshName(x.name.substring(0, 1)))(x.t)
val newB = replace.exprInExpr(newX, `for`=x, in=b)
super.expr(Lambda(newX, newB)(e.t))
}

However changing the alpha-renaming condition breaks tests like harrisCornerDetectionHalideCheck and cameraPipelineCheck, indicating another bug in our codebase. My intuition tells me that it could be related to #81, since alpha-renaming more often reduces the risk of having non-unique names.
@michel-steuwer @umazalakain

@Bastacyclop Bastacyclop added the bug Something isn't working label Apr 27, 2021
@Bastacyclop Bastacyclop changed the title Rise substitution alpha-renames too often Rise's capture avoiding substitution is bugged Apr 27, 2021
@Bastacyclop Bastacyclop mentioned this issue May 4, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
None yet
Development

No branches or pull requests

1 participant