human-friendly equations from PLE #569

facundominguez · 2022-05-16T13:48:27Z

Fixes #500

The equations produced by PLE are smaller and fewer. No benchmark worsens, some benchmarks improve, and the regular PLE catches up with the interpreted PLE speed ups.

Major changes in this PR:

Remove the surrounding context of unfoldings. This is point (4) in the description of A plan for optimizing PLE #500. Unexpected: Had to figure out how to deal with lambda expressions so I preserve the bindings.
Unfold equations only if any of the guards can really be reduced. This reduces equations drastically, since no nested if-then-else appear, only the results of reducing them. But it requires to refine proofs sometimes to do a case on inputs.
Separated selectors and constructor tests from the other measures, as the smt solver already knows about them. They are used for rewriting candidate expressions, but otherwise produce no unfolding equations themselves.
Have PLE and REST work with elaborated terms, where explicit casts appear to instantiate type variables. This allows to tell the smt solver what instantiation of polymorphic variables is needed by a proof.
Originally this PR unfolded measures as if they were reflected functions when the measure appears applied to an expression which isn't a constructor application. But we discovered that this worsened a benchmark. See Tame the dissemination of measure equations in constraints liquidhaskell#2005.
Iterate over the same candidates over an over, instead of producing new candidates on every iteration. This simplifies the PLE loop, which doesn't need to manage a dynamic list of candidates.
Treat variables as special cases of application. This condenses the code responsible for unfoldings in fewer places, and removes initialization logic related to measures and reflected functions without arguments.

facundominguez · 2022-05-16T13:56:49Z

The accompanying LH branch is ucsd-progsys/liquidhaskell@develop...facundominguez:fd/ple-opts2
It disables the expression interpreter which worsens performance since the regular PLE produces fewer and smaller equations.

I still keep this PR as draft because I have to address the missing test constructors when unfolding measures as reflected functions. This impairs my ability to verify stitch-lh for instance, and worsens the experience for users in general. I thought of making the PR, anyway, because it changes a lot of things, and it can use a review already. I'm rather confident that the remaining work won't need to rewrite these patches unless the review uncovers serious flaws. All tests should pass except for stitch-lh.

Update: I have solutions for the above issues in the branch for Liquid Haskell, so I have promoted this PR from the draft status.

ranjitjhala · 2022-05-16T14:01:46Z

Wow this is awesome! Let me know if you want to chat to go over whatever is missing/ needs to be fixed.

…

On Mon, May 16, 2022 at 6:57 AM Facundo Domínguez ***@***.***> wrote: The accompanying LH branch is ucsd-progsys/liquidhaskell@ develop...facundominguez:fd/ple-opts2 <https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquidhaskell_compare_develop...facundominguez-3Afd_ple-2Dopts2&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=ytb6oAc8STuCToF1DJEkLL8fiXmv0jfGoae2ByFoAbjYmy5gG1icyCYdX6PV2S8m&s=GA6RhZpmoNBFmKfujWgQ6U8JwOAPXU_6q7aRAI8lr-Y&e=> It disables the expression interpreter which worsens performance since the regular PLE produces fewer and smaller equations. I still keep this PR as draft because I have to address the missing test constructors when unfolding measures as reflected functions. This impairs my ability to verify stitch-lh for instance, and worsens the experience for users in general. I thought of making the PR, anyway, because it changes a lot of things, and it can use a review already. I'm rather confident that the remaining work won't need to rewrite these patches unless the review uncovers serious flaws. All tests should pass except for stitch-lh. — Reply to this email directly, view it on GitHub <https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquid-2Dfixpoint_pull_569-23issuecomment-2D1127709071&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=ytb6oAc8STuCToF1DJEkLL8fiXmv0jfGoae2ByFoAbjYmy5gG1icyCYdX6PV2S8m&s=mvT96gxw9gX_9CDOtQrH9kUejEHMBCdFeBwyGfXBsK8&e=>, or unsubscribe <https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_notifications_unsubscribe-2Dauth_AAMS4ODM5SETVO4P2R6OUSLVKJH3FANCNFSM5WBRXG3Q&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=ytb6oAc8STuCToF1DJEkLL8fiXmv0jfGoae2ByFoAbjYmy5gG1icyCYdX6PV2S8m&s=c0LjhlicpRrstpOLleHapWwlVtTzF8YjKY-h5lYSAJg&e=> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

facundominguez · 2022-05-18T12:19:27Z

Here is an example of the produced equalities. In tests/pos/Rest.hs there is a function

{-@
rewriteWith aClosedExpIsValidInAnyContext [appendLengh]
aClosedExpIsValidInAnyContext
  :: ctx0 : List Ty
  -> ctx1 : List Ty
  -> e : Exp
  -> { WellTyped e ctx0 <=>
       WellTyped e (append ctx0 ctx1) && numFreeVarsExp e <= length ctx0
     }
@-}
aClosedExpIsValidInAnyContext :: List Ty -> List Ty -> Exp -> Proof
aClosedExpIsValidInAnyContext ctx0 ctx1 e = case e of
  Var _ i ->
    if i < length ctx0 then elemAtThroughAppend i ctx0 ctx1
    else trivial
  Lam ty body ->
    aClosedExpIsValidInAnyContext (Cons ty ctx0) ctx1 body
  App e1 e2 ->
    aClosedExpIsValidInAnyContext ctx0 ctx1 e1 ? aClosedExpIsValidInAnyContext ctx0 ctx1 e2
  Let e1 e2 ->
    aClosedExpIsValidInAnyContext ctx0 ctx1 e1 ? aClosedExpIsValidInAnyContext (Cons (exprType e1) ctx0) ctx1 e2
  Arith e1 _ e2 ->
    aClosedExpIsValidInAnyContext ctx0 ctx1 e1 ? aClosedExpIsValidInAnyContext ctx0 ctx1 e2
  Cond e1 e2 e3 ->
    aClosedExpIsValidInAnyContext ctx0 ctx1 e1
      ? aClosedExpIsValidInAnyContext ctx0 ctx1 e2
      ? aClosedExpIsValidInAnyContext ctx0 ctx1 e3
  Fix body ->
    aClosedExpIsValidInAnyContext ctx0 ctx1 body
  IntE _ -> trivial
  BoolE _ -> trivial

This is proving that we can extend the environment of lambda expressions in de bruijn notation, and still preserve "closedness".

With this PR, in the last branch of the case

  ...
  BoolE _ -> trivial

PLE produces 18 equalities:

  ((Rest.length (Rest.append ctx0##a8it ctx1##a8iu)) =
     ((Rest.length ctx0##a8it) + (Rest.length ctx1##a8iu)))
  
  ((Rest.checkBindings (Rest.append ctx0##a8it ctx1##a8iu) e##a8iv) =
     true)
  
  ((Rest.checkBindings ctx0##a8it e##a8iv) = true)
  
  ((Rest.arithType Rest.Divide) = Rest.TInt)
  
  ((Rest.arithType Rest.Equals) = Rest.TBool)
  
  ((Rest.arithType Rest.Greater) = Rest.TBool)
  
  ((Rest.arithType Rest.GreaterE) = Rest.TBool)
  
  ((Rest.arithType Rest.Less) = Rest.TBool)
  
  ((Rest.arithType Rest.LessE) = Rest.TBool)
  
  ((Rest.arithType Rest.Minus) = Rest.TInt)
  
  ((Rest.arithType Rest.Mod) = Rest.TInt)
  
  ((Rest.arithType Rest.Plus) = Rest.TInt)
  
  ((Rest.arithType Rest.Times) = Rest.TInt)
  
  ((Rest.exprType e##a8iv) = Rest.TBool)
  
  ((Rest.isFunTy Rest.TBool) = false)
  
  ((Rest.isFunTy Rest.TInt) = false)
  
  ((Rest.numFreeVarsExp e##a8iv) = 0)
  
  (((Rest.length ctx0##a8it) + (Rest.length ctx1##a8iu)) =
     (Rest.length (Rest.append ctx0##a8it ctx1##a8iu)))

And this is close to the size of the equality set produced for every other branch in the function.

Without this PR, we get instead:

  ((Rest.arithType Rest.Divide) = Rest.TInt)
  
  ((Rest.arithType Rest.Equals) = Rest.TBool)
 
  ...

  ((is$Rest.App (Rest.BoolE ds_d1b8H)) = false)
  
  ((is$Rest.Arith (Rest.BoolE ds_d1b8H)) = false)
  
  ((is$Rest.BoolE (Rest.BoolE ds_d1b8H)) = true)
  
  ((is$Rest.Cond (Rest.BoolE ds_d1b8H)) = false)
  
  ((is$Rest.Cons Rest.Nil) = false)
  
  ((is$Rest.Divide Rest.Divide) = true)
  
  ((is$Rest.Divide Rest.Equals) = false)
  
  ((is$Rest.Divide Rest.Greater) = false)
  
  ((is$Rest.Divide Rest.GreaterE) = false)
  
  ...

  ((is$Rest.Greater Rest.Divide) = false)
  
  ((is$Rest.Greater Rest.Equals) = false)
  
  ((is$Rest.Greater Rest.Greater) = true)
  
  ((is$Rest.Greater Rest.GreaterE) = false)

  ...

  ... all combinations of is$some.operator another_operator

  ((Rest.append ctx0##a1aR1 ctx1##a1aR2) =
     (if (is$Rest.Cons ctx0##a1aR1) then
        (Rest.Cons (Rest.Cons##lqdc##$select##Rest.Cons##1 ctx0##a1aR1) (Rest.append (Rest.Cons##lqdc##$select##Rest.Cons##2 ctx0##a1aR1) ctx1##a1aR2))
      else
        ctx1##a1aR2))
  
  ((Rest.checkBindings ctx0##a1aR1 e##a1aR3) = true)
  
  ((Rest.checkBindings (Rest.append ctx0##a1aR1 ctx1##a1aR2) e##a1aR3) =
     (Rest.checkBindings (if (is$Rest.Cons ctx0##a1aR1) then
                            (Rest.Cons (Rest.Cons##lqdc##$select##Rest.Cons##1 ctx0##a1aR1) (Rest.append (Rest.Cons##lqdc##$select##Rest.Cons##2 ctx0##a1aR1) ctx1##a1aR2))
                          else
                            ctx1##a1aR2) e##a1aR3))
  
  ((Rest.checkBindings (if (is$Rest.Cons ctx0##a1aR1) then
                          (Rest.Cons (Rest.Cons##lqdc##$select##Rest.Cons##1 ctx0##a1aR1) (Rest.append (Rest.Cons##lqdc##$select##Rest.Cons##2 ctx0##a1aR1) ctx1##a1aR2))
                        else
                          ctx1##a1aR2) e##a1aR3) =
     true)
  
  ((if (is$Rest.App e##a1aR3) then
      && [(Rest.checkBindings ctx0##a1aR1 (Rest.e1 e##a1aR3));
          (Rest.checkBindings ctx0##a1aR1 (lqdc##$select##Rest.App##1 e##a1aR3))]
    else
      (if (is$Rest.Let e##a1aR3) then
         && [(Rest.checkBindings ctx0##a1aR1 (lqdc##$select##Rest.Let##2 e##a1aR3));
             (Rest.checkBindings (Rest.Cons (Rest.exprType (lqdc##$select##Rest.Let##2 e##a1aR3)) ctx0##a1aR1) (lqdc##$select##Rest.Let##1 e##a1aR3))]
       else
         (if (is$Rest.Arith e##a1aR3) then
            && [(Rest.checkBindings ctx0##a1aR1 (lqdc##$select##Rest.Arith##3 e##a1aR3));
                (Rest.checkBindings ctx0##a1aR1 (lqdc##$select##Rest.Arith##1 e##a1aR3))]
          else
            (if (is$Rest.Cond e##a1aR3) then
               && [(Rest.checkBindings ctx0##a1aR1 (lqdc##$select##Rest.Cond##3 e##a1aR3));
                   && [(Rest.checkBindings ctx0##a1aR1 (Rest.a e##a1aR3));
                       (Rest.checkBindings ctx0##a1aR1 (lqdc##$select##Rest.Cond##1 e##a1aR3))]]
             else
               (if (is$Rest.Fix e##a1aR3) then
                  (Rest.checkBindings ctx0##a1aR1 (lqdc##$select##Rest.Fix##1 e##a1aR3))
                else
                  (if (is$Rest.IntE e##a1aR3) then true else true)))))) =
     (if (is$Rest.Let e##a1aR3) then
        && [(Rest.checkBindings ctx0##a1aR1 (lqdc##$select##Rest.Let##2 e##a1aR3));
            (Rest.checkBindings (Rest.Cons (Rest.exprType (lqdc##$select##Rest.Let##2 e##a1aR3)) ctx0##a1aR1) (lqdc##$select##Rest.Let##1 e##a1aR3))]
      else
        (if (is$Rest.Arith e##a1aR3) then
           && [(Rest.checkBindings ctx0##a1aR1 (lqdc##$select##Rest.Arith##3 e##a1aR3));
               (Rest.checkBindings ctx0##a1aR1 (lqdc##$select##Rest.Arith##1 e##a1aR3))]
         else
           (if (is$Rest.Cond e##a1aR3) then
              && [(Rest.checkBindings ctx0##a1aR1 (lqdc##$select##Rest.Cond##3 e##a1aR3));
                  && [(Rest.checkBindings ctx0##a1aR1 (Rest.a e##a1aR3));
                      (Rest.checkBindings ctx0##a1aR1 (lqdc##$select##Rest.Cond##1 e##a1aR3))]]
            else
              (if (is$Rest.Fix e##a1aR3) then
                 (Rest.checkBindings ctx0##a1aR1 (lqdc##$select##Rest.Fix##1 e##a1aR3))
               else
                 (if (is$Rest.IntE e##a1aR3) then true else true))))))
  
  ((if (is$Rest.App e##a1aR3) then
      && [(Rest.checkBindings (if (is$Rest.Cons ctx0##a1aR1) then
                                 (Rest.Cons (Rest.Cons##lqdc##$select##Rest.Cons##1 ctx0##a1aR1) (Rest.append (Rest.Cons##lqdc##$select##Rest.Cons##2 ctx0##a1aR1) ctx1##a1aR2))
                               else
                                 ctx1##a1aR2) (Rest.e1 e##a1aR3));
          (Rest.checkBindings (if (is$Rest.Cons ctx0##a1aR1) then
                                 (Rest.Cons (Rest.Cons##lqdc##$select##Rest.Cons##1 ctx0##a1aR1) (Rest.append (Rest.Cons##lqdc##$select##Rest.Cons##2 ctx0##a1aR1) ctx1##a1aR2))
                               else
                                 ctx1##a1aR2) (lqdc##$select##Rest.App##1 e##a1aR3))]
    else
      (if (is$Rest.Let e##a1aR3) then
         && [(Rest.checkBindings (if (is$Rest.Cons ctx0##a1aR1) then
                                    (Rest.Cons (Rest.Cons##lqdc##$select##Rest.Cons##1 ctx0##a1aR1) (Rest.append (Rest.Cons##lqdc##$select##Rest.Cons##2 ctx0##a1aR1) ctx1##a1aR2))
                                  else
                                    ctx1##a1aR2) (lqdc##$select##Rest.Let##2 e##a1aR3));
             (Rest.checkBindings (Rest.Cons (Rest.exprType (lqdc##$select##Rest.Let##2 e##a1aR3)) (if (is$Rest.Cons ctx0##a1aR1) then
                                                                                                     (Rest.Cons (Rest.Cons##lqdc##$select##Rest.Cons##1 ctx0##a1aR1) (Rest.append (Rest.Cons##lqdc##$select##Rest.Cons##2 ctx0##a1aR1) ctx1##a1aR2))
                                                                                                   else
                                                                                                     ctx1##a1aR2)) (lqdc##$select##Rest.Let##1 e##a1aR3))]
       else
         (if (is$Rest.Arith e##a1aR3) then
            && [(Rest.checkBindings (if (is$Rest.Cons ctx0##a1aR1) then
                                       (Rest.Cons (Rest.Cons##lqdc##$select##Rest.Cons##1 ctx0##a1aR1) (Rest.append (Rest.Cons##lqdc##$select##Rest.Cons##2 ctx0##a1aR1) ctx1##a1aR2))
                                     else
                                       ctx1##a1aR2) (lqdc##$select##Rest.Arith##3 e##a1aR3));
                (Rest.checkBindings (if (is$Rest.Cons ctx0##a1aR1) then
                                       (Rest.Cons (Rest.Cons##lqdc##$select##Rest.Cons##1 ctx0##a1aR1) (Rest.append (Rest.Cons##lqdc##$select##Rest.Cons##2 ctx0##a1aR1) ctx1##a1aR2))
                                     else
                                       ctx1##a1aR2) (lqdc##$select##Rest.Arith##1 e##a1aR3))]
          else
            (if (is$Rest.Cond e##a1aR3) then
               && [(Rest.checkBindings (if (is$Rest.Cons ctx0##a1aR1) then
                                          (Rest.Cons (Rest.Cons##lqdc##$select##Rest.Cons##1 ctx0##a1aR1) (Rest.append (Rest.Cons##lqdc##$select##Rest.Cons##2 ctx0##a1aR1) ctx1##a1aR2))
                                        else
                                          ctx1##a1aR2) (lqdc##$select##Rest.Cond##3 e##a1aR3));
                   && [(Rest.checkBindings (if (is$Rest.Cons ctx0##a1aR1) then
                                              (Rest.Cons (Rest.Cons##lqdc##$select##Rest.Cons##1 ctx0##a1aR1) (Rest.append (Rest.Cons##lqdc##$select##Rest.Cons##2 ctx0##a1aR1) ctx1##a1aR2))
                                            else
                                              ctx1##a1aR2) (Rest.a e##a1aR3));
                       (Rest.checkBindings (if (is$Rest.Cons ctx0##a1aR1) then
                                              (Rest.Cons (Rest.Cons##lqdc##$select##Rest.Cons##1 ctx0##a1aR1) (Rest.append (Rest.Cons##lqdc##$select##Rest.Cons##2 ctx0##a1aR1) ctx1##a1aR2))
                                            else
                                              ctx1##a1aR2) (lqdc##$select##Rest.Cond##1 e##a1aR3))]]
             else
               (if (is$Rest.Fix e##a1aR3) then
                  (Rest.checkBindings (if (is$Rest.Cons ctx0##a1aR1) then
                                         (Rest.Cons (Rest.Cons##lqdc##$select##Rest.Cons##1 ctx0##a1aR1) (Rest.append (Rest.Cons##lqdc##$select##Rest.Cons##2 ctx0##a1aR1) ctx1##a1aR2))
                                       else
                                         ctx1##a1aR2) (lqdc##$select##Rest.Fix##1 e##a1aR3))
                else
                  (if (is$Rest.IntE e##a1aR3) then true else true)))))) =
     (if (is$Rest.Let e##a1aR3) then
        && [(Rest.checkBindings (if (is$Rest.Cons ctx0##a1aR1) then
                                   (Rest.Cons (Rest.Cons##lqdc##$select##Rest.Cons##1 ctx0##a1aR1) (Rest.append (Rest.Cons##lqdc##$select##Rest.Cons##2 ctx0##a1aR1) ctx1##a1aR2))
                                 else
                                   ctx1##a1aR2) (lqdc##$select##Rest.Let##2 e##a1aR3));
            (Rest.checkBindings (Rest.Cons (Rest.exprType (lqdc##$select##Rest.Let##2 e##a1aR3)) (if (is$Rest.Cons ctx0##a1aR1) then
                                                                                                    (Rest.Cons (Rest.Cons##lqdc##$select##Rest.Cons##1 ctx0##a1aR1) (Rest.append (Rest.Cons##lqdc##$select##Rest.Cons##2 ctx0##a1aR1) ctx1##a1aR2))
                                                                                                  else
                                                                                                    ctx1##a1aR2)) (lqdc##$select##Rest.Let##1 e##a1aR3))]
      else
        (if (is$Rest.Arith e##a1aR3) then
           && [(Rest.checkBindings (if (is$Rest.Cons ctx0##a1aR1) then
                                      (Rest.Cons (Rest.Cons##lqdc##$select##Rest.Cons##1 ctx0##a1aR1) (Rest.append (Rest.Cons##lqdc##$select##Rest.Cons##2 ctx0##a1aR1) ctx1##a1aR2))
                                    else
                                      ctx1##a1aR2) (lqdc##$select##Rest.Arith##3 e##a1aR3));
               (Rest.checkBindings (if (is$Rest.Cons ctx0##a1aR1) then
                                      (Rest.Cons (Rest.Cons##lqdc##$select##Rest.Cons##1 ctx0##a1aR1) (Rest.append (Rest.Cons##lqdc##$select##Rest.Cons##2 ctx0##a1aR1) ctx1##a1aR2))
                                    else
                                      ctx1##a1aR2) (lqdc##$select##Rest.Arith##1 e##a1aR3))]
         else
           (if (is$Rest.Cond e##a1aR3) then
              && [(Rest.checkBindings (if (is$Rest.Cons ctx0##a1aR1) then
                                         (Rest.Cons (Rest.Cons##lqdc##$select##Rest.Cons##1 ctx0##a1aR1) (Rest.append (Rest.Cons##lqdc##$select##Rest.Cons##2 ctx0##a1aR1) ctx1##a1aR2))
                                       else
                                         ctx1##a1aR2) (lqdc##$select##Rest.Cond##3 e##a1aR3));
                  && [(Rest.checkBindings (if (is$Rest.Cons ctx0##a1aR1) then
                                             (Rest.Cons (Rest.Cons##lqdc##$select##Rest.Cons##1 ctx0##a1aR1) (Rest.append (Rest.Cons##lqdc##$select##Rest.Cons##2 ctx0##a1aR1) ctx1##a1aR2))
                                           else
                                             ctx1##a1aR2) (Rest.a e##a1aR3));
                      (Rest.checkBindings (if (is$Rest.Cons ctx0##a1aR1) then
                                             (Rest.Cons (Rest.Cons##lqdc##$select##Rest.Cons##1 ctx0##a1aR1) (Rest.append (Rest.Cons##lqdc##$select##Rest.Cons##2 ctx0##a1aR1) ctx1##a1aR2))
                                           else
                                             ctx1##a1aR2) (lqdc##$select##Rest.Cond##1 e##a1aR3))]]
            else
              (if (is$Rest.Fix e##a1aR3) then
                 (Rest.checkBindings (if (is$Rest.Cons ctx0##a1aR1) then
                                        (Rest.Cons (Rest.Cons##lqdc##$select##Rest.Cons##1 ctx0##a1aR1) (Rest.append (Rest.Cons##lqdc##$select##Rest.Cons##2 ctx0##a1aR1) ctx1##a1aR2))
                                      else
                                        ctx1##a1aR2) (lqdc##$select##Rest.Fix##1 e##a1aR3))
               else
                 (if (is$Rest.IntE e##a1aR3) then true else true))))))
 
  ... a thousand more lines of equations like the above, 1300 lines in total.

Avoiding the use of rewriteWith gets the output down to a hundred equations which are small. But PLE still blows up to 1500 lines in other branches (like the Let branch).

facundominguez · 2022-05-24T17:52:03Z

This is ready for review and eventually merging. At least I think I have solutions for the remaining integration issues with LH. I'll work on solving the merge conflicts after review.

facundominguez · 2022-06-07T22:05:08Z

I rebased develop and reverted back to the old way of handling measures, after the discussions in slack that motivated ucsd-progsys/liquidhaskell#2005. There are some tests failing now in LH that I have to fix.

…ructor

facundominguez · 2022-06-11T00:25:29Z

I tested safe-coupling, it took 114s before this change, and 65 seconds after.
This is the branch before the change, and this is the branch after the change.

I need to look a liquidmeta next.

facundominguez · 2022-06-12T22:18:43Z

I tried liquidmeta. There are two commits here. The first commit updates LH to develop, and the second commit updates LH to this branch.

Unfortunately, develop already takes more time to verify than I'm willing to find out. I let it run for six hours, and it was still trying to verify the 26th module of 35. However, I did measure the 25 earlier modules. With develop they took 17 minutes to verify, with this branch, it took 14 minutes. The 26th module seems to take forever resolving liquid variables before calling PLE.

liquidmeta       > build (lib)
liquidmeta       > Preprocessing library for liquidmeta-0.0.0..
liquidmeta       > Building library for liquidmeta-0.0.0..
liquidmeta       > [ 1 of 35] Compiling Basics
liquidmeta       > [ 2 of 35] Compiling LocalClosure
liquidmeta       > [ 3 of 35] Compiling Semantics
liquidmeta       > [ 4 of 35] Compiling Strengthenings
liquidmeta       > [ 5 of 35] Compiling BasicPropsSubstitution
liquidmeta       > [ 6 of 35] Compiling SystemFWellFormedness
liquidmeta       > [ 7 of 35] Compiling SystemFTyping
liquidmeta       > [ 8 of 35] Compiling PrimitivesFTyping
liquidmeta       > [ 9 of 35] Compiling BasicPropsEnvironments
liquidmeta       > [10 of 35] Compiling WellFormedness
liquidmeta       > [11 of 35] Compiling Typing
liquidmeta       > [12 of 35] Compiling PrimitivesWFType
liquidmeta       > [13 of 35] Compiling BasicPropsWellFormedness
liquidmeta       > [14 of 35] Compiling SystemFLemmasWellFormedness
liquidmeta       > [15 of 35] Compiling SystemFLemmasWeaken
liquidmeta       > [16 of 35] Compiling LemmasWeakenWF
liquidmeta       > [17 of 35] Compiling LemmasWeakenWFTV
liquidmeta       > [18 of 35] Compiling LemmasWeakenTyp
liquidmeta       > [19 of 35] Compiling LemmasWeakenTypTV
liquidmeta       > [20 of 35] Compiling SystemFLemmasSubstitution
liquidmeta       > [21 of 35] Compiling SystemFSoundness
liquidmeta       > [22 of 35] Compiling SubstitutionLemmaWF
liquidmeta       > [23 of 35] Compiling LemmasWellFormedness
liquidmeta       > [24 of 35] Compiling SubstitutionLemmaWFTV
liquidmeta       > [25 of 35] Compiling LemmasTyping
liquidmeta       > [26 of 35] Compiling LemmasSubtyping
...

facundominguez · 2022-06-13T00:42:33Z

Here is the last comparison of tests.

The only miscarriaged value is ReWrite8 which gets a few seconds slower. I think it is because it causes REST to do some more work, and there is much to optimize in REST still.

facundominguez · 2022-06-13T01:43:22Z

@niki, @ranjitjhala, I think this is good to merge. But please, let me know if we need to do anything else in advance.

facundominguez · 2022-06-14T00:16:07Z

I updated the chart comparing test measures. It has the same results, but the formatting is no longer screwed.

facundominguez changed the title ~~human-like equations for PLE~~ human-readable equations from PLE May 16, 2022

facundominguez changed the title ~~human-readable equations from PLE~~ human-friendly equations from PLE May 16, 2022

facundominguez force-pushed the fd/ple-opts2-rebased branch from b895f04 to 20a7972 Compare May 23, 2022 18:47

facundominguez marked this pull request as ready for review May 24, 2022 13:19

facundominguez force-pushed the fd/ple-opts2-rebased branch 6 times, most recently from dad6574 to 8f893b7 Compare May 31, 2022 21:49

facundominguez mentioned this pull request Jun 3, 2022

Update LF to provide human-friendly equalities ucsd-progsys/liquidhaskell#1986

Merged

facundominguez force-pushed the fd/ple-opts2-rebased branch 2 times, most recently from 70bc523 to f73828c Compare June 7, 2022 18:31

facundominguez added 13 commits June 7, 2022 15:46

Avoid sending icEquals multiple times to the SMT solver in PLE

d3d3b35

Remove duplicated unElaboration in PLE

f748f85

Move dropECst

aa6aa99

Make smt2App resilient to nested casts

0addc3c

Drop redundant casts when elaborating an expression.

094ce1e

Have isSmt2App see through casts

b4461e8

Have defuncEApp output a top-level cast

c020f43

Explain the SubExpr type

0cdbd52

Prettify the format of ple dumps

e6ef090

Fix fuel test

43cbbe6

Fold constants through casts

4e23b74

Pass label for errors in toSMT

235f270

Fix syntax of autorewrites when producing fq files

69a5c74

facundominguez added 17 commits June 7, 2022 16:40

Rename local lookup function in elabExprE

339c47a

Use the faster mapExprOnExpr in unApply

f9797e5

Skip terms with KVars in REST

e76f95c

Convert PIff in REST

9ac4049

Simplify the rhs of equations but don't simplify the candidates

a8bdbff

Remove the Simplifiable class

81f6be8

Preserve the context of rewrites for lambda expressions

e696ea4

convert PImp for REST

00416b5

Remove initial equations, they will be discovered if needed

89a8e1a

Implement subexpressions for PAnd, POr and PIff in REST

348676a

Use let-statements and record names in PLE.instEnv

08bfb00

Cache algebra queries in REST

88ae9ce

Build ordering constraints without the context of rewrites

7d131fc

Remove duplicated equations from the output of PLE

c60ee8d

Add back bindings in pretty printing of environments

c41fe15

Dedup PLE equations with cast differences

de645fc

Use expected names for constructor tests in IndPal tests

99fd634

facundominguez added 2 commits June 8, 2022 10:07

Remove redundant equations in evalApp

59eecd6

Revert back to adding equations for all measures on a seen data const…

07d95d8

…ructor

facundominguez force-pushed the fd/ple-opts2-rebased branch from 7302ab9 to 07d95d8 Compare June 8, 2022 13:12

Add unfoldings for calls whose guards couldn't be resolved

7e18f70

nikivazou merged commit a8f3f05 into ucsd-progsys:develop Jun 21, 2022

facundominguez deleted the fd/ple-opts2-rebased branch June 21, 2022 11:24

facundominguez mentioned this pull request Oct 27, 2022

--no-adt breaks some data definitions ucsd-progsys/liquidhaskell#2089

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

human-friendly equations from PLE #569

human-friendly equations from PLE #569

facundominguez commented May 16, 2022 •

edited

Loading

facundominguez commented May 16, 2022 •

edited

Loading

ranjitjhala commented May 16, 2022 via email

facundominguez commented May 18, 2022 •

edited

Loading

facundominguez commented May 24, 2022 •

edited

Loading

facundominguez commented Jun 7, 2022 •

edited

Loading

facundominguez commented Jun 11, 2022

facundominguez commented Jun 12, 2022 •

edited

Loading

facundominguez commented Jun 13, 2022 •

edited

Loading

facundominguez commented Jun 13, 2022

facundominguez commented Jun 14, 2022

human-friendly equations from PLE #569

human-friendly equations from PLE #569

Conversation

facundominguez commented May 16, 2022 • edited Loading

facundominguez commented May 16, 2022 • edited Loading

ranjitjhala commented May 16, 2022 via email

facundominguez commented May 18, 2022 • edited Loading

facundominguez commented May 24, 2022 • edited Loading

facundominguez commented Jun 7, 2022 • edited Loading

facundominguez commented Jun 11, 2022

facundominguez commented Jun 12, 2022 • edited Loading

facundominguez commented Jun 13, 2022 • edited Loading

facundominguez commented Jun 13, 2022

facundominguez commented Jun 14, 2022

facundominguez commented May 16, 2022 •

edited

Loading

facundominguez commented May 16, 2022 •

edited

Loading

facundominguez commented May 18, 2022 •

edited

Loading

facundominguez commented May 24, 2022 •

edited

Loading

facundominguez commented Jun 7, 2022 •

edited

Loading

facundominguez commented Jun 12, 2022 •

edited

Loading

facundominguez commented Jun 13, 2022 •

edited

Loading