frame_instances: revise priorities for uses in "linear" bi
Note: For the purposes of this MR, "linear bi" includes those where BiAffine
instances aren't available to proof search.
- I pre-discussed this with @robbertkrebbers in https://mattermost.mpi-sws.org/iris/pl/wks7ckrj4j8g9docyjq7s3iy5y, but here's a self-contained summary:
The new workings are documented in the code. Today, instead, frame_here_absorbing | 0
will seldom succeed, so frame_here | 1
, but after other hints like frame_exist | 1
. So, to frame R
in R
, where R
is an existential, iFrame
will first try to pull the existential apart before framing R
as a whole, which might be expensive (especially for overly large R
s). The same applies to other connectives.
- For each instance, I added either an explicit priority or a comment, but I'm sure you might have different preferences.
Please count this as a Bedrock contribution — we've hit this in practice (and we've also sealed the offending R
).