Make iFrame able to accumulate assertions in an evar.
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 interleavingKnownFrame
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 applyingknown_frame
is completely trivial. -
Old instances of
Frame
are now instances ofKnownFrame
. This means that developments depending on Iris have to do this refactoring. However, in practice, as long as these developments never use evars of typePROP
in their goals when usingiFrame
, then defining an instance forFrame
instead ofKnownFrame
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.