Skip to content

Use `NoBackTrack` type class for framing with ▷

Robbert Krebbers requested to merge ci/robbert/no_backtracking into master

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?
Edited by Robbert Krebbers

Merge request reports