Extensional reasoning on Values

[AlecsFerra]

The extensionality flag fails when a function used as argument of a data constructor, take this as an example:

fixpoint "--rewrite"
fixpoint "--allowho"

constant f : (func(0 , [int; int; int]))
define f (x : int, y: int) : int = {(x + y)}

constant g : (func(0 , [int; int; int]))
define g (a : int, b: int) : int = {(b + a)}


data Ty 0 = [
    | Cons {mkCons : func(0 , [int; int; int])}
]

constant Cons : (func(0 , [func(0 , [int; int; int]); Ty]))

expand [1 : True; 2 : True]

constraint:
  env []
  lhs {VV1 : Tuple | true }
  rhs {VV2 : Tuple | (Cons f = Cons g) }
  id 2 tag []

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 of f and g to (\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.

[AlecsFerra]

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 crash: SMTLIB2 respSat = Error "line 3 column 18650: unknown constant lam_arg$35$$35$1" whenever a lambda is used this way in the refinements

This error is already present is not caused by this patch

[nikivazou]

Yes, right now there is no real support for lambdas in LH :)

[AlecsFerra]

Uhm ok then I'm stuck

[AlecsFerra]

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

[AlecsFerra]

I think I fixed the bug regarding lambdas, I'll run the tests on the main repo to double check

[AlecsFerra]

The tests on the liquidhaskell are passing!

But I still have to fix a minor bug for my tests

[facundominguez]

Hello @AlecsFerra. The changes make some sense to me. I contributed some questions and comments.

[AlecsFerra]

Can confirm that it's passing all the test on the main LH repo, now I'm running the benchmarks

[AlecsFerra]

Benchmarks:

On average we are not extremely slower than then original PLE

[facundominguez]

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.

[AlecsFerra]

I will squash the commits at the end

[AlecsFerra]

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

[facundominguez]

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 --etabeta I'd say it is fine to merge. If verification worsens even when not enabling the flags, then I'd prefer to understand why before merging.

[facundominguez]

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?

[AlecsFerra]

I've added a comment in the code

[AlecsFerra]

[facundominguez]

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.

[AlecsFerra]

[AlecsFerra]

Looks way better I guess the slowdowns were actually caused by the elaboration

[facundominguez]

@AlecsFerra, would you like to squash or make other edits ahead of merging?

[facundominguez]

Also, note the comment edits that I just contributed. Feel free to adjust them if you see anything amiss.

[AlecsFerra]

Ops

[AlecsFerra]

Ok now It's ok to merge