WIP: Strong framing

This MR makes an attempt at closing #71 (closed). Todo:

Syntax

I am not sure I like what we have now:

Lemma demo_17 (M : ucmraT) (P Q R : uPred M) :
  P -∗ Q -∗ R -∗ (P ∗ Q ∨ R ∗ False).
Proof.
  iIntros "^$ HQ HR {^$HR}".
  iAssert (Q ∨ False)%I with "[^$HQ]" as "[HQ|[]]".
  iFrame "^HQ".
Qed.

Note that we have syntax for framing in 1.) introduction patterns to frame introduced hypotheses on the fly 2.) The clear syntax {sel_pat} in introduction patterns 3.) specialization patterns 4.) the frame tactic. I tried to get some form of consistency, but suggestions for improvements are very welcome.

As I mentioned in #71 (closed):

It would be nice to have a "do more" modifier that we can also in other places.

For example, we have iIntros "!>" to introduce a modality. In #48 (closed) it is proposed to make the modality introduction behave like iNext (i.e. also strip modalities from the context). This will probably be costly, so in that case we may to keep !> letting introduce a modality, but have something like DO_MORE!> to also strip the modalities from all hypotheses.

The ^ token plays that role.

Approach

As I wrote in #71 (closed) this can be implemented in at least two ways:

1. Have an additional hint database strong_frame for dangerous frame instances.
2. Extend the Frame type class with a Boolean strong.

In this MR I went for (1) because it requires the least modifications. One has to be a bit careful about not introducing overlapping instances (and hence unneeded backtracking on failures) when using the typeclass_instances and strong_frame hint database together, but I think I managed.

Documentation

The new MaybeFrame type class and strong_frame hint database should be documented. Also ProofMode.md should be modified.

@janno @haidang @jung @jjourdan

I think the only thing left to do is bikeshed about syntax. ;) I think it's my turn to represent "blue", so here we go...

I don't have a strong opinion, but we should be careful not to burn through our characters too quickly. We should also IMHO learn from past mistakes and be careful about what we declare a token -- I've seen things like !>!#$%, which looks more like a curseword or Perl to me. I don't think there's any reason to accept such monstrosities, enforcing spaces in a few places could be a good thing. We can't do this with old constructors without breaking compatibility (though maybe it's worth it if it is not used a lot), but we can do that for new sigils.

I completely agree with you. There are two reasons that there things are accepted: 1.) Coq and ssreflect introduction patterns allow similar things like intros ????[]? 2.) Accepting fewer things is more difficult to code ;).

Since our introduction patterns have many more tokens, we maybe should stop allowing such things. Although it will be very easy to adapt proof scripts, I am not sure whether it is worth breaking backwards compatibility.

What do others think?

I don't really care about the spacing issue. I think we should probably just emit a warning when spaces are missing. This should not be too hard : the lexer should emit a "whitespace" token which should be ignored by the parser, but another parser could check that spaces are present between some pairs of tokens.

As for the question of the using the ASCII range : is there a strong reason we have to stick to the ASCII range? I understand that this is not particularly beautiful to write in the lexer, but technically there is no difficulty in detecting the first and second bytes of a non-ASCII UTF8 character.

We can support non-ASCII, and we are already doing that for the ∗ in the selection patterns.

Related to this discussion, I noticed that in lambda rust names for hypotheses like H↦∗: are used. Since Iris 9ae100fa, in which I unified the tokenizers, these names no longer work, as the ∗ is a token. Note that before 9ae100fa this name was already problematic, it could not be used in iClear, iRevert and iFrame.

What shall we do about that:

• Don't use such names for hypotheses
• Only consider ∗ to be a token when it has spaces around. This will brake stuff like iFrame "%H∗", which I have seen people using.

Don't use such names for hypotheses

I think this is what we should do.

We may still want to require whitespaces though, to make it easier to extend the tokenizer in the future.

I think this is what we should do.

I agree.

Alright, leaving the whitespace issue aside for a moment (we probably should open a new issue for that), what do we think about the syntax I proposed in this MR?

I kind of preferred € as it is more funny ;) but I don't think I can find any serious objection.

So is anyone already working on making lambdaRust compatible with current master? If not, I'd do that later today (as in, very soon).

Never mind, I see you already did it.

Ok, I guess we can merge this. @janno since you proposed this change, are you happy with it too?

This looks awesome! Thank you. I will try it out tomorrow in detail.

Two questions that came to my mind now:

1. Does this allow iFrame "^" and/or iFrame "^∗"?
2. Does this always enable framing in disjunctions for persistent assertions? This might already work now but I can't test it at the moment.

Does this allow iFrame "^" and/or iFrame "^∗"?

No, but I can add that.

Does this always enable framing in disjunctions for persistent assertions? This might already work now but I can't test it at the moment.

Yes.

added 17 commits

• 39a4dea0...e2882b61 - 14 commits from branch master
• 8cd46afc - Strong framing.
• e4239aca - Use strong framing for pure stuff.
• e567f240 - Support strong framing of the whole spatial context.

Compare with previous version

Does this allow iFrame "" and/or iFrame "∗"?

No, but I can add that.

Done.

added 2 commits

• c31078cf - Strong framing by default for persistent hypotheses.
• 4527c0a0 - Bench.

Compare with previous version

Does this always enable framing in disjunctions for persistent assertions? This might already work now but I can't test it at the moment.

Yes.

That turned out only to happen when framing the whole persistent context. Now it also does do that when framing individual persistent hypotheses.

added 4 commits

• bb16bae7 - Bench.
• 9578026e - Strong framing.
• 95b3911c - Use strong framing for pure stuff.
• f0582c61 - Support strong framing of the whole spatial context.

Compare with previous version

added 1 commit

• bc4b0cc2 - Strong framing by default for persistent hypotheses.

Compare with previous version

Hmm, it seems that the evar magic in bc4b0cc2 is making the whole compilation a bit slower.

Anyone an idea how to do this in a nicer (and hopefully faster way).