Heapster fix lowned proofs (#1415)

* added ppInfoAddTypedExprNames to use a base name for each variable depending on its type; also removed old PPInfo-related code

* whoops, fixed an infinite loop

* implemented lifetime subsumption

* started adding a new version of lowned permissions that include a notion of contained lifetimes, along with an lfinished permission

* bugfix: there was an infinite loop that kept copying a block permission before eliminating it and would then go right back to trying to eliminate that same permission again...

* added debug output for return statements, which is long overdue

* changed implElimLLVMBlock to always only eliminate one step of a memblock permission; changed proveVarLLVMBlocks to focus first on eliminating memblock permissions on the left that overlap with but are not contained in memblock permissions on the right

* unfold defined shapes on the left when their ranges match a shape we are trying to prove on the right

* whoops, do not try to eliminate LHS block perms when we are proving an empty block perm on the right

* added a case to proveVarLLVMBlocks to detect if the right-hand side is a tagged union type where we already know from something on the left what the tag is, in which case we can avoid searching for proofs of all the disjuncts other than the one that matches that known tag

* added another special case to proveVarLLVMBlocks, to eliminate a sequence shape sh;emptysh with the empty shape when necessary

* finished updating Implication.hs with the new lowned permission form

* reorganized proveVarLLVMBlocks into two separate stages represented by two separate functions, all of which now take lists of multi-bindings instead of multi-bindings of lists

* whoops, forgot to change a shadowed variable...

* implemented a few more suggestions from Eric Mertens

* fixed an infinite loop in proving the new lowned permissions; also added helper function implPushCopyM

* updated the translation for the new lfinished permission and the modified lowned permission, along with all the new and modified rules; also removed a bunch of whitespace from a previous commit

* updated the remaining Heapster files to reflect the new form of the lowned permission

* added  parser support for lfinished perms and for lowned perms with non-empty contained lifetimes

* whoops, fixed the parser rules for an optional list of lifetimes

* trying out a new approach for proving lowned permissions: instead of casting both sides to incorporate the equality permissions, change solveForPermListImpl to incorporate those equality permissions

* fixed localProveVars to recombine the input permissions in reverse order, since the left-most permissions (including any relevant equality permissions) are actually expected to be recombined first

* changed instantiateLifetimeVars to explicitly look for lowned permissions for the lifetimes it instantiates; also added debug tracing for when lifetimes begin and end

* changed implEndLifetimeRecM to no longer leave the lfinished permission on top of the stack, but to instead remove the finished lifetime from any other lowned permissions; also setPerm and setPerms, which have not been used in a long time

* added a case to simplify1PermForDetVars to end any indetermined lifetimes contained in lowned permissions for determined lifetimes

* whoops, fixed comments

* retrigger the CI checks

* updated arrays.v with its new translation