Use `NoBackTrack` type class for framing with ▷

As shown in #153 (closed) I noticed that uses of iFrame are pretty slow. The reason for this are the instances:

 Global Instance frame_later p R R' P Q Q' :
  IntoLaterN 1 R' R →
  Frame p R P Q →
  MakeLater Q Q' →
  Frame p R' (▷ P) Q'.

Global Instance frame_laterN p n R R' P Q Q' :
  IntoLaterN n R' R →
  Frame p R P Q →
  MakeLaterN n Q Q' →
  Frame p R' (▷^n P) Q'.

When establishing Frame p R P Q fails, which is quite often the case when you try to frame something that cannot be framed, type class search will back track like crazy on the various ways it can prove IntoLaterN n R' R.

So, in this MR I have introduced a class NoBackTrack which uses a dirty hack to make sure that no backtracking is performed. I then flag these IntoLaterN using NoBackTrack and the problem is solved.

On LambdaRust this gives a 17s speedup overall.

Todo

• Maybe move NoBackTrack to stdpp?

changed the description

When establishing Frame p R P Q fails, which is quite often the case when you try to frame something that cannot be framed, type class search will back track like crazy on the various ways it can prove IntoLaterN n R' R.

So it's finding tons of different ways to prove this for the same R, and then tried Frame p R P Q again for each of them?

Precisely.

Maybe move NoBackTrack to stdpp?

I think that would make sense.

Precisely.

Oh wow. That's bad. Proof-relevant Prolog turns out to be horrible.

LGTM.

Oh wow. That's bad. Proof-relevant Prolog turns out to be horrible.

Do you really think Prolog would not backtrack here ?

Doesn't it do caching?

Doesn't it do caching?

That may not always help, and likewise this does not necessarily have to do with proof relevance.

if you consider n and R' to be inputs and R to be the output of IntoLaterN n R' R, then there could be multiple possible outputs, i.e. multiple successes. How would caching help there?

added 2 commits

• 80a99e7e - Bump stdpp.
• 5e3416d3 - Fix issue #153 (closed) by using NoBackTrack in the Frame instances for ▷.

Compare with previous version

marked the checklist item Maybe move NoBackTrack to stdpp? as completed

unmarked as a Work In Progress

resolved all discussions

enabled an automatic merge when the pipeline for 5e3416d3 succeeds

Merging this. There may be more places where to add NoBackTrack, but let's do that when we notice similar problems.

canceled the automatic merge

changed title from {-NoBackTrack type class-} to {+Use NoBackTrack type class for framing with ▷+}

changed the description

merged

mentioned in commit 4ffff895