Local rewrites#710
Conversation
facundominguez
left a comment
There was a problem hiding this comment.
It is looking simple enough to me.
Some tests would be needed.
Also, the PR description says this is not implemented for the fq format, but it looks like it is.
| | deANFed <- deANF ctx e0 | ||
| , dropECst deANFed /= dropECst e0 | ||
| = do | ||
| return (Just $ eApps deANFed es, expand) |
There was a problem hiding this comment.
We would need an example of an expression that requires to inline anf bindings to unfold function calls in order to motivate this case.
There was a problem hiding this comment.
The issue is that I don't have a small example but the SKI example without lemmas doesn't pass without unfolding ANFs
There was a problem hiding this comment.
That sounds like we will need to do some debugging to explain why deANF is needed then.
There was a problem hiding this comment.
I suspect that is some bug in the code that does the deANFing because I suppose that ANF expressions shouldn't reach the evaluation loop, also the only other place where is called is in some code that does the REST rewrites
There was a problem hiding this comment.
Yes, REST does need to remove anf bindings, and that use I think I understand.
There was a problem hiding this comment.
SKIDC and the proposal are still passing? I would expect yes since it's a value
There was a problem hiding this comment.
Your tests continue to pass with it.
There was a problem hiding this comment.
I contributed another implementation that calls deANF only once per fork in the trie. It is passing all the tests as well. 2b8411e
In addition, it also explains the situations we have identified so far where ANF bindings interfere with PLE.
There was a problem hiding this comment.
Yeah looks way better
Forgot to update the comment |
|
There is a parser correct? If so, can you also add a small |
Done |
d4ed7a4 to
147f857
Compare
facundominguez
left a comment
There was a problem hiding this comment.
LGTM! Any last changes before merging @AlecsFerra?
|
I think we can merge it |
From the open discussion above, this is the only standing question, but I think it would be fine to handle it in some other PR. |
Following the discussion on #705 the local rewrites features is implemented standalone.
This PR implements proposal 1 of #2371/liquid-haskell
Depends on #2384/liquid-haskell
WIP: at the moment we don't read the local rewrites from
hornfiles.