saw-core: Use named variables for Lambda and Pi binders. #2671
Conversation
brianhuffman
force-pushed
the
bh/no-de-bruijn
branch
4 times, most recently
from
fa53dc4 to
aa1c14c
Compare
|
Apparently there is just a single failure left in the integration test suite: |
brianhuffman
force-pushed
the
bh/no-de-bruijn
branch
from
fb70b29 to
306e78c
Compare
brianhuffman
force-pushed
the
bh/no-de-bruijn
branch
from
306e78c to
1ce9ac2
Compare
brianhuffman
force-pushed
the
bh/no-de-bruijn
branch
3 times, most recently
from
1cec68d to
13b8e59
Compare
This avoids printing let bindings for subterms that are
really only printed once; for example we print
\(x : Vec 4 (Vec 8 Bool)) -> x
instead of
let { x@1 = Vec 4 (Vec 8 Bool)
}
in \(x : x@1) -> x
Previously it didn't get name scoping quite right in cases where the same VarName was shadowed in an inner scope. Also use stAppFreeVars field to implement an optimization.
brianhuffman
force-pushed
the
bh/no-de-bruijn
branch
from
13b8e59 to
afea661
Compare
As a result, many other functions now have pure types, including ones in SAWCore.Rewriter and SAWCore.Term.CtxTerm.
| Lambda _ t1 _ | not doBinders -> [t1] | ||
| Pi _ t1 _ | not doBinders -> [t1] | ||
| Constant{} -> [] | ||
| Variable{} -> [] |
There was a problem hiding this comment.
After some initial confusion I'm on board with this change, but I don't think the commit message accurately describes it. I think it actually avoids printing let bindings for subterms that are never printed, such as Variable types, which I believe is what was happening in test2049. Do you have a different understanding?
There was a problem hiding this comment.
Avoiding the let on terms like \(x : t) -> x was the reason why I created the commit in the first place, and it's what the commit message is based on. I also included the change to test2049 output because I noticed the test failure; I actually don't know why a let was printed on that one in the first place, because by my count there should only have been one occurrence of the type there.
With the switch to named variables, the SolverCache finger- print computed from the external format file no longer respects alpha-equivalence. It should still register cache hits if the same SAW proof script is run more than once.
This PR removes de Bruijn indices from SAWCore, replacing them with named variables in all SAWCore binding constructs. Fixes #2328.