Skip to content

Make iFrame able to accumulate assertions in an evar.

Jacques-Henri Jourdan requested to merge jh/evar_iframe into gen_proofmode

This is to address #162 (closed).

This requires changing the Hint Mode of the Frame type class because it should not fail if its parameter is an evar, but instantiate it instead. In order to prevent all the other instances of Frame to instantiate this evar themselves, we create a new type class KnownFrame, which corresponds to the old behavior.

I am worried about:

  • iFrame is pretty time consuming. I have no idea whether interleaving KnownFrame searches at each step of the type class search can have significant performance impact. The reason why it might not cost too much is that the unification problem that has to be solved for applying known_frame is completely trivial.

  • Old instances of Frame are now instances of KnownFrame. This means that developments depending on Iris have to do this refactoring. However, in practice, as long as these developments never use evars of type PROP in their goals when using iFrame, then defining an instance for Frame instead of KnownFrame should have no impact.

  • If existing developments had goals with evars, then the behavior of iFrame will change. We should see how much impact does this have.

Merge request reports