A follow up of !836 (merged) to fix two things:
Makeinstances still had expensive/recursive/non-constant-time
- There were some inconsistencies between the instances for the modalities and the conjunctions, for example, where
emp ∧ Pwas turned into
Pis affine, but
<affine> Premained just
<affine> Pregardless of whether
To fix these things, this MR introduces classes
QuickAbsorbing. These classes are aliases for [Affine] and [Absorbing], but their instances are severely restricted. They only inspect the top-level symbol or check if the whole BI is affine---thus fixing (1). Aside, we use these classes for both all
Make instances, thus ensuring consistent behavior and fixing (2).
As a consequence of this MR, one test fails:
Lemma demo_3 P1 P2 P3 : P1 ∗ P2 ∗ P3 -∗ P1 ∗ ▷ (P2 ∗ ∃ x, (P3 ∧ ⌜x = 0⌝) ∨ P3). Proof. iIntros "($ & $ & $)". iNext. by iExists 0. Qed.
What happens is that after framing, the subterm
(P3 ∧ ⌜x = 0⌝) ∨ P3 is turned into
(emp ∧ ⌜x = 0⌝) ∨ emp. Before, the instance for
∨ would be fired, since
emp ∧ ⌜x = 0⌝ is affine, thus turning the whole subterm into
emp. I don't see how we can support this example without performing a recursive search to check if terms are affine.
That said, this test seems artificial/contrived, so I am not bothered that it fails. This MR is an improvement for Iron, due to fixing (2), a single
iSplit can be removed somewhere.