feat: do not instantiate metavariables in kabstract/rw for disallowed occurrences#2539
feat: do not instantiate metavariables in kabstract/rw for disallowed occurrences#2539leodemoura merged 1 commit intoleanprover:masterfrom
Conversation
|
| -- We save the metavariable context here, | ||
| -- so that it can be rolled back unless `occs.contains i`. | ||
| let mctx ← getMCtx | ||
| if (← isDefEq e p) then |
There was a problem hiding this comment.
What about exceptions? We should handle them here, or add a comment saying why it is ok to not rollback the mctx in this case.
There was a problem hiding this comment.
Sorry, I don't understand how exception handling is relevant here.
-
Previously, if there was an exception at
isDefEqthen that would propagate to the caller ofkabstract. That is still the case. Why would we try handling the exception here now? -
We are now rolling back the mctx if the occurrence has been rejected by the caller. Why would we want to rollback the mctx on an exception? (Again, previously an exception in
isDefEqwould result in the caller ofkabstractreceiving whatever mctx resulted.)
There was a problem hiding this comment.
@leodemoura, could I ping you on this query?
|
Someone just ran into this on zulip. |
|
Fixing |
|
Another confused beginner here. |
|
Here is me stumbling over unexpected |
| else | ||
| -- We save the metavariable context here, | ||
| -- so that it can be rolled back unless `occs.contains i`. | ||
| let mctx ← getMCtx |
There was a problem hiding this comment.
I noticed that in the definition of checkPointDefEq, it uses the MonadBacktrack SavedState MetaM instance for restoring the state if isDefEq fails or returns false. Is there any reason that you instead use the MonadMCtx MetaM instance?
Fixes #2538.