Extensional reasoning on Values#705
Conversation
|
The issue on the liquid haskell main repo is related to programs like this: {-@ LIQUID "--reflection" @-}
{-@ LIQUID "--ple" @-}
module Example where
{-@ reflect idu @-}
{-@ idu :: Int -> Int @-}
idu :: Int -> Int
idu x = x
{-@ proof :: {(\x:Int -> x) = idu } @-}
proof = ()As it throws This error is already present is not caused by this patch |
|
Yes, right now there is no real support for lambdas in LH :) |
|
Uhm ok then I'm stuck |
|
Right now It's verifying the example but it's also making some tests in the LH repo fail because it's unfolding some types and inserting lambdas |
|
I think I fixed the bug regarding lambdas, I'll run the tests on the main repo to double check |
|
The tests on the liquidhaskell are passing! But I still have to fix a minor bug for my tests |
facundominguez
left a comment
There was a problem hiding this comment.
Hello @AlecsFerra. The changes make some sense to me. I contributed some questions and comments.
|
Can confirm that it's passing all the test on the main LH repo, now I'm running the benchmarks |
|
Benchmarks: On average we are not extremely slower than then original PLE |
facundominguez
left a comment
There was a problem hiding this comment.
Thanks @AlecsFerra. I added some comments about points I don't understand yet, but your comments helped me progress with my initial questions. Other than these, I guess only some tests would be necessary.
|
I will squash the commits at the end |
|
Following some discussion in private I decided to remove the code relating to make PLE aware of dependent pattern matching / unification The code of the reader monad still passes, the SKI calculus instead will require some extra lemmas |
|
The only open discussion that I could catch is about making a comment more instructive. Update: oh, I asked about a couple other things in comments later. Regarding performance, if the verification times worsen when enabling extensionality and |
| -- Clearly we need the higerorder flag active as we are generating lambda in | ||
| -- the constraints. | ||
| evalApp _γ _ctx e0 es _et | ||
| | ECst (EVar _f) sortAnnotation@FFunc{} <- e0 |
There was a problem hiding this comment.
I just noticed this is relying on ECst while the earlier equations look for the function definition in γ. What is the reason to not do the same here?
There was a problem hiding this comment.
I've added a comment in the code
|
|
| -- get a term annoptated with type `fun(0, [a#foo, a#foo])` | ||
| -- instead of `fun(0, [@foo, @foo])` thus when substituting | ||
| -- the body in a term we could encounter type mismatches. | ||
| newE <- elaborateExpr "EvalApp unfold full: " $ substEq env eq es1 |
There was a problem hiding this comment.
The result of the elaboration is going both into the new equalities and into the rewritten term that is returned. I think only the later is necessary, as it is the only place where ECst will be looked for by evalApp.
|
|
|
Looks way better I guess the slowdowns were actually caused by the elaboration |
cc60b4c to
b49e479
Compare
facundominguez
left a comment
There was a problem hiding this comment.
@AlecsFerra, would you like to squash or make other edits ahead of merging?
|
Also, note the comment edits that I just contributed. Feel free to adjust them if you see anything amiss. |
|
Ops |
|
Ok now It's ok to merge |
The extensionality flag fails when a function used as argument of a data constructor, take this as an example:
it cannot prove that f and g are the same function since it cannot add the
ext$...variable on the functions (and then cause their unfolding by PLE) since they would make the program ill-typed, the solution is eta-expanding the definitions offandgto(\x:Int -> \y:Int -> f x y)(\x:Int -> \y:Int -> g x y)to let PLE then unfold the definitions in the body of the lambda and prove the equality.DO NOT MERGE: This feature is exposing another LF bug in some tests in the liquidhaskell repo related to lambdas in the refinements.