A follow up of !836 (merged) to fix two things:
- Various
Make
instances still had expensive/recursive/non-constant-timeAffine
/Absorbing
premises. - There were some inconsistencies between the instances for the modalities and the conjunctions, for example, where
emp ∧ P
was turned intoP
ifP
is affine, but<affine> P
remained just<affine> P
regardless of whetherP
is affine.
To fix these things, this MR introduces classes QuickAffine
and 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.