This MR improves framing below modalities:
- It makes it possible to frame below an
<affine>
modality if the hypothesis that's framed is affine. (Previously, framing below<affine>
was only possible if the hypothesis that's framed resides in the intuitionistic context.) - It will "clean up" redundant modalities among the "spine" of the frame.
Feature (2) is achieved by making the classes MakeAffinely
, MakeIntuitionistically
, MakeAbsorbingly
, and MakePersistently
"smarter". These classes already had ad-hoc "clean up" instances to avoid wrapping the input into a modality if that is not needed. For example, MakeAffinely
would not wrap input P
in an <affine>
modality if P
is affine, and would not turn input True
into <affine> True
, but instead turn True
into emp
.
This MR simply adds all combinations of "clean up" instances that I could think of. Namely:
MakeAffinely True emp
-
new
MakeAffinely (<pers> P) (□ P)
-
new
MakeAffinely (<absorb> P1) P2
ifBiPositive PROP
andMakeAffinely P1 P2
-
MakeAffinely P P
ifAffine P
-
generalized
MakeIntuitionistically P1 P2
ifPersistent P1
andMakeAffinely P1 P2
(In particular, this instance maps input<pers> P
to output□ P
.) MakeAbsorbingly emp True
-
new
MakeAbsorbingly (<affine> P1) P2
ifPersistent P1
andMakeAbsorbingly P1 P2
-
new
MakeAbsorbingly P P
ifAbsorbing P
-
new
MakeAbsorbingly (□ P) (<pers> P)
MakePersistently emp True
-
new
MakePersistently P1 P2
ifPersistent P1
andMakeAbsorbingly P1 P2
(In particular, this instance maps input□ P
to output<pers> P
.)
I am not sure how useful this kind of "clean up" is in practice (it is only relevant for non-affine BIs anyway), but at least it now covers all combinations that I can think of instead of just some ad-hoc combinations as was done before. I have included a number of test cases to exercise this "clean up" as part of the iFrame
tactic.
Moreover, as as a consequence of MakePersistently
no longer creating redundant modalities, it can now be used to implement an alternative to the adhoc combination of FromPersistent
and IntoAbsorbingly
in !216 (closed). Concretely, similar to !216 (closed), this MR ensures that when using the [#]
pattern on a premise that is not persistent, it will wrap the goal (using MakePersistently
) into a <pers>
modality (specialization would fail before). If the premise is already persistent, but not absorbing, it will add an absorbing modality (as was done before).